|
| 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 |
|
VLPN Benchmarks
VLSAT Benchmarks VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
A description of MCL can be found in the articles [MT08, MR18], which also present the on-the-fly verification method implemented in evaluator.
MCL attempts to make a compromise between expressiveness, user-friendliness, and efficiency of model checking for temporal properties involving data. MCL is based on the alternation-free fragment of the modal mu-calculus [Koz83, EL86], to which it brings three kinds of extensions:
An overview of MCL is presented below. The abstract syntax of each language construct is defined by a BNF grammar and the semantics is described informally. In the grammar, terminal symbols are written between double quotes. Optional constructs are enclosed between square brackets. The axiom of the grammar is the F symbol.
The following convention is adopted for the lists of symbols occurring in the grammar rules: the index n of the last symbol in the list is always greater or equal to 0, meaning that if the index of the first symbol is 0 (e.g., E0, ..., En), then the list must contain at least one symbol, and if the index of the first symbol is 1 (e.g., E1, ..., En), then the list may be empty.
When referring to a certain construct of the grammar, the term "enclosing formula" denotes the (action, regular, or state) formula immediately surrounding that construct.
+--------+------------------------+
| Symbol | Description |
+----------+--------+------------------------+
| | E | expression |
| | P | pattern |
| | O | offer |
| Non- | AP | action pattern |
| terminal | A | action formula |
| | R | regular formula |
| | F | state formula |
+----------+--------+------------------------+
| | K | constant |
| | X | data variable |
| Terminal | Y | propositional variable |
| | H | function or operator |
| | T | type |
+----------+--------+------------------------+
The formulas A, R, F are interpreted over an LTS <S, A, T, 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), 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. An action a has the following structure:
G v1 ... vn
where G is the name of a gate (communication channel) and v1, ..., vn are the values exchanged on G when the rendezvous underlying action a was executed. In the case that there are no values exchanged, the action is simply a gate name. There is an invisible action (named i in LOTOS and tau in other process algebras).
Note: Actions are also represented as character strings, which is useful for expressing certain action predicates (see ACTION FORMULAS below). The character string representation of actions depends on the language from which the LTS spec is generated. For example, if the input is given as a LOTOS program spec[.lotos], an action having the structure shown above will be represented as the character string "G !v1 ... !vn".
Identifiers
are built from letters, digits, and underscores (beginning with a letter
or an underscore). evaluator is case-sensitive, except for the identifiers
of predefined types and functions (see TYPES, FUNCTIONS AND CONSTANTS below).
Keywords must be written in lowercase. Comments can be either single-line,
beginning with '--', or multi-line, enclosed between '(*' and '*)'. Nested comments
are not allowed. The keywords of MCL are listed below.
among | equ | in | repeat |
and | exists | let | step |
any | exit | loop | tau |
case | export | mu | then |
choice | false | nil | to |
continue | for | not | true |
do | forall | nu | until |
else | from | of | where |
elsif | if | on | while |
end | implies | or | xor |
bool, nat, natset, int, real, char, string), equipped with the
standard functions and operators listed below.
+--------------------------------+--------------------------+ | Operator | Meaning | +--------------------------------+--------------------------+ | false, true : -> bool | boolean constants | | not : bool -> bool | negation | | or, and, implies, equ, xor : | binary boolean operators | | bool, bool -> bool | | | <, <=, >, >=, =, <> : | comparison operators | | bool, bool -> bool | | +--------------------------------+--------------------------+ | succ : nat -> nat | successor | | - : nat -> int | unary minus | | +, - : nat, nat -> nat | addition, subtraction | | *, / : nat, nat -> nat | multiplication, division | | % : nat, nat -> nat | modulo | | ^ : nat, nat -> nat | power | | string : nat -> string | convert to string | | <, <=, >, >=, =, <> : | comparison operators | | nat, nat -> bool | | +--------------------------------+--------------------------+ | empty : -> natset | empty set | | insert : nat, natset -> natset | element insertion | | remove : nat, natset -> natset | element deletion | | isin : nat, natset -> bool | membership | | card : natset -> nat | cardinal | | union, inter, diff : | binary set operators | | natset, natset -> natset | | | <, <=, >, >=, =, <> : | comparison operators | | natset, natset -> bool | | +--------------------------------+--------------------------+ | succ : int -> int | successor | | abs : int -> nat | absolute value | | sign : int -> int | returns -1, 0, 1 if arg. | | | is < 0, = 0, > 0 | | - : int -> int | unary minus | | +, - : int, int -> int | addition, subtraction | | *, / : int, int -> int | multiplication, division | | % : int, int -> int | modulo | | ^ : int, nat -> int | power | | string : int -> string | convert to string | | <, <=, >, >=, =, <> : | comparison operators | | int, int -> bool | | +--------------------------------+--------------------------+ | - : real -> real | unary minus | | +, - : real, real -> real | addition, subtraction | | *, / : real, real -> real | multiplication, division | | ^ : real, real -> real | power | | string : real -> string | convert to string | | <, <=, >, >=, =, <> : | comparison operators | | real, real -> bool | | +--------------------------------+--------------------------+ | tolower, toupper : | convert letter to lower- | | char -> char | or upper-case | | islower, isupper : | test if lower- or upper- | | char -> bool | case letter | | isalpha, isdigit, isalnum : | test if letter, digit, | | char -> bool | letter or digit | | isxdigit : | test if hexadecimal | | char -> bool | digit | | string : char -> string | convert to string | | <, <=, >, >=, =, <> : | comparison operators | | char, char -> bool | | +--------------------------------+--------------------------+ | length : string -> nat | length (number of chars) | | empty : string -> bool | test if empty string | | concat : | concatenation | | string, string -> string | | | index, rindex : | index of the first/last | | string, string -> nat | occurrence of the | | | 2nd arg. in the 1st | | prefix, suffix : | prefix/suffix of given | | string, nat -> string | length | | nth : string, nat -> char | nth character | | substr : | substring starting at an | | string, nat, nat -> string | index and having a | | | given length | | <, <=, >, >=, =, <> : | comparison operators | | string, string -> bool | | +--------------------------------+--------------------------+
The numerical, character, and string constants have a C-like syntax (e.g.,
13, -1, 1.618, 'a', '\007', '\n', "hello world\n"). In order to allow implicit type
conversions, numerical constants are overloaded as follows: a constant
of type nat can also be of type int or real, and a constant of type int
can also be of type real.
The names of the operators of type bool (constants,
negation, and binary operators) that coincide with the keywords operating
on formulas must be written in lowercase.
The binary boolean operators,
binary set and membership operators, the arithmetic operators (of types
nat, int, and real), and all comparison operators must be written in infixed
form (e.g., 1 + 2, X inter Y, 1.0 < 2.0, etc.). All the other operators must
be written in prefixed form (e.g., insert (0, empty), concat ("a", "b"),
etc.).
The operands of the binary operators of type bool ("or", "and", "implies",
"equ", "xor") are evaluated from left to right in a lazy way, i.e., the right
operand is not evaluated if the value of the left operand can determine
the value of the whole expression.
All the binary operators of the predefined types shown above are left-associative. Unary operators have the highest precedence, followed by binary operators. In the current version of the tool all binary operators are considered to be of equal precedence; parentheses must be used for imposing a desired parsing/evaluation order.
E ::= K
| X
| H E
| E1 H E2
| H "(" E1"," ..."," En ")"
| E "of" T
| "(" E ")"
The semantics of MCL expressions is described informally below. The evaluation of an expression E in a context assigning values to all data variables occurring in E yields a unique value.
K
X
H E
E1 H E2
H "(" E1"," ..."," En ")"
E "of" T
"(" E ")"
x +
(y / 2) is different from x + y / 2, which is evaluated by default as (x
+ y) / 2 since all binary operators have the same precedence.
x01 "," ... "," x0m0 ":" T0
"," ... ","
xn1 "," ... "," xnmn ":" Tn
which declares the data variables xi1, ..., ximi of type Ti for each 0 <= i
<= n. This general form of declaration is equivalent to the simplified form
below, which will be used in the remainder of this manual page: x01 ":" T0 "," ... "," x0m0 ":" T0
"," ... ","
xn1 ":" Tn "," ... "," xnmn ":" Tn
In the same way, declarations with initialization have the following general
form: x01 "," ... "," x0m0 ":" T0 ":=" E0
"," ... ","
xn1 "," ... "," xnmn ":" Tn ":=" En
which declares the data variables xi1, ..., ximi of type Ti and initializes
them with the value of the expression Ei for each 0 <= i <= n. This general
form of declaration with initialization is equivalent to the simplified
form below, which will be used in the remainder of this manual page: x01 ":" T0 ":=" E0 "," ... "," x0m0 ":" T0 ":=" E0
"," ... ","
xn1 ":" Tn ":=" En "," ... "," xnmn ":" Tn ":=" En
P ::= "any" | K | X ":" T | P "of" T | P1 "|" P2
The semantics of MCL patterns is described informally below.
"any"
K
X ":" T
P "of" T
P1 "|" P2
O ::= "?" P | "!" E
The semantics of MCL offers is described informally below.
"?" P
"!" E
Note: Pattern and expression offers involving
constants have the same semantics, e.g., ? 3.1416 is equivalent to ! 3.1416.
AP ::= "{" O0 ... On [ "where" E ] "}"
| "{" O1 ... On "..." O'1 ... O'm [ "where" E ] "}"
Action patterns inspect the structure of actions G v1 ... vn by matching
values vi against expression offers or extracting them using pattern offers.
The optional clause "where" defines a boolean expression E (a guard) that
must evaluate to true for the action pattern to match the action. All variables
declared by the offers of an action pattern are visible in the guard E
(if present) and are also exported to the enclosing formula.
The gate name G can be matched by the first offer of an action pattern in three different ways:
!"Send");
!" mark (e.g., Send). This form of matching can be applied only when
the gate name has a syntax compatible with the syntax of MCL identifiers;
?gate:string).
The semantics of MCL action patterns is described informally below.
"{" O0 ... Om [ "where" E ] "}"
This is the basic action pattern, in which all values present in the action are explicitly matched by offers. The matching of the gate name G by the offer O0 can be done in one of the three ways indicated above.
{ Send }). For
conciseness, the curly braces can be omitted in this case: one can write
simply Send in order to match an action consisting only of a gate name
Send.
"{" O1 ... Om "..." O'1 ... O'p [ "where" E ] "}"
This is a form of action pattern that enables
matching only the first m and the last p values contained in an action,
and skipping the other values (if any) in the middle. The matching of the
gate name G by the offer O1 can be done in one of the three ways indicated
above. Either one, or both groups of offers O1 ... Om and O'1 ... O'p can be absent
(i.e., m = 0 or/and p = 0). The simplest action pattern of this form (which
is always matched by any action) is { ... }.
tau" constant operator) and boolean operators. The syntax of MCL
action formulas is defined by the following grammar:
A ::= AP
| action_string
| action_regexp
| "tau"
| "true"
| "false"
| "not" A
| A1 "or" A2
| A1 "xor" A2
| A1 "and" A2
| A1 "implies" A2
| A1 "equ" A2
| "(" A ")"
Syntactically, all binary operators on action formulas are left-associative.
The "not" operator has the highest precedence, followed by "and", followed
by "or" and "xor", followed by "implies", followed by "equ".
An action formula defines a predicate over the actions of the LTS. The semantics of MCL action formulas is described informally below.
AP
action_string
"'), which denotes an action of the LTS. A string may contain
any character but '\n' (end-of-line). Double quotes are also allowed, if preceded
by a backslash ('\'). Strings can be concatenated using the binary operator
'#' according to the grammar below:
action_string ::= "(any char but end-of-line)*"
| action_string1 "#" action_string2
An action of the LTS satisfies an action_string iff its string representation is identical to the corresponding character string (obtained after concatenation whenever needed).
action_regexp
''), which denotes a predicate on the actions of the
LTS. Regexps can be concatenated using the binary operator '#' according to
the grammar below. Strings can be concatenated to regexps, in which case
they are implicitly converted into regexps.
action_regexp ::= 'UNIX_regular_expression'
| action_regexp1 "#" action_regexp2
| action_string1 "#" action_regexp2
| action_regexp1 "#" action_string2
An action of the LTS satisfies an action_regexp iff its string representation matches the corresponding UNIX_regular_expression (obtained after concatenation whenever needed).
"tau"
"true"
"false"
"not" A
A1 "or" A2
A1 "xor" A2
A1 "and" A2
A1 "implies" A2
A1 "equ" A2
"(" A ")"
If an
action pattern AP occurs as operand of a unary or binary boolean operator,
none of the data variables declared by the pattern offers of AP is exported
to the enclosing formula (e.g., action formula not { Send ?msg:nat } does
not export variable msg to the enclosing formula). In other words, only
the action formulas consisting of action patterns can export data variables
to the enclosing formula (see also REGULAR FORMULAS and the description
of modalities in STATE FORMULAS below).
R ::= A
| "nil"
| R1 "." R2
| R1 "|" R2
| R "*"
| R "+"
| R "?"
| R "{" E "}"
| R "{" E "..." "}"
| R "{" E "," "}"
| R "{" E1 "..." E2 "}"
| R "{" E1 "," E2 "}"
| "let" X0 ":" T0 ":=" E0 "," ... "," Xn ":" Tn ":=" En "in"
R
"end" "let"
| "if" F0 "then"
R0
[ "elsif" F1 "then"
R1
...
"elsif" Fn "then"
Rn
"else"
Rn+1 ]
"end" "if"
| "case" E "in"
P0 [ "where" E0 ] "->" R0
...
"|" Pn [ "where" En ] "->" Rn
"end" "case"
| "choice" X0 ":" T0 [ "among" "{" E01 "..." E02 "}" ]
"," ... ","
Xn ":" Tn [ "among" "{" En1 "..." En2 "}" ]
"in"
R
"end" "choice"
| "while" F "do"
R
"end" "while"
| "repeat"
R
"until" F "end" "repeat"
| "for" X ":" T "from" E1 "to" E2 [ "step" E3 ] "do"
R
"end" "for"
| "loop" [ "(" X0 ":" T0 ":=" E0 "," ... "," Xn ":" Tn ":=" En ")" ]
[ ":" "(" X'0 ":" T'0 "," ... "," X'm ":" T'm ")" ]
"in"
R
"end" "loop"
| "continue" [ "(" E0 "," ..."," En ")" ]
| "exit" [ "(" E0 "," ... "," Em ")" ]
| "export" "(" X0 ":" T0 ":=" E0 "," ... "," Xn ":" Tn ":=" En ")"
| "(" R ")"
Syntactically, all binary operators on regular formulas are left-associative.
The "*", "+", "?", and "{ ... }" operators have the highest precedence, followed
by ".", followed by "|".
A regular formula R denotes a sequence (represented by the couple of its source and target states) of consecutive LTS transitions such that the word obtained by concatenating the actions labeling them belongs to the regular language defined by R.
A transition sequence weakly satisfies a regular formula R iff, by deleting some of its invisible transitions, the resulting sub-sequence satisfies R. In other words, the transitions of the sequence matched by the action predicates of R (which can denote either visible or invisible actions) can be interspersed with sub-sequences of 0 or more invisible transitions.
The semantics of MCL regular formulas is described informally below.
A
All data variables exported by A are also exported to the enclosing formula.
"nil"
R1 "." R2
All data variables exported by R1 are visible in R2. For each data variable X exported by both R1 and R2, the occurrence of X exported by R2 is also exported to the enclosing formula (i.e., it overrides the occurrence of X possibly exported by R1). All the other data variables (i.e., those exported by R1 only and by R2 only) are also exported to the enclosing formula.
R1 "|" R2
None of the data variables exported by R1 (resp. by R2) is visible in R2 (resp. in R1). All data variables exported both by R1 and by R2 are also exported to the enclosing formula.
R "*"
None of the data variables exported by R is exported to the enclosing formula, since none of these variables will be initialized when the repetition formula is satisfied by an empty sequence.
R "+"
All data variables exported by R are also exported to the enclosing formula, since R is always satisfied by at least one sub-sequence of the current sequence.
R "?"
None of the data variables exported by R is exported to the enclosing formula, since none of these variables will be initialized when the option formula is satisfied by an empty sequence.
R "{" E "}"
nat. It is satisfied by a sequence
of LTS transitions iff this sequence is the concatenation of exactly E
sub-sequences, each of them satisfying R. None of the data variables exported by R is exported to the enclosing formula, since none of these variables will be initialized when the value of E is 0 (i.e., when the counting formula is satisfied by an empty sequence).
R "{" E "..." "}"
or R "{" E "," "}"
nat.
It is satisfied by a sequence of LTS transitions iff this sequence is the
concatenation of E or more sub-sequences, each of them satisfying R. None of the data variables exported by R is exported to the enclosing formula, since none of these variables will be initialized when the value of E is 0 (i.e., when the left interval counting formula is satisfied by an empty sequence).
R "{" E1 "..." E2 "}"
or R "{" E1 "," E2 "}"
nat. It is satisfied by a sequence of LTS transitions
iff this sequence is the concatenation of E1 or more (but not more than
E2) sub-sequences, each of them satisfying R.
If the value of E1 is equal
to the value of E2, the regular formula is equivalent to R { E1 }.
If the
value of E1 is larger than the value of E2, the regular formula is equivalent
to nil.
None of the data variables exported by R is exported to the enclosing formula, since none of these variables will be initialized when the value of E1 is 0 (i.e., when the interval counting formula is satisfied by an empty sequence).
"let" X0 ":" T0 ":=" E0 "," ... "," Xn ":" Tn ":=" En "in"
R
"end" "let"
Variables X0, ..., Xn are visible in R but not in the enclosing formula. All data variables exported by R are also exported to the enclosing formula (regardless of whether or not they are identical to some of the variables X0, ..., Xn).
"if" F0 "then"
R0
[ "elsif" F1 "then"
R1
...
"elsif" Fn "then"
Rn
"else"
Rn+1 ]
"end" "if"
All state formulas F0, ..., Fn occurring as conditions of the branches must be propositionally closed (i.e., they cannot contain free occurrences of propositional variables, but may contain free occurrences of data variables) in order to ensure the syntactic monotonicity condition (see STATE FORMULAS below) for the whole MCL formula.
The branches "elsif" and "else" are optional; if they are all
absent and the source state of the sequence does not satisfy F0, then the
empty sequence consisting of that state satisfies the conditional formula.
In other words, the following equality holds:
"if" F "then" R "end if"
=
"if" F "then" R "else" "nil" "end" "if"
If the "else" clause is absent, none of the data variables exported by
the regular formulas R0, ..., Rn is exported to the enclosing formula, since
none of these variables will be initialized when the conditional formula
is satisfied by an empty sequence. If the "else" clause is present, each
data variable exported simultaneously by all regular formulas R0, ..., Rn+1
is also exported to the enclosing formula.
"case" E "in"
P0 [ "where" E0 ] "->" R0
...
"|" Pn [ "where" En ] "->" Rn
"end" "case"
- v matches the pattern Pi;
- the boolean expression Ei (if present) evaluates to true in a context in which all variables declared in Pi are replaced with the corresponding values extracted from v;
- the sequence satisfies Ri in the same context.
If the value of E does not match
any of the patterns P0, ..., Pn, then an empty sequence satisfies the selection
formula. In other words, in this case the selection formula becomes equivalent
to "nil".
If some pattern Pi for some 0 <= i <= n is any, then each data variable
exported simultaneously by all regular formulas R0, ..., Ri is also exported
to the enclosing formula, since at least one of these regular formulas
will be satisfied by the current sequence. If none of the patterns Pi is
any, then none of the data variables exported by the regular formulas R0,
..., Rn is exported to the enclosing formula, since none of these variables
will be initialized when the selection formula is satisfied by an empty
sequence.
Note: For technical reasons (syntactic ambiguity concerning the
"|" symbol occurring both as choice operator and as branch separator), formulas
R0, ..., Rn must not contain the "|" operator at top-level. For instance, the
following formula is illegal:
case E in
P0 -> R1 | R2
| P1 -> R3
end case
If regular formulas with the "|" operator at top-level are required as branches
of a selection formula, then they must be surrounded by parentheses, as
in the formula below: case E in
P0 -> (R1 | R2)
| P1 -> R3
end case
which is legal.
"choice" X0 ":" T0 [ "among" "{" E01 "..." E02 "}" ]
"," ... ","
Xn ":" Tn [ "among" "{" En1 "..." En2 "}" ]
"in"
R
"end" "choice"
bool and nat are allowed currently as Tis. All data variables exported by R are also exported to the enclosing formula (regardless of whether or not they are identical to some of the variables X0, ..., Xn).
"while" F "do"
R
"end" "while"
None of the data variables exported by R is exported to the enclosing formula, since none of these variables will be initialized when the initial condition loop formula is satisfied by an empty sequence (whose source state does not satisfy F).
"repeat"
R
"until" F "end" "repeat"
All data variables exported by R are also exported to the enclosing formula, since R is always satisfied by at least one sub-sequence of the current sequence (the body of the final condition loop formula is repeated at least once).
"for" X ":" T "from" E1 "to" E2 [ "step" E3 ] "do"
R
"end" "for"
None of the data variables exported by R is exported to the enclosing formula, since none of these variables will be initialized when the bounded loop formula is satisfied by an empty sequence.
The type T of the iteration variable
can be currently the nat type only.
"loop" [ "(" X0 ":" T0 ":=" E0 "," ... "," Xn ":" Tn ":=" En ")" ]
[ ":" "(" X'0 ":" T'0 "," ... "," X'm ":" T'm ")" ]
"in"
R
"end" "loop"
An iteration of the loop is triggered when the evaluation of R on a sub-sequence of the current sequence leads to the evaluation of a "continue" subformula of R (see below), which must assign values to the input parameters X0, ..., Xn. The loop terminates when the evaluation of R on a sub-sequence of the current sequence either does not lead to the evaluation of a "continue" subformula (in this case the loop must not have output parameters), or it leads to the evaluation of an "exit" subformula of R (see below), which must assign values to the output parameters X'0, ..., X'm.
None of the data variables exported by R is exported to the enclosing formula, since none of these variables will be initialized when the general loop formula is satisfied by an empty sequence.
"continue" [ "(" E0 "," ..."," En ")" ]
"exit" [ "(" E0 "," ... "," Em ")" ]
"export" "(" X0 ":" T0 ":=" E0 "," ... "," Xn ":" Tn ":=" En ")"
"loop" "(" X0 ":" T0"," ... "," Xn ":" Tn ")" "in"
"exit" "(" E0 "," ... "," En ")"
"end" "loop"
Note: The "let" regular formula (see above) also assigns values to variables, but these variables are visible only in the regular subformula of the "let" formula and are not exported to the enclosing formula.
"(" R ")"
F ::= E
| "true"
| "false"
| "not" F
| F1 "or" F2
| F1 "xor" F2
| F1 "and" F2
| F1 "implies" F2
| F1 "equ" F2
| "<" R ">" F
| "<<" R ">>" F
| "[" R "]" F
| "[[" R "]]" F
| "<" R ">" "@"
| "<<" R ">>" "@"
| "[" R "]" "-|"
| "[[" R "]]" "-|"
| Y [ "(" E0 "," ... "," En ")" ]
| "mu" Y [ "(" X0 ":" T0 ":=" E0 "," ... ","
Xn ":" Tn ":=" En ")" ]
"." F
| "nu" Y [ "(" X0 ":" T0 ":=" E0 "," ... ","
Xn ":" Tn ":=" En ")" ]
"." F
| "exists" X0 ":" T0 [ "among" "{" E01 "..." E02 "}" ]
"," ... ","
Xn ":" Tn [ "among" "{" En1 "..." En2 "}" ]
"." F
| "forall" X0 ":" T0 [ "among" "{" E01 "..." E02 "}" ]
"," ... ","
Xn ":" Tn [ "among" "{" En1 "..." En2 "}" ]
"." F
| "let" X0 ":" T0 ":=" E0 "," ... "," Xn ":" Tn ":=" En "in"
F
"end" "let"
| "if" F0 "then"
F'0
[ "elsif" F1 "then"
F'1
...
"elsif" Fn "then"
F'n
"else"
Fn+1 ]
"end" "if"
| "case" E "in"
P0 [ "where" E0 ] "->" F0
...
"|" Pn [ "where" En ] "->" Fn
"end" "case"
| "(" F ")"
Syntactically, all binary operators on state formulas are left-associative.
The unary operators "not", "<"...">", "<<"...">>", "["..."]", "[["..."]]", "mu", "nu", "exists",
and "forall" have the highest precedence, followed by "and", followed by
"or" and "xor", followed by "implies", followed by "equ".
The minimal and
maximal fixed point operators "mu" and "nu" act as binders for the propositional
variables Y in a way that is similar to quantifiers in first-order logic.
In each meaningful "mu Y (...) . F" or "nu Y (...) . F" formula, Y is assumed to
have free occurrences inside F.
State formulas must satisfy the following two syntactic conditions:
mu Y (...) . F" or "nu Y (...) . F", free occurrences
of the propositional variable Y in F may appear only under an even number
of negations and/or left-hand sides of implications. mu Y (...) . F" cannot contain
free occurrences of propositional variables Y' defined by "nu" operators,
and each fixed point formula "nu Y (...) . F" cannot contain free occurrences
of propositional variables Y' defined by "mu" operators. When checking this
condition on a formula, strong possibility (resp. necessity) modalities
whose regular subformulas contain an iteration operator, and weak possibility
(resp. necessity) modalities are interpreted as "hidden" minimal (resp. maximal)
fixed point operators. Notice that the state formulas corresponding to infinite
looping and finite saturation operators do not satisfy the alternation-freeness
condition (see REMARKS below).
A state formula defines a predicate over the states of the LTS. The semantics of MCL state formulas is described informally below.
E
true.
"true"
"false"
"not" F
F1 "or" F2
F1 "xor" F2
F1 "and" F2
F1 "implies" F2
F1 "equ" F2
"<" R ">" F
The evaluation of F on the target state of the transition sequence is carried out in a context in which all data variables exported by R are initialized with the corresponding values extracted from the sequence. If there is no transition sequence satisfying R, then the whole possibility modality is false and F is not evaluated at all.
All data variables exported by R are visible in F, but none of them is exported outside the whole possibility modality.
"<<" R ">>" F
The evaluation of F on the target state of the transition sequence is carried out in a context in which all data variables exported by R are initialized with the corresponding values extracted from the sequence. If there is no transition sequence weakly satisfying R, then the whole weak possibility modality is false and F is not evaluated at all.
All data variables exported by R are visible in F, but none of them is exported outside the whole weak possibility modality.
The regular formula R must not contain
any occurrence of the tau action formula.
"[" R "]" F
The evaluation of F on the target state of each transition sequence is carried out in a context in which all data variables exported by R are initialized with the corresponding values extracted from that sequence. If there is no transition sequence satisfying R, then the whole necessity modality is true and F is not evaluated at all.
All data variables exported by R are visible in F, but none of them is exported outside the whole necessity modality.
"[[" R "]]" F
The evaluation of F on the target state of each transition sequence is carried out in a context in which all data variables exported by R are initialized with the corresponding values extracted from that sequence. If there is no transition sequence weakly satisfying R, then the whole weak necessity modality is true and F is not evaluated at all.
All data variables exported by R are visible in F, but none of them is exported outside the whole weak necessity modality.
The regular formula R must not
contain any occurrence of the tau action formula.
"<" R ">" "@"
None of the data variables exported by R is exported outside of the infinite looping formula.
"<<" R ">>" "@"
None of the data variables exported by R is exported outside of the weak infinite looping formula.
The regular formula R must not contain
any occurrence of the tau action formula.
"[" R "]" "-|"
None of the data variables exported by R is exported outside of the finite saturation formula.
"[[" R "]]" "-|"
None of the data variables exported by R is exported outside of the weak finite saturation formula.
The regular formula R must not contain any occurrence of the tau
action formula.
Y [ "(" E0 "," ... "," En ")" ]
"mu" Y [ "(" X0 ":" T0 ":=" E0 "," ... ","
Xn ":" Tn ":=" En ")" ]
"." F
Intuitively, a parameterized minimal fixed point formula characterizes finite subgraphs contained in the LTS. The parameters enable one to perform arbitrary computations during a forward traversal of the subgraphs.
"nu" Y [ "(" X0 ":" T0 ":=" E0 "," ... ","
Xn ":" Tn ":=" En ")" ]
"." F
Intuitively, a parameterized maximal fixed point formula characterizes infinite subgraphs contained in the LTS. The parameters enable one to perform arbitrary computations during a forward traversal of the subgraphs.
"exists" X0 ":" T0 [ "among" "{" E01 "..." E02 "}" ]
"," ... ","
Xn ":" Tn [ "among" "{" En1 "..." En2 "}" ]
"." F
bool and nat are allowed currently as Tis. The variables X0, ..., Xn are visible only in F and are not exported outside the existential quantification formula.
Note: The existential quantifier is not, strictly speaking, a primitive
operator of MCL. It can be seen as an abbreviation of the disjunction operator.
Assuming that the domain of variable Xi is { vi0, ... vimi } for 0 <= i <= n,
the existential quantification formula is equivalent to the disjunction
below:
F (v00, ..., vn0) or ... or F (v00, ..., vnmn)
or ... or
F (v0m0, ..., vn0) or ... or F (v0m0, ..., vnmn)
where F (v0j, ..., vnk) denotes the state formula F in which all occurrences of variables X0, ..., Xn are substituted with the values v0j, ..., vnk, respectively. In practice, the usage of the existential quantifier may yield much more concise formulations of properties than its equivalent disjunctive formulation.
"forall" X0 ":" T0 [ "among" "{" E01 "..." E02 "}" ]
"," ... ","
Xn ":" Tn [ "among" "{" En1 "..." En2 "}" ]
"." F
bool and nat
are allowed currently as Tis. The variables X0, ..., Xn are visible only in F and are not exported outside the universal quantification formula.
Note:
The universal quantifier is not, strictly speaking, a primitive operator
of MCL. It can be seen as an abbreviation of the conjunction operator. Assuming
that the domain of variable Xi is { vi0, ... vimi } for 0 <= i <= n, the universal
quantification formula is equivalent to the conjunction below:
F (v00, ..., vn0) and ... and F (v00, ..., vnmn)
and ... and
F (v0m0, ..., vn0) and ... and F (v0m0, ..., vnmn)
where F (v0j, ..., vnk) denotes the state formula F in which all occurrences of variables X0, ..., Xn are substituted with the values v0j, ..., vnk, respectively. In practice, the usage of the universal quantifier may yield much more concise formulations of properties than its equivalent conjunctive formulation.
"let" X0 ":" T0 ":=" E0 "," ... "," Xn ":" Tn ":=" En "in"
F
"end" "let"
The variables X0, ..., Xn are visible only in F and are not exported outside the variable definition formula.
"if" F0 "then"
F'0
[ "elsif" F1 "then"
F'1
...
"elsif" Fn "then"
F'n
"else"
Fn+1 ]
"end" "if"
All state formulas F0, ..., Fn occurring as conditions of the branches must be propositionally closed (i.e., they cannot contain free occurrences of propositional variables, but may contain free occurrences of data variables) in order to ensure the syntactic monotonicity condition for the whole MCL formula.
The branches "elsif" and "else" are optional; if they are all absent
and the state does not satisfy F0, then this state satisfies the conditional
formula. In other words, the following equality holds:
"if" F0 "then" F'0 "end if"
=
"if" F0 "then" F'0 "else" "true" "end" "if"
"case" E "in"
P0 [ "where" E0 ] "->" F0
...
"|" Pn [ "where" En ] "->" Fn
"end" "case"
- v matches the pattern Pi;
- the boolean expression Ei (if present) evaluates to true in a context in which all variables declared in Pi are replaced with the corresponding values extracted from v;
- the state satisfies Fi in the same context.
If the value of E does not match any of the patterns P0, ..., Pn, then the selection formula is true.
"(" F ")"
An LTS satisfies a state formula F iff its initial state s0 satisfies F.
The PTS must contain only labeled 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 evaluator 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.
The probabilistic operator belongs to the state formulas of MCL. Its syntax is defined by the following grammar:
F ::= "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 evaluator
.
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" 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%:
prob
(not SEND)* . SEND . ((not RETRY)* . 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
(not GRANT)* . GRANT
is
>= 1
end prob
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):
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. This formula will be evaluated to TRUE and evaluator
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.
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:
[ 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.
prob" formula on a PTS is
translated into the resolution of a well-formed LES (i.e., without singularities),
the regular subformula R must be deterministic, meaning that it must satisfy
two conditions:
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. The deterministic conversion 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". The deterministic conversion of this regular subformula is "A* . (not (A or B))* . B".
The evaluator model checker determinizes automatically the dataless formulas, and thus the two nondeterministic formulas above are converted to deterministic ones and translated to well-formed LESs.
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 evaluator 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.
For efficiency reasons, when using fixed point operators, it is recommended to put the recursive call of the propositional variable at the rightmost place in the formula (as in all fixed point formulas shown below). This reduces both the evaluation time and the size of the diagnostic generated by evaluator for the formula.
Not all operators defined above are primitive
constructs of the logic. The boolean operators "false", "and", "implies",
and "equ" can be expressed in terms of "true", "or", and "not" in the usual
way. The diamond and box modalities are dual:
[ R ] F = not < R > not F
[[ R ]] F = not << R >> not F
The same holds for minimal and maximal fixed point operators (only parameterless versions are illustrated below):
nu Y . F = not mu Y . not F (not Y)
where F (not Y) denotes the syntactic substitution of Y by not Y in F.
The modalities containing regular formulas can be translated in terms of boolean operators, fixed point operators, and modalities containing only action formulas. A few examples of such translations are given below (see [MS03, MT08] for the translation of the other MCL modalities):
< nil > F = < false* > F
< R1 . R2 > F = < R1 > < R2 > F
< R1 | R2 > F = < R1 > F or < R2 > F
< R? > F = < nil | R > F
< R* > F = mu Y . (F or < R > Y)
< R+ > F = < R . R* > F
where Y is a "fresh" propositional variable (the corresponding identities
for box modalities are obtained by duality). The infinite looping operator and the finite saturation operator are opposites:
< R > @ = not [ R ] -|
<< R >> @ = not [[ R ]] -|
These operators can be translated in terms of fixed point operators (where Y is a "fresh" propositional variable) as follows:
< R > @ = nu Y . < R > Y
<< R >> @ = nu Y . << R >> Y
[ R ] -| = mu Y . [ R ] Y
[[ R ]] -| = mu Y . [[ R ]] Y
When the regular formula R contains iteration operators, the fixed point formulas above belong to the mu-calculus fragment of alternation depth two [EL86]. An example of such MCL formula is the following:
< true* . A > @This formula is equivalent (by applying the translations above) to the fixed point formula below:
nu Y1 . mu Y2 . (< A > Y1 or < true > Y2)This formula is of alternation depth two (and therefore not expressible in alternation-free mu-calculus) because it contains a maximal fixed point variable Y1 and a minimal fixed point variable Y2 that are mutually recursive.
evaluator handles in the same way the infinite looping and finite saturation operators or their equivalent fixed point formulas. Moreover, in the fixed point formulas equivalent to infinite looping and finite saturation operators, evaluator accepts propositional variables Y parameterized by data values (see FAIRNESS PROPERTIES below).
Note: Early versions of evaluator
accepted the syntax "@ ( R )" for the infinite looping operator. This syntax
is now obsolete, but still accepted by evaluator for backward compatibility.
It is recommended to use the new syntax "< R > @", which is closer to the
syntax of possibility modalities and reflects more intuitively the existence
of an infinite sequence, which always ends with a cycle ("@") in a finite-state
LTS.
A fixed point formula "mu" X "." F or "nu" X "." F is unguarded [Koz83]
if F contains at least one free occurrence of X which is not preceded (not
necessarily immediately) by a modality. The evaluation of an unguarded formula
on an LTS may yield a BES with cyclic dependencies between variables even
if the LTS is acyclic.
Typically, a state formula containing regular modalities with nested star operators may yield after translation an unguarded mu-calculus formula. For example, in the following formula:
< A1** . A2 > true =
mu X1 . (< A2 > true or mu X2 . (X1 or < A1 > X2)
the free occurrence of X1 is not preceded by any modality, and hence the formula is unguarded.
Unguarded occurrences of propositional variables can always be eliminated from a mu-calculus formula, at the price of an increase in size [Koz83, Mat02].
[ R ] false.
For example, mutual exclusion can be characterized by the following formula:
[ true* . "ENTER !1" . (not "LEAVE !1")* . "ENTER !2" ] false
which states that every time process 1 enters its critical section (action
"ENTER !1"), it is impossible that process 2 also enters its critical section
(action "ENTER !2") before process 1 has left its critical section (action
"LEAVE !1").
Notice that this formula does not make any assumption about
the fact that a process enters/leaves several times its critical section,
i.e., the formula does not forbid sequences of the form "ENTER !1 . ENTER
!1 . LEAVE !1 . LEAVE !1".
The above formula can be made parametric w.r.t. the number of processes in the system, by using action predicates equipped with data variables:
[ true* . { ENTER ?m:Nat } . (not { LEAVE !m })* .
{ ENTER ?n:Nat where m <> n } ] false
where the values of m, n captured by the action predicates { ENTER ?m:Nat
} and { ENTER ?n:Nat } are propagated to the enclosing formula in order
to ensure that a process n different from m cannot enter its critical section
before process m has left it (action predicate { LEAVE !m }).
Regular formulas equipped with counters provide a useful means for describing safety properties depending on data. The formula below expresses (part of) the safety of a n-place buffer:
[ (INPUT . (not OUTPUT)*) { n + 1 } ] false
by forbidding the existence of a sequence containing more than n insertions of elements in the buffer (action INPUT) without any deletions of elements in between (action OUTPUT).
A more precise formulation of the above property can be obtained by using a fixed point operator parameterized by a counter c, which stores the number of elements (initially 0) currently present in the buffer:
nu Buffer (c:Nat := 0) . (
[ INPUT ] ((c < n) and Buffer (c + 1))
and
[ OUTPUT ] ((c > 0) and Buffer (c - 1))
and
[ not (INPUT or OUTPUT) ] Buffer (c)
)
The number of elements c in the buffer is equal to the difference between the number of elements inserted and deleted from the buffer, and for a n-place buffer c must belong to 0..n.
Other typical safety properties are the invariants, expressing that every state of the LTS satisfies some "good" property. For example, deadlock freedom can be expressed by the formula below:
[ true* ] < true > true
stating that every state has at least one successor. Alternately, this formula may be expressed directly using a fixed point operator:
nu X . (< true > true and [ true ] X)
but less concisely than by using a regular formula.
The "natset" type is
useful for expressing the occurrence of a set of actions in any order. For
instance, the fact that natural numbers inserted in a bag (initially empty)
can be retrieved in any order can be expressed by the MCL formula below:
nu Bag (b:NatSet := empty) . (
[ { PUT ?n:nat } ] Bag (insert (n, b))
and
[ { GET ?n:nat } ] ((n isin b) and Bag (remove (n, b)))
and
[ not ({ PUT ... } or { GET ... }) ] Bag (b)
)
Here the action predicates { PUT ?n:Nat } and { GET ?n:Nat } denote the
insertion and retrieval of a natural number into/from the bag, respectively.
Potentiality assertions
can be directly expressed using diamond modalities of the form < R > true.
For instance, the following formula:
< true* . { PUT ?n:Nat } . true* . { GET !n } > true
states that there exists a sequence that passes (after 0 or more transitions) through a PUT n action for some natural number n, and then leads (after 0 or more transitions) to a GET n action.
Regular formulas allow to express succinctly complex potentiality assertions, such as the formula below:
< true* . SEND . (true* . RETRY) { 0 ... max } .
true* . RECV > true
stating that there exists a sequence leading (after 0 or more transitions) to a SEND action, possibly followed by a sequence of at most max RETRY actions (possibly separated by other actions) and leading (after 0 or more transitions) to a RECV action.
Inevitability assertions can be expressed using fixed point operators. For instance, the following formula:
mu X . (< true > true and [ not START ] X)
states that all transition sequences starting at the current state lead to START actions after a finite number of steps.
Similarly, temporal properties containing both safety and liveness aspects can be expressed by combining box modalities and inevitability operators. For example, the response property stating that every emission of a message must be inevitably followed in the future by the reception of the same message can be expressed by the MCL formula below:
[ true* . { SEND ?n:Nat } ]
mu X . (< true > true and [ not { RECV !n } ] X)
Notice how variable n is assigned in the box modality by capturing the
value of a message sent (action predicate { SEND ?n:Nat }) and is used
later in the body of the fixed point formula (action predicate { RECV !n
}).
[ true* . SEND . (not RECV)* ] < (not RECV)* . RECV > true
Intuitively, the formula above considers the sequences following the SEND action by "skipping" the cycles of the LTS that do not contain RECV actions: it states that from every state of such a cycle, there is still a finite sequence leading to a RECV action.
More elaborated forms of fairness can be expressed by specifying the absence of unfair execution sequences, which can be characterized using the infinite looping operator. For example, the formula MCL below expresses that after process i has requested access to a resource, it cannot be indefinitely preempted by another process j:
[ true* . { REQUEST ?i:Nat } ]
not < (not { GRANT !i })* . { REQUEST ?j:Nat where j <> i } .
(not { GRANT !i })* . { GRANT !j } > @
This formula can be expressed more concisely by propagating the negation in front of the infinite looping operator and using the finite saturation operator:
[ true* . { REQUEST ?i:Nat } ]
[ (not { GRANT !i })* . { REQUEST ?j:Nat where j <> i } .
(not { GRANT !i })* . { GRANT !j } ] -|
The existence of complex cycles can be specified using the fixed point
formulation of the infinite looping operator, in which the propositional
variable has data parameters. The formula below expresses the existence
of a cycle on which the pairs emission-reception of messages n=0..4 occur
in this order:
nu Y (n:Nat := 0) .
< true* . { PUT !n } . true* . { GET !n } >
Y ((n + 1) % 5)
Other, more elaborated examples of fairness properties can be found in [MT08, MS10].
< true* . 'SEND !1.*' and not 'SEND !1.*!2.*' > true
states the potential reachability of an action having the gate SEND followed by the value 1, possibly followed by other values different from 2.
Moreover, action formulas combined with modalities allow to express invariants over actions (i.e., action formulas that must be satisfied by all transition labels of the LTS). For instance, the following formula:
[ true* . { RECV ?src:Nat ?dest:Nat where src <> dest } ] false
states that all message receptions have different source and destination fields. Another way of formulating this property is by using regexps on character strings:
[ true* .
not ('RECV !.* !.*' and 'RECV !\(.*\) !\1')
] false
Notice the use of the UNIX regular expression construct `\( \)' allowing to match a portion of a string and to reuse it later in the same regexp.
"macro" M "(" P1"," ..."," Pn ")" "="
<text>
"end_macro"
The above construct defines a macro M having the parameters P1, ..., Pn and the body <text>, which is a string of alpha-numeric characters (normally) containing occurrences of the parameters P1, ..., Pn. For example, the following macro-definition:
macro EU_A (F1, A, F2) =
mu X . ((F2) or ((F1) and < A > X))
end_macro
encodes the "Exists Until" operator of ACTL, which states that there exists a sequence of transitions leading to a state satisfying F2 such that all intermediate states satisfy F1 and all intermediate labels satisfy A.
The calls of a macro M have the following form:
M "(" <text1>"," ..."," <textn> ")"
where the arguments <text1>, ..., <textn> are strings. The result of the call is the body <text> of the macro M in which all occurrences of the parameters Pi have been syntactically substituted with the arguments <texti>, for all i between 1 and n. For example, the following call:
EU_A (true, not "SEND", < "RECV" > true)
expands into the formula below:
mu X . ((< "RECV" > true) or ((true) and < not "SEND" > X))
A macro is visible from the point of its definition until the end of the MCL formula. Macros may be overloaded: several macros with the same name, but different arities, may be defined in the same scope.
Various macro-definitions (typically encoding the operators of some particular temporal logic) can be grouped into files called libraries. These files may be included in the MCL file using the following command:
"library"
<file0.mcl>"," ..."," <filen.mcl>
"end_library"
At the compilation of the MCL file, the above construct is syntactically replaced with the contents of the files <file0.mcl>, ..., <filen.mcl>, placed one after the other in this order. For example, the following command:
library actl.mcl end_library
is syntactically replaced with the contents of the file actl.mcl, which implements the ACTL operators.
The included files are searched first in the current directory, then in the directory referenced by $CADP/src/mcl. Multiple inclusions of the same file are silently discarded.
The infinite looping operator, whenever it is applied to a regular subformula containing iteration operators, belongs to the mu-calculus fragment of alternation depth two [EL86]. It is able to express the existence of complex cycles (containing regular sub-sequences) in the LTS, which cannot be expressed using the other operators of MCL because they belong to the alternation-free fragment of the modal mu-calculus. In particular, the infinite looping operator can express the existence of accepting cycles in Buchi automata, which underlies the classical verification procedure for LTL (Linear Time Logic) [CGP00].
Therefore, MCL strictly subsumes both CTL and LTL, since these two logics are not comparable w.r.t. their expressive power (each of them is able to express properties that the other one cannot). MCL also syntactically subsumes PDL-delta, which was shown to be more expressive than CTL* [Wol82].
When dealing with finite-state LTS models, the presence of data-handling constructs does not, strictly speaking, increase the expressiveness of MCL because one can instantiate all parameters present in an MCL formula based on the finite set of values contained in the transition labels of the LTS. However, in practice the data-handling constructs lead to significant simplifications and reductions in size of the formulas, thus facilitating the specification activity and reducing the risk of errors.
Note: The linear-time model checking complexity obtained for PDL-delta does not imply a similar result for LTL or CTL*, since the translations of these logics in PDL-delta are not guaranteed to be succinct.
The evaluation of fixed points having parameters of infinite types (e.g., nat, string, etc.) may diverge when the number of fixed point variable instances is unbounded. Therefore, parameterized fixed points should be used with the same care as recursive functions in programming languages (note however that cycles Y (v0, ..., vn) -> ... -> Y (v0, ..., vn) do no harm, since BES resolution algorithms can handle cyclic dependencies between variables). The evaluation of all extended regular operators involving counters is guaranteed to converge, because it always creates a finite number of fixed point variable instances, bounded by the values of counters and/or the number of LTS states.
A description of RAFMC can be found in [MS03, Mat06], which also present the linear-time, on-the-fly verification methods implemented in versions 3.0 and 3.5 of evaluator, respectively. The syntax of RAFMC is the following:
A ::= action_string
| action_regexp
| "true"
| "false"
| "not" A
| A1 "or" A2
| A1 "and" A2
| A1 "implies" A2
| A1 "equ" A2
R ::= A
| "nil"
| R1 "." R2
| R1 "|" R2
| R "?"
| R "*"
| R "+"
F ::= "true"
| "false"
| "not" F
| F1 "or" F2
| F1 "and" F2
| F1 "implies" F2
| F1 "equ" F2
| "<" R ">" F
| "[" R "]" F
| "<" R ">" "@"
| "[" R "]" "-|"
| Y
| "mu" Y "." F
| "nu" Y "." F
Action labels in RAFMC are considered merely as character strings, i.e., there is no handling of data values. The regular formulas contained in the infinite looping and finite saturation operators are iteration-free.
RAFMC has the same expressiveness as the alternation-free mu-calculus; however, in practice it enables a more concise and intuitive description of temporal logic properties, due to the presence of regular formulas.
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.