Skip to Main content Skip to Navigation
Reports

Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus

Abstract : Model-checking is a successful technique for automatically verifying concurrent finite-state systems. When building a model-checker, a good compromise must be made between the expressive power of the property description formalism, the complexity of the model-checking problem, and the user-friendliness of the interface. We present a temporal logic and an associated model-checking method that attempt to fulfill these criteria. The logic is an extension of the alternation-free mu-calculus with ACTL-like action formulas and PDL-like regular expressions, allowing a concise and intuitive description of safety, liveness, and fairness properties over labeled transition systems. The model-checking method is based upon a succinct translation of the verification problem into a boolean equation system, which is solved by means of an efficient local algorithm having a good average complexity. The algorithm also allows to generate full diagnostic information (examples and counterexamples) for temporal formulas. This method is at the heart of the EVALUATOR 3.0 model-checker that we implemented within the CADP toolset using the generic OPEN/CAESAR environment for on-the-fly verification.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072755
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:49:10 AM
Last modification on : Thursday, November 19, 2020 - 1:00:27 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:21:07 PM

Identifiers

  • HAL Id : inria-00072755, version 1

Collections

Citation

Radu Mateescu, Mihaela Sighireanu. Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. [Research Report] RR-3899, INRIA. 2000. ⟨inria-00072755⟩

Share

Metrics

Record views

322

Files downloads

566