Compositional model checking with divergence preserving branching bisimilarity is lively - Archive ouverte HAL Access content directly
Journal Articles Science of Computer Programming Year : 2020

Compositional model checking with divergence preserving branching bisimilarity is lively

(1) , (2) , (1)
1
2

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.
Fichier principal
Vignette du fichier
Compositional_Model_Checking_Is_Lively.pdf (652.19 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02890800 , version 1 (07-09-2020)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More