Model Checking of Safety Properties.
Of special interest in formal verification are safety properties, which assert that the system always stays within some allowed region. Proof rules for the verification of safety properties have been developed in the proof-based approach to verification, making verification of safety properties simpler than verification of general properties. In this paper we consider model checking of safety properties. A computation that violates a general linear property reaches a bad cycle, which witnesses the violation of the property. Accordingly, current methods and tools for model checking of linear properties are based on a search for bad cycles. A symbolic implementation of such a search involves the calculation of a nested fixed-point expression over the system's state space, and is often infeasible. Every computation that violates a safety property has a finite prefix along which the property is violated. We use this fact in order to base model checking of safety properties on a search for finite bad prefixes. Such a search can be performed using a simple forward or backward symbolic reachability check. A naive methodology that is based on such a search involves a construction of an automaton (or a tableau) that is doubly exponential in the property. We present an analysis of safety properties that enables us to prevent the doubly-exponential blow up and to use the same automaton used for model checking of general properties, replacing the search for bad cycles by a search for bad prefixes.
Introduction
Today's rapid development of complex and safety-critical systems requires reliable verication
methods. In formal verication, we verify that a system meets a desired property by checking
that a mathematical model of the system meets a formal specication that describes the property.
Of special interest are properties asserting that observed behavior of the system always stays
within some allowed set of nite behaviors, in which nothing \bad" happens. For example, we
This reasearch is supported by BSF grant 9800096.
y Address: School of Computer Science and Engineering, Jerusalem 91904, Israel. Email: orna@cs.huji.ac.il
z Address: Department of Computer Science, Houston,
in part by NSF grant CCR-9700061, and by a grant from the Intel Corporation.
may want to assert that every message received was previously sent. Such properties of systems
are called safety properties. Intuitively, a property is a safety property if every violation of
occurs after a nite execution of the system. In our example, if in a computation of the system
a message is received without previously being sent, this occurs after some nite execution of
the system.
In order to formally dene what safety properties are, we refer to computations of a nonterminating
system as innite words over an alphabet . Typically, is the set
of the system's atomic propositions. Consider a language L of innite words over . A nite
word x over  is a bad prex for L i for all innite words y over , the concatenation x  y of
x and y is not in L. Thus, a bad prex for L is a nite word that cannot be extended to an
innite word in L. A language L is a safety language if every word not in L has a nite bad
prex. For example, if is a safety language. To see this, note that
every word not in L contains either the sequence 01 or the sequence 10, and a prex that ends in
one of these sequences cannot be extended to a word in L. The denition of safety we consider
here is given in [AS85], it coincides with the denition of limit closure dened in [Eme83], and
is dierent from the denition in [Lam85], which also refers to the property being closed under
stuttering.
Linear properties of nonterminating systems are often specied using Buchi automata on
innite words or linear temporal logic (LTL) formulas. We say that an automaton A is a safety
automaton if it recognizes a safety language. Similarly, an LTL formula is a safety formula if
the set of computations that satisfy it form a safety language. Sistla shows that the problem
of determining whether a nondeterministic Buchi automaton or an LTL formula are safety is
PSPACE-complete [Sis94] (see also [AS87]). On the other hand, when the Buchi automaton is
deterministic, the problem can be solved in linear time [MP92]. Sistla also describes su-cient
syntactic requirements for safe LTL formulas. For example, a formula (in positive normal
whose only temporal operators are G (always) and X (next), is a safety formula [Sis94]. Suppose
that we want to verify the correctness of a system with respect to a safety property. Can we
use the fact that the property is known to be a safety property in order to improve general
verication methods? The positive answer to this question is the subject of this paper.
Much previous work on verication of safety properties follow the proof-based approach to
verication [Fra92]. In the proof-based approach, the system is annotated with assertions, and
proof rules are used to verify the assertions. In particular, Manna and Pnueli consider verication
of reactive systems with respect to safety properties in [MP92, MP95]. The denition of safety
formulas considered in [MP92, MP95] is syntactic: a safety formula is a formula of the form
G' where ' is a past formula. The syntactic denition is equivalent to the denition discussed
here [MP92]. Proof-based methods are also known for the verication of liveness properties
[OL82], which assert that the system eventually reaches some good set of states. While proof-
rule approaches are less sensitive to the size of the state space of the system, they require a
heavy user support. Our work here considers the state-exploration approach to verication,
where automatic model checking [CE81, QS81] is performed in order to verify the correctness of
a system with respect to a specication. Previous work in this subject considers special cases
of safety and liveness properties such as invariance checking [GW91, McM92, Val93, MR97], or
assume that a general safety property is given by the set of its bad prexes [GW91].
General methods for model checking of linear properties are based on a construction of a
tableau or an automaton A : that accepts exactly all the innite computations that violate the
property [LP85, VW94]. Given a system M and a property , verication of M with respect
to is reduced to checking the emptiness of the product of M and A : [VW86a]. This check
can be performed on-the-
y and symbolically [CVWY92, GPVW95, TBK95]. When is an
LTL formula, the size of A is exponential in the length of , and the complexity of verication
that follows is PSPACE, with a matching lower bound [SC85].
Consider a safety property . Let pref ( ) denote the set of all bad prexes for . For exam-
ple, pref (Gp) contains all nite words that have a position in which p does not hold. Recall that
every computation that violates has a prex in pref ( ). We say that an automaton on nite
words is tight for a safety property if it recognizes pref ( ). Since every system that violates
has a computation with a prex in pref ( ), an automaton tight for is practically more helpful
than A : . Indeed, reasoning about automata on nite words is easier than reasoning about
automata on innite words (cf. [HKSV97]). In particular, when the words are nite, we can
use backward or forward symbolic reachability analysis [BCM In addition, using an
automaton for bad prexes, we can return to the user a nite error trace, which is a bad prex,
and which is often more helpful than an innite error trace.
Given a safety property , we construct an automaton tight for . We show that the
construction involves an exponential blow-up in the case is given as a nondeterministic Buchi
automaton, and involves a doubly-exponential blow-up in the case is given in LTL. These
results are surprising, as they indicate that detection of bad prexes with a nondeterministic
automaton has the
avor of determinization. The tight automata we construct are indeed
deterministic. Nevertheless, our construction avoids the di-cult determinization of the Buchi
automaton for (cf. [Saf88]) and just uses a subset construction.
Our construction of tight automata reduces the problem of verication of safety properties
to the problem of invariance checking [Fra92, MP92]. Indeed, once we take the product of a
tight automaton with the system, we only have to check that we never reach an accepting state
of the tight automaton. Invariance checking is amenable to both model checking techniques
deductive verication techniques [BM83, SOR93, MAB + 94]. In practice,
the veried systems are often very large, and even clever symbolic methods cannot cope with the
state-explosion problem that model checking faces. The way we construct tight automata also
enables, in case the BDDs constructed during the symbolic reachability test get too large, an
analysis of the intermediate data that has been collected. The analysis can lead to a conclusion
that the system does not satisfy the property without further traversal of the system.
In view of the discouraging blow-ups described above, we release the requirement on tight
automata and seek, instead, an automaton that need not accept all the bad prexes, yet must
accept at least one bad prex of every computation that does not satisfy . We say that such
an automaton is ne for . For example, an automaton that recognizes p   (:p)  (p _:p) does
not accept all the words in pref (Gp), yet is ne for Gp. In practice, almost all the benet that
one obtain from a tight automaton can also be obtained from a ne automaton. We show that
for natural safety formulas , the construction of an automaton ne for is as easy as the
construction of A .
To formalize the notion of \natural safety formulas", consider the safety
G(p _ (Xq ^X:q)). A single state in which p does not hold is a bad prex for . Nevertheless,
this prex does not tell the whole story about the violation of . Indeed, the latter depends
on the fact that Xq ^ X:q is unsatisable, which (especially in more complicated examples),
may not be trivially noticed by the user. So, while some bad prexes are informative, namely,
they tell the whole violation story, other bad prexes may not be informative, and some user
intelligence is required in order to understand why they are bad prexes (the formal denition of
informative prexes is similar to the semantics of LTL over nite computations in which Xtrue
does not hold in the nal position).
The notion of informative prexes is the base for a classication of safety properties into
three distinct safety levels. A property is intentionally safe if all its bad prexes are informative.
For example, the formula Gp is intentionally safe. A property is accidentally safe if every
computation that violates has an informative bad prex. For example, the formula G(p_(Xq^
X:q)) is accidentally safe. Finally, a property is pathologically safe if there is a computation
that violates and has no informative bad prex. For example, the formula [G(q _ GFp) ^
G(r _ GF:p)] _ Gq _ Gr is pathologically safe. While intentionally safe properties are natural,
accidentally safe and especially pathologically safe properties contain some redundancy and we
do not expect to see them often in practice. We show that the automaton A : , which accepts
exactly all innite computations that violate , can easily (and with no blow-up) be modied
to an automaton A true
on nite words, which is tight for that is intentionally safe, and is ne
for that is accidentally safe.
We suggest a verication methodology that is based on the above observations. Given a
system M and a safety formula , we rst construct the automaton A true
, regardless of the type
of . If the intersection of M and A true
: is not empty, we get an error trace. Since A true
runs
on nite words, nonemptiness can be checked using forward reachability symbolic methods.
If the product is empty, then, as A true
: is tight for intentionally safe formulas and is ne for
accidentally safe formulas, there may be two reasons for this. One, is that M satises , and
the second is that is pathologically safe. To distinguish between these two cases, we check
whether is pathologically safe. This check requires space polynomial in the length of . If
is pathologically safe, we turn the user's attention to the fact that his specication is needlessly
complicated. According to the user's preference, we then either construct an automaton tight
for , proceed with usual LTL verication, or wait for an alternative specication.
So far, we discussed safety properties in the linear paradigm. One can also dene safety in
the branching paradigm. Then, a property, which describes trees, is a safety property if every
tree that violates it has a nite prex all whose extensions violate the property as well. We
dene safety in the branching paradigm and show that the problems of determining whether
a CTL or a universal CTL formula is safety are EXPTIME-complete and PSPACE-complete,
respectively. Given the linear complexity of CTL model checking, it is not clear yet whether
safety is a helpful notion for the branching paradigm. On the other hand, we show that safety
is a helpful notion for the assume-guarantee paradigm, where safety of either the assumption or
the guarantee is su-cient to improve general verication methods.
Preliminaries
2.1 Linear temporal logic
The logic LTL is a linear temporal logic. Formulas of LTL are constructed from a set AP of
atomic propositions using the usual Boolean operators and the temporal operators X (\next
time"), U (\until"), and V (\duality of until"). Formally, given a set AP , an LTL formula in a
positive normal form is dened as follows:
true, false, p, or :p, for p 2 AP .
are LTL formulas.
For an LTL formula , we use cl( ) to denote the closure of , namely, the set of 's
subformulas. We dene the semantics of LTL with respect to a computation
where for every j  0,  j is a subset of AP , denoting the set of atomic propositions that hold
in the j's position of . We denote the su-x  of  by  j . We use  j= to indicate
that an LTL formula holds in the path . The relation j= is inductively dened as follows:
For all , we have that  j= true and  6j= false.
For an atomic proposition p 2 AP ,
there is 0  i < k such that  i
Often, we interpret linear temporal logic formulas over a system with many computations.
Formally, a system is is the set of states, R  W  W is a
total transition relation (that is, for every w 2 W , there is at least one w 0 such that R(w; w 0 ),
the set W 0 is a set of initial states, and L maps each state to the sets of atomic
propositions that hold in it. A computation of M is a sequence w
and for all i  0 we have R(w
The model-checking problem for LTL is to determine, given an LTL formula and a system
M , whether all the computations of M satisfy . The problem is known to be PSPACE-complete
[SC85].
2.2 Safety languages and formulas
Consider a language L   ! of innite words over the alphabet . A nite word x 2   is a bad
prex for L i for all y 2  ! , we have x  y 62 L. Thus, a bad prex is a nite word that cannot
be extended to an innite word in L. Note that if x is a bad prex, then all the nite extensions
of x are also bad prexes. We say that a bad prex x is minimal i all the strict prexes of
x are not bad. A language L is a safety language i every w 62 L has a nite bad prex. For
a safety language L, we denote by pref (L) the set of all bad prexes for L. We say that a set
pref (L) is a trap for a safety language L i every word w 62 L has at least one bad prex in
X. Thus, while X need not contain all the bad prexes for L, it must contain su-ciently many
prexes to \trap" all the words not in L. We denote all the traps for L by trap(L).
For a language L   ! , we use comp(L) to denote the complement of L; i.e.,
We say that a language L   ! is a co-safety language i comp(L) is a safety language.
(The term used in [MP92] is guarantee language.) Equivalently, L is co-safety i every w 2 L
has a good prex x 2   such that for all y 2  ! , we have x  y 2 L. For a co-safety language L,
we denote by co-pref (L) the set of good prexes for L. Note that co-pref
For an LTL formula over a set AP of atomic propositions, let k k denote the set of
computations in (2 AP ) ! that satisfy . We say that is a safety formula i k k is a safety
language. Also, is a co-safety formula i k k is a co-safety language or, equivalently, k: k is
a safety language.
2.3 Word automata
Given an alphabet , an innite word over  is an innite sequence of letters
in . We denote by w l the su-x  l   l+1   l+2    of w. For a given set X, let (X) be
the set of positive Boolean formulas over X (i.e., Boolean formulas built from elements in X
using ^ and _), where we also allow the formulas true and false. For Y  X, we say that Y
the truth assignment that assigns true to the members of Y
and assigns false to the members of X n Y satises . For example, the sets fq
both satisfy the formula (q 1 _ q while the set fq 1 does not satisfy this formula. The
transition function of a nondeterministic automaton with state space Q and
alphabet  can be represented using (Q). For example, a transition (q; can
be written as (q; While transitions of nondeterministic automata correspond
to disjunctions, transitions of alternating automata can be arbitrary formulas in B (Q). We
can have, for instance, a transition -(q; meaning that the automaton
accepts from state q a su-x w l , starting by , of w, if it accepts w l+1 from both q 1 and q 2 or
from both q 3 and q 4 . Such a transition combines existential and universal choices.
Formally, an alternating automaton on innite words is  is the
input alphabet, Q is a nite set of states,
a set of initial states, and F  Q is a set of accepting states. While a run of a nondeterministic
automaton over a word w can be viewed as a function r : IN ! Q, a run of an alternating
automaton on w is a tree whose nodes are labeled by states in Q. Formally, a tree is a nonempty
set T  IN  , where for every x  c 2 T with x 2 IN  and c 2 IN, we have x 2 T . The elements of
are called nodes, and the empty word " is the root of T . For every x 2 T , the nodes x  c 2 T
are the children of x. A node with no children is a leaf . A path  of a tree T is a
set   T such that " 2  and for every x 2 , either x is a leaf, or there exists a unique c 2 IN
such that x  c 2 . Given a nite set , a -labeled tree is a pair hT ; V i where T is a tree and
maps each node of T to a letter in . A run of A on an innite word
is a Q-labeled tree hT r ; ri with T r  IN  such that r(") 2 Q 0 and for every node x 2 T r with
there is a (possibly empty) set such that S satises  and for
all 1  c  k, we have x  c 2 T r and r(x  c) = q c . For example, if -(q in ;  0
then possible runs of A on w have a root labeled q in , have one node in level 1 labeled q 1 or q 2 ,
and have another node in level 1 labeled q 3 or q 4 . Note that if for some y the function - has the
value true, then y need not have successors. Also, - can never have the value false in a run. For
a run r and an innite path   T r , let inf(rj) denote the set of states that r visits innitely
often along . That is, for innitely many x 2 ; we have As Q
is nite, it is guaranteed that inf(rj) 6= ;. When A is a Buchi automaton on innite words,
the run r is accepting i inf(rj) \ F 6= ; for all innite path in T r . That is, i every path in
the run visits at least one state in F innitely often.
The automaton A can also run on nite words in   . A run of A on a nite word
is a Q-labeled tree hT r ; ri with T r  IN n , where IN n is the set of all words of length at most
n over the alphabet IN. The run proceeds exactly like a run on an innite word, only that all
the nodes of level n in T r are leaves. A run hT r ; ri is accepting i all its nodes of level n visit
accepting states. Thus, if for all nodes x 2 T r \ IN n , we have r(x) 2 F .
A word (either nite or innite) is accepted by A i there exists an accepting run on it.
Note that while conjunctions in the transition function of A are re
ected in branches of hT r ; ri,
disjunctions are re
ected in the fact we can have many runs on the same word. The language of
denoted L(A), is the set of words that A accepts. As we already mentioned, deterministic and
nondeterministic automata can be viewed as special cases of alternating automata. Formally,
an alternating automaton is deterministic if for all q and , we have -(q;
it is nondeterministic if -(q; ) is always a disjunction over Q.
We dene the size of an alternating automaton as the sum of jQj and
j-j, where j-j is the sum of the lengths of the formulas in -. We say that the automaton A
over innite words is a safety (co-safety) automaton i L(A) is a safety (co-safety) language.
We use pref (A), co-pref (A), trap(A), and comp(A) to abbreviate pref (L(A)), co-pref (L(A)),
trap(L(A)), and comp(L(A)), respectively. For an automaton A and a set of states S, we
denote by A S the automaton obtained from A by dening the set of initial states to be S. We
say that an automaton A over innite words is universal i . When A runs on nite
words, it is universal i An automaton is empty if ;. A state q 2 Q is
nonempty if set S of states is universal (resp., rejecting), when A S is universal
empty). Note that the universality problem for nondeterministic automata is known to
be PSPACE-complete [MS72, Wol82].
We can now state the basic result concerning the analysis of safety, which generalizes Sistla's
result [Sis94] concerning safety of LTL formulas.
Theorem 2.1 Checking whether an alternating Buchi automaton is a safety (or a co-safety)
automaton is PSPACE-complete.
Proof: Let A be a given alternating Buchi automaton. There is an equivalent nondeterministic
Buchi automaton N , whose size is at most exponential in the size of A [MH84]. We assume
that each state in N accepts at least one word (otherwise, we can remove the state and simplify
the transitions relation). Let N loop be the automaton obtained from N by taking all states as
accepting states. As shown in [AS87, Sis94], A is a safety automaton i L(N loop ) is contained
in L(A). In order to check the latter, we rst construct from A a nondeterministic automaton
~
N such that L( ~
To construct ~
N , we rst complement A with a quadratic
blow-up [KV97], and then translate the result (which is an alternating Buchi automaton) to
a nondeterministic Buchi automaton, which involves an exponential blow up [MH84]. Thus,
the size of ~
N is at most exponential in the size of A. Now, L(N loop ) is contained in L(A)
i the intersection L(N loop ) \ L( ~
N) is empty. Since the constructions described above can be
performed on the
y, the emptiness of the intersection can be checked in space polynomial in
the size of A. The claim for co-safety follows since, as noted, alternating Buchi automata can be
complemented with a quadratic blow-up [KV97]. The lower bound follows from Sistla's lower
bound for LTL [Sis94], since LTL formulas can be translated to alternating Buchi automata
with a linear blow-up (see Theorem 2.2).
We note that the nonemptiness tests required by the algorithm can be performed using model
checking tools (cf. [CVWY92, TBK95]).
2.4 Automata and temporal logic
Given an LTL formula in positive normal form, one can build a nondeterministic Buchi
automaton A such that [VW94]. The size of A is exponential in j j. It is
shown in [KVW00, Var96] that when alternating automata are used, the translation of to A
as above involves only a linear blow up 1 The translation of LTL formulas to alternating Buchi
automata is going to be useful also for our methodology, and we describe it below.
Theorem 2.2 [KVW00, Var96] Given an LTL formula , we can construct, in linear running
time, an alternating Buchi automaton
Proof: The set F of accepting states consists of all the formulas of the form ' 1
It remains to dene the transition function -. For all  2 2 AP , we dene:
Using the translation described in [MH84] from alternating Buchi automata to nondeterministic
Buchi automata, we get:
Corollary 2.3 [VW94] Given an LTL formula , we can construct, in exponential running
time, a nondeterministic Buchi automaton N such that L(N
Combining Corollary 2.3 with Theorem 2.1, we get the following algorithm for checking safety
of an LTL formula . The algorithm is essentially as described in [Sis94], rephrased somewhat
to emphasize the usage of model checking.
1. Construct the nondeterministic Buchi automaton
1 The automaton A has linearly many states. Since the alphabet of A is 2 AP , which may be exponential in
the formula, a transition function of a linear size involves an implicit representation.
2. Use a model checker to compute the set of nonempty states, eliminate all other states,
and take all remaining states as accepting states. Let N loop
be the
resulting automaton. By Theorem 2.1, is a safety formula i kN loop
k  kN k; thus all
the computations accepted by N loop
satisfy .
3. Convert N loop
into a system M loop
where the transition
and the labeling function is such that
Thus, the system M loop
has exactly all the computations accepted by N loop
.
4. Use a model checker to verify that M loop
.
Detecting Bad Prexes
Linear properties of nonterminating systems are often specied using automata on innite words
or linear temporal logic (LTL) formulas. Given an LTL formula , one can build a nondeterministic
Buchi automaton A that recognizes k k. The size of A is, in the worst case, exponential
in [GPVW95, VW94]. In practice, when given a property that happens to be safe, what we
want is an automaton on nite words that detects bad prexes. As we discuss in the introduc-
tion, such an automaton is easier to reason about. In this section we construct, from a given
safety property, an automaton for its bad prexes.
We rst study the case where the property is given by a nondeterministic Buchi automaton.
When the given automaton A is deterministic, the construction of an automaton A 0 for pref (A) is
straightforward. Indeed, we can obtain A 0 from A by dening the set of accepting states to be the
set of states s for which A s is empty. Theorem 3.1 below shows that when A is a nondeterministic
automaton, things are not that simple. While we can avoid a di-cult determinization of A
(which may also require an acceptance condition that is stronger than Buchi) [Saf88], we cannot
avoid an exponential blow-up.
Theorem 3.1 Given a safety nondeterministic Buchi automaton A of size n, the size of an
automaton that recognizes pref (A) is 2 (n) .
Proof: We start with the upper bound. Let Recall that pref (L(A))
contains exactly all prexes x 2   such that for all y 2  ! , we have x  y 62 L(A). Accordingly,
the automaton for pref (A) accepts a prex x i the set of states that A could be in after reading x
is rejecting. Formally, we dene the (deterministic) automaton A
are as follows.
The transition function - 0 follows the subset construction induced by -; that is, for every
s2S -(s; ).
The set of accepting states contains all the rejecting sets of A.
We now turn to the lower bound. Essentially, it follows from the fact that pref (A) refers to
words that are not accepted by A, and hence, it has the
avor of complementation. Complementing
a nondeterministic automaton on nite words involves an exponential blow-up [MF71].
In fact, one can construct a nondeterministic automaton Qi, in which all states
are accepting, such that the smallest nondeterministic automaton that recognizes comp(A) has
states. (To see this, consider the language L n consisting of all words w such that either
jwj < 2n or Given A as above, let A 0 be A when
regarded as a Buchi automaton on innite words. We claim that pref To see
this, note that since all the states in A are accepting, a word w is rejected by A i all the runs
of A on w get stuck while reading it, which, as all the states in A 0 are accepting, holds i w is
in pref
We note that while constructing the deterministic automaton A 0 , one can apply to it minimization
techniques as used in the verication tool Mona [Kla98]. The lower bound in Theorem
3.1 is not surprising, as complementation of nondeterministic automata involves an exponential
blow-up, and, as we demonstrate in the lower-bound proof, there is a tight relation
between pref (A) and comp(A). We could hope, therefore, that when properties are specied
in a negative form (that is, they describe the forbidden behaviors of the system) or are given
in LTL, whose formulas can be negated, detection of bad prexes would not be harder than
detection of bad computations. In Theorems 3.2 and 3.3 we refute this hope.
Theorem 3.2 Given a co-safety nondeterministic Buchi automaton A of size n, the size of an
automaton that recognizes co-pref (L(A)) is 2 (n) .
Proof: The upper bound is similar to the one in Theorem 3.1, only that now we dene the
set of accepting states in A 0 as the set of all the universal sets of A. We prove a matching lower
bound. For n  1, let  &g. We dene L n as the language of all words w
such that w contains at least one & and the letter after the rst & is either & or it has already
appeared somewhere before the rst &. The language L n is a co-safety language. Indeed, each
word in L n has a good prex (e.g., the one that contains the rst & and its successor). We
can recognize L n with a nondeterministic Buchi automaton with O(n) states (the automaton
guesses the letter that appears after the rst &). Obvious good prexes for L n are 12&&, 123&2,
etc. We can recognize these prexes with a nondeterministic automaton with O(n) states. But
n also has some less obvious good prexes, like 1234    n& (a permutation of
by &). These prexes are indeed good, as every su-x we concatenate to them would start in
either & or a letter in ng that has appeared before the &. To recognize these prexes,
a nondeterministic automaton needs to keep track of subsets of ng, for which it needs
states. Consequently, a nondeterministic automaton for co-pref (L n ) must have at least 2 n
states.
We now extend the proof of Theorem 3.2 to get a doubly-exponential lower bound for going
from a safety LTL formula to a nondeterministic automaton for its bad prexes. The idea
is similar: while the proof in Theorem 3.2 uses the exponential lower bound for going from
nondeterministic to deterministic Buchi automata, the proof for this case is a variant of the
doubly exponential lower bound for going from LTL formulas to deterministic Buchi automata
[KV98]. In order to prove the latter, [KV98] dene the language L n  f0; 1; #;&g  by
A word w is in L n i the su-x of length n that comes after the single & in w appears somewhere
before the &. By [CKS81], the smallest deterministic automaton on nite words that accepts
L n has at least 2 2 n
states (reaching the &, the automaton should remember the possible set of
words in f0; 1g n that have appeared before). On the other hand, we can specify L n with the
following of length quadratic in n (we ignore here the technical fact that Buchi
automata and LTL formulas describe innite words).
1in
Theorem 3.3 Given a safety LTL formula of size n, the size of an automaton for pref ( )
and 2p n)
Proof: The upper bounds follows from the exponential translation of LTL formulas to non-deterministic
Buchi automata [VW94] and the exponential upper bound in Theorem 3.1. For
the lower bound, we dene, for n  1, the language L 0
n of innite words over f0; 1; #;&g where
every word in L 0
n contains at least one &, and after the rst & either there is a word in f0; 1g n
that has appeared before, or there is no word in f0; 1g n (that is, there is at least one # or &
in the rst n positions after the rst &). The language L 0
n is a co-safety language. As in the
proof of Theorem 3.2, a prex of the form x& such that x 2 f0; 1; #g  contains all the words in
f0; 1g n is a good prex, and a nondeterministic automaton needs 2 2 n
states to detect such good
prexes. This makes the automaton for co-pref (L 0
doubly exponential. On the other hand,
we can specify L 0
n with an LTL formula n that is quadratic in n. The formula is similar to the
one for L n , only that it is satised also by computations in which the rst & is not followed by
a word in f0; 1g n . Now, the is a safety formula of size quadratic in n and the
size of the smallest nondeterministic Buchi automaton for pref (: ) is
In order to get the upper bound in Theorem 3.3, we applied the exponential construction in
Theorem 3.1 to the exponential Buchi automaton A for k k. The construction in Theorem 3.1
is based on a subset construction for A , and it requires a check for the universality of sets of
states Q of A . Such a check corresponds to a validity check for a DNF formula in which each
disjunct corresponds to a state in Q. While the size of the formula can be exponential in j j, the
number of distinct literals in the formula is at most linear in j j, implying the following lemma.
Lemma 3.4 Consider an LTL formula and its nondeterministic Buchi automaton A . Let
Q be a set of states of A . The universality problem for Q can be checked using space polynomial
in j j.
Proof: Every state in A is associated with a set  of subformulas of . A set Q of states
of A then corresponds to a set f 1 of sets of subformulas. Let
l i
g.
The set Q is universal i the
j is valid. Though the formula
Q may be exponentially longer than , we can check its validity in PSPACE. To do this, we
rst negate it and get the formula :
. Clearly, Q is valid
not satisable. But : Q is satisable i at least one conjunction
in the disjunctive
normal . Thus, to check if : Q is satisable we
have to enumerate all such conjunctions and check whether one is satisable. Since each such
conjunction is of polynomial size, as the number of literals is bounded by j j, the claim follows.
Note that the satisability problem for LTL (and thus for all the :' i
's) can be reduced to the
nonemptiness problem for nondeterministic Buchi automata, and thus also to model checking
[CVWY92, TBK95]. In fact, the nondeterministic Buchi automaton A constructed in [VW94]
contains all sets of subformulas of as states. To run the universality test it su-ces to compute
the set of states of A accepting some innite word. Then a conjunction
is satisable
i the set f:' 1
g is contained in such a state.
Given a safety formula , we say that a nondeterministic automaton A over nite words
is tight for i In view of the lower bounds proven above, a construction
of tight automata may be too expensive. We say that a nondeterministic automaton A over
nite words is ne for i there exists X 2 trap(k k) such that X. Thus, a ne
automaton need not accept all the bad prexes, yet it must accept at least one bad prex of
every computation that does not satisfy . In practice, almost all the benet that one obtain
from a tight automaton can also be obtained from a ne automaton (we will get back to this
point in Section 6). It is an open question whether there are feasible constructions of ne
automata for general safety formulas. In Section 5 we show that for natural safety formulas ,
the construction of an automaton ne for is as easy as the construction of an automaton for .
4 Symbolic Verication of Safety Properties
Our construction of tight automata reduces the problem of verication of safety properties to the
problem of invariance checking, which is amenable to a large variety of techniques. In particular,
backward and forward symbolic reachability analysis have proven to be eective techniques for
checking invariant properties on systems with large state spaces [BCM In practice,
however, the veried systems are often very large, and even clever symbolic methods cannot cope
with the state-explosion problem that model checking faces. In this section we describe how the
way we construct tight automata enables, in case the BDDs constructed during the symbolic
reachability test get too big, an analysis of the intermediate data that has been collected. The
analysis solves the model-checking problem without further traversal of the system.
Consider a system n(M) be an automaton that accepts all
nite computations of M . Given , let A : be the nondeterministic co-safety automaton for
k. In the proof of Theorem 3.2, we construct an automaton A 0 such that
by following the subset construction of A : and dening the set of accepting
states to be the set of universal sets in A : . Then, one needs to verify the invariance that
the product n(M)  A 0 never reaches an accepting state of A 0 . In addition to forward and
backward symbolic reachability analysis, one could use a variety of recent techniques for doing
semi-exhaustive reachability analysis [RS95, YSAA97], including standard simulation techniques
[LWA98]. Also, one could use bounded model-checking techniques, in which a reduction to the
propositional satisability problem is used, to check whether there is a path of bounded length
from an initial state to an accepting state in n(M) A 0 [BCC however, that if A 0
is doubly exponential in j j, the BDD representation of A 0 will use exponentially (in j
Boolean variables. It is conceivable, however, that due to the determinism of A 0 , such a BDD
would have in practice a not too large width, and therefore would be of a manageable size (see
Section 6.2 for a related discussion.)
Another approach is to apply forward reachability analysis to the product M A : of the
system M and the automaton A : . Formally, let A let M be as
above. The product M  A : has state space W  Q, and the successors of a state hw; qi
are all pairs hw methods use
the predicate post(S), which, given a set of S of states (represented symbolically), returns the
successor set of S, that is, the set of all states t such that there is a transition from some state
in S to t. Starting from the initial set S methods iteratively
construct, for i  0, the set S could therefore say that this construction
implements the subset construction dynamically, \on the
y", during model checking, rather
than statically, before model checking. The calculation the S i 's proceeds symbolically, and
they are represented by BDDs. Doing so, forward symbolic methods actually follow the subset
construction of M A : . Indeed, for each w 2 W , the set Q w
is the set of
states that A : that can be reached via a path of length i in M from a state in W 0 to the state
w. Note that this set can be exponentially (in j large resulting possibly in a large BDD; on
the other hand, the number of Boolean variables used to represent A : is linear in j j. More
experimental work is needed to compare the merit of the two approaches (i.e., static vs. dynamic
subset construction).
The discussion above suggests the following technique for the case we encounter space prob-
lems. Suppose that at some point the BDD for S i gets too big. We then check whether there
is a state w such that the set Q w
i is universal. By Lemma 3.4, we can check the universality of
i in space polynomial in j j. Note that we do not need to enumerate all states w and then
check Q w
. We can enumerate directly the sets Q w
whose number is at most doubly exponential
in j j. (Repeatedly, select a state w 2 W , analyze Q w
i , and then remove all states u 2 W such
that Q u
.) By Lemma 4.1, encountering a universal Q w
solves the model-checking problem
without further traversal of the system.
Lemma 4.1 If is a safety formula, then M A : is nonempty i Q w
i is universal for some
Proof: Suppose Q w
i is universal. Consider any innite trace y that starts in w. Since Q w
is universal, there is some state q 2 Q w
i such that y is accepted by A q
. In addition, by the
denition of S i , there is a nite trace x from some state in W 0 to w such that, reading x, the
automaton A : reaches q. Hence, the innite trace x  y does not satisfy .
Suppose now that M  A : is nonempty. Then there is an innite trace y of M that is
accepted by A : . As is a safety formula, y has a bad prex x of length i such that -(Q 0 ; x)
is universal. If x ends in the state w, then Q w
i is universal.
Let j be the length of the shortest bad prex for that exists in M . The direction from left
to right in Lemma 4.1 can be strengthened, as the nonemptiness of M  A : implies that for
every i  j, there is w 2 W for which Q i
w is universal. While we do not want to (and sometime
we cannot) calculate j in advance, the stronger version gives more information on when and
why the method we discuss above is not only sound but also complete.
Note that it is possible to use semi-exhaustive reachability techniques also when analyzing
That is, instead of taking S i+1 to be post(S i ) we can take it to be a subset S 0
of
We have to ensure, however, that
is saturated with respect to
states of A : [LWA98]. Informally, we are allowed to drop states of M from S i+1 , but we are not
allowed to drop states of A : . Formally, if hw; qi 2 S 0
(in other words, if some pair in which the M-state element is w stays in the subset S 0
of
all the pairs in which the M-state element is w should stay). This ensures that if
the semi-exhaustive analysis follows a bad prex of length i in M , then Q 0w
is universal. In the extreme case, we follow only one trace of M , i.e., we simulate M . In that
case, we have that S 0
i . For related approaches see [CES97, ABG + 00]. Note that
while such a simulation cannot in general be performed for that is not a safety formula, we
can use it as a heuristic also for general formulas. We will get back to this point in Remarks 5.3
and 6.1.
5 Classication of Safety Properties
Consider the safety LTL formula Gp. A bad prex x for Gp must contain a state in which p
does not hold. If the user gets x as an error trace, he can immediately understand why Gp is
violated. Consider now the The formula is equivalent
to Gp and is therefore a safety formula. Moreover, the set of bad prexes for and Gp coincide.
Nevertheless, a minimal bad prex for (e.g., a single state in which p does not hold) does
not tell the whole story about the violation of . Indeed, the latter depends on the fact that
Xq^X:q is unsatisable, which (especially in more complicated examples), may not be trivially
noticed by the user. This intuition, of a prex that \tells the whole story", is the base for a
classication of safety properties into three distinct safety levels. We rst formalize this intuition
in terms of informative prexes. Recall that we assume that LTL formulas are given in positive
normal form, where negation is applied only to propositions (when we we refer to its
positive normal form).
For an LTL formula and a nite computation
that  is informative for i there exists a mapping such that the
following hold:
empty.
(3) For all 1  i  n and ' 2 L(i), the following hold.
If ' is a propositional assertion, it is satised by  i .
If
If
If
If
If
If  is informative for , the existing mapping L is called the witness for : in . Note
that the emptiness of L(n guarantees that all the requirements imposed by : are fullled
along . For example, while the nite computation fpg  ; is informative for Gp (e.g., with a
witness L for which it is not informative for
Xq)), an informative prex for
must contain at least one state after the rst state in which :p holds.
Theorem 5.1 Given an LTL formula and a nite computation  of length n, the problem of
deciding whether  is informative for can be solved in time O(n  j j).
Proof: Intuitively, since  has no branches, deciding whether  is informative for can proceed
similarly to CTL model checking. Given and we construct a mapping
ng contains exactly all the formulas :' 2 cl(: ) such
that the su-x  is informative for '. Then,  is informative for (1). The
construction of L max proceeds in a bottom-up manner. Initially L
Then, for each 1  i  n, we insert to L max (i) all the propositional assertions in cl(: ) that
are satised by  i . Then, we proceed by induction on the structure of the formula, inserting
a subformula ' to L max (i) i the conditions from item (3) above are satised for it, taking
;. In order to cope with the circular dependency in the conditions for ' of the
insertion of formulas proceeds from L max (n) to L max (1). Thus, for
example, the formula ' 1 _ ' 2 is added to L
X' 1 is added to L contains no formulas of the form
is added to L
that we insert ' 1 U' 2 to L before we
examine the insertion of ' 1 U' 2 to L max (i)). We have at most j j subformulas to examine, each
of which requires time linear in n, thus the overall complexity is O(n  j j).
Remark 5.2 A very similar argument shows that one can check in linear running time whether
an innite computation , represented as a prex followed by a cycle, satises an LTL formula .
Remark 5.3 Clearly, if an innite computation  has a prex  informative for , then  does
not satisfy . On the other hand, it may be that  does not satisfy and all the prexes of
up to a certain length (say, the length where the BDDs described in Section 4 explode) are not
informative. Hence, in practice, one may want to apply the check in Theorem 5.1 to both
and : . Then, one would get one of the following answers: fail (a prex that is informative for
exists, hence  does not satisfy ), pass (a prex that is informative for : exists, hence
satises ), and undetermined (neither prexes were found). Note that the above methodology
is independent of being a safety property.
We now use the notion of informative prex in order to distinguish between three types of
safety formulas.
A safety formula is intentionally safe i all the bad prexes for are informative. For
example, the formula Gp is intentionally safe.
A safety formula is accidentally safe i not all the bad prexes for are informative,
but every computation that violates has an informative bad prex. For example, the
are accidentally safe.
A safety formula is pathologically safe if there is a computation that violates and has
no informative bad prex. For example, the formula [G(q_FGp)^G(r_FG:p)]_Gq_Gr
is pathologically safe.
Sistla has shown that all temporal formulas in positive normal form constructed with the
temporal connectives X and V are safety formulas [Sis94]. We call such formulas syntactically
safe. The following strengthens Sistla's result.
Theorem 5.4 If is syntactically safe, then is intentionally or accidentally safe.
Proof: Let be a syntactically safe formula. Then, the only temporal operators in : are X
and U . Consider a computation
the semantics of LTL, there is a mapping conditions (1) and (3) for a
witness mapping hold for L (with 1), and there is i 2 IN such that L(i + 1) is empty. The
prex  1     i of  is then informative for . It follows that every computation that violates
has a prex informative for , thus is intentionally or accidentally safe.
As described in Section 2.4, given an LTL formula in positive normal form, one can build
an alternating Buchi automaton Essentially,
each state of L(A ) corresponds to a subformula of , and its transitions follow the semantics
of LTL. We dene the alternating Buchi automaton A true
redening
the set of accepting states to be the empty set. So, while in A a copy of the automaton
may accept by either reaching a state from which it proceed to true or visiting states of the
innitely often, in A true
all copies must reach a state from which they proceed to
true. Accordingly, A true
accepts exactly these computations that have a nite prex that is
informative for . To see this, note that such computations can be accepted by a run of A
in which all the copies eventually reach a state that is associated with propositional assertions
that are satised. Now, let n(A true
) be A true
when regarded as an automaton on nite words.
Theorem 5.5 For every safety formula , the automaton n(A true
accepts exactly all the
prexes that are informative for .
Proof: Assume rst that is a prex informative for in . Then, there is
a witness mapping ng in . The witness L induces a run r of
true
Formally, the set of states that r visits when it reads the su-x  i of  coincides
with L(i). By the denition of a witness mapping, all the states q that r visits when it reads  n
therefore, r is accepting.
The other direction is similar, thus every accepting run of n(A true
on  induces a witness
for : in .
Corollary 5.6 Consider a safety formula .
1. If is intentionally safe, then n(A true
is tight for .
2. If is accidentally safe, then n(A true
ne for .
Theorem 5.7 Deciding whether a given formula is pathologically safe is PSPACE-complete.
Proof: Consider a formula . Recall that the automaton A true
accepts exactly these computations
that have a nite prex that is informative for . Hence, is not pathologically safe i
every computation that does not satisfy is accepted by A true
. Accordingly, checking whether
is pathologically safe can be reduced to checking the containment of
Since the size of A is linear in the length of and containment for alternating Buchi automata
can be checked in polynomial space [KV97], we are done.
For the lower bound, we do a reduction from the problem of deciding whether a given formula
is a safety formula. Consider a formula , and let p; q, and r be atomic propositions not in .
The pathologically safe. It can be shown
that is a safety formula pathologically safe.
Note that the lower bound in Theorem 5.7 implies that the reverse direction of Theorem 5.4
does not hold.
Theorem 5.8 Deciding whether a given formula is intentionally safe is in EXPSPACE.
Proof: Consider a formula of size n. By Theorem 3.3, we can construct an automaton of
for pref ( ). By Theorem 5.5,
accepts all the prexes that are informative
for . Note that is intentionally safe i every prex in pref ( ) is an informative prex for
. Thus, to check that is intentionally safe, one has to complement n(A true
that its intersection with the automaton for pref ( ) is empty. A nondeterministic automaton
that complements n(A true
exponential in n [MH84], and its product with the automaton
for pref ( ) is doubly exponential in n. Since emptiness can be checked in nondeterministic
logarithmic space, the claim follows.
6 A Methodology
6.1 Exploiting the classication
In Section 5, we partitioned safety formulas into three safety levels and showed that for some
formulas, we can circumvent the blow-up involved in constructing a tight automaton for the
bad prexes. In particular, we showed that the automaton n(A true
: ), which is linear in the
length of , is tight for that is intentionally safe and is ne for that is accidentally safe.
In this section we describe a methodology for e-cient verication of safety properties that is
based on these observations. Consider a system M and a safety LTL formula . Let n(M) be
a nondeterministic automaton on nite words that accepts the prexes of computations of M ,
and let U true
be the nondeterministic automaton on nite words equivalent to the alternating
automaton
The size of U true
is exponential in the size of n(A true
it is exponential in the length of . Given M and , we suggest to proceed as follows (see

Figure

1).
Instead of checking the emptiness of M  A : , verication starts by checking n(M) with
respect to U true
. Since both automata refer to nite words, this can be done using nite forward
reachability analysis 2 . If the product n(M)  U true
is not empty, we return a word w in the
intersection, namely, a bad prex for that is generated by M 3 . If the product n(M)  U true
is empty, then, as U true
is ne for intentionally and accidentally safe formulas, there may be
two reasons for this. One, is that M satises , and the second is that is pathologically safe.
Therefore, we next check whether is pathologically safe. (Note that for syntactically safe
formulas this check is unnecessary, by Theorem 5.4.) If is not pathologically safe, we conclude
that M satises . Otherwise, we tell the user that his formula is pathologically safe, indicating
that his specication is needlessly complicated (accidentally and pathologically safe formulas
contain redundancy). At this point, the user would probably be surprised that his formula was
a safety formula (if he had known it is safety, he would have simplied it to an intentionally
If the user wishes to continue with this formula, we give up using the fact
that is safety and proceed with usual LTL model checking, thus we check the emptiness of
(Recall that the symbolic algorithm for emptiness of Buchi automata is in the worst
case quadratic [HKSV97, TBK95].) Note that at this point, the error trace that the user gets if
M does not satisfy consists of a prex and a cycle, yet since the user does not want to change
his formula, he probably has no idea why it is a safety formula and a nite non-informative error
trace would not help him. If the user prefers, or if M is very large (making the discovery of bad
cycles infeasible), we can build an automaton for pref ( ), hoping that by learning it, the user
would understand how to simplify his formula or that, in spite of the potential blow-up in ,
nite forward reachability would work better.
Section 6.2 for an alternative approach.
3 Note that since may not be intentionally safe, the automaton U true
may not be tight for , thus while w
is a minimal informative bad prex, it may not be a minimal bad prex.
4 An automatic translation of pathologically safe formulas to intentionally safe formulas is an open problem.
Such a translation may proceed through the automaton for the formula's bad prexes, in which case it would be
nonelementary.
Y
M is correct Consult user
n(M)  U true
M is incorrect
Y
Return error trace Is pathologically safe?

Figure

1: Verication of safety formulas
Remark 6.1 In fact, our methodology can be adjusted to formulas that are not (or not known
to be) safety formulas, and it can often terminate with a helpful output for such formulas. As
with safety formulas, we start by checking the emptiness of n(M)  U true
(note that U true
is
dened also for formulas that are not safety). If the intersection is not empty, it contains an error
trace, and M is incorrect. If the intersection is empty, we check whether is an intentionally
or accidentally safe formula. If it is, we conclude that M is correct. Otherwise, we consult the
user. Note also that by determinizing U true
, we can get a checker that can be used in simulation
6.2 On going backwards
As detailed above, given a system M and a safety formula , our method starts by checking
whether there is nite prex of a computation of M (a word accepted by n(M)) that is an
informative bad prex for (a word accepted by U true
both n(M) and U true
are
automata on nite words, so is their product, thus a search for a word in their intersection can
be done using nite forward reachability analysis. In this section we discuss another approach
for checking that no nite prex of a computation of M is an informative bad prex.
We say that a nondeterministic automaton
for every state q 2 Q and letter  2 , there is at most one state q 0 2 Q such that q 2 (q
Thus, given the current state of a run of U and the last letter read from the input, one can
determine the state visited before the current one. Let  the reverse
function of , thus  1 (q; )g. By the above, when U is reverse deterministic,
all the sets in the range of  1 are either empty or singletons. We extend  1 to sets in the
natural way as follows. For a set Q
contains all the states that may lead to some state in Q 0 when the letter in the input
is .
Assume that we have a reverse deterministic ne automaton U : for ; thus U : accepts
exactly all the bad prexes informative for . Consider the product
that M has a nite prex of a computation that is an informative
bad prex i P is nonempty; namely, there is a path in P from some state in S 0 to some state
in F . Each state in P is a pair hw; qi of a state w of M and a state q of U : . We say that a set
of states of P is Q-homogeneous if there is some q 2 Q such that S 0  Wfqg, where W is
the state of states of M ; that is, all the pairs in S 0 agree on their second element. For every state
hw; qi and letter  2 2 AP , the set  1 (hw; qi; ) may contain more than one state. Nevertheless,
since U : is reverse deterministic, the set  1 (hw; qi; ) is Q-homogeneous. Moreover, since
U : is reverse deterministic, then for every Q-homogeneous set S 0  S and for every  2 2 AP ,
the set  1 (S Q-homogeneous as well. Accordingly, if we start with some Q-homogeneous
set and traverse P backwards along one word in   , we need to maintain only Q-homogeneous
sets. In practice, it means that instead of maintaining sets in 2 W 2 Q (which is what we need to
do in a forward traversal), we only have to maintain sets in 2 W Q. If we conduct a backwards
breadth-rst search starting from F , we could hope that the sets maintained during the search
would be smaller, though not necessarily homogeneous, due to the reverse determinism. The
above suggests that when the ne automaton for is reverse deterministic, it may be useful
to check the nonemptiness of P using a backwards search, starting from the ne automaton's
accepting states.
The automaton U true
: is dened by means of the alternating word automaton A : , and is not
reverse deterministic. For example,
can reach the
state q from both states Xp _ Xq and Xq _ Xr. Below we describe a ne reverse deterministic
for , of size exponential in the length of . The automaton is based on the
reverse deterministic automata dened in [VW94] for LTL. As in [VW94], each state of the
associated with a set S of formulas in cl(: ). When the automaton is in
a state associated with S, it accepts exactly all innite words that satisfy all the formulas in
S. Unlike the automata in [VW94], a state of N : that is associated with S imposes only
requirements on the formulas (these in S) that should be satised, and imposes no requirements
on formulas (these in cl(: ) n S) that should not be satised. This property is crucial for
being ne. When the automaton N : visits a state associated with the empty set, it has no
requirements. Accordingly, we dene f;g to be the set of accepting states (note that the fact
that the set of accepting states is a singleton implies that in the product P we can start with
the single Q-homogeneous set W  f;g).
It is easy to dene N : formally in terms of its reverse deterministic function  1 . Consider
a state S  cl(: ) of N : and a letter  2 2 AP . The single state S 0 in  1 (S; ) is the maximal
subset of cl(: ) such that if a computation  satises all the formulas in S 0 and its rst position
is labeled by , then its su-x  1 satises all the formulas in S. Formally, S 0 contains exactly
all the propositional assertion in cl(: ) that are satised by , and for all formulas ' in cl(: )
for which the following hold.
If
If
If
If
If
It is easy to see that for every S and , there is a single S 0 that satises the above conditions.
Also, a sequence of states in N : that starts with some S 0 containing : and leads via the nite
computation induces a mapping showing that  is informative for
. It follows that N : is a reverse deterministic ne automaton for .
6.3 Safety in the assume-guarantee paradigm
Given a system M and two LTL formulas ' 1 and ' 2 , the linear assume-guarantee specication
holds i for every system M 0 such that the composition MkM 0 satises (the assump-
the composition MkM 0 also satises (the guarantee) ' 2 . Testing assume-guarantee
specications as above can be reduced to LTL model checking. Indeed, it is not hard to see
that system M satises i the
intersection M A ' 1
It may be that while is not a safety formula, ' 1 is a safety formula. Then, by the proof of
Theorem 2.1, the analysis of M A ' 1
can ignore the fairness conditions of A ' 1
and can proceed
with model checking ' 2 . (Note, however, that the system MA ' 1
may not be total, i.e., it may
have dead-end states, which need to be eliminated before model checking ' 2 .) Suppose now that
' 2 is a safety formula, while ' 1 is not a safety formula. We can then proceed as follows. We
rst ignore the fairness condition in M A ' 1
and use the techniques above to model check the
Suppose we found a bad prex that ends with the state hw; qi of M A '1 .
It remains to check that hw; qi is a fair state, i.e., that there is a fair path starting from hw; qi.
Instead of performing fair reachability analysis over the entire state space of M A ' 1
or on the
reachable state space of M  A '1 , it su-ces to perform this analysis on the set of states that
are reachable from hw; qi. This could potentially be much easier than doing full fair reachability
analysis.
In conclusion, when reasoning about assume-guarantee specications, it is useful to consider
the safety of the assumptions and the guarantee separately.
6.4 Safety in the branching paradigm
Consider a binary tree A prex of T is a nonempty prex-closed subset of T . For
a labeled tree prex P of T , a P -extension of hT labeled tree hT
which V and V 0 agree on the labels of the nodes in P . We say that a branching formula is a
violates , there exists a prex P such that all the
P -extensions of hT violates . The logic CTL is a branching temporal logic. In CTL, every
temporal operator is preceded by a path quantier, E (\for some path") or A (\for all paths").
Theorem 6.2 Given a CTL formula , deciding whether is a safety formula is EXPTIME-
complete.
Proof: Sistla's algorithm for checking safety of LTL formulas [Sis94] can be adapted to the
branching paradigm as follows. Consider a CTL formula . Recall that is not safe i there is
a tree that does not satisfy and all of whose prexes have at least one extension that satises
. Without loss of generality we can assume that the tree has a branching degree bounded
by
be a nondeterministic automaton for ; thus A d
accepts exactly
these d-ary trees that a satisfy . We assume that each state in A d
accepts at least one tree
(otherwise, we can remove it and simplify the transitions relation). Let A d;loop
be the automaton
obtained from A d
by taking all states to be accepting states. dening the set of accepting states
as the set of all states. Thus, A d;loop
accepts exactly all d-ary trees all of whose prexes that
have at least one extension accepted by A . Hence, is not safety i
not empty. Since the size of the automata is exponential in and the nonemptiness check is
quadratic [VW86b], the EXPTIME upper bound follows.
For the lower bound, we do a reduction from CTL satisability. Given a CTL formula , let
p be a proposition not in , and let We claim that ' is safe i is not satisable.
First, if is not satisable, then so is ', which is therefore safe. For the other direction assume,
by way of contradiction, that ' is safe and is satised by some tree hT ; V i. The tree
labeled only by the propositions appearing in . Let be an extension of hT refers
also to the proposition p and labels T so that hT does not
should have a bad prex P all of whose extensions violate '.
Consider a P extension that agrees with about the propositions in and has a frontier of
p's. Such a P -extension satises both and AFp, contradicting the fact that P is a bad prex.
Using similar arguments, we prove the following theorem, showing that when we disable
alternation between universal and existential quantication in the formula, the problem is as
complex as in the linear paradigm.
Theorem 6.3 Given an ACTL formula , deciding whether is a safety formula is PSPACE-complete

Since CTL and ACTL model checking can be completed in time linear [CES86], and can be
performed using symbolic methods, a tree automaton of exponential size that detects nite bad
prexes is not of much help. On the other hand, perhaps safety could oer an advantage in the
alternating-automata-theoretic framework of [KVW00]. At this point, it is an open question
whether safety is a useful notion in the branching-time paradigm.

Acknowledgment

The second author is grateful to Avner Landver for stimulating discussions.



--R



Recognizing safety and liveness.
Symbolic model checking using SAT procedures instead of BDDs.
Symbolic model check- ing: 10 20 states and beyond

Design and synthesis of synchronization skeletons using branching time temporal logic.
Automatic veri

Alternation. Journal of the Association for Computing Machinery
Memory e-cient algorithms for the veri cation of temporal properties
Alternative semantics for temporal logics.
Temporal and modal logic.
Program veri
Simple on-the- y automatic veri cation of linear temporal logic
Using partial orders for the e-cient veri cation of deadlock freedom and safety properties
A new heuristic for bad cycle detection using BDDs.
Forward model checking techniques oriented to buggy designs.

Weak alternating automata are not that weak.

An automata-theoretic approach to branching-time model checking
Logical foundation.
Checking that
Hybrid techniques for fast functional simulation.
The Stanford Temporal Prover.
Using unfolding to avoid the state explosion problem in the veri
Economy of description by automata

The Temporal Logic of Reactive and Concurrent Systems: Speci
The Temporal Logic of Reactive and Concurrent Systems: Safety.
Deadlock checking using net unfoldings.
The equivalence problem for regular expressions with squaring requires exponential time.
Proving liveness properties of concurrent programs.


On the complexity of
The complexity of propositional linear temporal logic.
Satefy, liveness and fairness in temporal logic.
The PVS proof checker: A reference manual (beta release).
Testing language containment for

An automata-theoretic approach to linear temporal logic
An automata-theoretic approach to automatic program veri ca- tion

Reasoning about in
Synthesis of Communicating Processes from Temporal Logic Speci
On combining formal and informal veri
--TR
The complexity of propositional linear temporal logics
Automatic verification of finite-state concurrent systems using temporal logic specifications
Automata-Theoretic techniques for modal logics of programs
Temporal and modal logic
The temporal logic of reactive and concurrent systems
Symbolic model checking
Memory-efficient algorithms for the verification of temporal properties
Reasoning about infinite computations
Testing language containment for MYAMPERSANDohgr;-automata using BDDs
High-density reachability analysis
An automata-theoretic approach to linear temporal logic
Forward model checking techniques oriented to buggy designs
Hybrid techniques for fast functional simulation
Symbolic model checking using SAT procedures instead of BDDs
Checking that finite state concurrent programs satisfy their linear specification
Alternation
An automata-theoretic approach to branching-time model checking
Proving Liveness Properties of Concurrent Programs
Program Verification
Simple on-the-fly automatic verification of linear temporal logic
Safety for Branching Time Semantics
Specification and verification of concurrent systems in CESAR
Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits
On-the-Fly Verification with Stubborn Sets
On Combining Formal and Informal Verification
Deadlock Checking Using Net Unfoldings
Mona MYAMPERSANDamp; Fido
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic
Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties
Freedom, Weakness, and Determinism
Checking formal specifications under simulation
Weak Alternating Automata Are Not That Weak
STeP: The Stanford Temporal Prover
Synthesis of communicating processes from temporal logic specifications

--CTR
Freddy Y.C. Mang , Pei-Hsin Ho, Abstraction refinement by controllability and cooperativeness analysis, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
R. Armoni , S. Egorov , R. Fraer , D. Korchemny , M. Y. Vardi, Efficient LTL compilation for SAT-based model checking, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.877-884, November 06-10, 2005, San Jose, CA
Orna Kupferman , Moshe Y. Vardi, From complementation to certification, Theoretical Computer Science, v.345 n.1, p.83-100, 21 November 2005
Roberto Sebastiani , Eli Singerman , Stefano Tonetta , Moshe Y. Vardi, GSTE is partitioned model checking, Formal Methods in System Design, v.31 n.2, p.177-196, October   2007
Chao Wang , Zijiang Yang , Franjo Ivani , Aarti Gupta, Disjunctive image computation for software verification, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.12 n.2, p.10-es, April 2007
automata;safety properties;model checking