Table of Contents
mcl, MCL - Model Checking Language (versions 3 and 4)
(Model Checking Language
) is an action-based, branching-time temporal logic
suitable for expressing properties of concurrent systems. MCL
on Labelled Transition Systems (LTSs).
Two versions of MCL are currently
- MCL version 3 (regular alternation-free mu-calculus) [MS03, Mat06]
is an extension of the alternation-free fragment of the modal mu-calculus
[Koz83, EL86] with action predicates similar to those of ACTL [DV90] and
regular expressions over action sequences similar to those of PDL [FL79].
In the temporal formulas of MCL version 3, the LTS actions are merely character
A description of MCL version 3 can be found in the mcl3
MCL version 3 is supported by the evaluator3
- MCL version 4 (value-passing modal mu-calculus) [MT08] is an
extension of MCL version 3 with data-handling constructs (data variables,
expressions, parameterized fixed point operators, programming language
constructs) and an infinite looping operator similar to that of PDL-delta
[Str82], able to express fairness properties. In the temporal formulas of
MCL version 4, the LTS actions are tuples containing channel names and
data values, which can be extracted and used in calculations, as originally
proposed in the RICO logic [Gar89].
A description of MCL version 4 can be
found in the mcl4
MCL version 4 is supported by the
on-the-fly model checker.
- R. De Nicola
and F. W. Vaandrager. "Action versus State based Logics for Transition Systems."
Proceedings Ecole de Printemps on Semantics of Concurrency, LNCS v. 469,
p. 407-419, 1990.
- E. A. Emerson and C-L. Lei. "Efficient Model Checking
in Fragments of the Propositional Mu-Calculus." Proceedings of the 1st LICS,
p. 267-278, 1986.
- M. J. Fischer and R. E. Ladner. "Propositional Dynamic
Logic of Regular Programs." Journal of Computer and System Sciences, no.
18, p. 194-211, 1979.
- H. Garavel. Chapter 9 of "Compilation et verification
de programmes LOTOS." PhD thesis, Universite Joseph-Fourier Grenoble, 1989.
Available from http://cadp.inria.fr/publications/Garavel-89-b.html
Kozen. "Results on the Propositional Mu-Calculus." Theoretical Computer Science,
v. 27, p. 333-354, 1983.
- R. Mateescu and M. Sighireanu. "Efficient On-the-Fly
Model-Checking for Regular Alternation-Free Mu-Calculus." Science of Computer
Programming, v. 46, no. 3, p. 255-281, 2003. Available from http://cadp.inria.fr/publications/Mateescu-Sighireanu-03.html
- R. Mateescu and D. Thivolle. "A Model Checking Language for Concurrent
Value-Passing Systems." Proceedings of the 15th International Symposium on
Formal Methods FM'08, LNCS v. 5014, p. 148-164, 2008. Available from http://cadp.inria.fr/publications/Mateescu-Thivolle-08.html
- R. S. Streett. "Propositional Dynamic Logic of Looping and Converse."
Information and Control, v. 54, p. 121-141, 1982.
Additional information is available from the CADP Web page located at http://cadp.inria.fr
Directives for installation are given in files $CADP/INSTALLATION_*.
changes and improvements to this software are reported and commented in
Please report bugs to Radu.Mateescu@inria.fr
Table of Contents