MCL5 manual page

Table of Contents## Name

mcl, MCL - Model Checking Language version 5 (probabilistic value-passing
modal mu-calculus)
## Description

This manual page presents the version 5 of
*MCL* (*Model Checking Language*), which is the temporal logic accepted as
input by **evaluator5**
. *MCL* version 5 conservatively extends *MCL* version
4 with a probabilistic operator specifying the probability measure of transition
sequences characterized by regular formulas. In the remainder of this page,
"*MCL*" denotes version 5 of *MCL*; see **mcl**
for other versions of *MCL*.
## Probabilistic Operator

The
probabilistic operator belongs to the *state formulas* of MCL. Its syntax
is defined by the following grammar: ## Examples of
Probabilistic Properties

### Dataless Properties

The "prob" operator expresses
constraints on the probability of certain sequences described using regular
formulas. The formula below specifies that the probability to send a message
along an unreliable channel and receive it finally (possibly after a finite
number of retries) is at least 90%: ### Data-handling Properties

MCL enables the formulation of probabilistic properties
involving data values, for instance using regular formulas with counting.
The formula below, concerning the Bounded Retransmission Protocol (BRP)
[DJJL01,MR18], evaluates the probability that the sender reports an unsuccessful
transmission (action INPUT_NOK) after more than eight chunks of the packet
have been transmitted (action REC_L): ## Relation to Other Probabilistic Logics

The "prob" operator
of MCL generalizes naturally the Until operators of classical probabilistic
branching-time logics. The Until operator of PCTL (Probabilistic Computation
Tree Logic) [HJ94] without discrete time can be expressed in MCL as follows:
## Determinization of Probabilistic Formulas

To ensure that the verification
of a "prob" formula on a PTS is translated correctly into the resolution
of a LES, the regular subformula *R* must be *deterministic*, meaning that
it must satisfy two conditions:
## Bibliography

## See Also

**bcg_steady**
, **evaluator**
,
**evaluator3**
, **evaluator4**
, **evaluator5**
, **mcl**
, **mcl3**
,
**mcl4**
, **regexp**
## Bugs

Please
report bugs to Radu.Mateescu@inria.fr

A description of the probabilistic operator of *MCL* can be found in article
[MR18], which also presents the verification method implemented in version
5.0 of EVALUATOR. This method is based on translating the problem into the
resolution of a Linear Equation System (LES) and a Parameterized Boolean
Equation System (PBES), which are carried out simultaneously on the fly.

*MCL* formulas are interpreted over a PTS (Probabilistic Transition System)
[LS91] *<S, A, T, P, s0>*, where: *S* is the set of *states*, *A* is the set of *actions*
(transition labels), *T* is the *transition relation* (a subset of *S * A *
S*), *P* is the *probability labeling* (a function from *T* to the range ]0..1]),
and *s0* is the *initial state*. A transition *(s1, a, s2)* of *T*, also written
*s1-a->s2*, indicates that the system can move from state *s1* to state *s2* by
performing action *a* with probability *P (s1, a, s2)*. For each state *s*, the
sum of the probabilities associated to its outgoing transitions *(s, a,
s')* is equal to 1. Note that this forbids the presence of sink states (deadlocks)
in the PTS, i.e., every state must have at least one outgoing transition.

The PTS must contain only labelled probabilistic transitions of the form
"*label***; prob** *%p*", where *%p* denotes a floating-point number in the range ]0..1]
(see the **bcg_steady**
manual page for details). An LTS can be converted
into a PTS on the fly by renaming its transition labels using the **-rename**
option of **evaluator5**
to append "**; prob** *%p*" suffixes. If after renaming
transition labels, the sum of the probabilities associated to the transitions
going out of a state is different from 1, these probabilities are normalized
to bring this sum to 1. If no **-rename** option is given, the LTS is converted
into a PTS by considering that, for every state, all its outgoing transitions
have equal probabilities, the sum of which is 1.

"prob" R "is" op [ "?" ] E "end" "prob"

where *R* is a regular formula on transition sequences, *op* is a comparison
operator among "<", "<=", ">", ">=", "=", "<>", and *E* is a data expression of
type `real`

denoting a probability.

Let *m (s, R)* be the probability measure
of the transition sequences going out of a state *s* and having a prefix
satisfying the regular formula *R*. A state *s* of the PTS satisfies the "prob"
formula above iff *m (s, R) op v* holds, where *v* is the value of expression
*E*.

If the optional "?" clause is present, the evaluation of the "prob" formula
on a state *s* will also display the value *m (s, R)* in addition to the Boolean
verdict (TRUE or FALSE) displayed by **evaluator5**
.

The regular formula
*R* and the expression *E* may contain occurrences of free data variables defined
outside the "prob" formula. The data variables exported by *R* are neither
visible in *E*, nor exported outside the whole "prob" formula.

prob SEND . (true* . RETRY)* . RECV is >= 0.9 end prob

By combining the modalities of PDL and the "prob" operator, one can express quantitative response properties. The formula below specifies that every request to access a resource will be granted with probability 1 (i.e., almost surely):

[ true* . REQUEST ] prob true* . GRANT is >= 1 end prob

prob ((not REC_L)* . REC_L) { 8 ... } . (not (REC_L or INPUT_NOK))* . INPUT_NOK is >= ? 0 end prob

where the regular subformula "*R* { 8 ... }" denotes the repetition of *R* at
least 8 times (see **mcl4**
for details). This formula will be evaluated
to TRUE and **evaluator5**
will display the computed probability, as
required by the "?" clause.

More complex properties about transition sequences
having certain cumulated costs can be expressed using data-handling action
predicates and the general iteration operator "loop" on regular formulas.
The following example deals with a mutual exclusion protocol that manages
the accesses of *n* processes *P1*, ..., *Pn* to a shared resource [MS13,MR18]. The
MCL formula below computes the probability that a process *Pi* performs memory
accesses of a total cost *max* before entering its critical section (*Pi* and
*max* are assumed to be defined outside of the formula). The regular subformula
expresses that, after executing its non critical section for the first
time (action predicate "{ NCS !i }"), process *Pi* begins its entry section
and, after a number of memory accesses (action predicate "{ MU ... ?c:nat
!i }"), enters its critical section (action predicate "{ CS !"ENTER" !i
}"):

prob (not { NCS !i })* . { NCS !i } . loop (total_cost:nat:=0) in (not ({ MU ... !i } or { CS !"ENTER" !i }))* . if total_cost < max then { MU ... ?c:nat !i } . continue (total_cost + c) else exit end if end loop . { CS !"ENTER" !i } is >= ? 0 end prob

The "loop" subformula captures the entry section of *Pi* and requires that
it terminates when the cost of all memory accesses performed by *Pi* (accumulated
in the iteration variable *total_cost*) exceeds a given value *max*. The costs
present on transitions are captured in the *c* variable of the action predicate
"{ MU ... ?c:nat !i }" and used in the "continue" subformula to update the
value of *total_cost*. The other processes can execute freely during the entry
section of *Pi*, in particular they can overtake *Pi* by accessing their critical
sections before it.

[ F1 U F2 ]{>= p} = prob (HOLDS (F1) . true)* . HOLDS (F2) is >= p end prob

where "HOLDS (*F*)" is the testing operator of PDL (Propositional Dynamic
Logic) [FL79], defined by the MCL regular formula below:

HOLDS (F) = if not (F) then false end if

Similarly, probabilistic versions of the two Until operators of ACTL (Action-based Computation Tree Logic) [DV90] can be defined in MCL as follows:

[ F1{A1} U F2 ]{>= p} = prob (HOLDS (F1) . A1)* . HOLDS (F2) is >= p end prob [ F1{A1} U{A2} F2 ]{>= p} = prob (HOLDS (F1) . A1)* . HOLDS (F1) . A2 . HOLDS (F2) is >= p end prob

The full Until operator of PCTL, as well as its action-based counterparts
derived from ACTL, can be expressed as follows (where *t* >= 0 is the number
of ticks until *F2* holds):

[ F1 U{<= t} F2 ]{>= p} = prob (HOLDS (F1) . true) { 0 ... t } . HOLDS (F2) is >= p end prob [ F1{A1} U{<= t} F2 ]{>= p} = prob (HOLDS (F1) . A1) { 0 ... t } . HOLDS (F2) is >= p end prob [ F1{A1} U{<= t}{A2} F2 ]{>= p} = prob (HOLDS (F1) . A1) { 0 ... t } . HOLDS (F1) . A2 . HOLDS (F2) is >= p end prob

where the regular subformula "*R* { 0 ... *t* }" denotes interval counting, i.e.,
the repetition of *R* between 0 and *t* times (see **mcl4**
for details).

- (a)
- if
*R*matches a transition sequence in the PTS, it cannot match also one of its prefixes. - (b)
- if
*R*matches a transition sequence in the PTS, it does this in a unique manner.

We illustrate these two conditions by considering the following PTS:

______________ | | A; prob 1 A; prob 1 | B; prob 1 | s0 ------------> s1 ------------> s2 <------------/

For condition (a), consider the following formula:

prob true* . A is >= 0 end prob

The regular subformula "true* . A" is nondeterministic, since it matches both the sequence s0--A-->s1--A-->s2 and its proper prefix s0--A-->s1. A deterministic version of this regular subformula is "(not A)* . A".

For condition (b), consider the following formula:

prob A* . (not B)* . B is >= 0 end prob

The regular subformula "A* . (not B)* . B" is nondeterministic, since it matches the sequence s0--A-->s1--A-->s2--B-->s2 both as "A* . B" and as "(not B)* . B". A deterministic version of this regular subformula is "A* . (not (A or B))* . B".

The **evaluator5**
model checker determinizes automatically the
dataless formulas, and thus the two formulas above are correctly handled.
However, the tool in its current version does not determinize data-handling
formulas, but only detects the presence of nondeterminism and signals it
by a specific warning message. It is the user's responsibility to constrain
the regular subformulas of "prob" operators so as to remove all warning
messages concerning nondeterminism, and thus to ensure the correctness
of verification.

To illustrate the warning messages concerning nondeterminism, consider the following PTS modeling a simple communication protocol:

RCV; prob 1 /------------------ s3 | ^ | | TRANS; prob 0.9 | | v SND; prob 1 | ERR; prob 0.1 s0 ----------------> s1 ----------------> s2 ^ | | | | | | RETRY; prob 1 | \--------------------/

and the MCL formula below, supposedly stored in a file "p.mcl" (with the line numbers indicated for clarity):

1 prob 2 SND . 3 ( 4 (not (RETRY or RCV))* . 5 RETRY 6 ) { 0 ... 2 } . 7 (not RCV)* . 8 RCV 9 is 10 < ? 0.9999 11 end prob

This formula expresses that the probability that a message sent (action
SND) is received (action RCV) after at most two retries (action RETRY)
caused by transmission errors is less than 99,99%. The invocation of **evaluator5**
for checking this formula on the PTS above produces the following output:

warning during optimisation phase: possibly nondeterministic probabilistic formula; check that the two sequences below do not overlap (and, if needed, ensure this by adding constraints on action formulas): SND . (* [p.mcl:2] *) not (RCV) (* [p.mcl:7] *) SND . (* [p.mcl:2] *) RETRY (* [p.mcl:5] *) 1.11 FALSE

The warning message above indicates that the regular subformula can match a transition sequence s0--SND--> ... --RETRY-->s1 in two different ways, caused by the fact that the action predicates "not (RCV)" and "RETRY" overlap (they are both satisfied by the RETRY action). Indeed, the following transition sequence:

s0--SND-->s1--ERR-->s2--RETRY-->s1--TRANS-->s3--RCV-->s0

in the PTS is matched by the regular subformula either as "SND . (not RCV)* . RCV" (corresponding to 0 retries) or as "SND . (not (RETRY or RCV))* . RETRY . (not RCV)* . RCV" (corresponding to one retry).

This nondeterminism makes the probabilities labeling the actions of this sequence to be counted twice, which yields an incorrect value 1.11 of the probability.

A deterministic version of the formula above is obtained by replacing the subformula "(not RCV)*" by the more constraining formula "(not (RETRY or RCV))*", which reflects the intended meaning of the initial property (i.e., a message is received after a number of retries between 0 and 2, these retries being captured by the "((not (RETRY or RCV))* . RETRY) { 0 ... 2 }" subformula). This revised formula is verified correctly, without any warning message, producing a probability value of 0.999 and a verdict TRUE.

Note: If a "prob" formula
triggers warning messages concerning nondeterminism, it is important to
eliminate *all* these warnings to achieve a correct verification. Indeed,
even if the computed probability is less than 1, the presence of such warnings
indicates an ambiguity in the formula, and thus the risk of having computed
a probability higher than the real one.

- [DJJL01]
- P. D'Argenio, B. Jeannet, H. Jensen, and K. Larsen. "Reachability Analysis of Probabilistic Systems by Successive Refinements." Proceedings of the Joint Intetnational Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification PAPM/PROBMIV'01, LNCS v. 2165, p. 39-56, 2001.
- [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.
- [HJ94]
- H. Hansson and B. Jonsson. "A Logic for Reasoning about Time and Reliability." Formal Aspects of Computing, v. 6, no. 5, p. 512-535, 1994.
- [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.
- [Mat06]
- R. Mateescu. "CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems." Springer International Journal on Software Tools for Technology Transfer (STTT), v. 8, no. 1, p. 37-56, 2006. Full version available as INRIA Research Report RR-5948. Available from http://cadp.inria.fr/publications/Mateescu-06-a.html
- [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.
- [MS13]
- R. Mateescu and W. Serwe. "Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols." Science of Computer Programming v. 78, no. 7, p. 843-861, 2013.
- [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**.