Tractable Temporal Reasoning

1 Introduction

Temporal logics have been used to describe a wide variety of systems, from both Computer Science and Artificial Intelligence. The basic idea of proof, within propositional, discrete temporal logics, is also both intuitive and appealing. However 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 automaton 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 interested in properties relating to how the agents progress under particular models of concurrency such as synchrony, asynchrony etc., or particular coordination or cooperation actions.

∗The work of the first and last authors was partially supported by EPRSC grant number GR/S63182/01 "Dynamic Ontologies: a Framework for Service Descriptions".

In this paper we consider a new fragment of PTL that incorporates the use of XOR operators, denoted (q1⊕q2⊕. . .⊕qn) meaning that exactly one qi holds for 1 ≤ i ≤ n. Since the complexity of unsatisfiability for XOR clauses in classical 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 introduce the PTL fragment to be considered, called TLX, and show a complete clausal resolution system for this. The fragment 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.

2 XOR Temporal Logic

The logic we consider is called "TLX", and its syntax and semantics 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, ti, is a set of proposition symbols, representing those propositions which are satisfied in the ith 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:

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 proposition from every set Pi is true in every state. For example, if we consider just one set of propositions P, we have

Furthermore, we assume that there exists a set of propositions 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 = {p1, p2, . . . , pl}, Q = {q1, q2, . . . , qm}, and R = {r1, r2, . . . , rn} where P, Q and R are disjoint, but also satisfying

2.1 Normal Form

Assume we have n sets of XOR propositions P1 = {p11, . . . p1N1 }, . . ., Pn = {pn1, . . . pnNn } and a set of additional propositions A = {a1, . . . aNa }. In the following:

• ∧ P - ij denotes a conjunction of negated XOR propositions from the set Pi;
• ∨ P + ij denotes a disjunction of (positive) XOR propositions from the set Pi;
• ∧Ai denotes a conjunction of non-XOR literals;
• ∨Ai denotes a disjunction of non-XOR literals.

A normal form for TLX is of the form ∧i Ci where each Ci is an initial, step or sometime clause (respectively) as follows:

Note that due to the semantics of the XOR clauses, if i ̸= k

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.2 Resolution Rules

We decide the validity of formulae in TLX using a form of clausal temporal resolution [Fisher et al., 2001]. The resolution 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 moment in time. Step resolution involves resolving two step clauses or deriving additional constraints when a contradiction 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(p1 ∨ p2, p2 ∨ p3) = p2.

Observe that IRESA and SRESA apply classical resolution to the right hand side of the parent clauses whereas IRESPk and SRESPk involve XOR resolution. Note we can only apply IRESA and SRESA between clauses with complementary (non-XOR) literals on the right hand side. We can also apply the IRESPk and SRESPk rules to these clauses but the disjunct ∨A1 ∨ ∨A2 on the right hand side of the conclusion will be equivalent to true.

3 Soundness 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 resolution 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 consisting of the rule RESA:

Lemma 1 If a set of classical propositional clauses is unsatisfiable than its unsatisfiability can be established by the rules RESA and RESPk in O(N1 × N2 × · · · × Nn ×2Na ) 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 RESPk . 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 p1, p2, . . . , pl, where pi ∈ Pi, the set Cp1,...,pl of clauses from C, which contain none of p1,. . . , pl, is nonempty. Indeed, otherwise every clause from C contains at least one of the propositions p1,. . . pl, so making p1, . . . , pl true satisfies C.

Assume all clauses from C consist of propositions from P1, . . . , Pk only (originally, k = n) and show that with the rule RESPk one can obtain an unsatisfiable set of clauses C ′ in which all clauses consist of propositions from P1,. . . , Pk-1 only.

Take arbitrary propositions p1 ∈ P1, p2 ∈ P2, . . . pk-1 ∈ Pk-1 and take arbitrary clauses C1 ∈ Cp1,p2,...,pk-1,pk,1 , C2 ∈ Cp1,p2,...,pk-1,pk,2 ,. . . , CNk ∈ Cp1,p2,...,pk-1,pk,Nk . Applying rule RESPk to C1,. . . , CNk one can obtain a clause C′ consisting of propositions from P1,. . . , Pk-1 only such that C′ does not contain any of p1, . . . , pk-1. The set C ′ is formed from such clauses C′ for all possible combinations of p1 ∈ P1, p2 ∈ P2, . . . pk-1 ∈ Pk-1. Clearly, for every l, 0 < l ≤ n, and every set of propositions p1, p2, . . . , pl, where pi ∈ Pi, the set C ′ p1,...,pl is nonempty, hence, C ′ is unsatisfiable. Applying this reasoning at most n times, one can obtain an empty clause.

Consider now a set of clauses C, which may contain nonXOR literals. For arbitrary p1 ∈ P1,. . . pn ∈ Pn consider Cp1,...,pn . Similarly to the previous case, every such

Initial Resolution:

For every k ∈ {1, . . . , n} we have the rule.

Step Resolution:

For every k ∈ {1, . . . , n} we have the rule

Temporal Resolution:

Figure 1: Resolution Rules for the XOR Fragment

Cp1,...,pn should be nonempty. Consider the set ˜ Cp1,...,pn of clauses obtained by deleting all XOR-propositions from clauses of Cp1,...,pn . Every ˜ Cp1,...,pn must be unsatisfiable (otherwise, extending the satisfying assignment for ˜ Cp1,...,pn with p1, . . . , pn we satisfy all the clauses in C). Then classical binary resolution will be able to prove unsatisfiability of ˜ Cp1,...,pn . Applying RESA "in the same way", one can obtain a clause C′ , which does not contain neither non-XOR literals, nor p1, . . . , pn. The set C ′ , formed from such clauses C′ for all possible combinations of p1 ∈ P1, p2 ∈ P2, . . . pk-1 ∈ Pk-1, is an unsatisfiable set of clauses not containing non-XOR literals.

Finally, one can see that it is possible to implement the described procedure in O(N1 × N2 × · · · × Nn ×2Na ) time.

□Next we sketch the proof of completeness of temporal resolution, which is obtained combining the ideas of [Fisher et al., 2001; Degtyarev et al., 2002] and Lemma 1.

Definition 1 (Behaviour Graph) We split the set of temporal 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 a finite 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 proposition from each set of XOR propositions Pi and any subset of propositions in A are true in I. This means that there at at most N1×N2×· · ·×Nn×2Na 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 ⇒ ❣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 subgraph 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 IRESA and IRESPk as described in Lemma 1 (and in O(N1 × N2 × · · · × Nn × 2Na ) time).

Now suppose G is not empty. Let I be a node of G which has no successors. Let {(Pi ⇒ ❣Qi)} be the set of all step clauses such that I |= Pi, then ∧Qi is unsatisfiable. Using Lemma 1, one can show that step resolution proves ∧Pi ⇒ ❣false. After the set of clauses is extended by the conclusion of the CONV rule, ∨¬Pi, 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 temporal resolution rule TRES. Note that we impose no restriction 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 fromwhat is already published [Fisher et al., 2001; Degtyarev et al., 2002].

4 Complexity

Again, we consider initial and step resolution first.

Lemma 2 Using 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 ((N1 × N2 × · · · × Nn × 2Na )3) time.

Proof: Consider the following resolution strategy. For every set of propositions p1 ∈ P1,. . . , pn ∈ Pn and a ∈ A, consider the set of all step-clauses

such that ∧ A1, ∧ P - 11 , . . . , . . . ∧ P - n1 do not contain any of a, p1, . . . , pn (there are at most N1 × N2 × · · · × Nn × 2Na such sets of clauses), and try establishing the unsatisfiability of the conjunction of the right-hand sides together with the universal clauses by step resolution (as Lemma 1 shows, this can be done in O(N1 × N2 × · · · × Nn × 2Na ) time. Then, all nodes without successors will be deleted from the behaviour graph (but some new such nodes may emerge). After N1 × N2 × · · ·× Nn × 2Na repetitions, we obtain a graph in which every node has a successor. □

Lemma 3 Given a set of temporal clauses, it is possible to find L such that L ⇒ ∧ k ¬qk, as required for the TRES

rule, in time polynomial in N1 × N2 × · · · × Nn × 2Na .

Proof: To find such L, it suffices to find a strongly connected component in the behaviour graph of the set of clauses, such that for every node I of this component, I |= ∧k ¬qk. The simplest brute-force algorithm would analyse all pairs of nodes (and there are (N1×N2×· · ·×Nn×2Na )2 such pairs), and this can be done more efficiently with step resolution as in [Degtyarev et al., 2006]. □

Theorem 4 If a set of temporal clauses is unsatisfiable, temporal resolution will deduce a contradiction in time polynomial in N1 × N2 × · · · × Nn × 2Na .

5 Example

Having described the underlying approach, we will now consider 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 represented 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) characterising agreements or concurrency 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 sa, sb, etc., while the automaton describing agent T is characterised using propositions such as tr, ts, etc. Both these sets are XOR sets. Thus, exactly one of sa, sb, . . ., and exactly one of tr, ts, . . ., 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 6 ensures that the automaton is infinitely often in a state other than st, ensuring that the automaton can not remain in state st forever.

We can also characterise how the computations within each automaton relate. To begin with, we assume a simple, synchronous, concurrent model where both automata make a transition at the same time (see Section 5 for 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 synchronised communication act. Logically, we use the proposition agree to denote this, and add the following clauses.

1. true ⇒♦agree
2. (agree ∧ sw ∧ tr) ⇒ ❣sa
3. (agree ∧ sw ∧ tr) ⇒ ❣tf
4. (¬agree ∧ sw) ⇒ ❣sw
5. (¬agree ∧ tr) ⇒ ❣tr
6. (sw ∧ agree ∧¬tr) ⇒ ❣sw
7. (¬sw ∧ agree ∧ tr) ⇒ ❣tr

Here, we say that agreements will occur infinitely often in the future (clause 11). Clauses 12 and 13 capture the exact synchronisation. If an agreement occurs while automaton S is in state sw and automaton T is in tr, then the automata make transitions forward to states sa and tf respectively. Finally, clauses 14-17 ensure 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 st and ts eventually. To verify this, we add the negation of this property, as characterised by clause 18:

Thus, if we can derive a contradiction from clauses 1-18 then we know the negated property is valid for this specification. We first rewrite clauses 1-18 in the correct format for the normal form. The refutation is given in Figure 3.

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, essentially by introducing the notion of a turn. Thus, when it is automaton S's turn to move, turns is true; when it is automaton T's turn to move, turnt is true. Then, each clause describing an automaton transition, for example, 3. sb ⇒ ❣sw is replaced by two clauses

In the example above, turns and turnt are effectively both true together (and forever). However, we can modify the synchronisation clauses and model a different form of concurrency. For example, if we were to introduce interleaving concurrency, we might use the following clauses 1 :

start ⇒ turns turns ⇒ ❣turnt turnt ⇒ ❣turns

If we go further still, and introduce an asynchronous model of concurrency, then we might get

In both the above cases if we want to ensure that exactly one of turns and turnt hold at each moment we implicitly have (turns ⊕ turnt) and so we are effectively using TLX(S,T ,{turns, turnt}).

6 Concluding Remarks and RelatedWork

In this paper we have developed a tractable sub-class of temporal logic, based on the central use of XOR operators. This logic can be decided, tractably, via clausal temporal resolution. Importantly, multiple XOR fragments can be combined. This new approach to temporal reasoning provides a framework 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 practical verification method. In addition, this approach has the potential to be extended to first-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 logics. 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 operations 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 propositions, the temporal operators allowed, and the depth of temporal 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 explanation 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.,

1 Note 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 resolution to be tractable. The fine 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¨uchi Automata. In that paper, a particular fragment 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 every resolvent within that calculus can be derived by applying resolution rules from the resolution calculus proposed in this paper restricted to two XOR sets.