CHAPTER 4
MODEL CHECKING OF
FINITE-STATE SYSTEMS
One way to show that a program or system meets the designer’s specification is to
manually construct a proof using axioms and inference rules in a deductive system
such as temporal logic, a first-order logic capable of expressing relative ordering
of events. This traditional, manual approach to concurrent program verification is
tedious and error-prone even for small programs. For finite-state concurrent systems
and systems that can be represented as such, we can use model checking instead of
proof construction to check their correctness relative to their specifications.
In the model checking approach, we represent the concurrent system as a finite-
state graph, which can be viewed as a finite Kripke structure. The specification or
safety assertion is expressed in propositional temporal logic formulas. We can then
check whether the system meets its specification using an algorithm called a model
checker. In other words, the model checker determines whether the Kripke structure
is a model of the formula(s). Several model checkers are available and they vary in
code and run-time complexity. Here we describe one of the first model checkers, pro-
posed by [Clarke, Emerson, and Sistla, 1986], and a more efficient symbolic model
checker, developed later by [Burch et al., 1990a].
In Clarke, Emerson, and Sistla’s [1986] approach, the system to be checked is
represented by a labeled finite-state graph and the specification is written in a propo-
sitional, branching-time temporal logic called computation tree logic (CTL). The use
of linear-time temporal logic, which can express fairness properties, is ruled out since
a model checker such as logic has high complexity. Instead, fairness requirements
are moved into the semantics of CTL. In this chapter, we use the terms program and
system interchangeably.
86
Real-Time Systems: Scheduling, Analysis, and Verification. Albert M. K. Cheng
Copyright
¶ 2002 John Wiley & Sons, Inc.
ISBN: 0-471-18406-3

program and observing the changes in the program variables. We can then construct
the finite-state graph as described above and shown in Figure 4.1.
Note that given a particular system to be specified, we can model it with the level
of details required by our goal. In the railroad crossing example, each position of the
train can be further divided into more precise numerical coordinates. This of course
requires more states and transitions in the CTL structure, which in turn makes the
analysis more complex.
The state-graph construction is very important since the correctness of the model
checking depends on correctly capturing the concurrent program to be checked in the
state graph. This construction is not discussed in [Clarke, Emerson, and Sistla, 1986]
but an algorithm for it can be easily implemented [Cheng et al., 1993; Zupan and
Cheng, 1994b] (see chapters 10 and 12). We first formally define the CTL structure.
88 MODEL CHECKING OF FINITE-STATE SYSTEMS
S
0
(GATE_UP, BEFORE_APPROACH)
(GATE_DOWN, AFTER_CROSSING)
(GATE_DOWN, CROSSING)
(GATE_DOWN, NEAR_CROSSING)
(GATE_UP, APPROACH)
S
1
S
2
S
3
S
4
Figure 4.1 CTL structure for the railroad crossing system.
CTL Structure: Formally, the CTL structure (state graph) is a triple, M =

computation path there exists an initial prefix of the path such that f
2
holds at the
CLARKE–EMERSON–SISTLA MODEL CHECKER 89
last state of the prefix and f
1
holds at all other states along the prefix. Alternatively,
the formula E[ f
1
U f
2
] means that for some computation path there exists an initial
prefix of the path such that f
2
holds at the last state of the prefix and f
1
holds at all
other states along the prefix.
To simplify the specification, we use the following abbreviations. AF( f ) means
A[True U f ]: f holds in the future along every path from the initial state s
0
,so f
is inevitable. EF( f ) means E[True U f ]: some path from the initial state s
0
exists
that leads to a state at which f holds, so f potentially holds. EG( f ) means NOT
AF(NOT f ): some path from the initial state s
0
exists on which f holds at every
state. AG( f ) means NOT EF(NOT f ): f holds at every state on every path from the

tation to write the formulas. Now the length of a formula is equal to the total number
of operands and operators in it. Suppose that formula f is assigned an integer i.If f
is unary (e.g., f = NOT f
1
), then we assign the integers i +1 through i + length( f
1
)
to the subformulas of f
1
.If f is binary (e.g., f = AU f
1
f
2
), then we assign the
integers i + 1 through i + length( f
1
) to the subformulas of f
1
and i + length( f
1
) + 1
through i + length( f
1
) +length( f
2
) to the subformulas of f
2
. Using this assignment,
in one pass through f , we can build two arrays, nf[length( f )] and sf[length( f )],
where nf[i] is the ith subformula of f in the above numbering and sf[i] is the list

short i;
switch(nf[fi-1][0].opcode)
{
case atomic:
atf(fi,s,b);
break;
case nt:
ntf(fi,s,b);
break;
case ad:
adf(fi,s,b);
break;
case ax:
axf(fi,s,b);
break;
case ex:
exf(fi,s,b);
break;
CLARKE–EMERSON–SISTLA MODEL CHECKER 91
case au:
for (i=0; i <= numstates; i++)
marked[i] = false;
for (i=0; i <= numstates; i++)
if (!marked[i])
auf(fi,s,b);
break;
case eu:
euf(fi,s,b);
break;
}

{
if (labeled[s][fi-1])
*b = true;
else *b = false;
}
92 MODEL CHECKING OF FINITE-STATE SYSTEMS
else
/*
#
# If the state has not been visited (marked), mark it and check to see
# if it is labeled with the argument 2.
#
*/ {
marked[s] = true;
if (labeled[s][a2-1] || initlabeled(s,nf[a2-1]))
{
addlabel(s,fi,labeled);
*b = true;
}
else if (!(labeled[s][a1-1] || initlabeled(s,nf[a1-1])))
{
*b = false;
}
else {
/*
#
# For all successor states of s, check to see if f is true.
#
*/
s1=0;

∗
,
(number of states in CTL structure + number of transitions)).
4.3 EXTENSIONS TO CTL
Extensions to CTL are needed to handle the verification of correctness along fair ex-
ecution sequences and to specify absolute time instead of relative ordering of events.
Here, we discuss how to extend CTL to handle fairness properties. For example, with
a real-time rule-based program, we would like to consider the execution paths (se-
quences of rule firings) in which enabled rules are equally likely to be selected for
execution, that is, a fair scheduler is assumed. Similarly, with a collection of con-
current processes, we would like to consider only the computation paths in which
each process is executed infinitely often. In general, a fairness condition asserts that
requests for service are granted sufficiently often [Garbay et al., 1980]. Many def-
initions exist of “requests” and “sufficiently often.” Here, we say a path is fair if
enabled events in each state along the path are equally likely to happen.
CTL cannot express the correctness of fair executions. More precisely, the prop-
erty that some proposition P should eventually hold on all fair executions cannot be
specified in CTL. To handle fairness while maintaining an efficient model checking
algorithm, we modify the semantics of CTL [Clarke, Emerson, and Sistla, 1986] to
yield a new logic called CTL-F. It has the same syntax but a structure is now a 4-tuple
(S, R, P, F ),whereS, R, P have the same meaning as described earlier and F is a
collection of predicates on S. A path is F-fair iff for each g ⊆ F, infinitely many
states on the path satisfy predicate g. In CTL-F, all path quantifiers range over fair
paths but the semantics remain the same as in CTL. For any given finite structure
M = (S, R, P), collection F = G
1
, ,G
n
of subsets of S,andstates
0

based program written in the EQL (equational logic) language (described in chapter
10) will always terminate. The purpose of the following program is to determine
whether an object is detected at each monitor-decide cycle. The system consists of
two processes and an external alarm clock which invokes the program by periodically
setting the variable wakeup to true.
(* Example EQL Program *)
PROGRAM distributed;
CONST
false = 0;
true = 1;
a=0;
b=1;
VAR
synca,
syncb,
wakeup,
objectdetected : BOOLEAN;
arbiter : INTEGER;
INPUTVAR
sensora,
sensorb : INTEGER;
INIT
synca := true,
syncb := true,
wakeup := true,
objectdetected := false,
arbiter := a
RULES
(* process A *)
objectdetected := true ! synca := false

other process. Initially, process A is given mutually exclusive access to variables
objectdetected and synca.
The EQL program with the initial input values can be represented by a finite state–
space graph. An automatic graph generator for this purpose is available [Cheng et al.,
1993].
Finite State Space Graph Corresponding to Input Program:

state next states

rule # 1 2 3 4 5 6
0: 100000
1: 112111
2: 222222
State Labels:

state (synca, syncb, wakeup, objectdetected, arbiter, sensora, sensorb)
0 1110010
1 0111010
2 1101110
Next, we write the CTL temporal logic formula for checking whether this program
will reach a fixed point in finite time from the initial state corresponding to the initial
96 MODEL CHECKING OF FINITE-STATE SYSTEMS
input and program variable values. This formula, together with the representation
of the labeled state–space graph, is the input to the model checker and the timing
analyzer.
3
110
011
001
0 n1 ;

j
|,where|X
i
|, |S
j
| are respectively the size
of the domains of the ith input and j th program variable. If all variables are binary,
then this number is 2
n+m
. In practice, the number of reachability graphs that must
be checked is substantially less because many combinations of input and program
variable values do not constitute initial states.
4.5 COMPLETE CTL MODEL CHECKER IN C
/*===========================================================================*/
/* */
/* Program Model Checker Albert Mo Kim Cheng */
/* */
/* Description of the Program: */
/* */
/* This program implements the Clarke-Emerson-Sistla algorithm */
/* for verifying finite-state concurrent systems using temporal logic */
/* specifications. */
/* */
/* */
COMPLETE CTL MODEL CHECKER IN C 97
/* */
/* Input: */
/* 1. global state transition graph e */
/* 2. initial labels flabel */
/* 3. temporal logic formula to be proved */

/* 17. readlabel - reads in the initial labels of the graph */
/* 18. printheading - prints program heading */
/* 19. printoutput - prints labeled graph and proof result */
/* */
/*===========================================================================*/
/* program modelchecker */
#include <stdio.h>
#include <local/ptc.h>
#define maxstates 100 /* maximum number of states in the global */
/* state transition graph */
#define maxflength 100 /* maximum length of the input formula */
/* */
98 MODEL CHECKING OF FINITE-STATE SYSTEMS
#define atomic 0
#define nt 1
#define ad 2
#define ax 3
#define ex 4
#define au 5
#define eu 6
typedef byte operatortype;
typedef struct item *itemptr;
struct item
{
short ip;
itemptr next;
};
typedef char codetype[2];
struct optype
{

ftype formula; /* input formula to be proved */
marktype marked; /* indicates which states in the */
/* state transition graph have been */
/* visited in procedure labelgraph */
COMPLETE CTL MODEL CHECKER IN C 99
Boolean correct; /* true if formula is true at state s */
flabeltype flabel; /* set of initial labels in character */
/* form */
/*===========================================================================*/
/* function typeoperator */
/* In : op = two letter code representing an operator or variable */
/* Out : typeoperator = type of operator */
/*===========================================================================*/
/* function typeoperator (op) */
operatortype typeoperator (_op)
codetype _op;
{
codetype op;
operatortype _typeoperator;
ARRAYcopy(_op,op,sizeof(op));
if ((op[0] != ’a’) && (op[0] != ’e’) && (op[0] != ’n’))
_typeoperator = atomic;
else {
switch(op[0])
{
case ’a’:
if ((op[1] != ’d’) && (op[1] != ’u’) && (op[1] != ’x’))
_typeoperator = atomic;
else {
switch(op[1])

}
}
return(_typeoperator);
}
/*typeoperator*/
/*===========================================================================*/
/* procedure readgraph */
/* Out : e = graph */
/* numstates = number of states in the graph */
/*===========================================================================*/
/* procedure readgraph (e,numstates) */
readgraph (e,numstates)
graphtype e;
short *numstates;
{
short i, j;
fprintf(stdout," Please enter the number of states in the graph:");
writeln(stdout);
writeln(stdout);
fscanf(stdin,"%d",numstates);
readln(stdin);
*numstates = *numstates - 1;
fprintf(stdout," Please enter graph in adjacency matrix form:");
writeln(stdout);
writeln(stdout);
for (i=0; i <= maxstates; i++)
for (j=0; j <= maxstates; j++)
e[i][j] = 0;
for (i=0; i <= *numstates; i++)
{

writeln(stdout);
fprintf(stdout," state number label1 label2 labeln ; ");
writeln(stdout);
writeln(stdout);
/*
#
# Read in the initial labels for each state.
#
*/
for (s=0; s <= numstates; s++)
{
fscanf(stdin,"%d",&i);
symbol = getc(stdin);
j=1;
while (symbol != ’;’)
{
if (symbol != ’ ’)
{
flabel[s][j][0] = symbol;
flabel[s][j][1] = getc(stdin);
j=j+1;
}
symbol = getc(stdin);
}
readln(stdin);
writeln(stdout);
fprintf(stdout,"%3d ",s);
j=1;
while (flabel[s][j][0] != ’ ’)
{

/*
#
# First, print out the numbered input formula.
#
*/
writeln(stdout);
fprintf(stdout," ");
writeln(stdout);
writeln(stdout);
fprintf(stdout," Temporal Logic Formula: ");
writeln(stdout);
fprintf(stdout," ");
writeln(stdout);
writeln(stdout);
for (i=1; i <= flength; i++)
fprintf(stdout,"%3d",i);
writeln(stdout);
putc(’ ’,stdout);
for (i=1; i <= flength; i++)
COMPLETE CTL MODEL CHECKER IN C 103
{
putc(formula[i-1].op[0],stdout);
fprintf(stdout,"%c ",formula[i-1].op[1]);
}
writeln(stdout);
writeln(stdout);
/*
#
# Now, rint the labeled transition graph.
#

}
}
/*printoutput*/
/*===========================================================================*/
/* procedure push */
/* In : p = integer */
/* top = top of stack */
/* Out : top = top of stack */
/*===========================================================================*/
104 MODEL CHECKING OF FINITE-STATE SYSTEMS
/* procedure push (p,top) */
push (p,top)
short p;
itemptr *top;
{
itemptr node;
node = (itemptr)malloc(sizeof(struct item));
node->ip = p;
node->next = *top;
*top = node;
}
/*push*/
/*===========================================================================*/
/* procedure pop */
/* In : top = top of the stack */
/*Out:p=integer */
/* top = top of the stack */
/*===========================================================================*/
/* procedure pop (p,top) */
pop (p,top)

/* flength = length of the formula */
/*===========================================================================*/
/* procedure readf (f,flength,s) */
readf (f,flength,s)
ftype f;
short *flength, *s;
{
itemptr ptop; /* top of the stack of numbers corresponding */
/* to parentheses found in the input formula */
short i, j, ip, lp; /* number of left parentheses read */
char lastsymbol, symbol; /* the input character */
fprintf(stdout," Please enter the formula to be in proved in prefix form:");
writeln(stdout);
writeln(stdout);
ptop = (itemptr)(NULL);
for (i=1; i <= maxflength; i++)
{
f[i-1].p = 0;
f[i-1].opcode = atomic;
for (j=1; j <= 2; j++)
f[i-1].op[j-1] = ’ ’;
}
i=1;
symbol = getc(stdin);
/*
#
# If the formula is not atomic, then the following code insures that
# all subformulas will be read properly.
#
*/

f[i-1].op[1] = symbol;
f[i-1].opcode = typeoperator(f[i-1].op);
i=i+1;
}
}
*flength = i;
}
else
/*
#
# If the formula is atomic, indicate that its length is one.
#
*/ {
f[i-1].op[0] = symbol;
symbol = getc(stdin);
if (((symbol >= ’a’) && (symbol <= ’z’)) || ((symbol >= ’0’) &&
(symbol <= ’9’)))
f[i-1].op[1] = symbol;
*flength = 1;
}
readln(stdin);
fprintf(stdout," Please enter the state at which the formula is to be
proved:");
writeln(stdout);
writeln(stdout);
fscanf(stdin,"%d",s);
readln(stdin);
for (i=1; i <= *flength; i++)
{
putc(f[i-1].op[0],stdout);

nf[fi-1][i-1].op[0] = ’ ’;
nf[fi-1][i-1].op[1] = ’ ’;
nf[fi-1][i-1].p = 0;
nf[fi-1][i-1].opcode = atomic;
}
sf[fi-1].arg1 = 0;
sf[fi-1].arg2 = 0;
}
/*
#
# In one pass, compute all values for arrays nf and sf using markers
# in f[i].p (parentheses help us determine the span of a formula).
#
*/
for (fi=1; fi <= fl; fi++)
{
nf[fi-1][0].op[0] = f[fi-1].op[0];
nf[fi-1][0].op[1] = f[fi-1].op[1];
nf[fi-1][0].opcode = f[fi-1].opcode;
nf[fi-1][0].p = f[fi-1].p;
lp = f[fi-1].p;
i = fi;
j=1;
/*
#
# If the operator opcode is not atomic, meaning that it is an
# operator, then we must find the end of the operand subformulas
# that this opcode is operating on by searching for the matching
# number corresponding to the matching parenthesis.
#

i=i+1;
} while (!(f[i-1].p <= lp));
sf[fi-1].arg2 = i + 1;
}
}
}
}
/*do*/
writeln(stdout);
fprintf(stdout," Array sf:");
writeln(stdout);
for (i=1; i <= fl; i++)
{
fprintf(stdout,"%3d %4d %4d",i,sf[i-1].arg1,sf[i-1].arg2);
writeln(stdout);
}
writeln(stdout);
}
/*buildnfsf*/
COMPLETE CTL MODEL CHECKER IN C 109
/*===========================================================================*/
/* function initlabeled */
/* In : s = state of the transition graph */
/* f = subformula */
/* Out : initlabeled = true if state s is initially labeled with f */
/* Description: */
/* Determine if state s is labeled with subformula f. */
/*===========================================================================*/
/* function initlabeled (s,f) */
Boolean initlabeled (s,_f)

# If the opcode is nt (not), then we have to search the whole array
# flabel to see if the input label is there. If it is found, then
# b is set to false, else true.
#
*/ else if (f[0].opcode == nt)
{
b = true;
i=0;
while (b && (flabel[s][i][0] != ’ ’))
110 MODEL CHECKING OF FINITE-STATE SYSTEMS
{
if ((flabel[s][i][0] == f[0].op[0]) && (flabel[s][i][1] ==
f[0].op[1]))
b = false;
i=i+1;
}
}
else b = false;
return(b);
}
/*initlabeled*/
/*===========================================================================*/
/* procedure addlabel */
/* In : s = state of the transition graph */
/* fi = number corresponding to a subformula */
/* Out : label = state s is labeled with nf[fi] */
/* Description: */
/* Label state s with label nf[fi] by setting the boolean */
/* value labeled[s,fi] to true. */
/*===========================================================================*/