Skip to Main content Skip to Navigation
Conference papers

Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities

Abstract : We showed in a recent paper that, when verifying a modal µ-calculus formula, the actions of the system under verification can be partitioned into sets of so-called weak and strong actions, depending on the combination of weak and strong modalities occurring in the formula. In a compositional verification setting, where the system consists of processes executing in parallel, this partition allows us to decide whether each individual process can be minimized for either divergence-preserving branching (if the process contains only weak actions) or strong (other-wise) bisimilarity, while preserving the truth value of the formula. In this paper, we refine this idea by devising a family of bisimilarity relations, named sharp bisimilarities, parameterized by the set of strong actions. We show that these relations have all the nice properties necessary to be used for compositional verification, in particular congruence and adequacy with the logic. We also illustrate their practical utility on several examples and case-studies, and report about our success in the RERS 2019 model checking challenge.
Complete list of metadatas

Cited literature [48 references]  Display  Hide  Download

https://hal.inria.fr/hal-02555692
Contributor : Radu Mateescu <>
Submitted on : Monday, April 27, 2020 - 3:03:54 PM
Last modification on : Thursday, April 30, 2020 - 10:01:16 PM

File

Lang-Mateescu-Mazzanti-20.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Frédéric Lang, Radu Mateescu, Franco Mazzanti. Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities. TACAS 2020 - Tools and Algorithms for the Construction and Analysis of Systems, Apr 2020, Dublin, Ireland. pp.57-76, ⟨10.1007/978-3-030-45237-7_4⟩. ⟨hal-02555692⟩

Share

Metrics

Record views

58

Files downloads

153