Inequality Constraints on Synchronization Counters

Walid Haddad

The state space of concurrent systems can grow exponentially in the number of system components. Thus, to a certain extent, it may be impossible to explore the entire state space with limited time and memory, a fact known as the state space explosion problem [Val98]. This problem arises, for instance, when dealing with reachability analysis. An approach to check synchronization behavior on concurrent systems, with the aim of possible error detection caused by this behavior, is one of the reachability problems. Dealing with this problem by checking all possible states of the system needs a state space that is constructed by the synchronous-product of all processes; this leads to the state space explosion problem.

The aim of this thesis is to attack the state space explosion problem by an approach which avoids an exhaustive construction of its state space, in order to perform reachability analysis. The approach intends to introduce synchronization counters for each process and generate inequality constraints on these counters. The generation of these inequality constraints is done by applying certain algorithms and computations on the parallel composed automata representing processes in a system. As a result, our approach can avoid the generation of the whole state space of a system and bypass the state space explosion problem, in order to reach the desired goal.

Bachelor Thesis.

(pdf)