Analysis of Concurrent Discrete Systems by Means of Reduced Reachability Graphs

The paper deals with formal verification of parallel discrete systems, for which state explosion is a major problem. We consider the Petri net models of parallel logical control algorithms. Such algorithms can usually be modeled by Petri nets belonging to specific classes. We propose two methods of verification of Petri nets by means of constructing reduced reachability graphs. First of them uses the stubborn sets and allows to decide well-formedness of the Petri nets having structures typical for control algorithms, and hence to verify such algorithms automatically. Second one allows to detect deadlocks of ordinary Petri nets by concurrent simulation, often reducing state spaces deeper than the first method.