EVALUATOR manual page
Table of Contents


evaluator - a family of on-the-fly model checkers


evaluator denotes a family of on-the-fly model checkers of CADP based on the modal mu-calculus. These tools take as inputs a Labelled Transition System (LTS) and a temporal logic formula, and produce as output a verdict indicating whether the LTS satisfies the formula or not, optionally accompanied by a diagnostic (fragment of the LTS) illustrating the verdict.

On the theoretical side, these model checkers rely on the resolution of Boolean Equation Systems (BES), Parameterized Boolean Equation Systems (PBES), and Linear Equation Systems (LES). On the practical side, they are implemented using the OPEN/CAESAR framework of CADP for on-the-fly verification.

Three versions of evaluator are currently available:

Note: Currently, for backward compatibility reasons, evaluator (located in $CADP/bin.*/evaluator.a) is a shorthand for evaluator3 (located in $CADP/bin.*/evaluator3.a).

History and Authors

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. These versions, which accepted as input alternation-free modal mu-calculus (without regular expressions), are no longer available.

Version 3.0 of EVALUATOR was developed by Radu Mateescu and Mihaela Sighireanu (both at INRIA/VASY) and used a completely new on-the-fly BES resolution algorithm. Hubert Garavel (INRIA/VASY) suggested the enhancement of action formulas with the string concatenation operator, which was implemented by David Champelovier (INRIA/VASY).

Versions 3.5 and 3.6 of EVALUATOR replaced the dedicated BES resolution algorithm by the more general algorithms available in the caesar_solve_1 library of OPEN/CAESAR for on-the-fly BES resolution. All of this was implemented by Radu Mateescu (INRIA/VASY).

Version 4.0 of EVALUATOR handles version 4 of the MCL language. It was implemented by Radu Mateescu and Damien Thivolle (both at INRIA/VASY).

Version 5.0 of EVALUATOR handles version 5 of the MCL language. It was implemented by Radu Mateescu (INRIA/CONVECS).

See Also

evaluator3 , evaluator4 , evaluator5 , mcl , mcl3 , mcl4 , mcl5

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in files $CADP/INSTALLATION_*.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.


Please report bugs to Radu.Mateescu@inria.fr

Table of Contents