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

*Radu Mateescu and Mihaela Sighireanu*

Proceedings of the 5th International Workshop on Formal Methods for
Industrial Critical Systems FMICS'2000 (Berlin, Germany),
April 2000

Also available as INRIA Research Report RR-3899.

An extended version is available here.

** 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.

24 pages | PostScript |

Cumulated slides about EVALUATOR 3.0 by R. Mateescu |