What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

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:

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

• MCL version 5 (probabilistic value-passing modal mu-calculus) [MR18] is an extension of MCL version 4 with a probabilistic operator specifying the probability of transition sequences described using generalized regular formulas. MCL version 5 is interpreted on Probabilistic Transition Systems (PTSs) [LS91], whose transitions are labeled by actions containing channel names, data values, and probabilities.

  A description of MCL version 5 can be found in the mcl5 manual page.

  MCL version 5 is supported by the evaluator5 on-the-fly model checker.

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

• Name
• Description
• Bibliography
• See Also
• Bugs