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