online read us now
Paper details
Number 1 - March 2023
Volume 33 - 2023
Generation of synchronizing state machines from a transition system: A region-based approach
Viktor Teren, Jordi Cortadella, Tiziano Villa
Abstract
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. This is a significant 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.
Keywords
transition system, Petri net, state machine, decomposition, theory of regions, SAT, pseudo-Boolean optimization