Seto: a framework for the decomposition of Petri nets and transition systems

This paper presents an overview of different approaches, based on theory of regions, for Transition System and Petri net decomposition into a synchronous product of restricted subclasses of Petri nets. A decomposition targeting State Machines was implemented in a prototype software, by reduction to maximal independent set which computes minimal sets of irredundant state machines. Then, states of single state machines were merged by reduction to the Boolean satisfiability problem (SAT). Furthermore, an extension to Free-choice Petri net decomposition was implemented, reducing the whole decomposition process to a series of SAT problems. We report experimental results that show a good trade-off between quality of results vs. time of computation, including different variants of the decomposition flows. In particular, we introduce a new approach allowing a simultaneous search of components, exploiting Binary Decision Diagrams and the excitation-closure property provided by theory of regions.