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.
Type de document :
[Research Report] RR-3899, INRIA. 2000
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:49:10
Dernière modification le : mercredi 11 avril 2018 - 01:51:53
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:21:07



  • HAL Id : inria-00072755, version 1



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



Consultations de la notice


Téléchargements de fichiers