Compositional verification of concurrent systems by combining bisimulations

Compositional verification is a promising technique for analyzing action-based temporal properties of concurrent systems. One approach to verify a property expressed as a modal ?-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Ldsbr fragment of ?-calculus (consistingofweakmodalitiesonly),individual processes can be minimized modulo divergence-sensitive branching (divbranching) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or divbranching bisimulation minimiza- tion on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend the existing Ldsbr fragment with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems.