Table of Contents
evaluator - on-the-fly model checking of regular alternation-free mu-calculus
formulas
bcg_open [
bcg_opt]
spec[
.bcg] [
cc_opt]
evaluator [
evaluator_opt]
prop[
.mcl]
or:
caesar.open [caesar_opt] spec[.lotos] [cc_opt] evaluator [evaluator_opt]
prop[.mcl]
or:
exp.open [exp_opt] spec[.exp] [cc_opt] evaluator [evaluator_opt]
prop[.mcl]
or:
fsp.open [fsp_opt] spec[.lts] [cc_opt] evaluator [evaluator_opt]
prop[.mcl]
or:
lnt.open [lnt_opt] spec[.lnt] [cc_opt] evaluator [evaluator_opt]
prop[.mcl]
or:
seq.open [seq_opt] spec[.seq] [cc_opt] evaluator [evaluator_opt]
prop[.mcl]
evaluator takes two different inputs:
- A Labelled Transition
System, expressed either as a BCG graph spec.bcg, a LOTOS program spec.lotos,
a composition expression spec.exp, an FSP program spec.lts, a LOTOS NT program
spec.lnt, or a sequence file spec.seq.
- A temporal logic property, contained
in the file prop[.mcl], expressed as a regular alternation-free mu-calculus
formula (a definition of this logic is given below).
evaluator performs
an on-the-fly verification of the temporal property on the given Labelled
Transition System (LTS for short). The result of this verification (TRUE
or FALSE) is displayed on the standard output, possibly accompanied by
a diagnostic (see OPTIONS below).
Note: The verification method underlying
the current version of evaluator is based upon a translation of the model
checking problem into the resolution of a Boolean Equation System (BES),
which is performed on-the-fly using the algorithms provided by the caesar_solve_1
library of OPEN/CAESAR (see the corresponding manual page and the article
[Mat06] for details). Complete descriptions of regular alternation-free mu-calculus
and of the verification method are available in [MS03] (the reference article
for version 3.0 of evaluator) and in [Mat06] (the reference article for
versions 3.5 and 3.6 of evaluator).
A new version 4.0 of the model checker
is also available as evaluator4
(see the corresponding manual page
for details).
The options
bcg_opt, if any, are passed to
bcg_lib
.
The options caesar_opt, if any, are passed to caesar
and to caesar.adt
.
The options exp_opt, if any, are passed to exp.open
.
The options fsp_opt,
if any, are passed to fsp.open
.
The options lnt_opt, if any, are passed
to lnt.open
.
The options seq_opt, if any, are passed to seq.open
.
The options cc_opt, if any, are passed to the C compiler.
The following
options evaluator_opt are currently available:
- -bes [ file[.bes[.ext]] ]
- Print
in file[.bes] or, if the file name argument is missing, in file evaluator.bes,
a textual description of the BES corresponding to the evaluation of the
formula on the LTS. If present, the extension .ext must correspond to a known
file compression format (e.g., .Z, .gz, .bz2, etc.). In this case, the file containing
the BES is compressed according to the corresponding format. The list of
currently supported extensions and compression formats is given by the
$CADP/src/com/cadp_zip shell-script. This option does not influence the evaluation
of the formula. Not a default option.
- -block
- Assume that the property is specified
as a system of modal equations in a file file[.blk] that must be given as
argument to evaluator instead of prop[.mcl]. This option is mainly intended
for debugging purposes. The format of the input file is undocumented and
subject to future changes. Not a default option.
- -acyclic
- Evaluate the formula
on the LTS using an algorithm optimized for acyclic graphs. If the LTS is
not acyclic, then an error message is displayed and the execution is aborted.
This option is exclusive with -bfs, meaning that if both options are present
on the command line, the first one has priority over the other. Not a default
option.
- -bfs
- Evaluate the formula on the LTS using a breadth-first search
algorithm. Compared to -dfs, this option is generally slower, but produces
diagnostics of smaller depth. This option is exclusive with -acyclic, meaning
that if both options are present on the command line, the first one has
priority over the other. Not a default option.
- -dfs
- Evaluate the formula on
the LTS using a depth-first search algorithm. Compared to -bfs, this option
produces diagnostics of greater depth, but is generally faster and consumes
less memory for certain classes of formulas (such as those shown in EXAMPLES
OF TEMPORAL PROPERTIES below). Default option.
- -diag [ diag[.bcg] ]
- Generate
a diagnostic in BCG format (see the bcg
manual page for details)
explaining the truth value of the formula. The diagnostic is generated in
the file diag[.bcg] or, if the file name argument is missing, in the file
evaluator.bcg. The BCG files containing diagnostics can be visualized using
the bcg_draw
and bcg_edit
tools of CADP (see respective manual
pages for details). Diagnostics are (usually small) portions of the LTS
on which the formula yields the same result as when it is evaluated on
the whole LTS. If the diagnostic is a sequence of LTS transitions, it will
also be displayed on standard output using the SEQUENCE format (see the
exhibitor
manual page for the definition of the SEQUENCE format).
Not a default option.
- -expand
- Expand the macro definitions and the source
files included as libraries in the file prop[.mcl], producing as output
a file prop.xm, and stop. This option is useful for debugging purposes. Not
a default option.
- -silent
- Execute silently. Opposite of -verbose. Default option.
- -stat
- Display statistical information about the resolution of the BES corresponding
to the evaluation of the formula on the LTS. Not a default option.
- -tauconfluence
- Reduce the LTS on-the-fly modulo tau-confluence (a form of partial order reduction
that preserves branching equivalence) while evaluating the formula. This
option can be safely used only for verifying formulas adequate w.r.t. branching
equivalence, i.e., whose evaluation yields the same result on all branching
equivalent LTSs. For example, formulas belonging to the fragment ACTL-X (i.e.,
ACTL without the next time operators) are adequate w.r.t. branching equivalence
[DV90]. In some cases, this option may improve speed and memory consumption
significantly. Not a default option.
- -verbose
- Animate the user's screen, telling
what is going on. Opposite of -silent. Default option is -silent.
- -version
- Display
the current version number of the tool and stop. To be effective, this option
should occur as the first argument on the command line. Subsequent options
and/or arguments, if any, will be discarded. Not a default option.
The temporal logic used as input language for
evaluator is called
regular alternation-free mu-calculus. It is an extension
of the alternation-free fragment of the modal mu-calculus [Koz83, EL86] with
action predicates and regular expressions over action sequences. A more
elaborate version of this logic, able to express temporal properties involving
data values, has been defined and studied in [Mat98]; however, the current
version of
evaluator does not handle the data-based version of the logic.
Regular alternation-free mu-calculus allows direct encodings of "pure" branching-time
logics like CTL [CES86] or ACTL [DV90], as well as of regular logics like
PDL [FL79] or PDL-delta [Str82]. Moreover, it has an efficient model checking
algorithm, linear in the size of the formula (number of operators) and
the size of the LTS model (number of states and transitions). The logic
is built from three types of formulas, indicated in the table below.
+--------+-----------------+
| Symbol | Description |
+--------+-----------------+
| A | action formula |
| R | regular formula |
| F | state formula |
+--------+-----------------+
The BNF syntax and the informal semantics of these formulas are defined
below. In the grammar, terminal symbols are written between double quotes.
The axiom of the grammar is the F symbol.
Identifiers are built from letters,
digits, and underscores (beginning with a letter or an underscore). Keywords
must be written in lowercase. Comments are enclosed between '(*' and '*)'. Nested
comments are not allowed. evaluator is case-sensitive.
The formulas 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 noted s1-a->s2, indicates that the program from which the LTS has been
generated can move from state s1 to state s2 by performing action a.
An
action formula is a logical formula built from basic action
predicates and boolean connectives, according to the grammar below:
A ::= string
| regexp
| "true"
| "false"
| "not" A
| A1 "or" A2
| A1 "and" A2
| A1 "implies" A2
| A1 "equ" A2
A string is a sequence of zero or more characters, enclosed between double
quotes ('"'), which denotes a label 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
'#'.
string ::= "(any char but end-of-line)*"
| string1 "#" string2
A transition label of the LTS satisfies a string iff it is identical
to the corresponding character string (obtained after concatenation whenever
needed).
A regexp is a UNIX regular expression (see the regexp
manual
page for a detailed description of UNIX regular expressions), enclosed
between single quotes ('''), which denotes a predicate on the labels of the
LTS. Regexp's can be concatenated using the binary operator '#'. Strings can
be concatenated to regexp's, in which case they are implicitly converted
into regexp's.
regexp ::= 'UNIX_regular_expression'
| regexp1 "#" regexp2
| string1 "#" regexp2
| regexp1 "#" string2
A label of the LTS satisfies a regexp if it matches the corresponding
UNIX_regular_expression (obtained after concatenation whenever needed).
Syntactically, all binary operators on action formulas are left-associative.
The "not" operator has the highest precedence, followed by "and", followed
by "or", followed by "implies", followed by "equ".
The boolean operators
have the usual semantics: a label of the LTS always satisfies "true"; it
never satisfies "false"; it satisfies "not" A iff it does not satisfy A;
it satisfies A1 "or" A2 iff it satisfies A1 or it satisfies A2; it satisfies
A1 "and" A2 iff it satisfies both A1 and A2; it satisfies A1 "implies"
A2 iff it does not satisfy A1 or it satisfies A2; it satisfies A1 "equ"
A2 iff either it satisfies both A1 and A2, or none of them.
A
regular formula is a logical formula built from action formulas and the
traditional regular expression operators, according to the grammar below:
R ::= A
| "nil"
| R1 "." R2
| R1 "|" R2
| R "*"
| R "+"
where "nil" is the empty operator, "." is the concatenation operator,
"|" is the choice operator, "*" is the transitive and reflexive closure
operator, and "+" is the transitive closure operator.
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 of (consecutive) LTS transitions such
that the word obtained by concatenating their labels belongs to the regular
language defined by R.
The regular operators have the following semantics:
a sequence of LTS transitions satisfies A iff it has the form s1-a->s2, where
the label a satisfies the formula A; it satisfies "nil" iff it is empty
(i.e., it contains no transition); it satisfies R1 "." R2 iff it is the concatenation
of two sequences satisfying R1 and R2, respectively; it satisfies R1 "|"
R2 iff it satisfies R1 or it satisfies R2; it satisfies R "*" iff it is
the concatenation of zero or more sequences satisfying R; it satisfies
R "+" iff it is the concatenation of one or more sequences satisfying R.
A
state formula is a logical formula built from boolean,
modal, and fixed point operators, according to the grammar below:
F ::= "true"
| "false"
| "not" F
| F1 "or" F2
| F1 "and" F2
| F1 "implies" F2
| F1 "equ" F2
| "<" R ">" F
| "[" R "]" F
| "@" "(" R ")"
| X
| "mu" X "." F
| "nu" X "." F
where "<" R ">" F and "[" R "]" F are the possibility and necessity modal
operators, "@" "(" R ")" is the infinite looping operator, "mu" X "." F
and "nu" X "." F are the minimal and maximal fixed point operators, and
X is a propositional variable.
Syntactically, all binary operators on state
formulas are left-associative. The "not", "< >", "[ ]", "mu", and "nu" operators
have the highest precedence, followed by "and", followed by "or", followed
by "implies", followed by "equ". The fixed point operators act as binders
for the variables X in a way similar to quantifiers in first-order logic.
In each meaningful "mu" X "." F or "nu" X "." F formula, X is supposed to
have free occurrences inside F. State formulas are assumed to be syntactically
monotonic (i.e., in each fixed point formula "mu" X "." F or "nu" X "." F,
free occurrences of X in F may appear only under an even number of negations
and/or left-hand sides of implications) and alternation-free (i.e., without
mutually recursive minimal and maximal fixed point variables).
The boolean
operators have the usual semantics: a state of the LTS always satisfies
"true"; it never satisfies "false"; it satisfies "not" F iff it does not
satisfy F; it satisfies F1 "or" F2 iff it satisfies F1 or it satisfies
F2; it satisfies F1 "and" F2 iff it satisfies both F1 and F2; it satisfies
F1 "implies" F2 iff it does not satisfy F1 or it satisfies F2; it satisfies
F1 "equ" F2 iff either it satisfies both F1 and F2, or none of them.
The
modal and looping operators have the following semantics: a state of the
LTS satisfies "<" R ">" F iff there is (at least) one transition sequence
starting at the state, satisfying R, and leading to a state satisfying
F; it satisfies "[" R "]" F iff all transition sequences starting at the
state and satisfying R are leading to states satisfying F; it satisfies
"@" "(" R ")" iff there is a transition sequence starting at the state
and being an infinite concatenation of sequences that satisfy R.
The fixed
point operators have the following semantics: a state satisfies "mu" X
"." F iff it belongs to the minimal solution of the fixed point equation
X = F (X), and it satisfies "nu" X "." F iff it belongs to the maximal solution
of the same equation, where the propositional variable X denotes a set
of LTS states. Intuitively, minimal (resp. maximal) fixed point operators
allow to characterize finite (resp. infinite) tree-like patterns in the LTS.
An LTS satisfies a state formula F iff its initial state s0 satisfies F.
- Note:
- When writing complex formulas containing many operators (especially
when mixing regular and boolean operators), it is safer to use parenthesis
to enclose subformulas whenever being in doubt about the relative priorities
of the operators. Otherwise, the tool may parse and evaluate the formulas
in a way different from the user's intentions, leading to erroneous results
that may be quite difficult to track down.
- Note:
- 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
The same holds for minimal and maximal fixed point operators:
nu X . F = not mu X . not F (not X)
where F (not X) denotes the syntactic substitution of X by not X in F. The
modalities containing regular expressions can be translated in terms of
boolean operators, fixed point operators, and modalities containing only
action formulas, by recursively applying the identities below:
< nil > F = < false* > F
< R1 . R2 > F = < R1 > < R2 > F
< R1 | R2 > F = < R1 > F or < R2 > F
< R* > F = mu X . (F or < R > X)
< R+ > F = < R . R* > F
where X is a "fresh" propositional variable (the corresponding identities
for box modalities are obtained by duality). Similarly, the infinite looping
operator is equivalent to the maximal fixed point formula below:
@ (R) = nu X . < R > X
with X a "fresh" propositional variable. Note that, since the fixed point
formulas resulting after the above translations must be alternation-free,
the regular expressions present inside "@" "(" R ")" formulas may not contain
"*" or "+" operators.
The regular alternation-free
mu-calculus allows to express concisely various interesting properties. The
most useful classes of temporal properties are illustrated below.
Informally, a safety property expresses that "something bad never
happens." Typical safety properties are those forbidding "bad" execution
sequences in the LTS. These properties can be naturally expressed using
box modalities containing regular formulas. For instance, mutual exclusion
can be characterized by the following formula:
[ true* . "OPEN !1" . (not "CLOSE !1")* . "OPEN !2" ] false
which states that every time process 1 enters its critical section (action
"OPEN !1"), it is impossible that process 2 also enters its critical section
(action "OPEN !2") before process 1 has left its critical section (action
"CLOSE !1").
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.
Informally,
a liveness property expresses that "something good eventually happens."
Typical liveness properties are
potentiality assertions (i.e., expressing
the reachability on a sequence) and
inevitability assertions (i.e., expressing
the reachability on all sequences).
Potentiality assertions can be directly
expressed using diamond modalities containing regular formulas. For instance,
the following formula:
< true* . "GET !0" > true
states that there exists a sequence leading to a "GET !0" action after
performing zero or more transitions. Regular formulas allow to express succinctly
complex potentiality assertions, such as the formula below:
< true* . "SEND" . (true* . "ERROR")* . true* . "RECV" > true
stating that there exists a sequence leading (after zero or more transitions)
to a "SEND" action, possibly followed by a sequence of "ERROR" actions
(possibly separated by other actions) and leading (after zero 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.
These
are similar to liveness properties, except that they express reachability
of actions by considering only
fair execution sequences. One notion of fairness
that can be easily encoded in the logic is the "fair reachability of predicates"
defined by Queille and Sifakis [QS83]: a sequence is fair iff it does not
infinitely often enable the reachability of a certain state without infinitely
often reaching it. For instance, the following formula expresses that after
every message emission (action "SEND"), all fair execution sequences will
lead to the reception of the message (action "RECV") after a finite number
of steps:
[ true* . "SEND" . (not "RECV")* ]
< (not "RECV")* . "RECV" > true
Intuitively, the formula above considers the sequences following the "SEND"
action by "skipping" the circuits of the LTS that do not contain "RECV"
actions: it states that from every state of such a circuit, there is still
a finite sequence leading to a "RECV" action.
The use of
action formulas (and, in particular, of regexp's) may be of considerable
help when dealing with LOTOS actions having the same gate but different
values in the offers. For instance, the following formula:
< true* . 'SEND !1.*' and not 'SEND !1.*!2' > true
states the potential reachability of an action having the gate SEND and
the value of the first offer equal to 1, possibly followed by other offers
with 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* .
not ('RECV !.* !.*' and 'RECV !\(.*\) !\1')
] false
states that all message receptions (actions "RECV !source !dest") have
different source and destination fields. Note the use of the UNIX regular
expression construct `\( \)' allowing to match a portion of a string and to
re-use it later in the same regexp.
- Note:
- 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 above). This reduces both the evaluation time
and the size of the diagnostic generated for the formula.
evaluator
allows to define and use macros for temporal operators parameterized by
action and/or state formulas. This feature is particularly useful for constructing
reusable libraries encoding various temporal operators of other logics
translatable in regular alternation-free mu-calculus (like CTL and ACTL).
The
macro-definitions have the following syntax:
"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
program. The 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
source program using the following command:
"library"
<file0.mcl>"," ..."," <filen.mcl>
"end_library"
At the compilation of the program, 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 content 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/xtl. Multiple inclusions
of the same file are silently discarded.
Exit status is 0 if
everything is alright, 1 otherwise.
When the source file
prop[
.mcl]
is erroneous, error messages are issued.
- [CES86]
- E. M. Clarke,
E. A. Emerson, and A. P. Sistla. "Automatic Verification of Finite-State Concurrent
Systems using Temporal Logic Specifications." ACM Transactions on Programming
Languages and Systems, v. 8, no. 2, p. 244-263, 1986.
- [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.
- [Koz83]
- D. Kozen. "Results on the Propositional Mu-Calculus."
Theoretical Computer Science, v. 27, p. 333-354, 1983.
- [Mat98]
- R. Mateescu. "Verification
des proprietes temporelles des programmes paralleles." PhD Thesis, Institut
National Polytechnique de Grenoble, April 1998.
- [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.
- [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.
- [QS83]
- J-P. Queille and J. Sifakis.
"Fairness and Related Properties in Transition Systems - A Temporal Logic
to Deal with Fairness." Acta Informatica, v. 19, p. 195-220, 1983.
- [Str82]
- R.
S. Streett. "Propositional Dynamic Logic of Looping and Converse." Information
and Control, v. 54, p. 121-141, 1982.
Versions 1.x and 2.x of
evaluator
were developed by Marius Dorel Bozga (IMAG) and used an on-the-fly BES resolution
algorithm proposed by J-C. Fernandez and L. Mounier.
Version 3.0 of evaluator
was developed by Radu Mateescu and Mihaela Sighireanu (INRIA/VASY) and
used a completely new on-the-fly BES resolution algorithm.
Hubert Garavel
suggested the enhancement of action formulas with the string concatenation
operator, which was implemented by David Champelovier.
The enhancements
leading to the versions 3.5 and 3.6 of evaluator, which use the caesar_solve_1
library of OPEN/CAESAR for on-the-fly BES resolution, were implemented by
Radu Mateescu (INRIA/VASY).
- spec.bcg
- BCG graph (input)
- spec.exp
- network
of communicating LTSs (input)
- spec.lotos
- LOTOS specification (input)
- spec.lts
- FSP specification (input)
- spec.lnt
- LOTOS NT specification (input)
- spec.seq
- sequence file (input)
- prop.mcl
- regular mu-calculus formula (input)
- diag.bcg
- diagnostic in BCG format (output)
- file.bes
- BES in textual format (output)
- $CADP/src/xtl/*.mcl
- predefined libraries (input)
bcg
,
bcg_open
,
caesar.adt
,
caesar.open
,
caesar_graph
,
caesar_solve_1
,
caesar
,
evaluator4
,
exhibitor
,
exp.open
,
fsp.open
,
lnt.open
,
seq.open
,
regexp
Additional information is available from the CADP Web page located at http://cadp.inria.fr
Please report bugs to
Radu.Mateescu@inria.fr
Table of Contents
