Tractable Temporal Reasoning∗Clare Dixon,Michael Fisher and Boris Konev Department of Computer Science,University of Liverpool,
Liverpool L693BX,UK
{clare,michael,konev}@csc.liv.ac.uk
Abstract
Temporal reasoning is widely used within both
Computer Science and A.I.However,the underly-
ing complexity of temporal proof in discrete tempo-
ral logics has led to the use of simplified formalisms
and techniques,such as temporal interval algebras
or model checking.In this paper we show that
tractable sub-classes of propositional linear tem-
poral logic can be developed,based on the use of
XOR fragments of the logic.We not only show
that such fragments can be decided,tractably,via
clausal temporal resolution,but also show the ben-
efits of combining multiple XOR fragments.For
such combinations we establish completeness and
complexity(of the resolution method),and also
describe how such a temporal language might be
used in application areas,for example the verifica-
tion of multi-agent systems.This new approach to
temporal reasoning provides a framework in which
tractable temporal logics can be engineered by in-
telligently combining appropriate XOR fragments.
1Introduction
Temporal logics have been used to describe a wide variety of systems,from both Computer Science and Artificial Intelli-gence.The basic idea of proof,within propositional,discrete temporal logics,is also both intuitive and appealing.How-ever the complexity of satisfiability for such logics is high. For example,the complexity of satisfiability for propositional linear time temporal logic(PTL)is PSPACE-complete[Sistla and Clarke,1985].Consequently,model checking[Clarke et al.,1999]has received much attention as it also allows users to check that a temporal property holds for some underlying model of the system.
Often temporal problems involve an underlying structure, such as an automaton,where a key property is that the au-tomaton can be in exactly one state at each moment.Such problems frequently involve several process or agents,each with underlying automaton-like structures,and we are inter-ested in properties relating to how the agents progress under ∗The work of the first and last authors was partially supported by EPRSC grant number GR/S63182/01“Dynamic Ontologies:a Framework for Ser
vice Descriptions”.particular models of concurrency such as synchrony,asyn-chrony etc.,or particular coordination or cooperation actions.
In this paper we consider a new fragment of PTL that incor-porates the use of XOR operators,denoted(q1⊕q2⊕...⊕q n) meaning that exactly one q i holds for1≤i≤n.Since
the complexity of unsatisfiability for XOR clauses in classi-cal propositional logic is low[Schaefer,1978],there is the potential to carry much of this over to the temporal case. Thus,in this paper we provide several results.First,we in-troduce the PTL fragment to be considered,called TLX,and show a complete clausal resolution system for this.The frag-ment allows us to split the underlying set of propositions into distinct subsets such that each subset(except one)represents a set of propositions where exactly one proposition can hold (termed XOR sets);the remaining set has no such constraints. Then we show that deciding unsatisfiability of specifications in such a logic is,indeed,tractable.
2XOR Temporal Logic
The logic we consider is called“TLX”,and its syntax and se-mantics essentially follow that of PTL[Gabbay et al.,1980], with models(isomorphic to the Natural Numbers,N)of the form:σ=t0,t1,t2,t3,...
where each state,t i,is a set of proposition symbols,representing those propositions which are satisfied in the i th moment in time.The notation(σ,i)|= A denotes the truth(or otherwise)of formula A in the model σat state index i∈N.This leads to semantic rules: (σ,i)|=g A iff(σ,i+1)|=A
(σ,i)|=♦A iff∃k∈N.(k i)and(σ,k)|=A (σ,i)|=A iff∀j∈N.if(j i)then(σ,j)|=A For any formula A,modelσ,and state index i∈N,then either(σ,i)|=A holds or(σ,i)|=A does not hold,denoted by(σ,i)|=A.If there is someσsuch that(σ,0)|=A,then A is said to be satisfiable.If(σ,0)|=A for all models,σ, then A is said to be valid and is written|=A.
The main novelty in TLX is that it is parameterised by XOR-sets P1,P2,...,and the formulae of TLX(P1,P2,...) are constructed under the restrictions that exactly one propo-sition from every set P i is true in every state.For example,if we consider just one set of propositions P,we have
(p1⊕p2⊕...⊕p n)for all p i∈P. Furthermore,we assume that there exists a set of proposi-tions in addition to those defined by the parameters,and that
these propositions are unconstrained as normal.Thus,TLX()is essentially a standard propositional,linear temporal logic,while TLX(P ,Q ,R )is a temporal logic containing at least the propositions P ∪Q ∪R ,where P ={p 1,p 2,...,p l },Q ={q 1,q 2,...,q m },and R ={r 1,r 2,...,r n }where P ,
Q and R are disjoint,but also satisfying
[(p 1⊕p 2⊕...⊕p l )∧(q 1⊕q 2⊕...⊕q m )∧(r 1⊕r 2⊕...⊕r n )]
2.1Normal Form
Assume we have n sets of XOR propositions P 1=
{p 11,...p 1N 1},...,P n ={p n 1,...p nN n }and a set of ad-ditional propositions A ={a 1,...a N a }.In the following:
•∧
P −ij denotes a conjunction of negated XOR propositions from the set P i ;
•∨P +ij denotes a disjunction of (positive)XOR proposi-tions from the set P i ;
•∧
A i denotes a conjunction of non-XOR literals;•∨
A i denotes a disjunction of non-XOR literals.
A normal form for TLX is of the form
i C i where each C i is an initial ,step or sometime clause (respectively)as fol-lows:
start ⇒∨P +1i ∨...∨∨P +
ni ∨∨
A i ∧
P −1j ∧...∧
P −nj
∧∧A j ⇒g (∨P +1j ∨...∨∨P +
nj
∨∨
A j )true ⇒♦(∨P +1k ∨...∨∨P +
nk ∨∨A k ).
Note that due to the semantics of the XOR clauses,if i =k p ji ∧p jk ≡false ¬p ji ∨¬p jk ≡true and
N j  i =1¬p ji ≡false N j  i =1p ji ≡true .Also p ji ≡ p jk ∈P j ,k =i
¬p jk ¬p ji ≡
p jk ∈P j ,k =i
p jk
allow us to maintain positive XOR propositions on the right hand sides of clauses and negated XOR propositions on the left hand side of clauses.
2.2Resolution Rules
We decide the validity of formulae in TLX using a form of clausal temporal resolution [Fisher et al.,2001].The reso-lution rules are split into three types:initial resolution ,step resolution and temporal resolution .These are presented in Fig.1.Initial resolution resolves constraints holding in the initial mom
ent in time.Step resolution involves resolving two step clauses or deriving additional constraints when a contra-diction in the next moment is derived.Temporal resolution resolves a sometime clause with a constraint that ensures that the right hand side of this clause cannot occur.
In the conclusion of these resolution rules com (∨P +ij
,∨P +ik )denotes the disjunction of the propositions in both ∨
P +
ij
and ∨
P +
ik or false if there are no propositions common to both.For example,com (p 1∨p 2,p 2∨p 3)=p 2.
Observe that IRES A and SRES A apply classical resolution to the right hand side of the parent clauses whereas IRES P k and SRES P k involve XOR resolution.Note we can only ap-ply IRES A and
SRES A between clauses with complementary (non-XOR)literals on the right hand side.We can also apply the IRES P k and SRES P k rules to these clauses but the dis-junct ∨A 1∨∨
A 2on the right hand side of the conclusion will be equivalent to true .
3Soundness and Completeness
Similarly to [Fisher et al.,2001;Degtyarev et al.,2006],one can show that whenever the parent clauses are satisfiable then so is the resolvent.Since all the rules of initial ,and step res-olution follow the same pattern,we first prove the classical propositional counterpart of the completeness theorem,and then use it to prove the completeness of temporal resolution.Consider the following classical set of resolution rules con-sisting of the rule RES A :
(∨
P +11∨...∨
P +n 1∨∨
A 1∨a );
(∨P +
12∨...∨P +n 2∨∨
A 2∨¬a )
(∨
P +11∨...∨
P +n 1∨∨
P +12∨...∨
P +
n 2∨∨
A 1∨∨
A 2)
and,for every k ∈{1,...,n },the rule RES P k :
(∨
P +11∨...∨
P +k 1∨...∨
P +
n 1∨A 1)(∨
P +12∨...∨
P +k 2∨...∨
P +n 2∨A 2)
(∨
P +11∨∨
P +12∨.. (∨
P +k 1,∨
P +k 2)∨...∨∨
P +n 1∨∨
P +
n 2∨∨
A 1∨∨
A 2)
Lemma 1If a set of classical propositional clauses is unsat-isfiable than its unsatisfiability can be established by the rules
RES A and RES P k in O (N 1×N 2×···×N n ×2N a )time.Proof:First we show that if an unsatisfiable set of clauses C does not contain non-XOR literals,then its unsatisfiability can be established by rules RE
S P k .Note that any such set of clauses C is unsatisfiable if,and only if,for every l ,0<l ≤n ,and every set of propositions p 1,p 2,...,p l ,where p i ∈P i ,the set C p 1,...,p l of clauses from C ,which contain none of p 1,...,p l ,is nonempty.Indeed,otherwise every clause from C contains at least one of the propositions p 1,...p l ,so making p 1,...,p l true satisfies C .
Assume all clauses from C consist of propositions from P 1,...,P k only (originally,k =n )and show that with the rule RES P k one can obtain an unsatisfiable set of clauses C  in which all clauses consist of propositions from P 1,...,P k −1only.
Take arbitrary propositions p 1∈P 1,p 2∈P 2,...p k −1∈P k −1and take arbitrary clauses C 1∈C p 1,p 2,...,p k −1,p k,1,C 2∈C p 1,p 2,...,p k −1,p k,2,...,C N k ∈C p 1,p 2,...,p k −1,p k,N k .Ap-plying rule RES P k to C 1,...,C N k one can obtain a clause C  consisting of propositions from P 1,...,P k −1only such that C  does not contain any of p 1,...,p k −1.The set C  is formed from such clauses C  for all possible combinations of p 1∈P 1,p 2∈P 2,...p k −1∈P k −1.Clearly,for every l ,0<l ≤n ,and every set of propositions p 1,p 2,...,p l ,where p i ∈P i ,the set C  p 1,...,p l is nonempty,hence,C  is unsatisfi-able.Applying this reasoning at most n times,one can obtain an empty clause.
Consider now a set of clauses C ,which may contain non-XOR literals.For arbitrary p 1∈P 1,...p n ∈P n con-sider C p 1,...,p n .Similarly to the previous case,every such
Initial Resolution:
IRES A start⇒(∨P+11∨...∨P+n1∨∨A1∨a)
start⇒(∨P+12∨...∨P+n2∨∨A2∨¬a)
start⇒(∨P+11∨...∨P+n1∨∨P+12∨...∨P+n2∨∨A1∨∨A2)
For every k∈{1,...,n}we have the rule.
IRES P
k start⇒(∨P+11∨...∨∨P+k1∨...∨P+n1∨∨A1)
start⇒(∨P+12∨...∨∨P+k2∨...∨P+n2∨∨A2)
start⇒(∨P+11∨∨P+12∨...∨com(∨P+k1,∨P+k2)∨...∨∨P+n1∨∨P+n2∨∨A1∨∨A2)
Step Resolution:
SRES A
∧
A1∧∧P−11∧...∧P−n1⇒g(∨P+11∨...∨P+n1∨∨A1∨a)
∧
A2∧∧P−12∧...∧P−n2⇒g(∨P+12∨...∨P+n2∨∨A2∨¬a)
∧
A1∧∧A2∧∧P−11∧...∧P−n1∧∧P−12∧...∧P−n2⇒g(∨P+11∨...∨P+n1∨∨P+12∨...∨P+n2∨∨A1∨∨A2)
For every k∈{1,...,n}we have the rule
∧
A1∧∧P−11∧...∧P−n1⇒g(∨P+11∨...∨∨P+k1∨...∨∨P+n1∨A1)
SRES P
k
∧
A2∧∧P−12∧...∧P−n2⇒g(∨P+12∨...∨∨P+k2∨...∨P+n2∨A2)
∧
A1∧∧A2∧∧P−11∧...∧P−n1∧∧P−12∧...∧P−n2⇒g(∨P+11∨∨P+12∨...∨com(∨P+k1,∨P+k2)∨...∨∨P+n1∨∨P+n2∨A1∨A2)
CONV
∧
A1∧∧P−11∧...∧P−n1⇒g false
start⇒(¬∧A−1∨¬∧P−11∨...¬∧P−n1);true⇒g(¬∧A−1∨¬∧P−11∨...¬∧P−n1)
Temporal Resolution:
TRES
L⇒(¬∨P+11∧...∧¬∨P+n1∧¬A1)
true⇒♦(∨P+11∨...∨∨P+n1∨A1) start⇒¬L true⇒g¬L
Figure1:Resolution Rules for the XOR Fragment
C p
1,...,p n should be nonempty.Consider the set C p1,...,p n
of clauses obtained by deleting all XOR-propositions from
clauses of C p
1,...,p n .Every C p1,...,p n must be unsatisfiable
(otherwise,extending the satisfying assignment for C p1,...,p n with p1,...,p n we satisfy all the clauses in C).Then clas-sical binary resolution will be able to prove unsatisfiability of C p1,...,p n.Applying RES A“in the same way”,one can obtain a clause C ,which does not contain neither non-XOR literals,nor p1,...,p n.The set C ,formed from such clauses C for all possible combinations of p1∈P1,p2∈P2, ...p k−1∈P k−1,is an unsatisfiable set of clauses not con-taining non-XOR literals.
Finally,one can see that it is possible to implement the described procedure in O(N1×N2×···×N n×2N a)time.
Next we sketch the proof of completeness of temporal resolu-tion,which is obtained combining the ideas of[Fisher et al., 2001;Degtyarev et al.,2002]and Lemma1.
Definition1(Behaviour Graph)We split the set of tempo-ral clauses into three groups.Let I denote the initial clauses;T be the set of all step clauses;and E be the sometime clauses.
Given a set of clauses over a set of propositional symbols P,we construct afinite directed graph G as follows.The nodes of G are interpretations of the set of propositions,that satisfy the XOR constraints over the XOR subsets.Notice that,because of the XOR-constraints,exactly one proposi-tion from each set of XOR propositions P i and any subset of propositions in A are true in I.This means that there at at most N1×N2×···×N n×2N a nodes in the behaviour graph. For each node,I,we construct an edge in G to a node I if,and only if,the following condition is satisfied:
•For every step clause(P⇒g Q)∈T,if I|=P then
I |=Q.
A node,I,is designated an initial node of G if I|=I.The behaviour graph G of the set of clauses is the maximal sub-graph of G given by the set of all nodes reachable from initial nodes.
If G is empty then the set I is unsatisfiable.In this case there must exist a derivation by IRES A and IRES P
k
as described in Lemma1(and in O(N1×N2×···×N n×2N a)time).
1.start ⇒s t
2.s t ⇒g (s t ∨s b )
3.s b ⇒g s w
4.s a ⇒g s t
5.s w ⇒g (s w ∨s a )
7.start ⇒t s
8.t s ⇒g t r
9.t r ⇒g (t r ∨t f
)10.t f ⇒g
t s ("finish")
Figure 2:Automata for agents S and T ,together with corresponding clauses in normal form.
Now suppose G is not empty.Let I be a node of G which
has no successors.Let {(P i ⇒g
Q i )}be the set of all step clauses such that I |=P i ,then ∧Q i is unsatisfiable.Using Lemma 1,one can show that step resolution proves
truncate的特征∧P i ⇒g
false .After the set of clauses is extended by the conclusion of the CONV rule,∨¬P i ,the node I is deleted from the graph.
In the case when all nodes of G have a successor,a contradiction can be derived with the help of the tempo-ral resolution rule TRES .Note that we impose no restric-tion on this rule (it coincides with the temporal resolution rule for the general calculi presented in [Fisher et al.,2001;Degtyarev et al.,2002])and the proof of completeness is no different from what is already published [Fisher et al.,2001;Degtyarev et al.,2002].
4Complexity
Again,we consider initial and step resolution first.
Lemma 2Using the rules of initial and step resolution,it is possible to reduce a set of temporal clauses to one whose behaviour graph does not have nodes without successors in O  N 1×N 2×···×N n ×2N a
3
time.Proof:Consider the following resolution strategy.For every
set of propositions p 1∈P 1,...,p n ∈P n and a ∈A ,consider the set of all step-clauses
∧A 1∧∧P −11∧...∧P −n 1⇒g (∨P +11∨...∨P +n 1
∨∨
A 1)such that ∧A 1,∧P −11,...,...∧
P −
n 1do not contain any of a,p 1,...,p n (there are at most N 1×N 2×···×N n ×2N a such sets of clauses),and try establishing the unsatisfiabil-ity of the conjunction of the right-hand sides together with the universal clauses by step resolution (as Lemma 1shows,this can be done in O (N 1×N 2×···×N n ×2N a )time.Then,all nodes without successors will be deleted from the behaviour graph (but some new such nodes may emerge).Af-ter N 1×N 2×···×N n ×2N a repetitions,we obtain a graph
in which every node has a successor.
Lemma 3Given a set of temporal clauses,it is possible to
find L such that L ⇒
k
¬q k ,as required for the TRES rule,in time polynomial in N 1×N 2×···×N n ×2N a .Proof:To find such L ,it suffices to find a strongly con-nected component in the behaviour graph of the set of clauses,such that for every node I of this component,I |= k ¬q k .The simplest brute-force algorithm would analyse all pairs of nodes (and there are (N 1×N 2×···×N n ×2N a )2such pairs),and this can be done more efficiently with step resolution as
in [Degtyarev et al.,2006].
Theorem 4If a set of temporal clauses is unsatisfiable,tem-poral resolution will deduce a contradiction in time polyno-mial in N 1×N 2×···×N n ×2N a .
5Example
Having described the underlying approach,we will now con-sider an example that makes use of some of these aspects.
In particular,we will have multiple XOR fragments,together with standard propositions (unconstrained by XOR clauses).The example we will use is a simplification and abstraction of agent negotiation protocols;see,for example [Ballarini et al.,2006].Here,several (in our case,two)agents exchange information in order to come to some agreement.Each agent essentially has a simple control cycle,which can be repre-sented as a finite state machine.In fact,we have simplified these still further,and sample basic control cycles are given in Fig.2(for both agents S and T ).
Thus,we aim to use these automata as models of the agents,then formalise these within our logic.Importantly,we will add additional clauses (and propositions)characteris-ing agreements or concur
rency and,finally,we will show how our resolution method can be used to carry out verification.We begin by characterising each agent separately as a set of clauses within our logic.To achieve this,we use a set of propositions for each agent.Thus,the automaton describing agent S is characterised through propositions of the form s a ,s b ,etc.,while the automaton describing agent T is charac-terised using propositions such as t r ,t s ,etc.Both these sets are XOR sets.Thus,exactly one of s a ,s b ,...,and exactly one of t r ,t s ,...,must be true at any moment in time.
Now,the set of clauses characterising the two automata are given in Fig.2.Regarding automaton S ’s description,note that clause 6ensures that the automaton is infinitely often in
1.start ⇒s t
2.¬s b ∧¬s w ∧¬s a ⇒g (s t ∨s b )
3.¬s t ∧¬s w ∧¬s a ⇒
g s w 4.¬s t ∧¬s b ∧¬s w ⇒g s t 5.¬s t ∧¬s b ∧¬s a ⇒g (s w ∨s a )
7.start ⇒t s
8.¬t r ∧¬t f ⇒g t r
9.¬t s ∧¬t f ⇒g (t r ∨t f )
10.¬t s ∧¬t r ⇒g
t ue ⇒♦agree
12.(agree ∧¬s t ∧¬s b ∧¬s a ∧¬t s ∧¬t f )⇒g s a 13.(agree ∧¬s t ∧¬s b ∧¬s a ∧¬t s ∧¬t f )⇒g t f 14.(¬agree ∧¬s t ∧¬s b ∧¬s a )⇒g s w 15.(¬agree ∧¬t s ∧¬t f )⇒g t r 16.(agree ∧¬s t ∧¬s b ∧¬s a ∧¬t r )⇒g s w 17.(agree ∧¬s w ∧¬t s ∧¬t f )⇒g t r
19.(¬s t ∧¬s b ∧¬s w ∧¬t s ∧¬t r )⇒g false [18,10,4SRES P k ]20.true ⇒g (s t ∨s b ∨s w ∨t s ∨t r )[19CONV ]21.(agree ∧¬s t ∧¬s b ∧¬s a ∧¬t s ∧¬t f )⇒g false [20,12,13SRES P k ]22.true ⇒g (¬agree ∨s t ∨s b ∨s a ∨t s ∨t f )[21CONV ]23.(¬agree ∧¬s t ∧¬s b ∧¬s a ∧¬t s ∧¬t f )⇒g ¬agree [22,14,15SRES P k ]24.true ⇒g (agree ∨s t ∨s b ∨s a ∨t s ∨t f )[23,15,14,11TRES ]25.true ⇒g (s t ∨s b ∨s a ∨t s ∨t f )[24,22SRES A ]26.(¬s t ∧¬s w ∧¬s a )⇒g (t s ∨t f )[25,3SRES P k ]27.(¬agree ∧¬s t ∧¬s w ∧¬s a ∧¬t s ∧¬t f )⇒g false [26,15SRES P k ]28.true ⇒g (agree ∨s t ∨s w ∨s a ∨t s ∨t f )[27C
ONV ]29.(agree ∧¬s t ∧¬s w ∧¬s a ∧¬t s ∧¬t f )⇒g false [26,17SRES P k ]30.true ⇒g (¬agree ∨s t ∨s w ∨s a ∨t s ∨t f )[29CONV ]31.true ⇒g (s t ∨s w ∨s a ∨t s ∨t f )[28,30SRES A ]32.¬s b ∧¬s w ∧¬s a ⇒g (s t ∨t s ∨t f )[31,2SRES P k ]33.(¬agree ∧¬s b ∧¬s w ∧¬s a ∧¬t s ∧¬t f )⇒g s t [32,15SRES P k ]34.(agree ∧¬s b ∧¬s w ∧¬s a ∧¬t s ∧¬t f )⇒g s t [32,17SRES P k ]35.true ⇒g (s b ∨s w ∨s a ∨t s ∨t f )[33,15,34,17,6TRES ]36.(¬agree ∧¬s t ∧¬s b ∧¬s w ∧¬t s ∧¬t f )⇒g false [35,15,4SRES P k ]37.true ⇒g (agree ∨s t ∨s b ∨s w ∨t s ∨t f )[36CONV ]38.(agree ∧¬s t ∧¬s b ∧¬s w ∧¬t s ∧¬t f )⇒g false [35,17,4SRES P k ]39.true ⇒g (¬agree ∨s t ∨s b ∨s w ∨t s ∨t f )[38CONV ]40.true ⇒g (s t ∨s b ∨s w ∨t s ∨t f )[37,39SRES A ]41.true ⇒g (t s ∨t f )[40,35,31,25SRES P k ]42.¬t r ∧¬t f ⇒g false [41,8SRES P k ]
43.start ⇒t r ∨t f
[42CONV ]44.start
⇒false [43,7IRES P k ]
Figure 3:Resolution Proof for Automata Agents Example.
a state other than s t ,ensuring that the automaton can not re-main in state s t forever.
We can also characterise how the computations within each automaton relate.To begin with,we assume a simple,syn-chronous,concurrent model where both automata make a transition at the same time (see Section 5for variations on this).Next we add a key aspect in negotiation protocols,namely a description of what happens when an agreement is reached.In our example,this is characterised as a synchro-nised communication act.Logically,we use the proposition agree to denote this,and add the following clauses.
12.(agree ∧s w ∧t r )⇒g s a 13.(agree ∧s w ∧t r )⇒g t f
14.(¬agree ∧s w )⇒g s w
15.(¬agree ∧t r )⇒g t r
16.(s w ∧agree ∧¬t r )⇒g s w
17.(¬s w ∧agree ∧t r )⇒g t r
Here,we say that agreements will occur infinitely often in
the future (clause 11).Clauses 12and 13capture the exact synchronisation.If an agreement occurs while automaton S is in state s w and automaton T is in t r ,then the automata make transitions forward to states s a and t f respectively.Finally,clauses 14–17ensure that,if no synchronised agreement is possible,then the automata remain in their relevant states.The clauses above represent the specification of a simple system.As an example of how resolution can be used,we also wish to verify that the system is simultaneously in states s t and t s eventually.To verify this,we add the negation of this property,as characterised by clause 18:
The example above essentially captures activity within a synchronous,truly concurrent,system.If we wish to move to
more complex models of computation,we can do so,essen-tially by introducing the notion of a turn.Thus,when it is au-tomaton S’s turn to move,turn s is true;when it is automaton T’s turn to move,turn t is true.Then,each clause describ-
ing an automaton transition,for example,3.s b⇒g s w is replaced by two clauses
3a.(s b∧turn s)⇒g s w
3b.(s b∧¬turn s)⇒g s b.
In the example above,turn s and turn t are effectively both true together(and forever).However,we can modify the synchronisation clauses and model a different form of con-currency.For example,if we were to introduce interleaving concurrency,we might use the following clauses1:
start⇒turn s turn s⇒g turn t turn t⇒g turn s If we go further still,and introduce an asynchronous model of concurrency,then we might get
true⇒♦turn s true⇒♦turn t
In both the above cases if we want to ensure that exactly one of turn s and turn t hold at each moment we implic-itly have(turn s⊕turn t)and so we are effectively using TLX(S,T,{turn s,turn t}).
6Concluding Remarks and Related Work
In this paper we have developed a tractable sub-class of tem-poral logic,based on the central use of XOR operators.This logic can be decided,tractably,via clausal temporal resolu-tion.Importantly,multiple XOR fragments can be combined. This new approach to temporal reasoning provides a frame-work in which tractable temporal logics can be engineered by intelligently combining appropriate XOR fragments.Further, this has the potential to provide a deductive approach,with a similar complexity to model checking,thus obtaining a prac-tical verification method.In addition,this approach has the potential to be extended tofirst-order temporal logics which can deal with infinite state systems.
The complexity result means that TLX is more amenable to efficient implementation than other similar temporal log-ics.Moreover,since no two propositions from the same XOR set can occur in the right-(or left-)hand side of any temporal clause,one can efficiently represent disjunctions of(positive) propositions(and conjunctions of negated propositions)as bit vectors and the rules of temporal resolution as bit-wise oper-ations on such bit vectors.Thus,temporal reasoning in TLX can be efficient not only in theory,but also in practice. Demri and Schnoebelen[2002]consider sub-fragments of PTL,particularly those restricting the number of proposi-tions,the temporal operators allowed,and the depth of tem-poral nesting in formulae.Demri and Schnoebelen show that, since the formulae tackled in practical model checking often fall within such fragments,then this provides a natural expla-nation for the viability of model checking in PTL.
Recent results relating to a clausal resolution calculus for propositional temporal logics can be found in[Fisher et al., 1Note that a different model of concurrency might also require modification in the agreement clauses.2001;Hustadt and Konev,2003;Hustadt et al.,2004].Since deciding unsatisfiability of PTL is also PSPACE-complete, then deductive verification of PTL formulae would seem to be an impractical way to proceed.However,just as Demri and Schnoebelen showed how PTL model checking can be seen as being tractable when we consider fragments of PTL,so we have been examining fragments of PTL that allow clausal res-olution to be tractable.Thefine grained complexity analysis shows that the calculus is polynomial in the number of XOR propositions(and exponential in the non-XOR propositions) making it efficient for problems with large numbers of XOR propositions and just a few non-XOR propositions. Related to the fragment presented in this paper is a more restricted case in[Dixon et al.,2006]which can be used to represent B¨u chi Automata.In that paper,a particular frag-ment allowing two XOR sets of propositions but where the
allowable clauses were further restricted is considered and a polynomial resolution calculus given.One can show that ev-ery resolvent within that calculus can be derived by applying resolution rules from the resolution calculus proposed in this paper restricted to two XOR sets.
References
[Ballarini et al.,2006]P.Ballarini,M.Fisher,and M.Wooldridge.
Automated Game Analysis via Probabilistic Model Checking:a case study.Electronic Notes in Theoretical Computer Science, 149(2):125–137,2006.
[Clarke et al.,1999]  E.M.Clarke,O.Grumberg,and D.Peled.
Model Checking.MIT Press,December1999.
[Degtyarev et al.,2002]  A.Degtyarev,M.Fisher,and B.Konev.
A Simplified Clausal Resolution Procedure for Propositional
Linear-Time Temporal Logic.In Proc.TABLEAUX-02,LNCS vol.2381,pages85–99.Springer-Verlag,2002.
[Degtyarev et al.,2006]  A.Degtyarev,M.Fisher,and B.Konev.
Monodic Temporal Resolution.ACM Transactions on Compu-tational Logic,7(1),January2006.
[Demri and Schnoebelen,2002]S.Demri and P.Schnoebelen.The Complexity of Propositional Linear Temporal Logic in Simple Cases.Information and Computation,174(1):84–103,2002. [Dixon et al.,2006]
  C.Dixon,M.Fisher,and B.Konev.Is There a Future for Deductive Temporal Verification?In Proc.TIME-06.
IEEE Computer Society Press,2006.
[Fisher et al.,2001]M.Fisher,C.Dixon,and M.Peim.Clausal Temporal Resolution.ACM Transactions on Computational Logic,2(1):12–56,January2001.
[Gabbay et al.,1980]  D.Gabbay,A.Pnueli,S.Shelah,and J.Stavi.
The Temporal Analysis of Fairness.In Proc.POPL-80,pages 163–173,January1980.
[Hustadt and Konev,2003]U.Hustadt and    B.Konev.TRP++
2.0:A Temporal Resolution Prover.In Proc.CADE-19,LNAI
vol.2741,pages274–278.Springer,2003.
[Hustadt et al.,2004]U.Hustadt,  B.Konev,  A.Riazanov,and
A.V oronkov.TeMP:A Temporal Monodic Prover.In Proc.
IJCAR-04,LNAI vol.3097,pages326–330.Springer,2004. [Schaefer,1978]T.J.Schaefer.The Complexity of Satisfiability Problems.In Proc.STOC-78,pages216–226,1978.
[Sistla and Clarke,1985]  A.P.Sistla and E.M.Clarke.Complexity of Propositional Linear Temporal Logics.Journal of the ACM, 32(3):733–749,July1985.

版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。