Skip to Main content Skip to Navigation
Journal articles

Compositional Verification of Concurrent Systems by Combining Bisimulations

Abstract : One approach to verify a property expressed as a modal μ-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Lμ-dbr fragment of the μ-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (div\-branching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or div\-branching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend Lμ-dbr with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by div\-branching bisimulation.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-03159616
Contributor : Frederic Lang <>
Submitted on : Thursday, March 4, 2021 - 4:10:31 PM
Last modification on : Saturday, March 6, 2021 - 3:28:57 AM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2021-09-04

Please log in to resquest access to the document

Identifiers

  • HAL Id : hal-03159616, version 1

Collections

Citation

Frederic Lang, Radu Mateescu, Franco Mazzanti. Compositional Verification of Concurrent Systems by Combining Bisimulations. Formal Methods in System Design, Springer Verlag, 2021. ⟨hal-03159616⟩

Share

Metrics

Record views

18