In: Lecture Notes in Computer Science, Vol. 1091; Proc. 17th International Conference in Application and Theory of Petri Nets (ICATPN'96), Osaka, Japan, pages 516-535. Springer-Verlag, June 1996.
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 representation of parallelism by interleaving. The covering step graphs are introduced as an alternative to labeled transition systems. A transition step consists of several possibly concurrent events. In a covering step graph, steps of independent transitions are substituted as much as possible to the subgraph which would result from the firing of the independent transitions. Attention must be paid to the case of conflict and confusion. An algorithm for the `on the fly' derivation of step graphs is proposed. This algorithm is then extended to behavior analysis by means of observational equivalence. A performance evaluation is made with respect to other methods.
Keywords: concurrent systems; state space exploration; partial-order; verification methods.
Back to the Petri Nets Bibliography