2021/06/25 by Viktor Teren, Jordi Cortadella, Teren, Viktor +3
Computer Science · #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Hardware Architecture (cs.AR) #Model-Driven Software Engineering Techniques #Petri Nets in System Modeling #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2106.13852
openalex publication_date 2021/06/25 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Transition systems (TS) and Petri nets (PN) are important models of\ncomputation ubiquitous in formal methods for modeling systems. An important\nproblem is how to extract from a given TS a PN whose reachability graph is\nequivalent (with a suitable notion of equivalence) to the original TS.\n This paper addresses the decomposition of transition systems into\nsynchronizing state machines (SMs), which are a class of Petri nets where each\ntransition has one incoming and one outgoing arc and all markings have exactly\none token. This is an important case of the general problem of extracting a PN\nfrom a TS. The decomposition is based on the theory of regions, and it is shown\nthat a property of regions called excitation-closure is a sufficient condition\nto guarantee the equivalence between the original TS and a decomposition into\nSMs.\n An efficient algorithm is provided which solves the problem by reducing its\ncritical steps to the maximal independent set problem (to compute a minimal set\nof irredundant SMs) or to satisfiability (to merge the SMs). We report\nexperimental results that show a good trade-off between quality of results vs.\ncomputation time.\n