Regular Vacuity
Doron Bustan2,Alon Flaisher1,Orna Grumberg1,Orna Kupferman3 ,and
Moshe Y.Vardi2
1Technion Haifa
2Rice University
3Hebrew University
Abstract.The application of model-checking tools to complex systems involves
a nontrivial step of modelling the system by afinite-state model and a translation
of the desired properties into a formal specification.While a positive answer of
the model checker guarantees that the model satisfies the specification,correct-
ness of the modelling is not checked.Vacuity detection is a successful approach
forfinding modelling errors that cause the satisfaction of the specification to be
trivial.For example,the specification“every request is eventually followed by a
grant”is satisfied vacuously in models in which requests are never sent.In gen-
eral,a specificationϕis satisfied vacuously in a model M ifϕhas a subformula
ψthat does not affect the satisfaction ofϕin M,where“does not affect”means
we can replaceψby a universally quantified proposition.Previous works focus
on temporal logics such as LTL,CTL,and CTL∗,and reduce vacuity detection to
standard model checking.
A major feature of recent industrial property-specification languages is their reg-
正则化英文ular layer,which includes regular expressions and formulas constructed from reg-
ular expressions.Our goal in this work is to extend vacuity detection to such a
regular layer of linear-temporal logics.We focus here on RELTL,which is the
extension of LTL with a regular layer.We define when a regular expression does
not affect the satisfaction of an RELTL formula by means of universally quan-
tified intervals.Thus,the transition to regular vacuity takes us from monadic
quantification to dyadic quantification.We argue for the generality of our defi-
nition and show that regular-vacuity detection is decidable,but involves an expo-
nential blow-up(in addition to the standard exponential blow-up for LTL model
checking).This suggests that,in practice,one may need to work with weaker
definitions of vacuity or restrict attention to specifications in which the usage of
regular events is constrained.We discuss such weaker definitions,and show that
their detection is not harder than standard model checking.We also show that,
under certain polarity constraints,even general regular-vacuity detection can be
reduced to standard model checking.
1Introduction
Model-checking tools are successfully used for checking whether systems have desired properties[9].The application of model-checking tools to complex systems involves
a nontrivial step of modelling the system by afinite-state mathematical model,and translation of the desired properties into a formal specification.When the model does not satisfy the specification,model-checking tools accompany a negative answer with a counterexample,which may point to a real error in the system[8].It is often the case, however,that there is an error in the modelling of the system and/or in the formal spec-ification.Such errors may not be detected when the answer of the model-checking tool is positive:while a positive answer does guarantee that the model satisfies the speci-fication,the answer to the real question,namely,whether the system has the desired properties,may be different.
The realization of this unfortunate situation has led to the development of several sanity checks for formal verification.The goal of these checks is to detect errors in the modelling of the system and the p
roperties.Sanity checks in industrial tools are typi-cally simple,often ad hoc,tests,such as checking for enabling conditions that are never enabled[20].A more systematic approach is based on vacuity detection.Intuitively,a specification is satisfied vacuously in a model if it is satisfied in some non-interesting way.For example,the LTL specificationθ=globally(req→eventually grant) (“every request is eventually followed by a grant”)is satisfied vacuously in a model with no requests.While vacuity checking cannot ensure that whenever a model satis-fies a formula,the model is correct,it does capture inconsistencies between the model and the verified property.Being automatic,vacuity checking avoids hidden false as-sumptions made by the verifier,and thus it is more likely to capture modelling and specification errors.
Several years of experience in practical formal verification have convinced the veri-fication group in IBM Haifa Research Laboratory that vacuity is a serious problem[5]. To quote from[5]:“Our experience has shown that typically20%of specifications pass vacuously during thefirst formal-verification runs of a new hardware design,and that vacuous passes always point to a real problem in either the design or its specification or environment.”Thefirst formal treatment of vacuity is described in[5].Consider a model M satisfying a specificationϕ.A subformulaψofϕdoes not affect(the sat-isfaction of)ϕin M if M also satisfies all formulas obtained by modifyingψ.In the example above,the subformula grant does not affe
ctθin a model with no requests. Now,M satisfiesϕvacuously ifϕhas a subformula that does not affectϕin M.A general method for vacuity detection was presented in[19],who showed that when all the occurrences ofψinϕare of a pure polarity(that is,they are either all under an even number of negations(positive polarity),or all under an odd number of negations (negative polarity)),thenψdoes not affectϕiff M satisfies the formula obtained from ϕby the single extreme modification ofψ(to true in caseψhas a negative polarity, and to false otherwise).This observation reduces vacuity detection to model checking. The usefulness of vacuity analysis is also demonstrated via several case studies in[22]. For more recent work on vacuity checking,see[16,15].
As shown in[19],the method described there can be used when subformulas ofϕare of a mixed polarity.In practice,however,one often needs to cope with mixed polar-ity.For example,the subformulaψhas a mixed polarity in formulas of the(commonly seen)form globally(ψ→θ)∧eventuallyψ.In fact,industrial-strength property-specification languages such as Sugar[4],ForSpec[3],and the recent standards PSL1.01
and SV A3.1a[1]contain operators in which even a single occurrence ofψmay not have a pure ,ψXORθorψ↔θ).
Once we allow subformulas of a mixed polarity,there is a need to re-examine the definition of whenψdoes not affectϕin M.Indeed,it is only in the pure-polarity case that the various modifications ofψmay be restricted to the single extreme modifica-tion.Such a re-examination was done in[2],who considered vacuity detection for LTL specifications.While the modifications toψin[5]are ,M has to satisfy all formulasϕ[ψ←ψ ],namely formulas obtained fromϕby substitutingψby an LTL formulaψ ,Armoni et al.argued that a right definition is one in which the modifica-tions toψare ,M has to satisfy the formula(∀x)ϕ[ψ←x],obtained by substitutingψby a universally quantified proposition1.Gurfinkel et al further extend this definition to CTL∗in[15]arguing that it is more robust than other definitions.. It is shown in[2]that,under such a semantic interpretation,vacuity detection of LTL formulas can still be reduced to LTL model checking.A tool used at Intel for vacuity detection is also described in[2].
As mentioned earlier,the work in[2]was motivated by the need to extend vacuity detection to recent industrial property-specification languages,which are significantly richer syntactically and semantically than LTL.A major feature of these languages, which does not exist in LTL,is a regular layer,which includes regular expressions and formulas constructed from regular expressions.The regular layer does not only add to the expressive power of the specification it can express the wholeω-
regular spectrum,but it also seemed to be more intuitive to hardware engineers.For some languages like SV A3.1a,the only way to express temporal properties is using regular expressions.
As an example of the use of the regular layer,consider the ForSpec formula e seqθ, where e is a regular expression andθis a formula,asserts that some e sequence is fol-lowed byθ,and the ForSpec formula e triggersθ,asserts that all e sequences are fol-lowed byθ.Our goal in this paper is to extend vacuity detection to such a regular layer of linear-temporal logics.Rather than treat the full complexity of industrial languages, we focus here on RELTL,which is the extension of LTL with a regular layer.Thus, we need to define,and then check,the notion of”does not affect,”not only for subfor-mulas but also for regular expressions.We refer to the latter as regular vacuity.As an example,consider the propertyϕ=globally((req·(¬ack)∗·ack)triggers grant), which says that a grant is given exactly one cycle after the cycle in which a request is acknowledged.Note that if(¬ack)∗·ack does not affect the satisfaction ofϕin M (that is,replacing(¬ack)∗·ack by any other sequence of events does not cause M to violateϕ),we can learn that acknowledgments are actually ignored:grants are given, and stay on forever,immediately after a request.Such a behavior is not referred to in the specification,but can be detected by regular vacuity.Note that if the same regular expression appears in the left-hand side of both seq and triggers formulas or on both sides of a triggers formula,then this expression has mixed polarity.
In order to understand our definition for regular vacuity,consider a formulaϕover a set AP of atomic propositions.LetΣbe the set of Boolean functions over AP,and let e be a regular expression overΣappearing inϕ.The regular expression e induces a language–a set offinite words overΣ.For a word w∈Σω,the regular expression e induces a set of intervals[3]:these intervals define subwords of w that are members in the language of e.By saying that e does not affectϕin M,we want to capture the fact that we could modify e,replace it with any other regular expression,and still M satis-fiesϕ.As has been the case with propositional vacuity,there is no known algorithmic approach to handle such syntactic modifications in the presence of regular expressions of mixed polarity.Accordingly,as in[2],we follow a semantic approach to modifi-cations of e,where“does not affect”is captured by means of universal quantification. Thus,in RELTL vacuity there are two types of elements we need to universally quantify to check vacuity.First,as in LTL,in order to check whether an RELTL subformulaψ, which is not a regular expression,affects the satisfaction ofϕ,we quantify universally over a proposition that replacesψ.In addition,checking whether a regular expression e that appears inϕaffects its satisfaction,we need to quantify universally over inter-vals.Thus,while LTL vacuity involved only monadic quantification(over the sets of points in which a subformula may hold),regular vacuity involves dyadic quantification (over intervals–sets of pairs of points,in which a regular expression may hold).In Section3.2,we discuss two weaker alternative definitions:a restriction of the univer-sally quantified inter
vals to intervals of the same duration as e,and an approximation of the dyadic quantification over intervals by monadic quantification over the Boolean events referred to in the regular expressions.As discussed there,the definition in terms of dyadic quantification is the most general one.
The transition from monadic to dyadic quantification is very challenging.Indeed, while monadic second-order logics are often decidable[7,23],this is not the case for dyadic second-order logics.For example,while monadic second-order theory of one successor is decidable[7],this is not the case for the dyadic theory[6].The main result of this work is that regular vacuity is decidable.We show that the automata-theoretic approach to LTL[27]can be extended to handle dyadic universal quantification.Unlike monadic universal quantification,which can be handled with no increase in computa-tional complexity[2],the extension to dyadic quantification involves an exponential blow-up(in addition to the standard exponential blow-up of handling LTL[25]),result-ing in an EXPSPACE upper bound,which should be contrasted with a PSPACE upper bound for RELTL model checking.Our NEXPTIME-hardness lower bound,while leav-ing a small gap with respect to the upper bound,shows that an exponential overhead on top of the complexity of RELTL model checking seems inevitable.The above results suggest that,in practice,one may need to restrict attention to specifications in which regular expressions are of pure polarity.We show that under this assumption,the tech-niques of[19]can
be extended to regular vacuity,which can then be reduced to standard model checking.In addition,for specifications of mixed polarity,the two weaker defi-nitions we suggest for regular vacuity can also be checked in PSPACE–like standard RELTL model checking.
2RELTL
The linear temporal logic RELTL extends LTL with a regular layer.We consider LTL in a positive normal form,where formulas are constructed from atomic propositions and their negations by means of Boolean(∧and∨)and temporal(next,until,and its dual release)connectives.For details,see[21].Let AP be afinite set of atomic propositions,and let B denote the set of all Boolean functions b:2AP→{false,true} (in practice,members of B are expressed by Boolean expressions over AP).Consider an infinite wordπ=π0,π1,...∈(2AP)ω.For integers j≥i≥0,and a language L⊆B∗,we say thatπi,...,πj−1tightly satisfies L,denotedπ,i,j|≡L,if there is a word b0·b1···b j−1−i∈L such that for all0≤k<j−i,we have that b k(πi+k)=true. Note that when i=j,the intervalπi,...,πj−1is empty,in which caseπ,i,j|≡L iff ∈L.
The logic RELTL contains two regular modalities:(e seqϕ)and(e triggersϕ), where e is a regular expression over the alphabet B,andϕis an RELTL formula.In-tuitively,(e seqϕ)asserts that some interval satisfying e is followed by a suffix sat-isfyingϕ,whereas(e triggersϕ)asserts that all intervals satisfying e
are followed by a suffix satisfyingϕ.Note that the seq and triggers connectives are essentially the “diamond”and“box”modalities of PDL[11].Formally,letπbe an infinite word over 2AP then,2
–π,i|=(e seqϕ)if for some j≥i,we haveπ,i,j|≡L(e)andπ,j|=ϕ.
–π,i|=(e triggersϕ)if for all j≥i such thatπ,i,j|≡L(e),we haveπ,j|=ϕ.
In the automata-theoretic approach to model checking,we translate temporal logic for-mulas to automata[27].A nondeterministic generalized B¨u chi word automaton(NGBW, for short)is a tuple A= Σ,S,δ,S0,F ,whereΣis afinite alphabet,S is afinite set of states,δ:S×Σ→2S is a transition function,S0⊆S is a set of initial states,and F⊆2S is a set of sets of accepting states.A runρof A is an infinite sequence of states in S that starts in a state in S0and obeysδ.Let inf(ρ)⊆S denote the set of states that are visited infinitely often inρ.Since the run is infinite and S isfinite,it must be that inf(ρ)is not empty.An NGBW A accepts an infinite wordπif it has an infinite run ρoverπsuch that for every F∈F,we have inf(ρ)∩F=∅.The full definition of NGBW is given in the full version.We now describe a translation of RELTL formulas to NGBW.The translation can be viewed as a special case of the translation of ETL to NGBW[27](see also[17]),but we need it as a preparation for our handling of regular vacuity.
Theorem1.Given an RELTL formulaϕover AP,we can construct an NGBW Aϕover the alphabet2AP suc
h that L(Aϕ)={π|π,0|=ϕ}and the size of Aϕis exponential inϕ.
Proof:The translation ofϕgoes via an intermediate formulaψin the temporal logic ALTL.The syntax of ALTL is identical to the one of RELTL,only that regular expres-sions over B are replaced by nondeterministicfinite word automata(NFW,for short) over2AP.The adjustment of the semantics is as expected:letπ=π0,π1,...be an infinite path over2AP.For integers i and j with0≤i≤j,and an NFW Z with al-phabet2AP,we say thatπi,...,πj−1tightly satisfies L(Z),denotedπ,i,j,|≡L(Z),if πi,...,πj−1∈L(Z).Then,the semantics of the seq and triggers modalities are as in RELTL,with L(Z)replacing L(e).
A regular expression e over the alphabet
B can be linearly translated to an equiv-alent NFW Z e with a single initial state[18].To complete the translation to ALTL, we need to adjust the constructed NFW to the alphabet2AP.Given the NFW Z e= B,Q,∆,q0,W ,let Z e= 2AP,Q,∆ ,q0,W ,where for every q,q ∈Q,and a∈2AP,we have that q ∈∆ (q,a)iff there exists b∈B such that q ∈∆(q,b)and b(a)=true.It is easy to see that for allπ,i,and j,we have thatπ,i,j|≡L(e)iff π,i,j|≡L(Z e).Letψbe the ALTL formula obtained fromϕby replacing every regular expression e inϕby the NFW Z e.It follows that for every infinite wordπand i≥0, we have thatπ,i|=ϕiffπ,i|=ψ.
It is left to show that ALTL formulas can be translated to NGBW.Letψbe an ALTL formula.For a state q∈Q of an NFW Z,we use Z q to denote Z with initial state q. Using this notation,ALTL formulas of the form(Z e seqϕ)and(Z e triggersϕ)now become(Z e q0seqϕ)and(Z e q0triggersϕ).The closure ofψ,denoted cl(ψ),is the set{ξ|ξis a subformula ofψ}∪{(Z q seqξ)|(Z q seqξ)is a subformula ofψand q is a state of Z q}∪{(Z q triggersξ)|(Z q triggersξ)is a subformula ofψand q is a state of Z q}.Let seq(ψ)denote the set of seq formulas in cl(ψ).A subset C⊆cl(ψ) is consistent if the following hold:(1)if p∈C,then¬p∈C,(2)ifϕ1∧ϕ2∈C,then ϕ1∈C andϕ2∈C,and(3)ifϕ1∨ϕ2∈C,thenϕ1∈C orϕ2∈C.
Givenψ,we define the NGBW Aψ= 2AP,S,δ,S0,F ,where S⊆2cl(ψ)×2seq(ψ)is the set of all pairs(L s,P s)such that L s is consistent,and P s⊆L s∩seq(ψ). Intuitively,when Aψreads the point i ofπand is in state(L s,P s),it guesses that the suffixπi,πi+1,...ofπsatisfies all the formulas in L s.In addition,as explained below, the set P s keeps track of the seq formulas in L s whose eventuality needs to be fulfilled. Accordingly,S0={(L s,∅)∈S:ψ∈L s}.
Before we describe the transition functionδ,let us explain how subformulas of the form(Z q seqψ)and(Z q triggersψ)are handled.In both subformulas,something should happen after an interval that tightly satisfies Z q is read.In order to“know”when an intervalπi,πi+1,...πj−1tightly satisfies Z q,the NGBW Aψsimulates a run of Z q on it.The seq operator requires a single interval that tightly satisfies Z q and i
s followed by a suffix satisfyingψ.Accordingly,Aψsimulates a single run,which it chooses nondeterministically.For the triggers operator,the requirement is for every interval that tightly satisfies Z q.Accordingly,here Aψsimulates all possible runs of Z q.Formally,δ:(S×2AP)→2S is defined as follows:(L t,P t)∈δ((L s,P s),a)iff the following conditions are satisfied:
–For all p∈AP,if p∈L s then p∈a,and if¬p∈L s then p∈a.
–If(nextϕ1)∈L s,thenϕ1∈L t.
–If(ϕ1untilϕ2)∈L s,then eitherϕ2∈L s,orϕ1∈L s and(ϕ1untilϕ2)∈L t.
版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。
发表评论