Decomposition of transition systems into sets of synchronizing state machines

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...