Skip to Main content Skip to Navigation
Journal articles

Compositional model checking with divergence preserving branching bisimilarity is lively

Sander de Putter 1 Frédéric Lang 2 Anton Wijs 1
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : 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 bisimilarity (DPBB). It has long been generally assumed that DPBB is a congruence for parallel composition. Recently, a congruence format has been proposed that implies that this is the case [1]. In parallel, we were the first to prove this by means of a proof assistant (Coq) for the parallel composition of Labelled Transition Systems (LTSs) with synchronisation on their common alphabet [2]. In the current article, we remove that restriction. In addition, we show that DPBB is a congruence for LTS networks in which many LTSs are composed in parallel at once with support for multi-party synchronisation. Additionally, we discuss how to safely decompose an existing LTS network into components such that their recomposition is equivalent to the original LTS network. 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.
Document type :
Journal articles
Complete list of metadata

Cited literature [59 references]  Display  Hide  Download

https://hal.inria.fr/hal-02890800
Contributor : Frederic Lang <>
Submitted on : Monday, September 7, 2020 - 4:32:11 PM
Last modification on : Tuesday, November 24, 2020 - 4:00:18 PM
Long-term archiving on: : Saturday, December 5, 2020 - 3:14:26 AM

File

Compositional_Model_Checking_I...
Files produced by the author(s)

Identifiers

Collections

Citation

Sander de Putter, Frédéric Lang, Anton Wijs. Compositional model checking with divergence preserving branching bisimilarity is lively. Science of Computer Programming, Elsevier, 2020, 196, pp.102493. ⟨10.1016/j.scico.2020.102493⟩. ⟨hal-02890800⟩

Share

Metrics

Record views

80

Files downloads

178