Covering step graph preserving failure semantics

Abstract

Within the framework of concurrent systems, several verification approaches require as a preliminary step the complete derivation of the state space. Partial-order methods are efficient for reducing the state explosion due to the modeling of parallelism by interleaving. In the case of persistent or sleep sets, only a subset of enable transitions is examined, the derived graph is then a subgraph of the whole graph. The resulting sub-graph may be used for verifying absence of deadlock or more specific properties. The covering step graph (CSG) approach visits all the transitions, but some independent events are put together to build a single transition step, the firing of this transition step is then atomic. In a CSG, steps of independent transitions are substituted as much as possible to the subgraph which would result from the firing of the independent transitions. The potential benefit of such a substitution may be exponential with respect to the number of "merged" independent transitions. This paper investigates the on-the-fly derivation of covering step graphs preserving failure semantics. Testing Equivalence and CSP semantics are considered.