MCL manual page
Table of Contents

Name

mcl, MCL - Model Checking Language (versions 3, 4, and 5)

Description

MCL (Model Checking Language) is an action-based, branching-time temporal logic suitable for expressing properties of concurrent systems. MCL is interpreted on Labelled Transition Systems (LTSs).

Three versions of MCL are currently available:

Bibliography

[DV90]
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.

[EL86]
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.

[FL79]
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.

[Gar89]
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

[Koz83]
D. Kozen. "Results on the Propositional Mu-Calculus." Theoretical Computer Science, v. 27, p. 333-354, 1983.

[LS91]
K. G. Larsen and A. Skou. "Bisimulation through Probabilistic Testing." Information and Computation, v. 94, no. 1, p. 1-28, 1991.

[MR18]
R. Mateescu and J. I. Requeno. "On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators." Springer International Journal on Software Tools for Technology Transfer (STTT), v. 20, no. 5, p. 563-587, 2018.

[MS03]
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

[MT08]
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

[Str82]
R. S. Streett. "Propositional Dynamic Logic of Looping and Converse." Information and Control, v. 54, p. 121-141, 1982.

See Also

evaluator , evaluator3 , evaluator4 , mcl3 , mcl4 , regexp

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in files $CADP/INSTALLATION_*.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report bugs to Radu.Mateescu@inria.fr


Table of Contents