Next: Symbolic Representation of Kripke
Up: Symbolic Model Checking
Previous: Symbolic Model Checking
A finite state system can be described as a tuple:
where
is a finite set of states,
is the set of initial states, and
is the transition relation, specifying
the possible transitions from state to state.
is a
function that labels states with the atomic propositions from a
given language. Such a tuple is called state transition graph or
Kripke structure [44].
Figure 1:
A State Transition Graph and its unwinding.

Temporal logics are used to predicate over the behavior defined by
Kripke structures.
A behavior in a Kripke structure is obtained starting from a state
,
and then repeatedly appending states reachable through
.
We require that the transition relation
be
total.^{2} As a consequence
all the behaviors of the system are infinite. Since a state can have more
than one successor, the structure can be thought of as unwinding into an
infinite tree, representing all the possible executions of the system
starting from the initial states. Figure 1 shows a state
transition graph and its unwinding from the state labeled with
``A''.
Two useful temporal logics are Computation Tree Logic (called
CTL) and Linear Temporal Logic (called LTL). They differ in
how they handle branching in the underlying computation tree. In CTL
temporal operators it is possible to quantify over the paths departing
from a given state. In LTL operators are intended to describe
properties of all possible computation paths.
The syntax of CTL formulas is given by the following rules:
 1.
 any atomic proposition is a CTL formula;
 2.
 if
and
are CTL formulas, then
and
are CTL formulas, where
is
any boolean connective (
);
 3.
 if
and
are CTL formulas, then
,
,
are CTL formulas.
Figure 2 describes the intuitive meaning of CTL formulas.
means that there exists (
E) a path starting
from a state
in which in the next (
X)
state
holds.
means that there exists a
path starting from a state s_{0} in which globally (
G)
holds.
there exists a
path starting from a state s_{0} in which
holds until
(
U)
holds.
The other CTL operators (e.g.,
,
meaning for all
paths eventually )
can be derived from these three according to the
rules listed in Table 1.
Table 1:
Definition of CTL operators.

For all paths, in
the next state


There
exists a path in which eventually 

Invariantly


For all paths,
until 

For all
paths, eventually 

Figure 2:
The meaning of temporal modalities.

The syntax of LTL formulas is the following:
 1.
 any atomic proposition is an LTL formula;
 2.
 if
and
are LTL formulas, then
and
are LTL formulas, where
is
any boolean connective (
);
 3.
 if
and
are LTL formulas, then
,
,
are
LTL formulas.
The model checking problem can be formally formulated as follows.
Given a Kripke structure
and a temporal logic formula
,
find the set of all states that satisfy ,
namely the set
of states

(1) 
We say that the system satisfies the specification provided that
all the initial states are in the set
:

(2) 
Each CTL formula
is identified by the set of states where it
holds,
.
CTL operators may be
characterized as a least or a greatest fixpoint of an appropriate
predicate transformer [12]:
This suggests an algorithm for symbolic model checking which
is driven by the structure of the formula. For example, the
computation of
corresponds to the
following iterations:
Iterations continue until
s_{i+1} = s_{i}. The existence of least and
greatest fixpoints is guaranteed by the monotonicity of the predicate
transformers and by the finiteness of the domain [12].
NuSMV <>