Decomposition of transition systems into sets of synchronizing state machines

TL;DR

This paper presents a method to decompose transition systems into sets of synchronizing state machines using region theory, providing an efficient algorithm with promising experimental results for system modeling.

Contribution

It introduces a novel decomposition approach based on excitation-closure regions and offers an efficient algorithm for extracting synchronizing state machines from transition systems.

Findings

Algorithm reduces critical steps to maximal independent set or satisfiability problems.

Experimental results show a good balance between result quality and computation time.

Decomposition guarantees equivalence between original TS and the set of SMs.

Abstract

Transition systems (TS) and Petri nets (PN) are important models of computation ubiquitous in formal methods for modeling systems. An important 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 and all markings have exactly one token. This is an important 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.