... checker.¹

The material presented in this paper is self-contained. This paper is readable with ordinary efforts for someone with some background in formal methods.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... total.²

A transition relation $\mathcal{R} \subseteq S\times S$ is total if and only if for each state $s \in \mathcal{S}$ there exists a state $s' \in \mathcal{S}$ such that $(s,s') \in \mathcal{R}$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...[23,28,51].³

This is almost true. However, the very first implementation of the CESAR tool was a symbolic model checker. See [52] for more details.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... variables.⁴

For non boolean state variables a boolean encoding can be performed.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... shell.⁵

The output was slightly modified to make it more readable.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... built.⁶

This file can be generated by hand by the user or automatically by activating the automatic variable ordering to reduce the size of the BDDs and saving the results with the write_order command.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

....⁷

This has the effect that for examples the BDD representing the encoding of st = c is only in terms of the boolean variables st₀ and st₁.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...$F_k(\ensuremath{\underline{x}} ) = R_k(\ensuremath{\underline{x}} )\wedge\overline{R_{k-1}(\ensuremath{\underline{x}} )}$⁸

If $\mathcal{A}$ is a set, then with $\overline{\mathcal{A}}$ we mean the complement set.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...INVAR⁹

INVAR specifies time invariants using propositional formulas.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... specification¹⁰

In the NUSMV input language this specification is written as SPEC AG(alpha -> ABF 0..4 beta)

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... fairness,¹¹

A typical fairness property is ``if a process is infinitely often executable then it is infinitely often executed'', that corresponds to the LTL formula: `` $\mathbf{GF}(P.executable) \rightarrow \mathbf{GF}(P.executed)$''.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... model.¹²

Other model checkers [6,41] are able to perform LTL model checking. In VIS [6], for example, it is possible to perform LTL model checking by using the language emptiness feature [60], but the user has to write by hand the automaton representing the acceptance condition of the LTL formula, and for each formula a different input file has to be generated and the computation must restart from scratch.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... extended.¹³

A similar philosophy of developing an open platform is advocated by the authors of the CADP tool-box [34].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... netlist¹⁴

A netlist is a representation of a design at the structural level. A FSM can be viewed as a behavioral description of the design. A netlist is much closer to the implementation of the design than a simple FSM. A netlist is essentially the data structure used by many logic synthesis tools ,like VIS[6], to internally represent designs derived from HDL descriptions.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...Purify¹⁵

More information on this tool can be found at the url ``|http://www.pureatria.com|''.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... tool.¹⁶

More information about the ext documentation tool can be found at the url ``|http://alumnus.caltech.edu/ sedwards/ext|''

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... memory¹⁷

It is the maximum amount of memory allocated during state space generation and search, namely, the amount of memory allocated since the program starts to the end of the computation before freeing all the memory allocated.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...[20,21].¹⁸

See [37] for an introduction and a survey of planning as model checking.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.