Table of Contents
mcl, MCL - Model Checking Language (versions 3, 4, and 5)
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.
- [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.
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.
Please report bugs to
[email protected]
Table of Contents
