<abstract xmlns="http://www.w3.org/1999/xhtml">

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

Generation of Synchronizing State Machines from a Transition System: A Region–Based Approach

International Journal of Applied Mathematics and Computer Science

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Transition systems (TSs) and Petri nets (PNs) are important models of computation ubiquitous in formal methods for modeling systems. A crucial problem is how...

Generation of Synchronizing State Machines from a Transition System: A Region–Based Approach

Publicado en línea: 29 mar 2023

Páginas: 133 - 149

Recibido: 28 ene 2022

Aceptado: 25 oct 2022

DOI: https://doi.org/10.34768/amcs-2023-0011

Palabras clave
transition system, Petri net, state machine, decomposition, theory of regions, SAT, pseudo-Boolean optimization

© 2023 Viktor Teren et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Generation of Synchronizing State Machines from a Transition System: A Region–Based Approach

Publicado en línea: 29 mar 2023

Páginas: 133 - 149

Recibido: 28 ene 2022

Aceptado: 25 oct 2022

DOI: https://doi.org/10.34768/amcs-2023-0011

Palabras clavetransition system, Petri net, state machine, decomposition, theory of regions, SAT, pseudo-Boolean optimization

© 2023 Viktor Teren et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Palabras clave
transition system, Petri net, state machine, decomposition, theory of regions, SAT, pseudo-Boolean optimization