- Tytuł:
- Generation of synchronizing state machines from a transition system: A region-based approach
- Autorzy:
-
Teren, Viktor
Cortadella, Jordi
Villa, Tiziano - Powiązania:
- https://bibliotekanauki.pl/articles/2201022.pdf
- Data publikacji:
- 2023
- Wydawca:
- Uniwersytet Zielonogórski. Oficyna Wydawnicza
- Tematy:
-
transition system
Petri net
state machine
theory of regions
SAT
pseudo Boolean optimization
układ przejściowy
sieć Petriego
maszyna stanów
teoria regionów - Opis:
- 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.
- Źródło:
-
International Journal of Applied Mathematics and Computer Science; 2023, 33, 1; 133--149
1641-876X
2083-8492 - Pojawia się w:
- International Journal of Applied Mathematics and Computer Science
- Dostawca treści:
- Biblioteka Nauki
Artykuł