Generation of synchronizing state machines from a transition system: A region-based approach - Teren, Viktor; Cortadella, Jordi; Villa, Tiziano (Zielona Góra: Uniwersytet Zielonogórski)
Transition systems (TSs) and Petri nets (PNs) are important models of computation ubiquitous in formal methods for modeling systems. A crucial 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. Furthermore, all reachable markings (non-negative vectors representing the number of tokens for each place) of an SM have only one marked place with only one token.
Keywords: transition systems; Petri nets; state machine; decomposition; theory of regions; SAT; pseudo-Boolean optimization