排序公式A Lattice-Theoretic Characterization of Safety and
Liveness
Panagiotis Manolios Georgia Institute of T echnology College of Computing,CERCS Lab
801Atlantic Drive
Atlanta,Georgia,30332,USA www.gatech.edu/∼manolios manolios@cc.gatech.edu
Richard Trefler
University of Waterloo
School of Computer Science
200University Avenue West Waterloo,Ontario,N2L3G1,Canada .uwaterloo.ca/∼trefler
trefler@cs.uwaterloo.ca
ABSTRACT
The distinction between safety and liveness properties is due to Lamport who gave the following informal characteriza-tion.Safety properties asrt that nothing bad ever happens while liveness properties asrt that something good hap-pens eventually.In a well-known paper Alpern and Schnei-der gave a topological characterization of safety and liveness for the linear time framework.Gumm has stated the no-tions in the more abstract tting of∨-complete Boolean algebras.Recently,we characterized safety and liveness for the branching time framework and found that neither the topological characterization nor Gumm’s characterization were general enough for our needs.We prent a lattice-theoretic characterization that allows us to unify previous results on safety and liveness,including the results for the linear time and branching time frameworks and forω-regular string and tree languages.
Categories and Subject Descriptors
F.3.1[Logics and Meanings of Programs]:Specifying and Verifying and Reasoning about Programs
1.INTRODUCTION
Reactive systems are non-terminating systems engaged in ongoing interaction with an environment[9];examples in-clude network protocols,operating systems,on-board con-trollers,cache
coherence protocols,distributed databas, etc.In a minal paper,Lamport grouped linear time prop-erties of reactive systems into three categories:safety prop-erties,liveness properties,and properties that are neither[13]. Informally,safety properties asrt that nothing bad ever happens,whereas liveness properties asrt that something good happens eventually.
Understanding the distinction between safety and liveness Permission to make digital or hard copies of all or part of this work for personal or classroom u is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on thefirst page.To copy otherwi,to republish,to post on rvers or to redistribute to lists,requires prior specific permission and/or a fee.
PODC2003,July13-16,2003,Boston,Massachutts,USA.
Copyright2003ACM X-XXXXX-XX-X/$5.00.—which now appears in introductory textbooks on distributed computing—has been an ongoing rearch endeavor that has yielded numerous results,some of which we now recount. Alpern and Schneider gave a formal mantic characteri-zation of safety and liveness in the linear time framework, where properties and the mantics of programs are ts of infinite strings[3].They gave a topological characteri-zation where safety proper
ties are clod ts and liveness properties are den ts and they proved that every linear time property can be expresd as the conjunction of a live-ness property and a safety property.In a subquent paper they showed that given a B¨u chi automaton,B,over infinite strings(which recognizes anω-regular language),it is possi-ble to decompo B into automata B S and B L such that the t of strings accepted by B S is a safety property,the t of strings accepted by B L is a liveness property,and the t of strings accepted by B is equal to the interction of the t of strings accepted by B S and B L[4].
Sistla characterized safety and liveness for temporal logic formulas[21],an important problem due to the wide u of temporal logic(which was propod for specifying and verifying reactive systems by Pnueli[17]).
Recently,we have extended the Alpern and Schneider lin-ear time characterization of safety and liveness properties to branching time,where properties and the mantics of programs are ts of infinite trees[14].The branching time framework includes process algebra[15]and temporal log-ics such as CTL[5](which is ud by many model checkers and is of great practical importance),CTL∗[7],and the µ-calculus[11].We showed that any branching time prop-erty can be decompod into the conjunction of a safety and liveness property.In the ca where a t of trees is
given implicitly as a Rabin tree automaton,B,we showed that it is possible to compute the Rabin automata corresponding to the closures of the language of B.This allows us to ef-fectively compute B S and B L such that the language of B S is safe,the language of B L is live,and the language of B is the interction of the languages of B S and B L.
The distinction between safety and liveness plays an impor-tant role in the design and analysis of reactive systems,as the proof methods employed to check safety properties differ
from tho ud to check liveness properties.For example, proofs of liveness properties frequently require the construc-tion of well-founded relations—to show that the desired be-havior cannot be avoided forever—while safety properties are usually proved by induction on the transition relation—to show that the prohibited behavior is never exhibited[16]. In addition,automatic proof techniques available for safety properties often do not work with liveness properties.For example,in some infinite state systems one can automati-cally determine if a safety property can be violated,whereas the existence of a fair computation cannot be so determined [2].In the context of model checking[5,18],Kupferman and Vardi show that proving safety properties is simpler than es-tablishing general temporal logic properties[12].
The distinction between safety and liveness also has con-quences for curity properties,as Schneider argues that en-forceable curity properties correspond to safety properties and that curity automata,which can be ud to enforce curity policies,correspond to B¨u chi automata that accept safe languages[20].
冬红果海棠
A lattice theoretic characterization of safety and liveness was given by Gumm[8].Gumm shows that given a∨-prerving map between complete Boolean algebras,one can derive the Alpern and Schneider theorem characterizing safety and liveness.This generalization was not motivated by any prac-tical problem;in a survey of safety and liveness Kindler[10] says of Gumm’s work“it remains an open question whether ...his characterization has practical relevance”. However,there is a practical conquence,which we discov-ered when we defined safety and liveness for branching time logics.In the branching time framework,our mantic char-acterization does not give ri to a topology,but it doesfit in Gumm’s framework.
But,there is a problem with Gumm’s framework.If we consider the lattice of B¨u chi automata definable languages, where meet corresponds to interction,join to union,and complementation to negation,then we have a Boolean al-gebra that is not∨-complete,so it does notfit in Gumm’s framework.Similarly,the lattice of Rabin tree automata de-finable languages forms a Boolean algebra
that also does not satisfy Gumm’s conditions.Therefore,we cannot appeal to the Alpern and Schneider theorem or any of its variants to establish that anω-regular language(over strings or trees) can be expresd as the interction of a safe and live lan-guage.
In this paper we prent a simpler and more general charac-terization of safety and liveness.As a conquence,we fur-ther clarify the distinction between safety and liveness and provide more powerful tools for analyzing the concepts.
1.Our results allow us to simplify previous proofs.For
example,the characterization of safety and liveness for B¨u chi automata and the decomposition theorem,the main results in[4],now follow directly from the results in this paper.Similarly,many of our proofs on safety and liveness in the branching time logic and for Rabin tree automata now follow directly from the results in this paper[14].
胜任的英语2.We carefully analyze the conditions required to prove
the decomposition theorem for safety and liveness.We discuss why each of the conditions in our proofs is required,often by providing counterexamples.Such considerations led us to a lattice-theoretic approach, where the basic results are stated in terms of modular, complemented lattices.
3.Our lattice-theoretic framework is more general,there-
fore simpler than topological ,we do not require closure operators to distribute over joins (unions),thus,not only are our results applicable in more contexts,but they are easier to apply,as one needs to establish fewer properties than were previ-ously required.气度非凡造句
In the next ction,we review the Alpern and Schneider characterization of safety and liveness for the linear time framework and we consider examples due to Rem[19].In Section3we give our lattice-theoretic characterization and show how it applies to the linear time ca.In Section4we give our branching time characterization and relate it to the lattice-theoretic view.Conclusions are given in Section5.
2.LINEAR TIME FRAMEWORK
2.1Preliminaries
andωboth denote the natural numbers.Function ap-plication is sometimes denoted by an infix dot“.”and is left associative.P(S)denotes the powert of S.Dom.f denotes the domain of function f.S∗denotes the t of finite quences over S;Sωdenotes the t of infinite -quences(functions fro
mω)over S;S∞=S∗∪Sω.Suppo s,t∈S∞,|s|denotes the length of s;s is a prefix of t(s t) iffDom.s⊆Dom.t and for all i∈Dom.s,s.i=t.i;s is a proper prefix of t(s≺t)iffs t and s=t.
Qx:r:b denotes a quantified expression,where Q is the quantifier,x the bound variable,r the range of x(true if omitted),and b the body.We sometimes write Qx∈X: r:b as an abbreviation for Qx:x∈X∧r:b ,where r is true if omitted,as before.From highest to lowest binding power,we have:parenthes,function application,binary ,sBw),equality(=)and membership(∈), negation(¬),conjunction(∧)and disjunction(∨),impli-cation(⇒),andfinally,binary equivalence(≡).Spacing is ud to reinforce binding:more space indicates lower bind-ing.
We u a proof format that we exhibit with an example. Suppo that is a preorder,then a proof A Z is given in the following form.
Proof
A
{Hint why A B}
B
...
Z
Thefirst three lines establish that A B,as per the hint. Lines three throughfive establish that B is related to the expression on linefive of the proof by (or any restriction of ,usually=),and so on.Chaining the steps together, we conclude that A Z.
Throughout this paperΣdenotes afixed alphabet,a non-empty t of symbols.
We assume familiarity with the Linear Temporal Logic(LTL) operators X(next-time,sometimes written ),F(eventu-ally,sometimes written3),G(always,sometimes written 2)and the CTL and CTL∗operators A(along all paths), and E(there exists a path).A good reference is[6].
2.2Safety and Liveness
We review the main results of the Alpern and Schneider characterization for the linear time framework[3].Our pre-ntation differs from the ,we u a closure operator,but the results are the same.The linear time clo-sure operator over strings,lcl:P(Σω)→P(Σω),can be defined as follows.
lcl.T={t∈Σω| ∀x:x≺t: ∃t ∈T::x t }
We say that cl:P(X)→P(X)is a topological-closure op-erator on X if it satisfies the following four properties.
1.cl.∅=∅
2.A⊆cl.A
3.cl(cl.A)=cl.A
4.cl(A∪B)=cl.A∪cl.B
From a basic result of topology,a topological-closure oper-ator on X defines a topology,where a t A⊆X is clod iffcl.A=A.
It turns out that lcl is a topological-closure operator onΣω. Safety properties are defined to be the clod ts and live-ness properties are defined to be the den ts.It then follows from topological considerations that any property P is the interction of lcl.P,a safety property,and P∪¬lcl.P, a liveness property.
Lemma1P∪¬lcl.P is a liveness property.
Proof高中能入党吗
lcl(P∪¬lcl.P)
={lcl distributes over∪}
lcl.P∪lcl(¬lcl.P)
⊇{lcl.A⊇A,Set theory}
lcl.P∪¬lcl.P
={Set theory}
Σω Theorem1Any property can be decompod into the in-terction of a safety and liveness property.
Proof
lcl.P∩(P∪¬lcl.P)
={Set theory}
(lcl.P∩P)∪(lcl.P∩¬lcl.P)
={A⊆lcl.A,Set theory}
P∪∅
={Set theory}
P
2.3Examples
We now take a moment to consider some examples due to Martin Rem[19].In the examples t is an infinite quence overΣ.
p0:fal(corresponds to∅)
p1:thefirst symbol of t is a
p2:thefirst symbol of t differs from a
成本会计实训报告
p3:thefirst symbol of t is a
and t contains a symbol that differs from a
p4:the number of a’s in t isfinite
p5:the number of a’s in t is infinite
p6:true(corresponds toΣω)
Below,we give our translation of the above properties to LTL.Recall that F means eventually(and is sometimes writ-ten3)and G means always(and is sometimes written2). p0:fal
p1:a
p2:¬a
p3:a∧F¬a
p4:FG¬a
p5:GF a
p6:true
Note that p0,p1,p2,and p6are safety properties.The closure of p3is p1,so p3is neither a safety property nor a liveness property.The closures of p4and p5are bothΣω; thus,they are liveness properties,but they are not safety properties.
2.4B¨uchi Automata
In this ction,we review the results in[4].A B¨u chi au-tomaton B is a5-tuple(Σ,Q,q0,δ,F)whereΣis afinite alphabet,Q is afinite t of states,q0∈Q is the start state,δ:Q×Σ→P(Q)is the transition relation,and F is a t of accepting states.
Let t∈Σω.A run of B on t is a Q-labeled quenceσsuch thatσ.0=q0and for all i∈ω,σ(i+1)∈δ(σ.i,t.i).Runσis accepting iffsome state of F occurs infinitely often inσ. L(B)={t∈Σω|there is an accepting run of B on t}is the language of B.
It is possible to decompo B into automata B S and B L such that the t of strings accepted by B S is a safety property
and the t of strings accepted by B L is a liveness property [4].Furthermore,the t of strings accept
ed by B is equal to the interction of the t of strings accepted by B S and B L, as before.The idea is to define a closure operator on B¨u chi automata.The operatorfirst removes states that cannot reach an accepting state and then makes every remaining state an accepting state.In this way,the fairness condition is made trivial.It can then be shown that applying this operator to B results in an automaton who language is the lcl of the language of B.Since B¨u chi automata are clod under complementation and union,the liveness automaton is the union of B with the negation of the closure of B,as in Theorem1.
3.LATTICE THEORETIC CHARACTERI-
ZATION
Recall that a lattice L,≤ consists of a t L and a partial order≤on L such that any pair of elements has a meet (∧)and join(∨).From a more algebraic,but equivalent, viewpoint,a lattice is a triple L,∧,∨ where∧and∨satisfy the associative,commutative,idempotency,and absorption laws.句子英文
(associative law)(a∨b)∨c=a∨(b∨c)
(commutative law)a∨b=b∨a
(idempotency law)a∨a=a
(absorption law)a∨(a∧b)=a
Each law also has a dual,which is obtained by interchanging ∨and∧.We can then define a≤b≡(a∧b)=a and it follows that a≤b≡(a∨b)=b.We will stick to the algebraic view.Note that in light of associativity and commutativity,we do not need parenthes for quences of joins or meets.
Lemma2
1.a≤b⇒a∨c≤b∨c
2.a≤b⇒a∧c≤b∧c
Proof
a∨c
≤{Absorption(x≤x∨y),Associativity,Commutativity} a∨c∨b
={a≤b,hence a∨b=b}
b∨c
The proof of(2)is similar.
A lattice-closure on L is a function cl:L→L such that the following hold.
1.a≤cl.a
2.cl.a=cl(cl.a)
3.a≤b⇒cl.a≤cl.b Lemma3cl(a∨b)≥cl.a∨cl.b.
Proof
cl(a∨b)
={x∨x=x}
cl(a∨b)∨cl(a∨b)
≥{a∨b≥a,monotonicity of cl,Lemma2}
cl.a∨cl.b
A lattice has a unit element,1,if a∧1=a for all a∈L.
A lattice has a zero element,0,if a∨0=a for all a∈L. Suppo we have a lattice with a0and a1,then b is a complement of a iffb∧a=0and b∨a=1.Note that b need not be unique.The t of complements of a is denoted cmp.a.A complemented lattice is one in which every element has a complement.
A lattice is modular if a≥c⇒a∧(b∨c)=(a∧b)∨(a∧c).
For the remainder of this ction,unless we say otherwi,we assume that we are working with L,∧,∨,0,1 ,a modular complemented lattice.Notice that a Boolean algebra is a special ca of a modular complemented lattice.
A cl-safety element is one where a=cl.a.Note that cl.a is a safety element(as cl.a=cl(cl.a)).
A cl-liveness element is one where cl.a=1.
Lemma4If b∈cmp(cl.a)then a∨b is a cl-liveness ele-ment.
Proof
cl(a∨b)
≥{Lemma3}
cl.a∨cl.b
≥{cl.x≥x}
cl.a∨b
={b∈cmp(cl.a)}
1
Theorem2If cl is a lattice closures,then every element in L is the meet of a cl-safety and cl-liveness element. Proof By Theorem3where cl2,cl1=cl.
Theorem2is a simple corollary of Theorem3,which will be uful when we consider branching time,and is prented next.The significance of Theorem2is that it can be ud to obtain the Alpern Schneider results.To e why,note that P(Σω),∩,∪,∅,Σω,¬ is a Boolean algebra and lcl is a lattice-clo
sure operator.Similarly the t of languages defin-able by B¨u chi automata is clod under union,interction,
1
c
奶酪豆腐b
Figure1:Why we need modularity in Theorem3. The above Has diagram depicts a lattice.Circles denote elements and x≤y if there is an upward path from x to y.The lattice depicted is not modular: b≥a but b∧(c∨a)is b whereas(b∧c)∨(b∧a)is a. Consider the closure cl,where cl.a=b and cl is the identity otherwi.Element a cannot be expresd as the conjunction of a cl-safety element and a cl-liveness element,as per Lemma6.
and complementation so it too defines a Boolean algebra and we have shown that the closure opera
tor on B¨u chi automata corresponds to lcl,so it too is a lattice-closure operator.Re-call,that neither the original Alpern and Schneider topolog-ical characterization nor Gumm’s characterization applies to the B¨u chi automata ca.In fact,the main results of the paper by Alpern and Schneider on safety and liveness for B¨u chi automata follow directly from our results and basic closure properties of B¨u chi automata.
Theorem3Suppo cl1and cl2are lattice closures such that for all x∈L,cl1.x≤Then any element in L is the meet of a cl1-safety and a cl2-liveness element.
Proof Suppo a∈L and b∈cmp(cl2.a).
cl1.a∧(a∨b)
={cl1.a≥a,Modularity}
(cl1.a∧a)∨(cl1.a∧b)
={a≤cl1.a}
a∨(cl1.a∧b)
={Lemma5(a,b,c←cl1.a,cl2.a,b)and x∨0=x} a
Lemma5c∈cmp.b∧a≤b⇒a∧c=0
Proof
a∧c
≤{a≤b,Lemma2}
b∧c
={c∈cmp.b}
We end this ction by showing why modularity is needed. Consider the Has diagram in Figure1.It corresponds to a lattice—where circles denote elements of the lattice and x≤y if there is an upward path from x to y—that is not modular.Consider the closure cl,where cl.a=b and cl is the identity otherwi.
Lemma6Element a of the(non-modular)lattice depicted in Figure1cannot be expresd as the conjun
ction of a cl-safety element and a cl-liveness element,where cl.a=b and cl is the identity otherwi.
Proof The only liveness element is1,but since x∧1=x, x∧1=a iffx=a and a is not a safety element.
4.BRANCHING TIME FRAMEWORK
4.1Preliminaries
For a relation R,we write R|S for R left-restricted to the t ,R|S={ a,b |( a,b ∈R)∧(a∈S)}.[i..j] denotes the t{k∈|i≤k≤j}.A t U⊆S∞is prefix-clod ifffor all u∈U and for all t u,t∈U.
An unlabeled tree is a prefix-clod subt of∗.A tree w is a pair W,w where W is an unlabeled tree and w:W→Σ.
A tree W,w is total if W=∅and for allσ∈W,there exists ρ∈W such thatσ≺ρ.A tree W,w isfinite-depth if there exists n∈such that for allσ∈W,|σ|≤n.By A tot,A nt, and A f we denote the t of total,non-total,andfinite-depth trees,respectively.The t of trees is denoted by A all;note A all=A tot∪A nt and A f⊂A nt.Let t= W,w be a tree.
A p⊆W is a path in t iffp is a totally ordered(by ),prefix-clod subt of W.Given a tree W,w and a no
deσ∈W we define the pathσ={σ ∈W|σ σ}.We extend w to paths:given path p=p0p1···,w(p)=(w.p0)(w.p1)···. We now define what it means to concatenate trees and u this notion to define what it means for one tree to be a prefix of another.The closure,safety elements,and liveness elements can then be defined as in the linear time ca. 4.2Safety and Liveness
Given trees w and x,we define a preliminary notion of tree concatenation,denoted w·x.
Definition1Let w= W,w and x= X,x be trees. w·x= W∪X,w∪(x|X\W) .
Note that w·x is a tree.The above notion of concatenation is not what we need.The problem is that it allows one to extend w at non-leaf nodes.To remedy this,we define an appropriate notion of concatenation after we define the notion of a leaf.
Definition2Let w= W,w be a tree.leaf(z,w)≡z∈W∧¬ ∃y∈W::z≺y .
Given trees w and x,we define the notion of tree concate-nation,denoted wx,as follows.
Definition3Let w= W,w and x= X,x be trees.Let X ={y∈X|y∈W∨ ∃z:leaf(z,w):z≺y }.Let x = X ,x|X .wx=w·x .
Clearly,wx is a tree;the proof amounts to showing that x is a tree.We now define when one tree is a prefix of another. Definition4x y≡ ∃z::xz=y
In[14],we show that is a partial order and that if x y then for all w,wx wy.P(A tot)is the t of branching time properties.Note that P(A tot),A tot,∅,∪,∩,¬ and P(A all),A all,∅,∪,∩,¬ are Boolean algebras.We define two closure operators on P(A tot),the non-total andfinite-depth closures,as follows.
Definition5ncl.p={y∈A tot| ∀x∈A nt:x y: ∃z∈p::x z }
Definition6fcl.p={y∈A tot| ∀x∈A f:x y: ∃z∈p::x z }
The proofs that ncl,fcl are lattice-closures and that ncl.p⊆fcl.p follow directly from results in[14].
Since we have two types of closures,we have two types of safety properties:existentially safe(ES)and universally safe (US).The intuition is that the existentially safe properties guarantee at least one computation along which nothing bad happens.The universally safe properties guarantee that nothing bad happens during any computation.
Definition7(Existentially Safe)p∈ES≡p=ncl.p
Definition8(Universally Safe)p∈US≡p=fcl.p
It turns out that fcl defines a topology,as fcl.p∪fcl.q= fcl.(p∪q).However,ncl.(p∪q)⊆ncl.p∪ncl.q is not a theorem,thus ncl does not define a topology.
Definition9(Existentially Live)p∈EL≡ncl.p=A tot Definition10(Universally Live)p∈UL≡fcl.p=A tot Theorem4Every branching time property is the interc-tion of:
1.An existentially safe and an existentially live property;
2.A universally safe and a universally live property;and
3.An existentially safe and a universally live property.
Proof By Theorem3.
The above theorem shows that three of the four obvious ways of decomposing a property into the meet of a safety and liveness property hold.What about the fourth?The following theorem allows us to show that it does not hold. Theorem5Suppo cl1and cl2are closure operators such that cl2.a=1and cl1.a<1.Then there do not exist s,l such that cl2.s=s,cl1.l=1and a=s∧l.Proof Suppo cl2.s=s,cl1.l=1,and a=s∧l.Then: a=s∧l
⇒{Def.of≤}
a≤s
⇒{cl2is a lattice-closure}
cl2.a≤cl2.s
⇒{cl2.a=1}
cl2.s=1
⇒{s=cl2.s}
s=1
⇒{a=s∧l}
a=l
⇒{cl1.l=1}
cl1.a=1
⇒{cl1.a<1}
fal
Since the t of trees satisfying the CTL formula AF p(along all paths,eventually p)satisfies the preconditions on the previous theorem,we have shown that not every property can be expresd as the interction of a universally safe and an existentially live property.
Our decomposition of a property into a safety property and
a liveness property is extreme in the following n.(See
[19]for a linear-time version of the extremal theorems.) Theorem6Suppo cl1and cl2are lattice closures such that for all x∈L,cl1.x≤If s=cl1.s or s=cl2.s and a=s∧z,then cl1.a≤s.
Proof
a=s∧z
⇒{Def.of≤}
a≤s
⇒{cl1is a lattice closure}
cl1.a≤cl1.s
⇒{cl1.s≤cl2.s,s=cl1.s or s=cl2.s}
cl1.a≤s
Note that tting cl1=cl2gives us a version of the theorem applicable to cas where there is only one lattice closure ,in the linear time ca,we t cl1=cl2=lcl. Theorem6says that any decomposition of a into a cl1-safety or cl2-safety element and some other element(not necessarily a liveness element)requires that the safety ele-ment be ,above or≥)than cl1.a.Thus,cl1.a
