Efficient Detection of Vacuity in Temporal Model Checking.
The ability to generate a counter-example is an important feature of model checking tools, because a counter-example provides information to the user in the case that the formula being checked is found to be non-valid. In this paper, we turn our attention to providing similar feedback to the user in the case that the formula is found to be valid, because valid formulas can hide real problems in the model. For instance, propositional logic formulas containing implications can suffer from antecedent failure, in which the formula is trivially valid because the pre-condition of the implication is not satisfiable. We call this vacuity, and extend the definition to cover other kinds of trivial validity. For non-vacuously valid formulas, we define an interesting witness as a non-trivial example of the validity of the formula. We formalize the notions of vacuity and interesting witness, and show how to detect vacuity and generate interesting witnesses in temporal model checking. Finally, we provide a practical solution for a useful subset of ACTL formulas.
Introduction
The ability to generate a counter-example is an important feature of model checking
tools, because a counter-example provides information to the user in the case that the
formula being checked is found to be non-valid. In this paper, we turn our attention
to providing similar feedback to the user in the case that the formula is found to be
valid. At first glance, such a goal may seem strange, because proving formulas valid is
the supposed goal of model checking. However, additional information regarding valid
formulas is indeed important, because a valid formula may hide real problems in the
model.
Several years of experience in practical formal verification of hardware at IBM
[BB+96] have shown us that during the first formal verification runs of a new hardware
design, typically 20% of formulas are found to be trivially valid, and that trivial validity
always points to a real problem in either the design or its specification or environment.
Of the formulas which are found to be non-trivially valid, examination of a non-trivial
example trace discovers a problem for approximately 10% of the formulas.
The problem of a trivially valid formula was first noted by Beatty and Bryant [BB94],
who termed it antecedent failure. Antecedent failure means that a formula is trivially
valid because the pre-condition (antecedent) of the formula is not satisfiable in the
model. If the validity of a formula is trivial, this must be indicated to the user. If it is not,
the usefulness of formal verification is compromised, since a trivially valid formula is
not intentionally part of a specification (and therefore indicates a problem in the design
or an error in the specification). For instance, consider the following formula:
AG(request
In a model M in which a request is never made, i.e., M
is trivially valid.
Antecedent failure is an intuitively easy concept to grasp. However, the fact that it
depends on the use of a particular operator is disturbing. We would like to capture the
same problem in the equivalent formula:
AG(:request - AXack) (2)
Because we are concerned with temporal logic, we would also like the notion of a
trivially valid formula to include a temporal aspect. For instance, consider the following
If p never occurs, and thus M is trivial by antecedent
failure. However, we would also like the notion of a trivially valid formula to cover the
case that, while q may occur, and thus M never occurs at a next state of p,
and thus M
In addition, the notion of a trivially valid formula should capture other potential
problems, such as that illustrated by the following formula:
AG(request ! A[:data valid Uwrite enable]) (4)
As with the previous examples, Formula 4 is trivially valid in a model in which a
request is never made. However, even in a modelM in whichM it is possible
that the validity of Formula 4 is trivial. If M AG(request ! write enable),
then there are no states in which it is required that the sub-formula :data valid hold;
in other words, there is "nothing left for the model checker to check". In such a model,
the validity of Formula 4 is trivial. In this paper, we extend and formalize the notion
of trivial validity to these and other cases. We use the term vacuity for the extended
definition, and call a formula which suffers from vacuity a vacuously valid formula.
Trivial validity is usually an indication of a problem in the model (rather than
the specification). A related problem is a formula which is non-vacuously valid, but
which does not express the property that was intended by the user. In other words,
we would like to provide a way to discover errors in the formula, even when the
formula is non-vacuously valid. We confront this problem by formalizing the notion
of an interesting witness: a trace which shows a non-trivial example of the validity of
a formula. Examining a positive example provides some confidence that the formal
specification accurately reflects the intent of the user, one of the weak links in the
practical application of formal verification to hardware design.
As an example, consider Formula 3. An interesting witness to Formula 3 is a path
on which p occurs at some state s i , q occurs at state s i+1 , and r occurs at state s i+2 .
Note that simply negating the original formula will not provide a non-trivial example.
If we negate Formula 3, we get:
Obviously, since Formula 5 is the negation of Formula 3, Formula 5 is false if
Formula 3 is true. However, because Formula 5 is an existential formula, there is no
trace which can show it is false, and the counter-example mechanisms of [HBK93] and
of SMV [McM93, CG+95] will not generate a trace.
Negating the single operand of the AG operator in Formula 3 as follows:
will also not guarantee an interesting witness. For instance, a valid counter-example to
Formula 6 is a path to a state in which p does not occur. Once again, this is a trivial
positive example of the truth of the original Formula 3.
Our motivation is temporal model checking. However, the notions of vacuity and
interesting witness are not limited to temporal logics. Therefore, we will first define our
terms in general, and only then discuss vacuity detection and generation of interesting
witnesses in temporal model checking. Finally, we will show a practical solution for a
useful subset of ACTL formulas under temporal model checking.
The remainder of this paper is organized as follows. In Section 2 we define some
important temporal logics. In Section 3 we formalize the notion of vacuity, and show
how to efficiently detect vacuity using a model checker. In Section 4 we formalize the
notion of interesting witness and show how to generate interesting witnesses using a
model checker. In Section 5 we provide a practical solution for a useful subset of ACTL.
In Section 6 we compare our work with a previous version of our theory, and with related
work. In Section 7 we conclude.
Preliminaries
is a logic with the following syntax:
1. Every atomic proposition is a formula.
2. If f and g are formulas, then so are :f and f - g.
3. If f is a formula, then Ef is also a formula.
4. If f and g are formulas, then fUg and Xf are also formulas.
Additional operators can be viewed as abbreviations of the above, as follows:
The semantics of a CTL   formula is defined with respect to a Kripke structure K.
A Kripke structure is a quadruple (S; S 0 ; R; L), where S is a finite set of states, S 0 ' S
is a set of initial states, R ' S \Theta S is the transition relation, and L is the valuation,
a function mapping each state with a set of atomic propositions true in that state. We
require that there is at least one transition from every state.
A path - of a Kripke structure K is an infinite sequence of states -
such that R(- true for every i. Given a path -, we will denote by - +i the path
starting from the i-th state in -. More formally:
The semantics of CTL   is then as follows:
is an atomic proposition.
starting from - 0 , (K; - 0 )
and for all i such that
We say that K for every path - in K , such that - 0 2 S 0 , we have (K; -)
A CTL   formula is in normal form when the operator : modifies only atomic
propositions.
is a subset of CTL   in which the only path quantifier is A (when the formula
is in normal form).
CTL [CE81] is a subset of CTL   in which each temporal operator
X) must be immediately preceded by a path quantifier E).
ACTL [GL91] is a subset of CTL in which the only path quantifier is A (when the
formula is in normal form).
LTL [Pnu81] is a subset of CTL   is which there are no path quantifiers.
The intuitive notion of vacuity derives from that of propositional antecedent failure.
Propositionalantecedent failure means that a formula is trivially valid because some pre-condition
is not satisfiable, where a pre-condition is the left-hand-side of an implication.
Another way to think of it is to say that the right-hand-side of the implication does not
affect the validity of the formula. This gives an intuitive extension of vacuity to any
operator: vacuity occurs when one of the operands does not affect the validity of the
formula. We use the notation '[ 0 ] to denote the formula obtained from ' by
replacing sub-formula with 0 .
Definition 1 (Affect). A sub-formula of formula ' affects ' in model M if there is
a formula 0 , such that the truth values of ' and '[ 0 ] are different in M .
vacuous in model M if there is a sub-formula /
of ' such that / does not affect ' in M .
These definitions capture the intuitive notion of vacuity in a manner which is independent
of a particular logic. However, they are not very useful when it comes to vacuity
detection, because there are an infinite number of cases to check. In the remainder of
this section we will show sufficient conditions on logics such that only a finite and small
number of cases are required. We will first show that it is enough to check only a subset
of the sub-formulas. Then, we will define logics with polarity for which it is enough to
check the replacement of a sub-formula by either true or false.
3.1 Vacuity with Respect to a Minimal Set of Sub-formulas
In this section, we will show that vacuity can be checked by examining only a subset
of the sub-formulas. These will be the sub-formulas which are minimal with respect
to the sub-formula pre-order (denoted -). We assume that each sub-formula is unique.
That is, we consider two separate occurrences of the same sub-formula to be different
sub-formulas.
Lemma 3. If - ', and / does not affect ' in model M , then - does not affect
in M .
Proof. Assume / does not affect ' in M , but - does affect '. Then there is a formula
- 0 such that the truth value of '[- 0 in M is different than that of ' in M . Since
- / we get that
But the truth value of '[- 0 in M is different than
the truth value of ' in M . Thus the truth value of '[/ / in M is different than the
truth value of ' in M , which means that / affects the value of ' in M , contradicting
our assumption. ut
For the sequel, we will need the following definitions:
Definition 4 (Vacuity With Respect to a Sub-formula). Let - be a sub-formula of
(denoted - '). Formula ' is vacuous in model M if - does not affect '
in M .
Respect to a Set of Sub-formulas). Let S be a set of
sub-formulas of formula ' ( S ` f-j- 'g ). Formula ' is S-vacuous in model M if
there exists - 2 S such that ' is -vacuous in M .
Definition 6 (Minimal Sub-formulas). Let S be a set of sub-formulas. We define the
minimal sub-formulas of S as:
There is no -
Theorem 7. ' is S-vacuous iff ' is min(S)-vacuous.
Proof. - (=)) If ' is S-vacuous in M , there is a - 2 S that does not affect '. Since
S is finite and - is a pre-order, there is a - 0 2 min(S) such that - 0 -. Using
Lemma 3, since - does not affect ' in M , - 0 does not affect ' in M either. This
means that ' is min(S)-vacuous in M .
- ((=) If ' is min(S)-vacuous in M , there is a - 2 min(S) ' S that does not
affect ' in M , and therefore ' is S-vacuous in M .
ut
It follows immediately that to check vacuity of ' it is enough to check for vacuity
with respect to only the minimal sub-formulas of '. We will now show that for logics
with polarity, it is enough to check the replacement of a sub-formula by either true or
false.
3.2 Logics with Polarity
In this section we will define logics with polarity. First, we will need a notation with
which to denote all models M in which a formula ' is valid. We use the following
We use the notation [[']] c to denote the complement of [[']]. We will now define what
we mean by the polarity of an operand, then define operators with polarity, and finally
define logics with polarity.
Definition 8 (Polarity of an Operand) If oe is an n-ary operator in a logic, we
say that the i-th operand of oe has positive(negative) polarity if for every fixing of
and two formulas
we have that
We say that an operator has polarity if every one of its operands has some polarity
(positive or negative).
Definition 9 (Logic with Polarity). A logic with polarity is a logic in which every
operator has polarity.
For example, the standard Boolean logic with operators -; : is a logic with
polarity, since for every two formulas
This immediately implies that the operands of - and - have positive polarity, and the
single operand of : has negative polarity.
An example of a logic which is not a logic with polarity is the standard Boolean
logic with the addition of the exclusive-or operator:
If we set a = true, we get:
But if we set a = false, we get
In the first case the polarity of the second operand is negative, and in the second positive.
This means that \Phi does not have polarity.
is a logic with polarity.
Proof. First, note that the set of models that a CTL   formula satisfies is a subset
of f(K; -)j- is a path in the structure Kg. As we have already shown, the standard
Boolean operators - and : all have polarity.
We now show that the single operand of the path quantifier E has a positive polarity.
Given there is a path - 0
in K that starts at the same state that - does, and (K; - 0 ) This implies that
We proceed to prove that both operands of the U operator have positive polarity.
1. Let us fix the second operand of the U operator to be some . Given ' 1 and ' 2 ,
then there is an integer n, s.t.
- for all
Which proves that (K; -)
2. Let us fix the first operand of U to be some /, Given ' 1 and ' 2 , where [[' 1
if (K; -) there is an integer n, s.t.
- for all
which proves that (K; -)
Finally, we show that the single operand of the operator X has positive polarity.
Given
the assumption (K; - +1 ) meaning that (K; -) which concludes the
proof. ut
3.3 Vacuity Detection in Logics with Polarity
In this section we will show that in logics with polarity it is enough to check the
replacement of a sub-formula by either true or false.
First we define the polarity of a sub-formula, then we will present the main result of
this section.
Definition 11 (Polarity of Sub-formula). Given a formula ', we define the polarity
of sub-formulas of ' recursively:
- ' has positive polarity
is of positive(negative) polarity, then - i has positive
polarity if the i-th operand of oe has a positive(negative) polarity, and- i has negative
polarity otherwise.
Lemma 12. In a logic with polarity, if - ', and- is witha positive(negative) polarity,
then if [[- 0
Proof. The proof proceeds by induction on the size of the formula '.
(base case:) ' is an atom, so - has positive polarity, and '[- 0
Therefore, if
(induction step:) then we have the same as in the
base case. Otherwise, we know that there is one i such that - i . There are two
cases:
1. The i-th operand of oe is of positive polarity. In this case, the polarity of - in
i is as it is in ', therefore, according to the induction hypothesis,
and since the i-th operand of oe is of positive polarity, then by
Definition 8 we have
2. The i-th operand of oe is of negative polarity. In this case, the polarity of - in
i is the opposite of it's polarity in '. Therefore, by the induction hypothesis
and since the i-th operand of oe is of negative polarity, we
have
ut
In [BB+97] we defined a subset of ACTL, and a set of important sub-formulas,
and proved that in order to detect vacuity with respect to this set it is enough to show
that M j= '[ false] where is the minimal sub-formula of all the important
sub-formulas (See section 5). In [KV99], Kupferman and Vardi expand on this result by
showing that for CTL   , a formula ' is vacuous iff there is some minimal sub-formula
of ' such that M satisfies '[ true] iff M satisfies '[ false]. We will now
prove a very similar result that holds for all logics with polarity. The proof is practically
the same as the one in [KV99]; we give it here for the sake of completeness.
We define the semantics of true and false as follows: is a modelg
and
Theorem 13. Let be a sub-formula of formula ' in a logic with polarity. Then, for
every model M the following are equivalent:
1. does not affect ' in M .
2.
Where and is of positive polarity, or M 6j= ' and is of
negative polarity. Otherwise
Proof.
does not affect ' in M . This means that for every / 0 , and specifically for
which concludes this
part of the proof.
- ((=) Note that for every / 0 we have:
Two cases:
1. If / is of positive polarity, then using Lemma 12, we get
then by the assumption M but by the
containment above, this implies that for every
meaning that / does not affect ' in M .
then by the assumption M 6j= '[/ / true]. By the same
argument as above we get that for every meaning that
/ does not affect ' in M .
2. If / is of negative polarity, then using Lemma 12, we get
then by the assumption M but by the containment
above, this implies that for every meaning that
/ does not affect ' in M .
then by the assumption M 6j= '[/ / false], but by the
containment above, this implies that for every
meaning that / does not affect ' in M .
ut
In Section 3.1 we showed that it is enough to check vacuity for ' with respect to a
subset of the sub-formulas '. In this section we showed that for logics with polarity, it
is enough to check the replacement of a sub-formula by either true or false. We now
combine these two results in the following corollary:
Corollary 14 In a logic with polarity, for a formula ', and a set S of sub-formulas of
for every model M , the following are equivalent:
- ' is S-vacuous in M
- There is / 2 min(S) such that:
Where and / is of positive(negative) polarity.
Otherwise,
This corollary gives us the ability to check vacuity of a formula in a logic with
polarity by checking a relatively small number of other formulas, each of them of
size not greater than that of '. To be more precise, for S-vacuity, we need to check
1. Check '.
2. For each sub-formula / 2 min(S), check the new formula '[/ / X]. The value
of X is either true or false, according to whether ' is valid or not, and the polarity
of .
Formula ' is S-vacuous iff at least one of these formulas has the same truth value
as that of '.
Since CTL   is a logic with polarity, we have shown the result of [KV99]: We can
use a CTL   model checker to check vacuity in complexity O(j'j \Delta CM (j'j)), where
CM (n) is the complexity of checking a formula of size n in model M .
Interesting
The definition of vacuity refines the traditional distinction between valid and non-valid
formulas with respect to a model M . We now classify formulas as either non-valid,
vacuously valid, or non-vacuously valid. We would like to make the same refinement
in the method we use to distinguish between the classes. Traditionally, we show that
a formula is valid by means of a proof, and that a formula is non-valid by means of a
counter-example. We will now define an interesting witness, which is the means we will
use to show that a formula is non-vacuously valid. In this section we assume that the
formula in question ' is valid in model M .
To make our definitions clear we use model checking problem of propositionallogic
as an example: The logic is the standard propositional logic on n boolean variables. A
Model M is some non-empty subset of the set of assignments to the n variables. We say
that M is true under all assignments in M . For example, if M is the set of all
assignments, then M is a tautology.
4.1 Pre-order and Counter-Examples
Before defining an interesting witness, we first formalize the notion of a counter-
example. We will require two things from a counter-example to a formula.
1. That its existence proves the non-validity of the formula.
2. That it is small.
The second requirement is natural, since the smaller the counter-example is, the
more useful it is to the user. Our approach is to define a pre-order on the set of models,
such that non-validity on a smaller model always proves non-validity of a larger one.
Then, we will require that a counter-example be a model which is minimal with respect
to this pre-order.
Definition 15 (The natural pre-order of a logic) Given a logic L, we define the
natural pre-order of the logic OE L on the set of models. M 0 OE L M iff for all ' 2 L we
have that M
The natural pre-order of propositional logic is containment.
Proof.
propositional formula that is valid for all assignments
in M , will also be valid for all assignments in M 0 .
, then there is at least one assignment
the n variables that is in M 0 and not in M . We define the following propositional
This formula is true on any assignment that is not equal to ff, and false on ff itself.
Therefore we have that M 0 6j=
ut
We can now define a counter-example:
Definition 17 (Counter-Example) In logic L, a model C is a counter-example to ' in
model M , if it satisfies the following conditions:
1. C OE L M .
2. C 6j= '.
3. C is minimal w.r.t. OE L among the models that satisfy properties 1 and 2.
It follows immediately from the definition that:
there exists a counter-example to ' in M .
We now return to our example of propositional logic, and show that counter-examples
are as we expected:
In propositional logic, If C is a counter-example to formula ' in model M ,
then C is a model with one assignment.
Proof. If C is a counter-example, then C 6j= ', therefore there is an assignment ff 2 C
such that '(ff) is false. fffg is a model, A ` C and A 6j= '. Since C is minimal
w.r.t. ', we get that since there is no model A 0 such that A 0 ' A (we required
that models are non-empty). ut
4.2 Pre-orders and Counter-Examples in temporal logic
We have previously shown that for the case of propositional logic, Definition 17 captures
our intuitive notion of what a counter-example is. Since the motivation of this paper
is temporal logic, we would like to examine more closely the properties of a counter-example
in some important temporal logics.
- LTL: in [Pnu85] Pnueli has proved that the natural pre-order for LTL according to
Definition 15 is:
is a computation path in Mg.
In LTL, if M 6j= ', then there is a computation path - in M , such that f-g 6j= '.
Using the same arguments as in the proof of claim 19, we can show that a counter-example
to ' will always be a model with one computation path in it.
- CTL and CTL   : Milner in [Mil71] has proved that for CTL and CTL   , the natural
pre-order is:
. This means that CTL and CTL   have only
trivial counter-examples that are the model itself. Indeed, the formula EF (p) cannot
be shown false by any model that has less behavior than the original, since we might
have removed states where p was true. Note that even if we did have some method
of specifying larger models as counter-examples, CTL would still be problematic.
The formula EF (p) -AG(q), cannot be proved false using neither a larger model,
nor a smaller one.
Using the same proof as in [Mil71], it can be shown that for
ACTL and ACTL   , the natural pre-order is:
. For these logics, it is difficult to characterize
counter-examples. A model M always simulates a computation path - in it (- OE ACTL
meaning that computation paths may serve as counter-examples. For instance,
a counter-example to the formula AG(p) is a path on which :p holds at some state.
However, there are formulas and models for which a path cannot serve as a counter-
example. The formula AX(p)-AX(:p) cannot have a path as a counter-example,
since on any deterministic path it will be evaluated to be true. A counter-example
for this formula must be more complex. Buccafurri, Eiter, Gottlob and Leone have
addressed this problem in detail in [BEGL99].
4.3 Interesting Witnesses
In the case of a non-valid formula, a standard model checker provides a counter-example
to the user. If the formula is valid, and using our vacuity checking procedure we can
prove it non-vacuous, we would like to provide an interesting witness to the user, which
is an analog of a counter-example - it proves non-vacuity, while a counter-example
proves non-validity.
(Interesting Witness With Respect to a Sub-formula). In logic L, a
model W is a -interesting witness to ' in M , if it satisfies the following conditions:
1. W OE L M .
2. W j= ', and ' is not -vacuous in W .
3. W is minimal w.r.t OE L among the models that satisfy properties 1 and 2.
We now get an analogous claim to claim 18:
there exists a /-interesting witness W to ' in M iff ' is not
/-vacuous in M .
Proof.
' is not /-vacuous in W ,
there is a / 0 such that W 6j= '[/ / / 0 ]. Again, since W OE L M , M 6j= '[/ / / 0 ].
This means that ' is not /-vacuous in M .
((=) The set of models that are smaller than M , and ' is not /-vacuous in them
is non-empty, since M is such a model. Therefore any one of the minimal elements
in this set is a /-interesting witness to ' in M .
ut
So, under the assumption that ' is valid in M , an interesting witness proves the non-
vacuity of one sub-formula. Now we would like to have such proofs of more general
non-vacuity, for sets of sub-formulas (and in particular , for the set of all sub-formulas).
However, a single interesting witness will not always suffice.
Consider the formula in a model M such that M
non-vacuous there is no single example which can show non-vacuity. In order to show
p-non-vacuity, q must be set to 0, and in order to show q-non-vacuity, p must be set
to 0. But since M j= ', we cannot show an example in which both p and q are 0
simultaneously.
The naive solution would be to generate one interesting witness for every sub-
formula. However, an interesting witness to one sub-formula, may also be an interesting
witness to a different sub-formula. This is shown in the following proposition.
Proposition 22 Assume M is a /-interesting witness to ' in M , and
then W is also a interesting witness to ' in M .
Proof. Since W is a /-interesting witness to ', / affects ' in W , and according to
affects ' in W , meaning that W is a interesting witness to ' in M .
We shall now use Proposition 22 to get a more general result:
Corollary 23. If M j= ', and ' is not S-vacuous in M , then a set that has a /-
interesting witness for every / in min(S) also has a /-interesting witness for every /
in S.
4.4 Interesting Witness Generation in Logics with Polarity
In Section 3.3 we have shown that if our logic is a logic with polarity, then checking
vacuity is much easier than the general case. The same result holds for interesting
witness generation.
Lemma 24. In a logic with polarity L, if M is of
positive(negative) polarity, then the following are equivalent:
- ' is not -vacuous in C .
Proof.
we get that C since C 6j= '[ X],
' is not -vacuous in C.
we get that C ' is not -vacuous
in C, then using Theorem 13, we get that C 6j= '[ X].
ut
Theorem 25. In a logic with polarity L, if M j= ', and - ' is of positive(negative)
polarity in ', the following are equivalent:
- C is a counter-example to '[ X], Where
- C is a -interesting witness to ' in M .
The proof follows directly from Lemma 24, which proves that the two are equivalent,
but omits the requirement of minimality. Adding this requirement to both of them
obviously leaves them equivalent.
This theorem gives us the ability to easily generate interesting witnesses if we can
generate counter-examples to the formulas in the logic: a -interesting witness to ' in
M is really a counter-example to one specific formula obtained by replacing by true
or false, depending on the polarity of in '. Note that if this formula is valid in M ,
then ' is -vacuous in M .
If we now assume that we have a logic with polarity, and that we have a model
checker for this logic that generates counter-examples to non-valid formulas, then we
can enhance our model checker to have the following properties:
Enhanced Model-Checker
Given a formula ', a model M , and a set S of sub-formulas of ':
1. If M 6j= ', generate a counter-example.
2. If M j= ', and ' is S-vacuous in M , then output all sub-formulas in min(S) that
do not affect ' in M .
3. If M j= ', and ' is not S-vacuous in M , then generate jmin(S)j interesting
of M , such that for each 2 S, at least one of them is a -interesting
witness for ' in M .
The number of formulas checked if the formula is valid is jmin(S)j + 1, since for
each in min(S) we generate a formula to be model checked. If it is valid, then ' is
S-vacuously valid. Otherwise, the model checker returns a counter-example, which is
an -interesting witness for '. Since all formulas we generate are smaller in size than ',
we get that the complexity of the enhanced model checker is O(jmin(S)j \Delta CM (j'j)),
where CM (n) is the complexity of model checking a formula of size n.
In the case where ' is S-vacuous, the enhanced model checker only outputs all
the minimal sub-formulas that do not affect '. However, the user may be interested in
knowing exactly which of the sub-formulas in S are vacuous. To achieve this goal, we
may need to check as many as jSj formulas.
5 Practical Vacuity Detection and Interesting Witness Generation
The motivation of this work was to provide an indication of vacuity and interesting
witnesses to users of model checking. However, the complexity results of Sections 3.3
and 4.4 do not allow this in reasonable time. While the complexity of determining
vacuity and generating interesting witnesses is only j'j times the complexity of model
checking a formula of size j'j, in practical terms this is too high, because a typical
may take hours of CPU time to verify. We would like a method of determining
vacuity and generating an interesting witness for a formula ' that is no more expensive
than model checking '.
In order to give an efficient solution, we will limit ourselves to a subset of ACTL,
called w-ACTL, and to a subset of the sub-formulas, called important sub-formulas
with respect to which we will check vacuity. We will then show that the complexity of
checking vacuity of important sub-formulas in w-ACTL is exactly the complexity of the
model checking ' in M . Finally, we show some examples.
5.1
In this section we define witness-ACTL (w-ACTL), a subset of ACTL, which is in turn a
subset of CTL. Informally, w-ACTL formulas are ACTL formulas in which for all binary
operators (-, AU, AV), at least one of the operands is a propositional formula. We
divide the ACTL operators into propositionaloperators (:, -) and temporal operators
(AX, AG, AF, AU, AV), and call a formula which has only propositional operators, a
simple formula. w-ACTL is the set of state formulas described by the following:
Definition 26 (w-ACTL).
1. Every simple formula is a state formula.
2. If f is a simple formula, - is a state formula, and ffi is some binary operator of
are state formulas.
3. If - is a state formula, and ffi is some unary temporal operator of ACTL (AG, AF,
AX), then ffi(-) is a state formula.
The definition of w-ACTL may seem artificial at first glance. However, in our
experience this is not the case. Most of the formulas written by users are w-ACTL
formulas, which capture nicely the linear nature of most specifications.
5.2 Important sub-formulas
In order to be able to efficiently check vacuity and generate interesting witnesses for w-
we have to restrict ourselves to a subset of the sub-formulas for which
vacuity will be detected. Rather than being a drawback, we show that distinguishing
between important and non-important sub-formulas is an advantage, as it is a reflection
of how engineers use CTL to specify their designs.
We first define the set of important sub-formulas of a formula, with respect to which
vacuity will be checked. Basically, the important sub-formulas are all the temporal
(non-simple) ones.
Definition 27 (Important sub-formulas). Let ' be a w-ACTL formula, we define
Imp(') recursively:
1. If ' is simple, then f'g.
2. If is non-simple, and f is simple, then
3. If are simple, then
4. If
The choice made in item 3 above may seem arbitrary. The reason that only f 1 is
important is that f 2 is the only operand that can cause vacuity. For A[f 1 U f 2
cause vacuity of f 1 if it is always true immediately. However, f 1 cannot cause vacuity
of f 2 because even if f 1 is always true forever, the AU operator still requires something
of eventually it occurs. For the AV operator, f 2 can cause vacuity of f 1 if it is
always true forever, because then nothing is required of f 1 . However, f 1 cannot cause
vacuity of f 2 if it is always true immediately, because in that case, the AV operator still
requires something of f 2 : that it occurs at the same time.
We justify our choice of the temporal sub-formula of a binary operator as an important
sub-formula as follows. The choice is simply a reflection of how engineers tend to
use CTL to code a specification, as well as how they tend to design their hardware. For
instance, consider the following specification:
AG(request
which expresses the requirement that if a request is accepted (which happens or not
one cycle after it appears), then two cycles later either the read busy signal is asserted,
or the write busy signal is asserted. Logically, this is equivalent to the formula:
AG(:request -AX(:req accepted - AXAX(read busy - write busy))) (8)
Vacuity of Formula 7, which detects that M j= AG(:request) would probably
detect a problem in the model, because otherwise the signal called request is mean-
ingless. However, a vacuity which detects that M j= AG(AX(:req accepted -
AXAX(read busy - write busy))) is quite often useless to the engineer, as it is
highly likely that she has designed her logic intentionally for this to be so, and prevents
read busy or write busy from being asserted spuriously by not asserting req accepted
if there was not a request the previous cycle. Thus, for the binary operators, we have
chosen the non-simple operand to be the important sub-formula.
5.3 Vacuity and Interesting Witnesses for w-ACTL formulas
Recall that ' is Imp(')-vacuous, if it is vacuous with respect to a sub-formula
(Theorem 7). We now show that min(Imp(')) has only one
sub-formula in it, meaning that Imp(')-vacuity checking will be easy.
28 For every ' in w-ACTL the size of min(Imp(')) is one.
Proof. The proof proceeds by induction:
1. If ' is simple, then and we are done.
2. If Every sub-formula in Imp( )
is a sub-formula of and therefore of '. This means that ' is not minimal
in Imp('), so using the induction hypothesis
3. If
Using the same argument as above, ' is not in min(Imp(')), meaning that
or in the second case
Again, using the induction hypothesis, we conclude that
ut
Since we are dealing with ACTL formulas (negation can be applied to atomic
propositions only), and because of the way we choose the important sub-formula (an
important sub-formula is never an operand of ":"), we get that min(Imp(')) always
has a positive polarity in '. We now define the formula witness(') as follows:
According to Corollary 14 and Theorem 25, it is enough to check witness(') in order
to detect Imp(')-vacuity and generate an Imp(')-interesting witness. Given a model
checker that can generate counter-examples for ACTL formulas, we can design an
enhanced model checker for w-ACTL (see Section 4.4) with the following properties:
Given a w-ACTL formula ' and model M ,
1. If M 6j= ' generate a counter example.
2. If M output that the formula passed vacuously.
3. If M j= ' and M 6j= witness(') output one interesting witness W , such that
and for every important sub-formula ( 2 Imp(')), W is a -
interesting witness to ' in M .
5.4 Detailed Vacuity
If Imp(')-vacuity is detected by our enhanced model checker, there is no indication of
which of the pre-conditions caused the vacuity. As we said before, we can solve this by
checking jImp(')j+1 formulas instead of just 2. However, in our specific case, we can
actually check only log formulas. One can easily prove (using the
same proof as in Claim 28) that the sub-formulas in Imp(') are linearly ordered. Also,
it follows directly from Lemma 3 that if - then if ' is -vacuous, then ' is also
-vacuous. Combining these observations, we get that there is one minimal sub-formula
2 Imp('), such that for all - 2 Imp('), ' is -vacuous iff - . This means that
we can use binary search on Imp(') to find this . To implement this, we need only
check log
5.5 Semantic refinements
The careful reader will have noted that our definition of important sub-formulas will not
detect vacuity in some basic cases, among them propositional antecedent failure. For
instance, consider the following formula:
AG(read request ! read enable)
The vacuity detection (and witness generation) formula we generate for Formula 9
as defined above is:
only in a model with no fair paths, and thus detects vacuity
only in that case. Intuitively, this is not satisfying. We would like to be able to detect
propositional antecedent failure.
Another problem is shown by the following Sugar 1 formula:
AG(request ! next event(grant)(acknowledge)) (11)
Formula 11 expresses the requirement that the first grant after a request must be
accompanied by an acknowledge. The ACTL normal form of Formula 11 is:
AG(:request -A[grantV (:grant - acknowledge)]) (12)
Thus, the vacuity detection formula for Formula 11 as defined above is:
AG(:request - A[falseV :grant - acknowledge]) (13)
Simplification of the above formula gives:
AG(:request - AG(:grant - acknowledge)) (14)
1 Sugar is a syntactic sugaring of CTL [CE81] formulas, and is the specification language used
by the RuleBase formal verification tool. In [BB+96] we outlined its basic features.
14 will not detect vacuity in the case that a request is never followed by a
grant. Once again, this is not intuitively satisfying. The next event operator expresses
a kind of temporal implication, thus the failure of a grant to occur is a kind of temporal
antecedent failure, and we would like to detect it.
We therefore expand our definition of important sub-formulas as follows:
1. If are simple, and the - operator
is derived from the use of the ! operator by the user
2. If are simple, then
5.6 Implementation details
In theory, a computation path is infinite and therefore, every example is infinite. In prac-
tice, however, the algorithm of [CG+95] will sometimes give finite counter-examples,
when a finite counter-example is enough to show that the formula is false. In every case
but one, the finite counter-example given by [CG+95] is "interesting enough" for our
purposes. The exception is the AU operator. As a positive example to A[-U ], we would
like to see a trace on which occurs, but [CG+95] may give us a counter-example to
A[falseU/] which ends before / has occurred. Therefore, we use A[(AF false)U/] to
get an infinite counter-example, just as [CG+95] uses EG true to get an infinite example.
5.7 Examples
We now show the generation of an interesting witness formula. We use a typical Sugar
formula as an example:
AG(request ! next event(data)[4](last data)) (15)
Formula 15 states that last data should be asserted with the fourth data after a
request. Since last data is considered to be non-simple (because it is the second operand
of a next event operator) the interesting witness formula is:
AG(request ! next event(data)[4](false)) (16)
We convert Formula 16 into ACTL normal form:
AG(:request - A[dataV (:data - AXA[dataV (:data -
(:data - AXA[dataV (:data - false)])])])]) (17)
It is easy to see that Formula 17 is valid iff either a request never occurs, or no
request is ever followed by four datas. Also, it is clear that if Formula 17 is found to be
non-valid, the counter-example will be an interesting witness of Formula 15, on which
a request followed by four datas will occur.
Now examine the following formula, which expresses the fact that we require q to
occur an infinite number of times:
The interesting witness formula for Formula
AG AF false (19)
If Formula cannot be vacuously valid unless there are no fair paths,
and indeed Formula 19 is non-valid in all non-empty models. The counter-example to
Formula 19 will be a computation path, on which q will appear infinitely many times
(because Formula
6 Comparison with Previous and Related Work
In this section, we compare our work with a previous version of our theory, and with
related work.
6.1 Comparison with Previous Work
In a previous version of this paper [BB+97], we required that an interesting witness to
formula ' to be a single path, on which all important sub-formulas affect the validity
of '. This requirement was a result of the practical motivation of our original work. In
this paper, an interesting witness is defined per sub-formula, so that interesting validity
is demonstrated by multiple paths. The new definition is more natural, because, as we
showed in Section 4.4, it allows us to guarantee interesting witnesses whenever we
can guarantee counter-examples. It thus solves the problem raised by [KV99] of the
following
G(request
Consider a model M with two paths, one path that never satisfies request and
a second path that always satisfies grant. If we require that an interesting witness
be a single path, then there is no interesting witness to Formula 20 in such a model,
despite the fact that there exists a counter-example to Formula 20 in any model in which
Formula 20 is not valid.
6.2 Comparison with Related Work
Other works, including [BB94] and [PP95], have noted the problem of trivial validity,
and shown how to avoid them using hand-written checks. Our original paper [BB+97]
was, we believe, the first attempt to formalize the notion of trivial validity, as well as
the first attempt to detect it automatically under symbolic model checking.
Philosophers have also dealt with the problem of trivial validity. Relevance logic
(also known as relevant logic) is a non-standard logic designed to prevent the paradoxes
of material and strict implication. These occur when an antecedent is irrelevant to the
consequent, as in the formula While relevance logic
deals with the problem by defining a new logic, our approach is different. We formalize
the notion of vacuity and provide a method to detect it while leaving the logic itself
unchanged.
In this paper, we use the term interesting witness to mean a computation path
showing one non-trivial example of the validity of a valid formula. We are the first to
use the term interesting witness, and the first to generate positive examples for valid
non-existential formulas. In [HBK93], Hojati, Brayton and Kurshan describe counter-example
generation for model checking using CTL and language containment using
L-automata [Kur90]. In [CG+95], Clarke, Grumberg, McMillan and Zhao describe the
counter-example and witness generation algorithmof SMV [McM93]. Neither [HBK93]
nor [CG+95] produce interesting witnesses for valid non-existential formulas.
In [KV99], Kupferman and Vardi presented an extension of [BB+97] from w-ACTL
to CTL   . Their results for vacuity are the same as those presented here, but they require
that an interesting witness to a CTL   formula be a single path.
7 Conclusions and future work
We have formalized the notion of vacuity and interesting witness for logics with polarity.
We have shown a practical method for detecting vacuity and generating interesting
witnesses for w-ACTL formulas. As discussed above, the ability to detect vacuity and
provide an interesting witness are extremely important in the practical application of
model checking to industrial hardware designs.
Although the definition of vacuity we have presented is simple and elegant, there
is still territory left uncovered. Pnueli [Pnu97] has suggested the following example:
in a model M such that M j= AGp, the formula AGAFp is valid, but our intuition
tells us that the user is somehow "missing the point". A possible approach for solving
this problem, is to refine our definition of vacuity. Instead of checking whether a sub-formula
can be replaced by any other sub-formula, we will check whether it can be
replaced by some "simpler" formula. The term "simpler" is a vague notion, but there
are some immediate examples: p is simpler than AF (p), AG(p) is simpler than AF (p),
and perhaps even AG(p) - AF (q) is simpler than A[pUq].
A possible improvement could be done to the efficiency of vacuity checking. Instead
of using the model checker as a black box, devise efficient model checking algorithms
specifically for vacuity checking. A trivial enhancement would be to cache intermediate
results in the model checker, since all the vacuity checking formulas are very similar.



--R

The Logic of Relevanceand Necessity.
"Formally verifying a microprocessor using a simulation methodology"
"RuleBase: an Industry-Oriented Formal Verification Tool"
"Efficient Detection of Vacuity in ACTL Formulas"
"Characterizing finite Kripke structures in propositional temporal logic"
"On ACTL Formulas Having Deterministic Counterexamples"
"Design and synthesis of synchronization skeletons using Branching Time Temporal Logic"
"Characterizing Properties of Parallel Programs as Fixed-point"
"Efficient Generation of Counterexamples and Witnesses in Symbolic
MIT Press
"'Sometimes' and 'Not Never' Revisited: On Branching versus Linear Time Temporal Logic"
"Model checkingandmodular verification."
"BDD-based debugging of designs using language containment and fair CTL."
"Vacuity Detection in Temporal
"Analysis of Discrete Event Coordination,"

"Relevance Logic"
"Symbolic
"An Algebraic Definition of Simulation between Programs"
"Formal Verification of a Commercial Serial Bus Interface"
"A Temporal Logic of Concurrent Programs"
"Linear and Branching Structures in the semantics and logics of reactive systems"
"Fair Synchronous Transition Systems and Their Liveness Proofs"
question from the audience
"The Computer-Aided Modular Framework - Motivation, Solutions and Evaluation Criteria"
--TR
MYAMPERSANDldquo;SometimesMYAMPERSANDrdquo; and MYAMPERSANDldquo;not neverMYAMPERSANDrdquo; revisited
Characterizing finite Kripke structures in propositional temporal logic
Model checking, abstraction, and compositional verification
Formally verifying a microprocessor using a simulation methodology
Efficient generation of counterexamples and witnesses in symbolic model checking
RuleBase
Model checking
Symbolic Model Checking
Characterizing Correctness Properties of Parallel Programs Using Fixpoints
Linear and Branching Structures in the Semantics and Logics of Reactive Systems
Vacuity Detection in Temporal Model Checking
Model Checking and Modular Verification
Fair Synchronous Transition Systems and Their Liveness Proofs
Efficient Detection of Vacuity in ACTL Formulaas
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic
Analysis of Discrete Event Coordination
BDD-Based Debugging Of Design Using Language Containment and Fair CTL

--CTR
Mats P. E. Heimdahl, Safety and Software Intensive Systems: Challenges Old and New, 2007 Future of Software Engineering, p.137-152, May 23-25, 2007
Hana Chockler , Orna Kupferman , Moshe Y. Vardi, Coverage metrics for temporal logic model checking, Formal Methods in System Design, v.28 n.3, p.189-212, May 2006
Michael W. Whalen , Ajitha Rajan , Mats P.E. Heimdahl , Steven P. Miller, Coverage metrics for requirements-based testing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
I. Pill , S. Semprini , R. Cavada , M. Roveri , R. Bloem , A. Cimatti, Formal analysis of hardware requirements, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
Marsha Chechik , Arie Gurfinkel , Benet Devereux , Albert Lai , Steve Easterbrook, Data structures for symbolic multi-valued model-checking, Formal Methods in System Design, v.29 n.3, p.295-344, November  2006
Shoham Ben-David , Cindy Eisner , Daniel Geist , Yaron Wolfsthal, Model Checking at IBM, Formal Methods in System Design, v.22 n.2, p.101-108, March
model checking;interesting witness;formal verification;vacuity;temporal logic