Seminaire Oasis - Lemme, ARC Modocop

Radu Mateescu

projet Vasy, INRIALPES

Mercredi 27 mars, 10h, salle E002

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.

Retour au sommaire / Back to schedule

Eric Madelaine

Last modified: Fri Feb 1 16:55:34 MET 2002