Property-dependent reductions adequate with divergence-sensitive branching bisimilarity

R. Mateescu, A.J. Wijs

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

11 Citaten (Scopus)

Samenvatting

When analyzing the behavior of finite-state concurrent systems by model checking, one way of fighting state space 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 µ-calculus (L_µ). First, we determine, for any L_µ formula, the maximal set of actions that can be hidden in the Lts without changing the interpretation of the formula. Then, we define L_{µ}^{dsbr}, a fragment of Lµ which is adequate w.r.t. divergence-sensitive branching bisimilarity. This enables us to apply the maximal hiding and to reduce the Lts on-the-fly using divergence-sensitive t-confluence during the verification of any L_{µ}^{dsbr} 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. Keywords: Divergence-sensitive branching bisimulation; Labeled transition system; Modal µ-calculus;Model checking; On-the-fly verification
Originele taal-2Engels
Pagina's (van-tot)354-376
Aantal pagina's23
TijdschriftScience of Computer Programming
Volume96
Nummer van het tijdschrift3
DOI's
StatusGepubliceerd - 2014

Vingerafdruk

Duik in de onderzoeksthema's van 'Property-dependent reductions adequate with divergence-sensitive branching bisimilarity'. Samen vormen ze een unieke vingerafdruk.

Citeer dit