Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities

Résumé

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.
Fichier principal
Vignette du fichier
Lang-Mateescu-Mazzanti-20.pdf (559.24 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02555692 , version 1 (27-04-2020)

Identifiants

Citer

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⟩
229 Consultations
94 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More