MCL manual page

Table of Contents## Name

mcl, MCL - Model Checking Language (versions 3 and 4)
## 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). ## Bibliography

## See Also

**evaluator**
,
**evaluator3**
, **evaluator4**
, **mcl3**
, **mcl4**
, **regexp**
## Bugs

Please report bugs to Radu.Mateescu@inria.fr

Two versions of *MCL* are currently
available:

*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 strings.A description of

*MCL*version 3 can be found in the**mcl3**manual page.*MCL*version 3 is supported by the**evaluator3**on-the-fly model checker.*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**manual page.*MCL*version 4 is supported by the**evaluator4**on-the-fly model checker.

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

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