In: ACM Trans. on Programming Languages and Systems, Vol. 20, No. 5, pages 917-979. 1998.
Abstract: The state explosion problem of formal verification has obstructed its application to large-scale software systems. This paper introduces a set of new condensation theories: IOT-failure equivalence, IOT-state equivalence, and firing-dependence theory to cope with this problem. The proposed condensation theories are much weaker than current theories used for the compositional verification of Petri nets. More significantly, the proposed condensation theories can eliminate the interleaved behaviors caused by asynchronously sending actions. Therefore, the proposed technique provides a much more powerful means for the compositional verification of asynchronous processes. This technique can efficiently analyze several state-based properties: boundedness, reachable markings, reachable submarkings, and deadlock states. Based on the notion of the proposed theories, a set of condensation rules is developed for efficient verification of large-scale software systems. The experimental results show a significant improvement in the analysis of large-scale concurrent systems.
Keywords: IOT-failure equivalence, IOT-state equivalence, Petri nets, compositional verification, concurrent systems, condensation rules, deadlock states, firing-dependence theory, reachability analysis, reachability graphs.