BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1368
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Verification of Temporal Properties
AUTHOR:: Fix, Limor 
AUTHOR:: Grumberg, Orna
DATE:: August 1993
PAGES:: 20
ABSTRACT::
The paper presents a relatively complete deductive system for proving 
branching time temporal properties of reactive programs. No deductive system 
for verifying branching time temporal properties has been presented before. 
Our deductive system enjoys the following advantages. First, given a 
well-formed specification there is no need to translate it into a normal-form 
specification since the system can handle any well-formed specification. 
Second, given a specification to be verified, the proof rule to be applied is 
easily determined according to the top level operator of the specification. 
Third, the system reduces temporal verification to assertional reasoning 
rather than to temporal reasoning. 
END:: CORNELLCS//TR93-1368
BODY::
Verification of Temporal Properties
Limor Fix
Orna Grumberg
TR 93-1368
August 1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
Verification of temporal properties
Limor Fix
Upson Hall, Computer Science Dept.
Cornell University, Ithaca, NY 14850
e-mail:fix?cs.cornell.edu
Tel: (607) (255-9223)
Fax: (607) (255-4428)
Orna Grumberg
AT&T Bell Laboratories
Murray Hill, NJ 07974
e-mail:orna?research.att.com
Tel:(908)(582-5641)
Fax: (908) (582-7550)
July 20,1993
Abstract
The paper presents a relatively complete deductive system for proving branching time
temporal properties of reactive programs. No deductive system for verifying branching
time temporal properties has been presented before. Our deductive system enjoys the
following advantages. First, given a well-formed specification there is no need to translate it
into a normal-form specification since the system can handle any well-formed specification.
Second, given a specification to be verified, the proof rule to be applied is easily determined
according to the top level operator of the specification. Third, the system reduces temporal
verification to assertional reasoning rather than to temporal reasoning.
1 Introduction
Temporal logics are widely accepted and frequently used for specifying concurrent and reactive pro-
grams. In recent years, many fully automatic methods for verifying temporal specifications have been
presented such as model checkers [4]. However, the scope of these methods is still very limited; the
fully automatic methods mainly apply to finite state programs and to special cases of infinite state
programs. Therefore, the main tool for establishing that a program satisfies its temporal specification
is still that of deductive verification, using a set of axioms and inference rules.
Deductive verification can also be aided by the computer. A deductive verification system can
easily be embedded ill automated theorem provers, llke Nupri [5], Hol [8], Boyer-Moore [3] and Coq
[6]. An automated theorem prover is an interactive environment for proof generation. It assists the
development of proofs by exploring the possible proof steps, checking and writing intermediate results
and assembling the solution.
We present a relatively complete deductive system for verifying fair branching-time temporal logic
specifications (fair CTL). No deductive verification system has been presented before for fair CTL. All
previous deductive systems for verifying temporal properties, e.g., [16] ,[9] ,[17] ,[12],[15], are concerned
only with linear temporal logic (LTL). The previous deductive systems also suffer from the following
drawback. They offer a relatively complete deductive system only for normal-form formulas. Thus,
all other properties whose expression in LTL does not fall into the restricted normal-form can be
verified only by translating them into normal-form formulas. The known method for translating an
arbitrary (future) LTL formula into a normal-form is very complex in both the time complexity of the
translation and the size of the resulting formula. First a tableau method is used to translate a future
formula into a counter-free w-automata and then this automaton is translated into a normal-form
formula [11], [18]. In contrast, our deductive system can handle an arbitrary nesting of temporal
operators in a formula while no normal-form is required.
Our deductive system also enjoys the following two advantages. First, given a specification to be
verified the possible rules or axioms to be applied are solely determined by the top level operator of
the specification. Moreover, in most cases, the next possible rule to be applied is uniquely defined.
This property of the deduction system is very helpful when embedding the system in an automated
theorem prover. Second, all rules in our system reduce the task of verifying a temporal property
into subgoals that either require proving the valldity of assertional formulas or the verification of
simpler temporal properties. In other words, none of the generated subgoals require proving validity
of temporal formulas.
Next we describe our work in some more details. The deduction system proves validity of correct-
ness formulas of the form "P Sat p f", where P is a program, p is a precondition given in some
assertional language and f is a fair CTL formula. A program is defined as a set of transitions. A
program step is executed by choosing nondeterministically, in a weakly fair manner [7], an enabled
transition for execution. The weak fairness guarantees that, every constantly enabled transition is
eventually chosen for execution. Formulas of fair CTL are interpreted over a node in a computation
tree of a program. Every temporal operator consists of a path quantifier together with one modal
operator. A path quantifier is either A for "all fair paths" or E for "there exists a fair path". A
modal operator is either X for "next-state", G for "globally" or U, for "until". A correctness formula
"P Sat p f" is valid iff for every computation tree of P, the root node satisfies p f, where
denotes implication (defined as usual).
Of special interest is the rule for verifying the formula P Sat p --H EGf1. This formula specifies the
existence of a fair infinite path in the computation tree of P along which fi is continuously satisfied.
We prove that an infinite path is fair by showing that it consists of infinitely many finite fair intervals.
A fair interval is an interval along which every transition is either disabled or executed. To establish
that, we introduce a proof tool for identifying the end points of fair intervals and in addition we
formulate an inductive argument that implies infinitely many occurrences of such end points along the
path (see page 6).
The rest of the paper is organized as follows. In Section 2 the computation model is presented.
Section 3 defines fair CTL and correctness formulas. Section 4 presents the deduction system and
an example is given in Section 5. In Section 6 we compare our deduction system with CTL model
checking and discuss other verification approach.
2 The computation model
The model of computation we consider is a fair transition system in which each transition r is a binary
relation over a set of states ?. a1ra2 is used to denote that (ai, a2) E r. We say that a transition 7
is enabled in a state a if there exists a state a' such that ara'. Otherwise, r is disabled. We denote
by En(r) the set of all states in which r is enabled. A program P over a set of states ? is a set
of transitions over ?. We assume the existence of a dummy transition, r?, which is enabled exactly
when all other transitions are disabled and which leaves the program state unchanged. The dummy
transition ensures that all computations of the program are infinite.
Next we formally define the meaning of a program as a set of marked trees. A node ? is a finite
sequence over the natural numbers. A tree T is a set of nodes closed under the prefix operation. A
node ?i is an immediate successor of a node ? if there exists a natural number n such that ? n = ?. The
root of a tree is the empty sequence. An edge e is a pair of nodes (?, ?) such that TI is an immediate
successor of ?. A path 7r from a node n is an infinite sequence ....... such that 111 = ?? and for all
> 0, 7ii+i is an immediate successor of ?. A marked tree is a triple < T, Mn, Me >, where T is a tree,
Mn is a function that maps every node ofT to a state in ?. If Mn(7i) = s then we say that ?1 is marked
by s. Me is a function that maps every edge in T to a transition of P. A marked tree <T, Mn, Me >
is a computation tree of P iff the set of immediate successors of every node ?i in T is marked exactly
by the set of all states that are reachable from Mn(71i) via the execution of a single transition of P.
More formally, for every node ?i in T and for every state s in " and for every transition r of P
(Mn(iii),S) E r
iff
an immediate successor of TIi : Mn(m) = 5 A AIe(m,m) = r
Finally, the meaning of a program P is the set of all computation trees of P.
A transition 7 is enabled in a node n in a computation tree < T, Mn, Me > iff 7 is enabled in
Mn(7?). 7 is executed along a path 7r = ....... of the computation tree iff there exists i > 0 such that
Me(71i, 7?i+i) = 7. A path 7r = ?,?... in a computation tree of P is fair iff for every transition 7 of
P, if 7 is continuously enabled from some point along 7r then 7 is infinitely often executed along r.
Note that, every finite prefix of a path can be extended to a fair path and that every path with an
infinite suffix of ?* executions is fair.
2
3
Fair CTL and correctness formulas
Assume an assertional language L whose formulas are interpreted over ?. ? A fair CTL formula is
either a formula from L or, ?ft, fi A f2, AXf1, EXf1, AGf1, EGf1, A[j\uf2], and E[f1Uf2], where
fi and f2 are fair CTL formulas. Fair CTL formulas are interpreted over a node in a marked tree.
Given a node 71, a marked tree MT and a fair CTL formula f, the satisfaction relation MT, 71 ? f is
defined by induction on the structure of the formula. Intuitively, an assertion p in L is satisfied at a
node 71 iff the state that marks 71, that is Mn(71), satisfies p. ?f and fi A f2 are defined as usuai. AXf1
(EXf1) is satisfied at 71 iff every (at least one) immediate successor of 71 satisfies fi. AGf1 (EGf1)
is satisfied at 71 iff every node in every (at least one) fair path from 71 satisfies fi. Finally, A[fiUf2]
(E[fiuf2]) is satisfied at 71 iff every (at least one) fair path from 71 satisfy fi until f2, i.e., there exists
a node 71' along the path that satisfies f2 and every node from 71 to 71' satisfies fi. The set of operators
presented above is not minimal, for example, the operators AC and EC can be expresses in terms of
AU and EU, respectively. We choose to introduce a wider set than necessary in order to simplify the
presentation of the proof rules.
A fair CTL correctness formula consists of three components: a precondition p in L, a program P
and a fair CTL formula f, and is of the form "P Sat p f". A formula "P Sat p f" is interpreted
over the root node of a computation tree of P. A fair CTL correctness formula is valid, to be denoted
k P Sat p f, iff for every computation tree of P the root node satisfies p
An assertional correetness formula consists also of three components: p and q in L and a set of
transitions F, and is of the form "fpJF?q?". A formula ???pJF?qJfl is interpreted over a pair of states
(cri, a?) such that there exists r E F for which a1ra2 holds. An assertional correctness formula is
valid, to be denoted k fpJEfq?, iff for every transition r in F and every pair of states (a1, a2) such
that a1ra2 holds: if al p then a2 k q.
4 The deduction system
In this section we present our deductive system. Proof rules of special interest are explained in details
and their soundness is motivated. The completeness proof is postponed to Appendix A.
4.1 The next-rules
To verify a specification of the form P Sat p AXf1, we require that every transition of the program
P that starts in a state satisfying p results in a state satisfying an assertion q. And moreover, if P'
denotes the program left to be executed after the execution of a single step of P then every root node
of a computation tree of P' that satisfies q should also satisfy fi. Since a program in our model has
a single control point the program left to be executed after performing a single step of the program,
is the program itself. Therefore, we get:
?pJP?qJ
P Sat q			fi
P Sat p --H AXf1
1We assume L is expressible enough to formalize all the sets of states required for the relative completeness of our
system. As is known [i9],[i4] L should at least include the predicate calculus, interpreted symbols for expressing the
standard operations and relations over integers and the fixed-point operators , and v.
3
To verify a specification of the form P Sat p EXf1, we require that there exists a transition r in
P such that 7 is enabled in all states satisfying p and its execution results in a state satisfying an
assertion q. And moreover, every root node of a computation tree of P that satisfies q also satisfies
fi:
There exists r : p En(r) and (pjr(qJ
P Sat q fi
P Sat EXf1
To verify the negations of the above two specifications we relay on the following fair CTL valldities:
?AXjj			EX?fj
?EXf1			?` AX?fj
Thus we get:
and
4.2 The ttntil-rules
P Sat p			ThY?f1
P Sat p			?`AXjj
PSatpAX?f1
P Sat p			?EXh
Next we present conditions for verifying P Sat p A[11u12], where li and 12 are in L. Let a prefix
of a path in which all nodes satisfy ?I2 be called I2-avoiding. We have to verify that all I2-avoiding
prefixes that start in roots satisfying p are finite and that Ii is continuously satisfied along these
prefixes. The following verification conditions establlsh a weWfounded induction on the length of
the I2-avoiding prefixes. The induction hypothesis assumes that all nodes along I2-avoiding prefixes
satisfy some state predicate ? and that a ranking function 6 is defined for all states that mark these
nodes, where 6 maps states into a well-founded, partially ordered set (W, <). Moreover, the induction
hypothesis assumes that the ranks defined by 6 along an I2-avoiding prefix never increase. In the
induction basis we deal with the case of I2-avoiding prefixes of length zero. We require that every
state that satisfies p also satisfies either 12 or it satisfies ? and 6 is defined for that state (denoted by
6 E W):
AUl. p (12 V (? A (6 E W)))
In the induction step we require that every transition of the program that starts in a state satisfying
? and for which a rank w is defined by 6 results in a state that either satisfies 12 or it satisfies ? and
it is mapped by 6 to a rank lower or equal to w:
AU2. ?? A (6 = w)?P?j? V (? A (6 ?
We add the requirement that every state that satisfies ? also satisfies Ii:
AU3. ?--HA
Conditions AUl-AU3 guarantee that every path in a computation tree of P from a root satisfying p
satisfies Ii as long as 12 is not satisfies. To ensure that 12 will eventually be satisfied we relay on the
4
fairness of the computation model, the well-foundedness of W and the additional requirement that
for every state that satisfies ? A (6 w) there exists an enabled transition of the program whose
execution results in a state that either satisfies J2 or satisfies ? and for which a lower rank than w is
defined by 6:
AU4. For every w E )`V there exists r E P
(1) (?A(6=w))?En(r)
(2) ?? A (6 = w)JrfI2 V (? A (6 < w))?
The fairness of the computation model implies that a transition that causes the rank to decrease will
eventually be executed and the well-foundness of W guarantees that only finitdy many times the rank
can decrease and therefore a node satisfying 12 must be reached. Thus, we get:
AUl - AU4
P Sat p			A[111AI2j
where 11,12 ? L
A specification P Sat p [j?uI2], where li, 12 E L, is verified by the above verification conditions
AUl, AU3 and AU4. Condition AU2 is omitted in order to relax the set of verification conditions such
that they only imply the existence of a fair path with a finite prefix ....... ? such that 6(Mn(n0)) >
6(Mn(m)) > ... > 6(Mn(?ii)), ? satisfies 12 and every other node along this prefix satisfies Ji:
AUl, AU3, AU4
P Sat p E[AUI2]
where Ii, 12 E L
To verify a specification of the form A[f1uf2], where either fi or f2 is not in L, we decompose the
verification task into three subtasks. One requires that every path in a computation tree of P that
starts in a node satisfying p satisfies Ii until 12, where both Ii and 12 are in L. The other two require
that every root of a computation tree of P that satisfies Ii or 12 also satisfies fi or f2, respectively:
P Sat p A[ijUI2]
P Sat Ii			fi
P Sat 12			f2
P Sat p A[f?uf2]
where fi ? L or f2 ?
Again the soundness of this rule relies on the fact that a program has a single control point and the
program left to be executed after performing one or more steps, is the program itself.
To verify a specification of the form P Sat p ?A[f?Uf2] we relay on the following fair CTL valid
formula:
??A[f1uf2] (EG?f2 V E[(?f?)ZA(?f? A ?f?)j)
5
P Sat p			EG?f?
or
P Sat p			E[(?f?W(?fi A ?`f?)]
Thus we get:
P Sat ?A[fjuf2]
To verify a specification of the form P Sat p ?E[fjUj?] we observe that there does not exist
a fair path that satisfies fi until f2 iff either ?jj A ?f2 holds at the root or there exists an assertion
I that holds in every node of every path from the root until ?fj A ?f2 holds and in addition I must
imply f2. Thus we get:
4.3 The global-rules
P Sat p (?fi A ?f2)
or
p?r
P Sat I ?f2 A Ax(Iv (?jj A f2))
P Sat p ?E[fiUf2]
Next we present conditions for verifying P Sat p EGf1 To prove that a path is fair we exploit the
following observation, taken from the completeness proof for the weak fair termination rule in [10]: a
path 7r in a computation tree of P is fair iff for every transition r? of P, either r? is infinitely often
disabled or rj is infinitely often executed along ?. Note that, along every path the dummy transition
r* is either disabled or continuously executed from some point on. Thus, we can relax the above
condition and conclude that a path 7r is fair iff for every non-dummy transition r?, i.e., r? is not equai
to r*, either rj is infinitely often disabled or r? is infinitely often executed aiong 7r. This implies that
r can be partitioned into infinitely many disjoint intervals of finite length, each of which contains for
every non-dummy transition rj? either a state in which r? is disabled or a step in which rj is executed.
We call such an interval fair. Thus, a path is fair iff it can be partitioned into infinitely many finite
fair intervals.
A proof tool for identifying the end points of fair intervals, is introduced next. Let P be a program
with m non-dummy transitions .1...., rm and let dis : [0, 11m be a function that maps a state
? to a binary vector of length m such that dis(a)(j) = 0 iff the transition r, is disabled in a. Let
0 (T) stands for a vector of m zeros (ones). And for a natural number j let j be a vector of m ones
except that if 1 < J < m then the j-th element in this vector is zero. Let A be the point wise logical
conjunction of binary vectors. Eor example, let m = 3 and dis = 101, the value of the expression
TA?Adis, that is illAllOAlOl, is equal to 100. We use a function g from the program states to
[0, lyrn and require the following proof obligations that ensure that g = 0 indicates the end of a fair
interval. The condition
EGi. p			(g ? [0, 1Y?)
requires that initially 9 is defined. The condition
EG2. For every ? E P: [g =0?T?fg = 4Adis)?
requires that the first step taken after the end of a fair interval results in a state in which the value of
g is reset, that is, 9 = (w1Wm) where Wj = 0 iff ? is disabled at the current state or ? has just
6
been executed and Wj = 1, otherwise. The condition
EC3. For every ? E P and every w E (0, 1?m (g = WA w $ O?r?fg = (w?jA dis)?
requires that g assigns Wj = 0 to states within a fair interval iff r? has either been executed or has
been disabled in that fair interval.
Introducing the above method for identifying the end points of fair intervals, we still have to prove
that there exists a path along which infinitely often an end of a fair interval is encountered:
EG4.
EG5.
EG6.
I?g=O
P Satp? E[fju(IAjj)]
P Sat I EXE[fjU(I A f')]
The condition G4 sets the connection between the satisfaction of I and the end points of fair intervals.
Conditions EG5 and C6 ensure that there exists a path in which I holds infinitely often and moreover
fi continuously holds along that path. Thus we get:
EGi - EG6
P Sat p			EGf1
To verify the other global specifications we relay on the following fair CTL validities,
AGf1 ?E[true UrnA]
?EGfi A[true U?fi]
?ACf1 E[true U?fi]
which imply:
PSatp?E[trueU?fi]			PSatpA[trueU?f?]
P Sat p			AUf1			P Sat p			?EGfj
The entire deductive system is presented in Figure 1.
5			Example
Consider the simple program,
Ti
It
II
x + 1 if x < 10
y := 5 if 5 < x A y = 0
P Sat p E[true U?fi]
P Sat p ?AGfj
which has three transitions. Transition ri increases the value of x by 1 and is enabled whenever the
value of x is smaller than 10. Transition ?2 sets y to 5 and is enabled whenever the value of x is
7
bigger than 5 and the value y is equal to 0. Transition 73* is the dummy transition. Next we verify
the correctness formula:
P Sat x = 0 A y = 0			EG(x < 10			y = 0)
This specification implies that there exists a fair computation of P in which the execution of the
second transition is postponed until the first one is not enabled any more. Let
Ol			if x > 5 A y = 0
We prove that the premises ECi --H C6 hold:
o+ ECi. According to the definition of g, x = 0 A y = 0 g = 00 holds.
o+ C2. According to the definition of g if g = 00 then 0 < x < 5 V y $ 0 holds. Therefore,
transition ri is either not enabled or its execution results in a state in which g = Oc, where
c = 1 if x > 5 A y = 0 and c = 0 otherwise. According to the definition of dis, the value of
the expression Ol A dis is Od, where d = 1 if x > 5 A y = 0 and d = 0 otherwise. Thus, in the
resulting state 9 = (01 A dis) and we conclude that
= 00Yrifg = (OlAdis))
holds. Transition r2 is not enabled in a state satisfying 0 ? x < 5 V y $ 0. Therefore
(9 = 00)72(9 = (lOAdis))
holds. For transition 73*
= 00Jr?(? = (11Adis))
holds since either 73* is not enabled or it is enabled and in both starting and resulting states
dis = 00 and g = 00.
EG3. According to the definition of g, 9 = w A w $ 0 implies that g = 01 and thus the
corresponding starting state satisfies x > 5 A y = 0. Transition ?i is either not enabled or its
execution results in a state satisfies x > 5 A y = 0. Therefore according to the definition of 9 in
the resulting state 9 = Ol holds. The value of the expression 01 A 01 A dis is equal to 01 since
?2 is enabled in the resulting state and thus
(9 = 01)71(9 = (O1AO1Adis))
holds. The execution of ?2 from a state satisfying x > 5 A y = 0 results in a state satisfying
x > SAy $ 0 and thereforeg = 00 in the resulting state. The value of the expression 01 A 10 A dis
is equal to 00 and thus
(9 = 01)72(9 = (01 A 10 A dis))
holds. The transition 73* is not enabled in a state satisfying x > 5 A y = 0 and therefore
(9 = 01)r?(? = (O1A11Adis))
8
holds.
o+ EC4. Let I = (0 < x < 5 A y = 0) v (x > 10 A y $ 0). According to the definition of g we get:
I g = 00
o+ G5. Next we prove that
P Sat x = 0 A y = 0			E[(x < 10			y = 0)U(I A (x < 10			y = 0))]
Using first order manipulation the assertion (IA(x < 10 y = 0)) can we rewritten as (0 < x <
5 A y = 0) v (y $ 0 A x > 10). Let ? = 0 < x < 10 A y = 0 and W = (true,frlse] x (0..10Y with
lexicographical order where < false, 0 > is the minimal element. We define 6 =< y = 0, 10--Hx >.
--H AUl. x = 0Ay = 0? ?A(6 E W).
--H AU3. 0 <x < 10 A y = 0 (x < 10 y = 0).
--H AU4. For 6< trne,d>, where 1 < d < lOwe get
(1) ? A 6 =< true,d> Al <d < 10 En(r1)
(2) ?? A6 =< trtte,d> Al <d < 10]rif?A 6 =< true,d--H 1 >)
For 6 =< trte,0>, we get
(1) ? A 6 =< true,0 >? En(r2)
(2) f? A 6 =< trte, 0 >Jr2?y $ 0 A x > 10 A 6 =< false, 0 >J
For 6 =< false, d >, the assertion ? A 6 =< false, d > is false and therefore both require-
ments (1) and (2) hold for any transition.
o+ EG6. Next we prove that
(*) P Sat I EXE[(x < 10 y = 0)U(I A (x < 10 y = 0))]
Recall that I = (0 < x < 5 A y = 0) v (x > 10 A y $ 0) therefore (*) holds iff
(1)			P Sat 0 < x <5 A y = 0			EXE[(x < 10			y = 0)U(I A (x < 10			y = 0))]
holds and
(2) P Sat x> I0Ay $ 0			EXE[(x <10			y= 0)U(IA(x <10			y= 0))]
holds.
To prove (1) we apply the next-rule for proving EX and get the following subgoals:
(1.1)			0 < x <5 A y = 0			x < 10
(1.2) f0<x<5Ay=0]??0<x<6Ay=0)
(1.3) P Sat 0 < x < 6 A y = 0 E[(x < 10 y = 0)U(I A (x < 10 y = 0))]
It is easy to see that (1.1) and (1.2) hold and (1.3) is proved using ? and 6 just as in EGS.
To prove (2) we apply the rule for proving EX and get the following subgoals:
(2.1) x> 10 A y $ 0 ? En(r3?), where En(r;) = x > 10 A y $ 0
(2.2) fx > 10 A y $ 0]r3*fx > 10 A y $ 0]
(2.3) P Sat x > 10 A y $ 0 E[(x < 10 y = 0)U(I A (x < 10 y = 0))]
It is easy to see that (2.1) and (2.2) hold and (2.3) is easily proved using ? = false and any 6.
We can choose ? and 6 as such since the precondition implies the second argument of the until
specification, that is x > 10 A y $ 0			IA (x < 10			y = 0).
9
6 Discussion
CTL model checking [4] is a verification algoritlim that given a program described as a finite-state
transition graph, a state in the program, and a formula ill propositional CTL, determines whether or
not the computation tree of the program, starting at this state, satisfies the formula. It is interesting
to notice the similarity and difference between the model checking approach and ours.
Both methods are similar in that, the verification of a formula depends on the verification of its
subformulas. Moreover, they are both syntax directed, i.e., the rule (or procedure) applied in the
verification of a formula is determined by the formula's top level operator.
One of the differences between the methods stems from the fact that while [4] solves a recursive
problem, we suggests a method for a non-recursive one. As a result, model checking suggests no special
rules for negated formulas. To determine whether or not a formula ?? is true in a state they check
? at this state and complement the result. Dealing with a non-recursive problem, our method cannot
expect, in general, to get a negative answer. Thus direct rules to handle negation as the top level
operator are introduced.
In [4], a more general notion of fairness is considered. Therefore, handling fairness requires a
preliminary step, that marks all state from which a fair computation starts ( they all satisfy some
proposition Q). To check now that E[fiuf2] is true in a state, they check that E[f1u(f2 A Q)] is
true in that state. In this case, our method is simpler. Since from every state there is a fair weak
computation starting at this state, we can verify E[f1uf2] as if no fairness is concerned.
The case of All is solved in [4] by using EU and EG. Their procedure for EG heavily depends
on the finiteness of the program description, and involves graph manipulations. Clearly, a similar
method is not applicable to our case. To conclude, both methods are similar in the way they take
advantage of the structure of CTL formulas. As expected, they diverge significantly in the way they
exploit properties of the program description.
Other verification approach that can handle general liveness properties were introduced in the
automata theoretic framework. In [1],[2],[13] assertional verification conditions are presented for veri-
fying properties which are specified by finite-state automata. Those results are extended in [20] to deal
with properties specified by recursive w-automata. In contrast, we specify properties in a relatively
intuitive and high level temporal language and no automata is constructed.
Acknowledgments.
We thank Nissim Francez for fruitful discussions in the preliminary stage of this work.
References
[1] B. Alpern and F.B. Schneider. Proving boolean combinations of deterministic properties. In 2nd
IEEE Symp. on Logic in Computer Science, pages 131--H137, 1987.
[2] B. Alpern and F.B. Schneider. Verifying temporal properties without temporal logic. ACM Trans.
Prog. Lang. Sys., 11:147--H167, 1989.
[3] R.S. Boyer and J.S. Moore. Integrating Recursion Procedures into Heuristic Theorem Provers: A
Case Study in Linear Arithmetic. Oxford University Press, 1988.
10
[4]
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent sys-
tems using temporal logic specifications. ACM Trans. on Programming Languages and Systems,
8(2):244 263, 1986.
[5] R. L. Constable et al. Implementing Mathematics with the Nuprl Development System. Prentice-
Hall, NJ, 1986.
[6] T. Coquand and G Huet. The Calculus of Constructions. Information and Computation, 76:95-
120, 1988.
[7] N. Francez. Fairness. Springer-Verlag, 1986.
[8] M. Gordon. Hol: A machine oriented formalization of higher order logic. Technical Report 68,
Cambridge University, 1985.
[9] L. Lamport. The hoare logic of concurrent programs. Acta Informatica, 14,1980.
[10] D. Lehmann, A. Pnuell, and J. Stavi. Impartiality, justice and fairness: the ethics of concurrent
termination. In 8th ICALP. LNCS 115, Springer-Verlag, 1981.
[11] 0. Maler and A. Pnueli. Tight bounds on the complexity of cascaded decomposition of automata.
In In Proc. 3Jth IEEE Symp. Found. of Comp. Sci., pages 672--H682, 1990.
[12] Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In lath
ACM Symp. Princ. of Prog. Lang., pages 141--H154, 1983.
[13] Z. Manna and A. Pnueli. Specification and verification of concurrent programs by V-automata.
In 14th ACM Symp. on Principles of Programming Languages, pages 1--H12, 1987.
[14]
Z. Manna and A. Pnueli. Completing the temporal picture. In G. Ausiello, M. Dezani-Ciancaglini,
and 5. Ronchi Della Rocca, editors, 16th Int. Colloq. Aut. Lang. Prog. LNCS 372, Springer-Verlag,
1989. Also in Theor. Comp. Sci., 1991, 83(1):97-130.
[15] Z. Manna and A. Pnuell. The temporal logic of reactive and concurrent systems: specification.
Springer-Verlag, 1991.
[16] Z. Manna and R. Waldinger. Is sometime sometime better than always? intermittent assertions
in proving program correctness. Communications ACM, 21(2):159--H172, 1978.
[17] 5. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM transactions
on programming languages and systems, 4(3):455--H495, 1982.
[18] A. Pnueli and L. Zuck. In and out of temporal logic. In In Proc. 8th IEEE Symp. Logic in Comp.
Sci., pages 124--H135, 1993.
[19] F.A. Stomp, W.-P. de Roever, and R.T. Gerth. The ?calculus as an assertion language for
fairness arguments. Technical Report 84-12, Utrecht, 1984.
[20] M. Vardi. Verification of concurrent programs: The automata-theoretic framework. Annals of
Pure and Applied Logic, 51:79--H98, 1991.
11
A Relative completeness
To prove the relative completeness of our deductive system we first prove that there is no circularity
in the system. That is, we prove that every premise of every rule can be verified by applying less proof
rules than required for the verification of the goal of the rule. To do so, we introduce a mapping Q
that maps every fair CTL formula to a natural number. Then, we show that for every rule of the form
P Sat Pi
P Sat p?
P Sat p
the relation ?(??) < ?(?) holds for every 1 < i < m.
The function ? is:
o+ if f E L then ?f) = 1,
o+ iff = fi Af2 then ?(f) = ?fi)+?f2),
o+ if f = EXf1 or f = AXf1 then g(f) = Q(fi) $ 1,
o+ if f = A[fiuf2] or f = E[f1uf2] then ?f) = 2 x (?(fj) + ?f2)),
o+ if f = EGf1 then ?(f) = 4 x ?(f?) + 4,
o+ if f = AGJ1 then ?f) = (2 x (?jj))2 + 4)2,
o+ if f = ?fi then ?f) = (?fi))2
Here we demonstrate the above for only one rule:
P Sat p			A[true U?fj]
P Sat ?ECh
According to the definition of ? we get:
?A[true U?f1]) = 2 x (1 + (?(fj))2)
and
?(?ECf1) = (4 x ?(fj) + 4)2
It is easy to see that ?(?EGfi) > ?A[ true U?fi]).
Since there is no circularity in the system the relative completeness of the system can be proved
by separately proving the relative completeness of every proof rule. We bring here some of the more
interesting proofs.
p?q
P Sat p q
For q E L
o+ The assertion rule:
12
Assume k P Sat p q. Thus for every computation tree of P if the root node satisfies p then it
satisfies q as well. Since every state in the state space can serve as a root node for a computation
tree of P we can conclude k p
. The AX rule:
P Sat q `fi
fpJPfq?
P Sat p ` AXf1
Assume k P Sat p AXf1. Thus for every computation tree of P if the root node 71 satisfies
p then every immediate successor of? satisfies fi Let q be an assertion that holds exactly at
all immediate successors of root nodes that satisfy p. The program left to be executed after the
execution of any transition from P is P itself, therefore, k P Sat q			fi.			Moreover, for every
r E P and every pair of states (a1, a?) such that a1ra2 holds: if al k p then a2			q, that is,
k (pJP?qJ.
. The ?AX rule:
P Sat EX?f1
P Sat ?AXA
The relative completeness of this rule is a consequence of the validity of the fair CTL formula:
EX?jj			?AXf?
First direction, the formula EX?f? holds at a node 71 in a marked tree MT iff there exists
an immediate successor 71i of 71 such that 711 does not satisfy fi Therefore not all immediate
successors of 71 satisfy fi, that is MT, 71 k ?AXf1. The second direction is also easy, omitted
here.
. The ?AU rule:
P Sat p ` EG?f2
or
PSatp"E[(?f2)U(?fiA?f2)]
P Sat ?A[f1uf2]
Again, the relative completeness of this rule is a consequence of the valldity of the fair CTL
formula:
(EC?f2) v (E[(?f2)U(?ji A ?f2)])"" ?A(fjUf2]
First direction, the formula (EG?f2) v ([(?f2)U(?ji A ?f2)i) holds at a node 71 in a marked
tree MT iff either there exists a fair path from 71 in which ?f2 continuously holds or there exists
a fair path from 71 such that ?f2 holds in an initiai prefix of that path until ?fj A ?`f2 holds.
Thus, we can conclude that there exists a fair path from 71 in which fiuf2 does not hold, that
is, MT, 71 k ?A[fjuf2]. Using similar consideration the second direction can aiso be proved.
ECi - EC6
P Sat p ECfi
. The EG rule:
Assume ? P Sat p EGf1. Thus for every computation tree of P if the root node satisfies p
then there exists a fair path that continuously satisfy fi We translate P into another program
P' by adding to P an history (auxiliary) variable h. initially, the value of h is the empty sequence
E. Every transition rj in P is translated into
h := h o a 0 j
That is, the state at which r? is executed (i.e., a) and the index number of r? (i.e., j) are
concatenated to h.
Let T be the set of all computation trees of P' such that their root node is marked by a state
satisfying p A h =
For every state a that marks a node in a tree in T we define the value of the function g as
follows:
--H The states that mark root nodes are mapped by g to the vector 1.
If a node ?1 is marked by a and g(a) = w, where w ? 0, then every state a' that marks an
immediate successor ij' of fl is mapped by g to wAjAdis, where j is st. Me(ii,ii,) =
and dis is evaluated at the state
If a node ? is marked by a and g(a) 0 then every state a' that marks an immediate
successor ?` of " is mapped by g to jAdis, where j is s.t. Me(?i,7?') = r? and dis is
evaluated at the state
The above partial function 9 is well-defined since every two states that mark nodes in T (of
either different trees or of the same tree) are different since h has different values.
We define I to be the set of all states that g maps to 0. Next we prove that the premises
EGi --H EG6 hold for the above g and I and the precondition p A h =
--H EGi. Every state that satisfies p A h = E marks a root node of one of the trees in T and
every such state is also mapped by 9' to 1, therefore
kpA h = e			(g E f0,llm)
--H EG2. According to the definition of g:
For every r? E P' : = Ojrjfy = (jA dis)J
--H EG3. Again according to the definition of g:
ForeverymEp' andevery?wE?,1lm: tg=wAw#0)rj?=(wAjAdis)Y
--H G4. immediate from the definition of I we get
?I?g=0
EG5 --H G6. Assuming the relative completeness of the other rules it is sufficient to prove
that conditions EG5 --H EG6 are semantically true. By the initial assumption we know that
in every computation tree of P'that starts in a state satisfying pA h = E there exists a fair
path that continuously satisfy fi. According to the definition of I and g and the observation
14
that every falr path can be divided into infinity many fair intervals we can conclude that I
holds infinitely many times in that fair path. Therefore,
k P Sat p			E[f1u(IA fi)]
and
0 The basic-AU rule:
k P Sat I EX[f1U(IA fi)]
AUl - AU4
P Sat p A[11u12]
where 11,12 E L
Assume k P Sat p A[11u12J. Given a computation tree MT' =< T', M?', Me' > of P that
starts ill a root node 710 satisfying p (i.e., Mn'(Th) k p) we know that every fair path from
710 satisfies jiUl2. To prove the relative completeness of the rule we have to find an assertion
a well-founded, partially ordered set (W, <?) and a partial ranking function ? such that the
premises AUl. --H AU4. hold.
We start by truncating MT' into a smaller tree MT =< T, Mn, Me > in the following way.
Every fair path from the root is truncated exactly after the first node that satisfies 12.
According to the assumption ? P Sat p A[I1UI2j we know that MT has either infinite unfair
paths or finite paths in which all intermediate nodes satisfy Ii and the leaf nodes (nodes that
have no successors) satisfy 12. Next we construct another marked tree that will have only finite
paths. First we need some definitions.
A path r is r-avoiding if and only if r is enabled at every node in r and moreover r is not
executed along ir. A CONEr(71) is the set of all nodes in MT residing on infinite r-avoiding
paths starting from the node 71. r is called the CONE `s directive. A path r in MT is leaving
a CONEr(71) at a node 711 if 71i is in Ir and 71i also belongs to CONEr(71) and the node which
immediately follows 71i in 7r does not belong to CONEr(71).
Next we inductively define the construction of another marked tree, to be denoted MT* =<
T*, M?*, M? >. The function M?* maps each node of T* to a subset of T and the function M?
maps each edge of T* to a transition of P.
At the base step we define the value of M?* for the root of the new tree MT*. in the induction
step we assume that the subtree of MT* of depth n is already built. We define for each leaf ? 2
of depth n the set of its immediate successors ?i,..., ?k in T*. We also define for each successor
? of ? the value of M?*(?) and the value of M:(?, ?)).
To define the base and the induction step we need a function RT : T* T which maps each
node in T* to a node in T. This function is also defined inductively. Let 71o and ? denote the
roots of MT and MT*, respectively.
Base Step: If there exists in MT a r-avoiding path starting from the root 71o for some ? E P
then Mn*(?) = CONEr(710). Else, Mn*(?b) = ???. in both cases we define ftT(?) = 71o.
2In the sequel nodes of MT are denoted by the symbols n, ? ... or ?` and the nodes of MT are denoted by the
symbols?,?,...or?.
15
Induction Step: Let ? be a leaf of depth n and let RT(?) = 71. We add immediate successors
to ? according to the following clauses:
--H If Mn*(?) = CONEr(7i) then for every path 7r in MT leaving CONE?(71) we add to ? an
immediate successor ? in MT* and we define RT(?) = 711, where 711 is the first node in Ir
after r leaves CONET(71) and M:(?,?) = Me(71', 71), where 71' is the predecessor of 71 in ir.
--H If M?*(?) = (71) where 71 is not a leaf in MT we add for every immediate successor 711 of 71
an immediate successor ? to ?. We define RT(?) = 711 and Me*(?, ?) = Me(71, 711)'
--H If M?*(?) = (71) where 71 is a leaf in MT then ? is a leaf in MT* and ftT(?) = 71.
Next, we define M?* for all nodes added in step n + 1 of the induction. Let ? be such a node.
Two cases:
--H If there is no mavoiding path starting from RT(?) in MT for any r E P then Mn*(?) =
--H Otherwise, consider the set S of all transitions, r, for which there is an infinite r'-avoiding
path starting from RT(?) in MT. Let r1 be the transition chosen least recently, possible
not at all, as a CONE's directive along the sequence Mn*(?6),Mn*(?),. ,M?*(??i), where
???...?--H?? is the path from the root to ? in MT*. We define M?*(?) = CONET1(RT(?)).
In the case there are more than one such transitions in S the transition with the smallest
index (assume all transitions in P are indexed) is chosen.
Lemma A.1:
--H For every node ? in MT*, RT(?) ?
--H For every two nodes ? and ? in MT*, M?*(?) n M?*(?) =
--H MT* covers MT, i.e., every node of MT belongs to some M?*(?), where ? is a node of MT*?
Proof:
According to the definition of MT*, Mn*(?) is either (RT(?)J or CONEr1(RT(?)) in both
cases 1?T(?) E M?*(?)
According to the definition of MT*, at every step of the induction M?*(?) contains nodes
of T that are not included in any previously defined M?*(?) Moreover, if ? and ? are
added to MT* in the same induction step then RT(?) and RT(?) do not reside on a
common path in T. Therefore according to the definition of M?* and the tree structure of
T, M?*(?) n M?*(?) =
According to the definition of MT*, the root of MT* covers the root of MT and in the
induction step, given a node ?, all immediate successors in T of nodes in M?*(?) are covered.
Lemma A.2: The tree MT* is well-founded, i.e., contains finite paths only.
16
Proof: Assume there exists an infinite path ?* = ....... in MT*. According to the definition
of the function RT the nodes RT(?),RT(?1),... are nodes in MT. Moreover, according to the
definition of MT* there exists a path 7r = ....... in MT such that for every i > 0, RT(?+1)
belongs to 7r and it appears ill 7r after, but not necessarily immediately after, RT(&). Since the
sequence RT(?),RT(?1),... is infinite, ? is also infinite and thus, unfair.
Therefore, there are several (at lease one) transitions such that from some point on in ir are
continuously enabled but are never selected for execution. Let r be such a transition with the
smallest index and let 7ri=RT(?)?1k7?k+1... be a suffix of ? which is r-avoiding and which starts
from RT(?).
Two possibilities:
--H r is not selected as a CONE's directive along M?*(?), M?*(?1) . ., M?*(??1) then according
to the definition of MT*, Mn*(?) = CONET(RT(?)).
--H r is selected as a CONE's directive along Mn*(?),M?*(?)..., Mn*(??i) then according to
the definition of MT* there exists j > i such that r is least recently selected as a CONE's
directive along M?*(?),Mn*(?)..., M?*(??1) and thus Mn*(?) = CONET(RT(?)).
Let k denote i if the first case holds and j otherwise. In both cases, the infinite tall of r which
is r-avoiding is contained in CONEr(RT(?)). Therefore, all the nodes RT(?+1), llT(?+2),
are contained in M?*(?), a contradiction to Lemma B.1. c
Based on the properties of MT* proved in Lemmas B.l and B.2 we next continue the AU-rule
completeness proof. Both trees MT and MT* are constructed for a specific initial state ?
that satisfies p, i.e., the root node of MT is mapped by M? to ?. In order to get rid of the
dependency of the trees on o? we combine all trees MT such that their root node is mapped
to a state satisfying p into an infinitary tree MT = < T, Mn, Me >. A new root is added and
its immediate successors are all the trees MT s.t. Mn(?1o) ?p. Similarity we combine all MT*
trees into an infinitary well-founded tree MT* =< T*, M?*, M? >.
Next, the nodes of MT* are ranked by countable ordinals. All leaves are ranked with 0, an
intermediate node is ranked with the successor of the least upper bound of the ranks of its
immediate successors. In order to rank nodes with a unique rank a rank-shift is performed. Let
?(?) denote the rank defined for node ? by the above procedure.
Let Q be the set of all nodes in MT that reside on finite paths and are nor leaves neither the
root of MT. We define ? to be the assertion satisfied by exactly all states that mark the nodes
in Q, that is:
= ?I??: a Mn(?)A?7? QY
We define the ranking function 6 to be:
6(a)=w iff 3B:B#?ABC?T*A(?EB?aEMn(Mn*(?bAw=min(U ??)
Next we show that the premises AUl. --H AU4. hold for ? and 6 above.
17
--H AUl._According to the construction of MT all states that satisfy p mark at least one node
in MT. Moreover, every state that satisfy peither mark a node in Q (thus it satisfies ?)
or a leaf of MT (recall that every leaf 71 in MT satisfies Mn(71) k 12) therefore
k p			? V `2
Moreover, MT* covers MT and therefore the ranking function 6 is defined for every state
that mark a node in MT. In particular, all states in p mark nodes in MT and thus
?p?(6EW)
AU2. From every state (7 that satisfies ? and 6(a) = w the execution of any transition from
p leads to a state that mark either a leaf of MT and therefore I2 is satisfied or it leads to a
state that mark an internal node (not a leaf) 71 of MT. Since every finite prefix of a path
can be extended to a fair path 71 E Q and therefore Mn(71) k ? Thus,
f?A(6 = w)JP?I2v?J
Moreover, according to the definition of MT* if (7 marks ? in T* then any transition of P
leads to a state that either mark ? or mark an immediate successor of ? and therefore
f? A (6 = w))Pf(6 <
--H AU3. According to the construction of MT and the definition of Q all nodes in Q are
marked by states satisfying li therefore
k ? "Ii
AU4. Given w E W if there does not exist a state a such that (7 k ? and 6(a) = w then
? A (6 = w) false and therefore both conditions in AU4. hold vacuously.
In there exists a state (7 such that (7 ? and 6((7) = w then 3? E MT* such that ?(?) = w
and (7E Mn(M?*(?)) Consider two cases:
Case 1: M?*(?) = CONEr(RT(?)).
According to the definition of CONEr, ? is enabled in all states (7, such that
a' E Mn( CONEr(RT(?)) therefore (7 ? En(r) and we conclude
According to the definition of CONEr every r-move leaves CONEr(RT(?))and therefore a
r?move reaches an immediate successor ? of ? in MT*. Since the nodes in MT* are ranked
leaves up we know ?(?`) < ?(?). Thus,
A (6 = w)J?f6 < Wi
Moreover, if the 7-move reaches a leaf of MT then the resulting state satisfies 12 otherwise
it satisfies ?. Thus,
f? A (6 = w)Yrti? v ??
Case 2: M?*(?) =
In this case, a = Mn(RT(?)). a ? implies that ?? : a = AIn(?) A ? E Q therefore ? and
ftT(?) areroots to identical subtrees of MT and thus RT(?) E Q. Thus, RT(?) is not a
leaf in MT and there exists r such that a k En(r) and we conclude
k(?A(6=w))?En(r)
Moreover, the r-move reaches an immediate successor ?` of ? in MT* and we know ?(?`) <
f?A(6=w)1rf?<w1
ff the T-move reaches a leaf of MT then the resulting state satisfies `2 otherwise it satisfies
?. Thus,
A (6 = w)Jr?I2 v ?J
19
Figure 1: The ??duction system
EGI.--HEGe.			PSatpA[trueu?!1]
P Sat p --H EGJ1			F Sat p			EGA
,?Ji "			-
PSat;;--HE[trueU?f1]			PSatp--HEttrueU?!ii
P Sat p --H AGf1			P Sat p			AGJ1
pq			p--H?q
P Sat p			q			P Sat p --H
For q E L			For q E L
f2))
P Sat p			(?!i A
p?I
PSatI--H?f2AAX(Iv
P Sat p --H E[f1uJ2]
P Sat li			li
P Sat 12 --H f2
P Sat p --H E[11u12]
P Sat p E[J1uf2]
tuAere, Ji ? L or f2 ?
AUI,AUS,AU?
P Sat p --H Etl1ul2]
tuhere, 11,12 E L.
P Sat p --H Ii			P Sat Pi --H!
PSatp--H!2			PSatp?--Hf
PSatp?(f1 A!2)			PSat (pi vp2)?J
P Sat p
PSatp--H?(!iAf?)
P Sat q --H fi			PSatp--HEX?f1
(p)P(q)
PSatp?AXfi			PSatp--H AX!1
P Sat q --H
TAcreexistsr?p)r(q)andp--HEn(r)			PSatp--HAX?!1
P Sat;; --H EX!1			PSatp??EXf1
P Sat Ii --H Ji
P Sat 12
P Sat p--HA(liUli]
P Sat p --H A(f1uf2]
tuAcre, Ji ? L or !2 ?
Aul -AU?
P Sat ;; --H A(IiUI2l
where, 11,12 EL.
P Sat p --H EG?b
or
P Sat p --H E[(?!i)u(?A A
P Sat p --H A[f1uf?]
