Transition systems (TS) and Petri nets (PN) are important models of computation ubiquitous in formal methods for modeling systems. An important problem is how to extract from a given TS a PN whose reachability graph is equivalent (with a suitable notion of equivalence) to the original TS. This paper addresses the decomposition of transition systems into synchronizing state machines (SMs), which are a class of Petri nets where each transition has one incoming and one outgoing arc and all markings have exactly one token. This is an important case of the general problem of extracting a PN from a TS. The decomposition is based on the theory of regions, and it is shown that a property of regions called excitation-closure is a sufficient condition to guarantee the equivalence between the original TS and a decomposition into SMs. An efficient algorithm is provided which solves the problem by reducing its critical steps to the maximal independent set problem (to compute a minimal set of irredundant SMs) or to satisfiability (to merge the SMs). We report experimental results that show a good trade-off between quality of results vs. computation time.

翻译：过渡系统(TS)和Petrinet(PN)是模拟系统正式方法中无处不在的计算的重要模型,一个重要问题是如何从给定的TS中提取一个PN,其可达性图相当于(具有适当的等同概念)原TS。本文件论述过渡系统分解成同步的国家机器(SMS)的问题,这是Petrinet的一类,其中每个过渡都有一个进入和输出的弧线,所有标记都具有完全的象征意义。这是从TS中提取一个PN的一般性问题的一个重要案例。分解基于区域理论,并表明称为Excurus-locure的区域属性足以保证原TS和分解到SMS的等同性。提供了高效的算法,通过将其关键步骤减少到最大独立的设置问题(计算最低限度的互不相容SMSM)或对等性(合并SMSM)来解决问题。我们报告实验结果显示结果之间的良好交易质量。