Skip to Main content Skip to Navigation
Reports

Property-Dependent Reductions for the Modal Mu-Calculus

Radu Mateescu 1 Anton Wijs 2
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : When analyzing the behavior of finite-state concurrent systems by model checking, one way of fighting state explosion is to reduce the model as much as possible whilst preserving the properties under verification. We consider the framework of action-based systems, whose behaviors can be represented by labeled transition systems (LTSs), and whose temporal properties of interest can be formulated in modal mu-calculus (Lmu). First, we determine, for any Lmu formula, the maximal set of actions that can be hidden in the LTS without changing the interpretation of the formula. Then, we define dsbrLmu, a fragment of Lmu which is compatible with divergence-sensitive branching bisimulation. This enables us to apply the maximal hiding and to reduce the LTS on-the-fly using divergence-sensitive tau-confluence during the verification of any dsbrLmu formula. The experiments that we performed on various examples of communication protocols and distributed systems show that this reduction approach can significantly improve the performance of on-the-fly verification.
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00609585
Contributor : Radu Mateescu <>
Submitted on : Tuesday, July 19, 2011 - 2:41:11 PM
Last modification on : Thursday, November 19, 2020 - 1:00:20 PM
Long-term archiving on: : Thursday, October 20, 2011 - 2:25:34 AM

File

RR-7690.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00609585, version 1

Citation

Radu Mateescu, Anton Wijs. Property-Dependent Reductions for the Modal Mu-Calculus. [Research Report] RR-7690, INRIA. 2011, pp.30. ⟨inria-00609585⟩

Share

Metrics

Record views

249

Files downloads

289