5th International Workshop on

Formal Methods for Industrial Critical Systems

Berlin, April 3-4, 2000


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

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 tempo- ral logic and an associated model-checking method that attempt to ful ll these criteria. The logic is an extension of the alternation-free -calculus with Actl-like action formulas and Pdl-like regular expressions, allow- ing 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/CÆsar environment for on-the- y verification.


Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.


ERCIM FMICS Home Page, GMD FOKUS Home Page

Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch