Compositional model checking is lively

Compositional model checking approaches attempt to limit state space explosion by iteratively combining behaviour of some of the components in the system and reducing the result modulo an appropriate equivalence relation. For an equivalence relation to be applicable, it should be a congruence for parallel composition where synchronisations between the components may be introduced. An equivalence relation preserving both safety and liveness properties is divergence-preserving branching bisimulation (DPBB). It is generally assumed that DPBB is a congruence for parallel composition, even in the context of synchronisations between components. However, so far, no such results have been published. This work finally proves that this is the case. Furthermore, we discuss how to safely decompose an existing LTS network in components such that the re-composition is equivalent to the original LTS network. All proofs have been mechanically verified using the Coq proof assistant. Finally, to demonstrate the effectiveness of compositional model checking with intermediate DPBB reductions, we discuss the results we obtained after having conducted a number of experiments.