Compositional verification of concurrent systems using Petri-net-based condensation rules

The state-explosion problem of formal verification has obstructed its appli cation to large-scale software systems. In this article, we introduce a set of new condensation theories: IOT-failure equivalence, IOT-state equivalen ce, and firing-dependence theory to cope with this problem. Our condensatio n theories are much weaker than current theories used for the compositional verification of Petri nets. More significantly, our new condensation theor ies can eliminate the interleaved behaviors caused by asynchronously sendin g actions. Therefore, our technique provides a much more powerful means for the compositional verification of asynchronous processes. Our technique ca n efficiently analyze several state-based properties: boundedness, reachabl e markings, reachable submarkings, and deadlock states. Based on the notion of our new theories, we develop a set of condensation rules for efficient verification of large-scale software systems. The experimental results show a significant improvement in the analysis of large-scale concurrent system s.