Mathematical Foundations of Computer Science, 1996 Proceedings, Wojtek Penczek (Ed.), Lecture Notes in Computer Science 1113, Springer-Verlag (1996) 32–62

Linear Time Temporal Logics over Mazurkiewicz Traces

Madhavan Mukund and P.S. Thiagarajan

School of Mathematics, SPIC Science Foundation, 92 G N Chetty Rd, Madras 600 017, India E-mail: {madhavan,pst}@ssf.ernet.in

Abstract. Temporal logics are a well-established tool for specifying and reasoning about the computations performed by distributed systems. Although temporal logics are interpreted over sequences, it is often the case that such sequences can be gathered together into equivalence classes where all members of an equivalence class represent the same partially ordered stretch of behaviour of the system. This appears to have important implications for improving the practical efficiency of automated verification methods based on temporal logics. With this as motivation, we study logics that are directly interpreted over partial orders. We survey a number of linear time temporal logics whose underlying frames are Mazurkiewicz traces. We describe automata theoretic methods for solving the satisfiability and model checking problems for these logics. It turns out that we still do not know what the “canonical” linear time temporal logic over Mazurkiewicz traces looks like. We identify here the criteria that should be met by this elusive logic.

Introduction

Propositional Linear time Temporal Logic (LTL) proposed by Pnueli [Pnu] has become a well established tool for specifying and reasoning about complex distributed behaviours [MP]. A central feature of LTL is that its formulas are interpreted over infinite sequences. In applications of LTL, the infinite sequences consist of the runs of a distributed system with each run being an infinite sequence of states assumed by the system or an infinite sequence of actions executed by the system during the course of a computation. Interesting distributed systems consist of a number of autonomous sequential agents that coordinate their behaviour with the help of some communication mechanism. In such systems, substantial portions of a computation will consist of causally independent tasks performed by different agents at separate locations. Consequently a single partially ordered stretch of behaviour of the system will be modelled by many different runs that differ from each other only in the order in which they record causally independent occurrences of actions. This kind of run-based view is often referred to as an interleaved semantics of distributed systems.

The interleaved view of the behaviour of distributed systems has proved to be very successful and popular. However it has been known for some time that the practical effectiveness of LTL and related formalisms can be often enhanced by modelling and analyzing the concerned behaviours in terms of partial orders rather than sequences.

In typical applications, an LTL formula constitutes the specification of the system behaviour and the verification problem consists of checking whether every run of the system is a model of the formula and therefore whether the system meets the specification. The property expressed by the specification is very often of the kind where either all the interleaved runs corresponding to a single partially ordered computation have the property or none of the interleavings have the property. A typical example of such a property is freedom from deadlock, as pointed out by Valmari [Val]. As a result, it suffices to verify the desired property for just one representative run of each partially ordered computation. The resulting saving in running time and memory usage can be substantial in practice [GW]. This is the background and motivation underlying the so called partial order based verification methods which are a subject of active research [GW, KP, Val].

There is an alternative way to exploit non-sequential behaviours and the attendant partial order based verification methods. It consists of developing temporal logics and related techniques that can be directly applied to specify and reason about the properties of partial order based runs of a distributed system. In this paper we survey linear time temporal logics that have arisen from this approach.

In going from sequences to partial orders it is easy to go overboard because so many possibilities are available. Fortunately, in the context of distributed behaviours, Mazurkiewicz has formulated a tractable and yet very fruitful way of passing from sequences to partial orders [Maz]. The resulting restricted partial orders are known as Mazurkiewicz traces, often called—as we shall do here— just traces. The theory of traces is well developed [Die, DR] and is strongly related to the theory of other well known formalisms such as Petri nets and event structures. Further, the classical theory of ω-regular (word) languages in terms of its logical, algebraic and automata-theoretic aspects has been successfully extended to ω-regular trace languages [EM, GP]. Finally, the structures that underlie the partial order based verification methods being developed recently can be almost always be viewed as traces.

Hence there is a good deal of motivation for formulating linear time temporal logics that are to be directly interpreted over traces. Many such logics are now available. In the present survey, we will mainly concentrate on the ones that fulfill two criteria:

(i) The logic should be expressible within the first order theory of traces. (ii) The satisfiability problem for the logic should admit a treatment in terms of

asynchronous Büchi automata.

This seemingly arbitrary choice of criteria can be justified as follows. LTL is the linear time temporal logic over sequences in that it is equivalent in expressive power to the first order theory of sequences [Zuc]. We consider the task of identifying the counterpart of LTL for traces to be an important one both from a theoretical and practical standpoint (see the last portion of Section 4). At present we do not know what this counterpart of LTL looks like. However, it seems a good starting point to concentrate on those linear time temporal logics that are at least no more expressive than the first order theory of traces.

As for the second criterion, an appealing feature of LTL is that its satisfiability and model checking problems can be transparently solved using Büchi automata [VW]. This has led to a clean separation of the logical and combinatorial aspects of these problems, thus contributing to the development of automated verification methods and related optimization techniques. The evidence available at present suggests that asynchronous Büchi automata are an appropriate machine model for dealing with ω-regular trace languages. Hence it seems worthwhile to lift the interplay between LTL and Büchi automata to the level of traces.

In the next section we review the basic aspects of traces. In Section 2 we describe asynchronous Büchi automata and present our version of these automata called, for want of a better name, A2-automata. In Section 3, the heart of the paper, we present the logic TrPTL (Trace based Propositional Temporal logic of Linear time) and two of its sublogics TrPTL^{con} and TrPTL^{⊗}. The logic TrPTL is directly interpreted over traces. We show that the satisfiability and model checking problems for TrPTL can be solved using A2-automata. We then show that the syntactic restrictions imposed to obtain TrPTL^{con} and TrPTL^{⊗} lead to corresponding simplifications in the world of automata. After presenting these results we survey a number of other temporal logics that use traces as their underlying frames. In Section 4 we show that TrPTL is expressible within the first order theory of traces. The final section contains concluding remarks.

Most of the results will be presented without proofs. The proofs are either available in the literature or can be easily manufactured using the results available in the literature.

1 Traces

The starting point for trace theory is a trace alphabet (Σ, I), where Σ, the alphabet, is a finite set and I ⊆ Σ × Σ is an irreflexive and symmetric independence relation. In most applications, Σ consists of the actions performed by a distributed system while I captures a strong static notion of causal independence between actions. The idea is that contiguous independent actions occur with no causal order between them. Thus, every sequence of actions from Σ corresponds to an interleaved observation of a partially-ordered stretch of system behaviour. This leads to a natural equivalence relation over execution sequences: two sequences are equated iff they correspond to different interleavings of the same partially-ordered stretch of behaviour.

To formulate this equivalence relation precisely, we need some terminology. For the rest of the section we fix a trace alphabet (Σ, I) and let a, b range over Σ. D = (Σ × Σ) − I is called the dependency relation. Note that D is reflexive and symmetric. A set p ⊆ Σ is called a D-clique iff p×p ⊆ D. We set Σ^{∞} = Σ^{∗} ∪Σ^{ω} where Σ^{∗} is the set of finite words over Σ and Σ^{ω} is the set of infinite words over Σ. We let σ, σ′ with or without subscripts range over Σ^{∞} and τ, τ′ with or without subscripts range over Σ^{∗}. The equivalence relation ∼_{I} ⊆ Σ^{∞} × Σ^{∞} induced by I is given by:

σ ∼_{I} σ′ iff σ ↾p = σ′ ↾p for every D-clique p.

Here and elsewhere, if A is a finite set, ρ ∈ A^{∞} and B ⊆ A then ρ ↾B is the sequence obtained by erasing from ρ all occurrences of letters in A − B.

Clearly ∼_{I} is an equivalence relation. Notice that if σ = τabσ_{1} and σ′ = τbaσ_{1} with (a, b) ∈ I then σ ∼_{I} σ′. Thus σ and σ′ are identified if they differ only in the order of appearance of a pair of adjacent independent actions. In fact, for finite words, an alternative way to characterize ∼_{I} is to say that σ ∼_{I} σ′ iff σ′ can be obtained from σ by a finite sequence of permutations of adjacent independent actions. Unfortunately, the definition of ∼_{I} in terms of permutations is too naïve to be transported to infinite words, which is why we work with the less intuitive definition presented here.

The equivalence classes generated by ∼_{I} are called (Mazurkiewicz) traces. The theory of traces is well developed and documented—see [Die, DR] for basic material as well as a substantial number of references to related work.

Traces have many equivalent representations. We shall view traces as special kinds of labelled partial orders. Since sequences can be viewed as labelled total orders, this representation emphasizes that traces are an elegant and non-trivial generalization of sequences.

Recall that a Σ-labelled poset is a structure F = (E, ≤, λ) where ≤ is a partial order on the set E and λ : E → Σ is a labelling function. The covering relation ⋖ ⊆ E × E is given by: e ⋖ e′ iff e < e′ (i.e., e ≤ e′ and e ≠ e′) and for every e′′ ∈ E, e ≤ e′′ ≤ e′ implies e = e′′ or e′′ = e′.

For X ⊆ E we define ↓X to be the set {y | y ≤ x for some x ∈ X}. If X is a singleton {x}, we write ↓x instead of ↓{x}.

We can now formulate traces in terms of labelled partial orders. A trace over (Σ, I) is a Σ-labelled poset F = (E, ≤, λ) which satisfies the following conditions.

• E is a countable set.

• For each e ∈ E, ↓e is a finite set.

• For all e, e′ ∈ E, if e ⋖ e′ then (λ(e), λ(e′)) ∈ D.

• For all e, e′ ∈ E, if (λ(e), λ(e′)) ∈ D then e ≤ e′ or e′ ≤ e.

Let T R(Σ, I) denote the set of Σ-labelled posets that satisfy the definition above. We now sketch briefly the proof that Σ^{∞}/∼_{I} and T R(Σ, I) represent the same class of objects. We construct representation maps str : Σ^{∞} → T R(Σ, I) and trs : T R(Σ, I) → Σ^{∞}/ ∼_{I} and state some results which show that these maps are “inverses” of each other. We shall not prove these results. The details can be easily obtained using the constructions developed in [WN] for relating traces and event structures.

Henceforth, we will not distinguish between isomorphic elements in T R(Σ, I). In other words, whenever we write F = F′ for traces F = (E, ≤, λ) and F′ = (E′, ≤′, λ′), we mean that there is a label-preserving isomorphism between F and F′.

For σ ∈ Σ^{∞}, [σ] stands for the ∼_{I}-equivalence class containing σ. We use ⪯ to describe the usual prefix ordering over sequences. Let prf(σ) denote the set of finite prefixes of σ.

We now define str : Σ^{∞} → T R(Σ, I). Let σ ∈ Σ^{∞}. Then str(σ) = (E, ≤, λ) where:

• E = {τa | τa ∈ prf(σ)}. Recall that τ ∈ Σ^{∗} and a ∈ Σ. Thus E = prf(σ) − {ε}, where ε is the null string.

• ≤ ⊆ E × E is the least partial order which satisfies:

For all τa, τ′b ∈ E, if τa ⪯ τ′b and (a, b) ∈ D then τa ≤ τ′b.

• For τa ∈ E, λ(τa) = a.

The map str induces a natural map str′ from Σ^{∞}/ ∼_{I} to T R(Σ, I) defined by str′([σ]) = str(σ). One can show that if σ, σ′ ∈ Σ^{∞}, then σ ∼_{I} σ′ iff str(σ) = str(σ′). This observation guarantees that str′ is well defined. In fact, henceforth we shall write str to denote both str and str′.

To go in the other direction let F = (E, ≤, λ) be a trace over (Σ, I). Then ρ ∈ E^{∞} is called a linearization of F iff every e ∈ E appears exactly once in ρ and, moreover, whenever e, e′ ∈ E and e < e′, e appears before e′ in ρ.

As usual, we can extend the labelling function λ : E → Σ to words over E in a canonical way. If ρ = e_{0}e_{1} … is a word in E^{∞} then λ(ρ) denotes the corresponding word λ(e_{0})λ(e_{1}) … in Σ^{∞}. We can now define the map trs : T R(Σ, I) → Σ^{∞}/ ∼_{I} as follows:

trs(F) = {λ(ρ) | ρ is a linearization of F }.

Proposition 1.1

(i) For every σ ∈ Σ^{∞}, trs(str(σ)) = [σ]. (ii) For every F ∈ Σ^{∞}, str(trs(F)) = F.

This result justifies our claim that Σ^{∞}/ ∼_{I} and T R(Σ, I) are indeed two equivalent ways of talking about the same class of objects.

In the poset representation of traces, finite configurations play the same role that finite prefixes do in sequences. Let F = (E, ≤, λ) be a trace over (Σ, I). Then c ⊆ E is a configuration iff c is finite and ↓c = c. We let C_{F} denote the set of configurations of F. Notice that ∅, the empty set, is a configuration. It is the least configuration under set inclusion. More importantly, ↓e is a configuration for every e. These “pointed” configurations associated with the events are also called prime configurations. They constitute the building blocks for the Scott domains induced by traces [NPW]. We shall see that they also play a fundamental role in defining linear time temporal logics over traces.

We now turn our attention to distributed alphabets. Distributed alphabets can be viewed as “implementations” of trace alphabets. They form the basis for defining machine models with a built-in notion of independence which recognize trace languages.

Let P be a finite set of sequential agents called processes. A distributed alphabet is a family {Σ_{p}}_{p∈P} where Σ_{p} is a finite non-empty alphabet for each p ∈ P. The idea is that whenever an action from Σ_{p} occurs, the agent p must participate in it. Hence the agents can constrain each other’s behaviour, both directly and indirectly.

Trace alphabets and distributed alphabets are closely related to each other. Let Σ̃ = {Σ_{p}}_{p∈P} be a distributed alphabet. Then Σ_{P}, the global alphabet associated with Σ̃, is the collection ⋃_{p∈P} Σ_{p}. The distribution of Σ_{P} over P can be described using a location function loc_{Σ} : Σ_{P} → 2^{P} defined as follows:

loc_{Σ}(a) = {p | a ∈ Σ_{p}}.

This in turn induces the relation I_{Σ} ⊆ Σ_{P} × Σ_{P} given by:

(a, b) ∈ I_{Σ} iff loc_{Σ}(a) ∩ loc_{Σ}(b) = ∅.

Clearly I_{Σ} is irreflexive and symmetric and hence (Σ_{P}, I_{Σ}) is a trace alphabet. Thus every distributed alphabet canonically induces a trace alphabet. Two actions are independent according to Σ̃ if they are executed by disjoint sets of processes. Henceforth, we write loc for loc_{Σ} whenever Σ̃ is clear from the context.

Going in the other direction there are, in general, many different ways to implement a trace alphabet as a distributed alphabet. A standard approach is to create a separate agent for each maximal D-clique generated by (Σ, I). Recall that a D-clique of (Σ, I) is a non-empty subset p ⊆ Σ such that p × p ⊆ D. Let P be the set of maximal D-cliques of (Σ, I). This set of processes induces the distributed alphabet Σ̃ = {Σ_{p}}_{p∈P} where Σ_{p} = p for every process p. The alphabet Σ̃ implements (Σ, I) in the sense that the canonical trace alphabet induced by it is exactly (Σ, I). In other words, Σ_{P} = Σ and I_{Σ} = I.

For example, consider the trace alphabet (Σ, I) where Σ = {a, b, d} and I = {(a, b), (b, a)}. The canonical D-clique implementation of (Σ, I) yields the distributed alphabet Σ̃ = {{a, d}, {d, b}}.

As mentioned earlier, distributed alphabets play a crucial role in the automatatheoretic aspects of trace theory. The fundamental result of Zielonka [Zie] says that every regular trace language over (Σ, I) can be recognized by an asynchronous automaton over a distributed alphabet Σ̃ which implements (Σ, I). This result has been extended to ω-regular trace languages in terms of asynchronous Büchi automata by Gastin and Petit [GP].

Distributed alphabets arise naturally in a variety of models of distributed systems. In particular they are associated with the restricted but very useful model of a distributed system consisting of a network of sequential agents that coordinate their behaviour by performing common actions together. The linear time temporal logics that we consider in this paper will be based on distributed alphabets.

We conclude this section with a technical remark. Most of the theory of traces presented in this paper, including the automata-theoretic and logical aspects, constitutes a natural and conservative extension of the existing theory in the sequential setting. The sequential theory can almost always be recovered by setting I = ∅ when dealing with trace alphabets. Correspondingly, when dealing with distributed alphabets, the sequential case corresponds to having just one agent—i.e., |P| = 1.

2 Automata over Infinite Traces

From now on we shall focus on infinite traces. With a little additional work most of the material we shall present on automata and logics can be extended to handle finite traces as well. Through the rest of this section we fix a distributed alphabet Σ̃ = {Σ_{p}}_{p∈P} with the induced trace alphabet (Σ, I), where Σ = ⋃_{p∈P} Σ_{p} and I = {(a, b) | loc(a) ∩ loc(b) = ∅}.

The terminology and notational conventions developed in the previous section are assumed here as well. We will be dealing with many P-indexed families. For convenience we shall often write {X_{p}} to denote the P-indexed family {X_{p}}_{p∈P}. A similar convention will be followed in dealing with Σ-indexed families: {Y_{a}} will denote the family {Y_{a}}_{a∈Σ}.

Asynchronous Büchi automata, due to Gastin and Petit [GP], are the basic class of automata operating over infinite traces. They constitute a common generalization of the asynchronous automata of Zielonka [Zie] operating over finite traces and a mild variant of the classical Büchi automata operating over infinite sequences. We shall consider here a number of variants of asynchronous Büchi automata, each with a slightly different acceptance condition.

We begin with a brief and slightly non-standard presentation of Büchi automata. A word ω-automaton over Σ is a pair B = (T S, T ) where

• T S = (S, {→_{a}}, S_{in}) is a finite state transition system over Σ. In other words, S is a finite set of states, →_{a} ⊆ S × S is an a-labelled transition relation for each a ∈ Σ and S_{in} ⊆ S is a set of initial states.

• T is an acceptance table accompanied by an acceptance condition.

Before considering a number of possibilities for T , let us define the notion of a run. The Σ-indexed family of transition relations {→_{a}} induces a global transition relation →_{B} ⊆ S × Σ × S given by s ⟶^{a}_{B} s′ iff (s, s′) ∈ →_{a}. Where B is clear from the context →_{B} will be written as →.

Let σ ∈ Σ^{ω} (i.e., σ : ω → Σ where, as usual, ω = {0, 1, 2, …} is the set of natural numbers). A run of T S over σ is a map ρ : ω → S such that ρ(0) ∈ S_{in}

and ρ(i) ⟶^{σ(i)} ρ(i+1) for every i ≥ 0.

The set of states encountered infinitely along the run ρ is denoted inf(ρ): inf(ρ) = {s | for infinitely many i, ρ(i) = s}.

Let us now consider just two of the various possibilities for T .

(B0) T = F ⊆ S.

A run ρ over σ is accepting with respect to B0 iff inf(ρ) ∩ F ≠ ∅. We shall say that A is a B0-automaton if it uses B0 as its acceptance criterion. Of course, we shall also refer to these by their standard name; Büchi automata.

L(A), the language accepted (recognized) by A, is the set of infinite words σ such that there is an accepting run of A on σ. A language L ⊆ Σ^{ω} is said to be ω-regular iff there exists a Büchi automaton A over Σ such that L(A) = L. As is well known, ω-regular languages have equivalent algebraic and logical presentations, as detailed in the excellent survey [Tho].

A second possibility for T is:

(B1) T ⊆ 2^{S}.

A run ρ over σ is accepting with respect to B1 iff there exists F ∈ T such that inf(ρ) ⊇ F. It is easy to show that L ⊆ Σ^{ω} is ω-regular iff there exists a B1-automaton A (i.e., an automaton A that uses B1 as its acceptance criterion) such that L = L(A). Thus at the level of sequences there is no difference in expressive power between Büchi automata and B1-automata. As we shall see, at the level of traces, B0 is weaker than B1.

For defining automata on infinite traces we need to develop some notation. Let F = (E, ≤, λ) ∈ T R(Σ, I). Then F is an infinite trace iff E is an infinite set. Let T R^{ω}(Σ, I) denote the subclass of infinite traces over (Σ, I). Often, we shall write T R^{ω} instead of T R^{ω}(Σ, I).

Let F ∈ T R^{ω} with F = (E, ≤, λ) and let p ∈ P. Then e ∈ E is a p-event iff λ(e) ∈ Σ_{p}. Similarly, e is an a-event iff λ(e) = a. We let E_{p} denote the set of p-events and E_{a} denote the set of a-events.

There are two natural transition relations that one can associate with F. The event based transition relation ⇒_{F} ⊆ C_{F} × E × C_{F} is defined as c ⟹^{e}_{F} c′ iff e ∉ c and c ∪ {e} = c′. The action-based transition relation →_{F} ⊆ C_{F} × Σ × C_{F} is defined as c ⟶^{a}_{F} c′ iff there exists e ∈ E such that λ(e) = a and c ⟹^{e}_{F} c′.

To define automata on infinite traces, we have to first define a distributed version of transition systems. The distributed transition systems we work with here are essentially the asynchronous automata of Zielonka [Zie]. We begin with some notation involving local and global states.

Let P be a set of processes. We equip each process p ∈ P with a finite nonempty set of local p-states, denoted S_{p}. We set S = ⋃_{p∈P} S_{p} and call S the set of local states.

We let P, Q range over non-empty subsets of P and let p, q range over P. A Q-state is a map s : Q → S such that s(q) ∈ S_{q} for every q ∈ Q. We let S_{Q} denote the set Q-states. We call S_{P} the set of global states.

If Q′ ⊆ Q and s ∈ S_{Q} then s_{Q′} is s restricted to Q′. In other words s_{Q′} is the Q′-state s′ which satisfies s′(q′) = s(q′) for every q′ in Q′. We use a to abbreviate loc(a) when talking about states (recall that loc(a) = {p | a ∈ Σ_{p}}). Thus an a-state is just a loc(a)-state and S_{a} denotes the set of all loc(a)-states. If loc(a) ⊆ Q and s is a Q-state we shall write s_{a} to mean s_{loc(a)}.

A distributed transition system T S over Σ̃ is a structure ({S_{p}}, {→_{a}}, S_{in}) where

• S_{p} is a finite non-empty set of p-states for each process p.

• For a ∈ Σ, →_{a} ⊆ S_{a} × S_{a} is a transition relation between a-states.

• S_{in} ⊆ S_{P} is a set of initial global states.

The idea is that an a-move by T S involves only the local states of the agents which participate in the execution a. This is reflected in the global transition relation →_{T S} ⊆ S_{P} × Σ × S_{P} which is defined as:

s ⟶^{a}_{T S} s′ iff (s_{a}, s′_{a}) ∈ →_{a} and s_{P−loc(a)} = s′_{P−loc(a)}.

From the definition of →_{T S}, it is clear that actions which are executed by disjoint sets of agents are processed independently by T S.

A trace ω-automaton over Σ̃ = {Σ_{p}} is a pair A = (T S, T ) where T S = ({S_{p}}, {→_{a}}, S_{in}) is a distributed transition system over Σ̃ and T is an acceptance table (which we will elaborate on later).

A trace run of T S over F ∈ T R^{ω} is a map ρ : C_{F} → S_{P} such that ρ(∅) ∈ S_{in} and for every (c, a, c′) ∈ →_{F}, ρ(c) ⟶^{a}_{T S} ρ(c′).

To define acceptance we must now compute inf_{p}(ρ), the set of p-states that are encountered infinitely often along ρ. The obvious definition, namely inf_{p}(ρ) = {s_{p} | ρ(c)(p) = s_{p} for infinitely many c ∈ C_{F} }, will not work. The complication arises because some processes may make only finitely many moves, even though the overall trace consists of an infinite number of events.

For instance, consider the distributed alphabet Σ̃_{0} = {{a}, {b}}. In the corresponding distributed transition system, there are two processes p and q which execute a’s and b’s completely independently. Consider the trace F = (E, ≤, λ) where |E_{p}| = 1 and E_{q} is infinite—i.e., all the infinite words in trs(F) contain one a and infinitely many b’s. Let s_{p} be the state of p after executing a. Then, there will be infinitely many configurations whose p-state is s_{p}, even though p only moves a finite number of times.

Continuing with the same example, consider another infinite trace F′ = (E′, ≤′, λ′) over the same alphabet where both E_{p} and E_{q} are infinite. Once again, let s_{p} be the local state of p after reading one a. Further, let us suppose that after reading the second a, p never returns to the state s_{p}. It will still be the case that there are infinitely many configurations whose p-state is s_{p}: consider the configurations c_{0}, c_{1}, c_{2}, … where c_{j} is the finite configuration after one a and j b’s have occurred.

So, we have to define inf_{p}(ρ) carefully in order to be able to distinguish whether or not process p is making progress. The appropriate formulation is as follows:

Case 1 E_{p} is finite: inf_{p}(ρ) = {s_{p}}, where ρ(↓E_{p}) = s and s_{p} = s(p). Case 2 E_{p} is an infinite set:

inf_{p}(ρ) = {s_{p} | for infinitely many e ∈ E_{p}, s_{e}(p) = s_{p}, where ρ(↓e) = s_{e}}.

We can now begin to consider various acceptance tables.

(A0) T = {F_{p}} with F_{p} ⊆ S_{p} for each p.

A run ρ over F is accepting with respect to A0 iff inf_{p}(ρ) ∩ F_{p} ≠ ∅ for every p. The trace language accepted by the A0-automaton A (i.e., where T is of the form A0) is the set L_{T r}(A) = {F | ∃ an accepting run of T S over F }. A0-automata are the obvious common generalization of asynchronous automata and Büchi automata. It turns out that A0-automata are not expressive enough: the acceptance criterion cannot distinguish whether or not an agent executes infinitely many actions.

To bring this out and to motivate the acceptance condition we are after, we will put down a crude definition of ω-regular trace languages.

A trace language over Σ̃ is just a subset of T R^{ω}. To define ω-regular trace languages, we exploit the result from the previous section linking Σ^{∞}/ ∼_{I} and T R(Σ, I) which permits us to associate a language of infinite words with each trace language. We can then transport the definition of ω-regularity from subsets of Σ^{ω} to infinite traces.

Let L ⊆ Σ^{ω}. Then L is I-consistent iff for every σ ∈ Σ^{ω}, if σ ∈ L then [σ] ⊆ L. Thus if L is I-consistent either all members of the ∼_{I}-equivalence class [σ] are in L or none of them are in L.

Let L′ ⊆ T R^{ω}. We say that L′ is an ω-regular trace language iff there exists an I-consistent ω-regular language L ⊆ Σ^{ω} such that L′ = {str(σ) | σ ∈ L}. Stated differently, L′ ⊆ T R^{ω} is a ω-regular trace language iff L = ⋃{trs(F) | F ∈ L′} is a ω-regular subset of Σ^{ω}. As in the word case, algebraic and logical presentations of ω-regular trace languages have been worked out [EM, GP]. These presentations have a flavour which is pleasingly similar to the classical algebraic and logical characterisations of ω-regular subsets of Σ^{ω}.

Returning to the distributed alphabet Σ̃_{0} = ({a}, {b}), let (Σ_{0}, I_{0}) denote the corresponding trace alphabet. Consider L ⊆ T R^{ω}(Σ_{0}, I_{0}) consisting of the single trace F = (E, ≤, λ) such that E_{a} and E_{b} are both infinite sets. It is easy to check that L is a ω-regular trace language but, as argued in [GP], no A0-automaton over Σ̃ can recognize L.

It is worth noting that having multiple entries in the acceptance table does not help. In other words, one might consider the following acceptance criterion.

(A0′) T = {T_{0}, T_{1}, …, T_{n}} with T_{i} = {F_{p}^{i}}_{p∈P} and F_{p}^{i} ⊆ S_{p} for each i ∈ {1, 2, …, n} and each p ∈ P. A run ρ of T S over F ∈ T R^{ω} is accepting with respect to A0′ iff there exists i such that inf_{p}(ρ) ∩ F_{p}^{i} ≠ ∅ for each p.

The reason why A0′ does not help is that the class of languages accepted by A0-automata is closed under union, thanks to the presence of multiple global initial states. We can construct an A0-automaton A_{i} = (T S, T_{i}) for each entry T_{i} from the table of an A0′-automaton A = (T S, T ). If T = {T_{0}, T_{1}, …, T_{n}}, it is clear that L(A) = ⋃_{i∈{1,2,...,n}} L(A_{i}). Thus, every A0′-automaton can be simulated by an A0-automaton.

Gastin and Petit showed that the following acceptance condition provides a suitable generalization of classical Büchi automata to the setting of infinite traces.

(A1) T = {T_{1}, T_{2}, …, T_{n}} with T_{i} = {F_{p}^{i}}_{p∈P} and F_{p}^{i} ⊆ S_{p} for each i ∈ {1, 2, …, n} and each p ∈ P. A run ρ of T S over F ∈ T R^{ω} is accepting with respect to A1 iff there exists i such that inf_{p}(ρ) ⊇ F_{p}^{i} for each p.

The condition A1 is an extension of the sequential condition B1 in a distributed setting. Notice that A1 “couples” together final sets of the components in each entry T_{i} ∈ T .

Theorem 2.1 ([GP]) L ⊆ T R^{ω} is a ω-regular trace language iff there exists an A1-automaton A such that L_{T r}(A) = L.

Subsequently, Niebert has shown that the A1 condition can be modified to avoid coupling final sets across processes [Nie]. In effect, it is possible to have a local B1 table for each process and define a run ρ to be accepting if for each process p, inf_{p}(ρ) satisfies p’s B1 table. Going one step further, we arrive at the acceptance criterion A2, which is the one we will use in connection with the logics to be studied in the next section.

(A2) T = {(F_{p}^{ω}, F_{p})}_{p∈P} with F_{p}^{ω}, F_{p} ⊆ S_{p} for each p.

A run ρ over F = (E, ≤, λ) is accepting with respect to A2 iff for each process p the following conditions are met.

Case 1 E_{p} is finite: Then inf_{p}(ρ) ∩ F_{p} ≠ ∅.

Case 2 E_{p} is an infinite set: Then inf_{p}(ρ) ∩ F_{p}^{ω} ≠ ∅.

Thus, on an input F, the decision as to whether a process p uses F_{p} or F_{p}^{ω} to determine acceptance depends on whether or not p executes infinitely many actions in F.

Theorem 2.2

(i) The class of languages accepted by A2-automata is closed under union. (ii) The class of languages accepted by A1-automata is identical to the class of

languages accepted by A2-automata.

Proof Sketch.

(i) Suppose A_{1} and A_{2} are two A2-automata. Then we construct an A2-automaton A which is the disjoint union of A_{1} and A_{2}. The global initial states of A will determine for each run whether A_{1} or A_{2} (but not both!) is going to be explored. It is easy to check that L(A) = L(A_{1}) ∪ L(A_{2}).

(ii) Let A = (T S, T ) be an A1-automaton. From part (i), it suffices to consider the case where T has just one entry. So assume that T = {T_{1}} and T_{1} = {F_{p}}. Let T S = ({S_{p}}, {→_{a}}, S_{in}). Define the A2-automaton A′ = (T S′, T′) as follows. T S′ = ({S′_{p}}, {⇒_{a}}, S′_{in}) where:

• S′_{p} = S_{p} × 2^{F_{p}} × {on, off} for each p.

• Let s′_{a}, t′_{a} be a-states in T S′ such that s′_{a}(p) = (s_{p}, X_{p}, u_{p}) and t′_{a}(p) = (t_{p}, Y_{p}, v_{p}) for each p ∈ P. Then (s′_{a}, t′_{a}) ∈ ⇒_{a} iff there exists (s_{a}, t_{a}) ∈ →_{a} such that the following conditions are satisfied for each p ∈ loc(a).

(1) u_{p} = on, s_{p} = s_{a}(p) and t_{p} = t_{a}(p).

(2) If X_{p} = ∅ then Y_{p} = F_{p}. Otherwise, Y_{p} = X_{p} − {t_{p}}.

• S′_{in} = {s′ ∈ S′_{P} | ∃s ∈ S_{in}. ∀p ∈ P. ∃u_{p} ∈ {on, off}. s′(p) = (s(p), ∅, u_{p})}

• T′ = {(G_{p}^{ω}, G_{p})} where for each p,

\begin{aligned}G_{p}^{ω} & = & S_{p} × \{∅\} × \{on\} \\ G_{p} & = & F_{p} × 2^{F_{p}} × \{off\} \end{aligned}

It is easy to check that L_{T r}(A) = L_{T r}(A′).

Conversely, let A = (T S, T ) be an A2-automaton with T S = ({S_{p}}, {→_{a}}, S_{in}) and T = {(F_{p}^{ω}, F_{p})}. We say that A is in standard form if it satisfies:

• F_{p}^{ω} ∩ F_{p} = ∅ for each p.

• If (s_{a}, t_{a}) ∈ →_{a} and p ∈ loc(a), then s_{a}(p) ∉ F_{p}.

Thus, if A is in standard form, the p-states in F_{p} are “dead” and are disjoint from F_{p}^{ω}. It is a simple exercise to verify that every A2-automaton A can be converted to an A2-automaton A′ in standard form such that L_{T r}(A) = L_{T r}(A′).

So, let A = (T S, T ) be an A2-automaton in standard form with T S = ({S_{p}}, {→_{a}}, S_{in}) and T = {(F_{p}^{ω}, F_{p})}. Let G be the set of functions of the form g : P → S such that g(p) ∈ F_{p}^{ω} ∪ F_{p} for each p. Define the A1-automaton A′ = (T S′, T′) where T S′ = T S and T′ = {T′_{g}}_{g∈G}, such that for each g ∈ G, T′_{g} = {{g(p)}}_{p∈P}. It is easy to verify that L_{T r}(A) = L_{T r}(A′). □

We now argue that the emptiness problem for A2-automata is decidable. This will be required to settle the satisfiability problem for the logics considered in the next section. Let A = (T S, T ) be an A2-automaton be with T S = ({S_{p}}, {→_{a}}, S_{in}) and T = {(F_{p}^{ω}, F_{p})}. Though it is not strictly necessary, it will be illuminating to first associate a language of infinite words with A.

Let σ ∈ Σ^{ω}. Then a (word) run of T S over σ is a map ρ : ω → S_{P} such that

ρ(0) ∈ S_{in} and ρ(i) ⟶^{σ(i)}_{T S} ρ(i+1) for each i ≥ 0. The run ρ over σ is accepting iff the following conditions are satisfied for each p.

(i) If i ∈ ω such that σ(j) ∉ Σ_{p} for every j ≥ i then s_{i}(p) ∈ F_{p}, where s_{i} = ρ(i). (ii) If σ(j) ∈ Σ_{p} for infinitely many j then for infinitely many i it is the case

that s_{i}(p) ∈ F_{p}^{ω}, where s_{i} = ρ(i).

We define L_{seq}(A), the language of infinite words accepted by A to be the set of all words σ such that there exists an accepting run of A over σ. The distributed nature of T S together with the basic properties of the maps str and trs defined earlier lead to the next result.

Theorem 2.3 For any A2-automaton A, L_{T r}(A) = {str(σ) | σ ∈ L_{seq}(A)}. Consequently L_{T r}(A) ≠ ∅ iff L_{seq}(A) ≠ ∅.

Similar statements hold, of course, for A0-automata and A1-automata.

All the A2-automata that we construct in the next section will be in standard form. So assume that A = (T S, T ) is an A2-automaton in standard form with T S = ({S_{p}}, {→_{a}}, S_{in}) and T = {(F_{p}^{ω}, F_{p})}. Construct the directed graph G_{A} = (S_{P}, E_{A}) where S_{P} is the set of global states of T S and (s, s′) ∈ E_{A} if there exists a ∈ Σ such that s ⟶^{a}_{T S} s′. We also label each edge in G_{A} with a set of processes. Let π : E_{A} → 2^{P} be given by π((s, s′)) = ⋃{loc(a) | s ⟶^{a}_{T S} s′}.

We call X ⊆ S_{P} a good component iff X is a maximal strongly connected component in G_{A} which meets one the following conditions for each p.

(i) There exists s ∈ X such that s(p) ∈ F_{p}. (Because A is in standard form this implies that s′(p) = s′′(p) ∈ F_{p} for every s′, s′′ ∈ X).

(ii) There exists s ∈ X such that s(p) ∈ F_{p}^{ω} and for some s′ ∈ X, (s′, s) ∈ E_{A} and p ∈ π((s′, s)).

From Theorem 2.3 we know that L_{T r}(A) is non-empty iff L_{seq}(A) is. It is not difficult to prove that L_{seq}(A) is non-empty iff G_{A} has a good component. It is known that the maximal strongly connected components of a digraph can be computed in time which is linear in the size of the digraph [AHU]. Clearly, the size of G_{A} is bounded by the number of global states of A. As a consequence it is easy to derive the next result.

Theorem 2.4 Let A be an A2-automaton in standard form. Then L_{T r}(A) ≠ ∅ iff G_{A} has a good component. For p ∈ P, let n_{p} = |S_{p}| denote the number of p-states. Let n = max{n_{p}}_{p∈P} and m = |P|. Then checking that G_{A} has a good component can be done in time O(m^{2n}).

We conclude this section with a few remarks on deterministic automata over infinite traces. As with automata on infinite words, non-deterministic A2automata on infinite traces are strictly more expressive than deterministic A2automata. In the absence of determinacy, complementation is difficult. When applying these automata to settle questions in logic, complementation is often required to handle negation in formulas. (Fortunately, the automata-theoretic treatment of linear time temporal logic on traces which we will describe here does not require complementation.)

To obtain determinacy without loss of expressive power one must use a more sophisticated acceptance criterion corresponding to the Muller, Rabin or Streett acceptance conditions for infinite words. Here, we will look only at the Muller acceptance condition.

(M) T = {T_{1}, …, T_{n}} with T_{i} = {F_{p}^{i}} and F_{p}^{i} ⊆ S_{p} for each i and each p. A run ρ over F ∈ T R^{ω} is accepting with respect to M iff there exists T_{i} ∈ T such that inf_{p}(ρ) = F_{p}^{i} for each p.

Diekert and Muscholl [DM] showed that deterministic M-automata are as expressive as non-deterministic A1-automata. Their proof however does not lead to a determinization construction for A1-automata.

There are two independent solutions available in the literature for the difficult problem of complementing A1-automata. Muscholl first showed how to directly construct a non-deterministic A1-automaton which is the complement of the given automaton [Mus]—this approach does not yield a determinization construction for A1-automata. In [Mus] the complementation is carried out for asynchronous cellular Büchi automata, in which there is one agent for each letter. To transport this complementation result to A1-automata, one has to resort to a simulation which carries non-trivial overheads in the size of the alphabet. The second solution due to Klarlund, Mukund and Sohoni [KMS] is a direct determinization construction for A1-automata which then easily leads to the complementation result. In both cases, the blow-up in the local state space of each process is exponential in the global state space of the original automaton, which is essentially optimal. Surprisingly in both [Mus] and [KMS], the A1 acceptance condition must be first transformed into an equivalent one which describes in considerable detail the communication patterns established by the infinite trace that is being examined for acceptance.

3 Linear Time Temporal Logics over Traces

A variety of linear time temporal logics to be interpreted over traces have been proposed in the literature. As mentioned in the Introduction, our focus here will be on those logics which meet the following criteria:

(i) The logic should be expressible within the first order theory of traces. (ii) The logic should admit a treatment in terms of asynchronous Büchi automata

of one kind or the other.

We begin with the logic TrPTL (Trace based Propositional Temporal logic of Linear time). This is the earliest and—to date—the most expressive linear time logic of the chosen kind. For a detailed treatment of this logic the reader is referred to [Thi1]. After presenting TrPTL we will consider two subsystems denoted TrPTL^{con} (connected TrPTL) and TrPTL^{⊗} (product TrPTL). These subsystems are obtained by placing suitable syntactic restrictions on the formulas. The interesting point is that these restrictions result in proportionate simplification of the automata theoretic constructions associated with the logics. Towards the end of the section we will take a quick look at other temporal logics that have been proposed with traces as the underlying frames.

Henceforth, it will be notationally convenient to deal with distributed alphabets in which the names of the processes are positive integers. Through this section and the next, we fix a distributed alphabet Σ̃ = {Σ_{i}}_{i∈P} with P = {1, 2, …, K} and K ≥ 1. We let i, j and k range over P. As before, let P, Q range over non-empty subsets of P. The trace alphabet induced by Σ̃ is denoted (Σ, I). We assume the terminology and notations developed in the previous sections. In particular when dealing with a P-indexed family {X_{i}}_{i∈P}, we will often write just {X_{i}}.

The logic TrPTL is parameterized by the class of distributed alphabets. Having fixed Σ̃ we shall often almost always write TrPTL to mean TrPTL(Σ̃), the logic associated with Σ̃. Fix a set of atomic propositions AP with p, q ranging over AP. Then Φ_{TrPTL(_{Σ})}, the set of formulas of TrPTL(Σ̃), is defined inductively via:

• For p ∈ AP and i ∈ P, p(i) is a formula (which is to be read “p at i”).

• If α and β are formulas, so are ¬α and α ∨ β.

• If α is a formula and a ∈ Σ_{i} then ⟨a⟩_{i}α is a formula.

• If α and β are formulas so is α U_{i}β.

From now on, we denote Φ_{TrPTL(_{Σ})} as just Φ. In the semantics of the logic which will be based on infinite traces, the i-view of a configuration will play a crucial role. Let F ∈ T R^{ω} with F = (E, ≤, λ). Recall that E_{i} = {e | e ∈ E and λ(e) ∈ Σ_{i}}. Let c ∈ C_{F} and i ∈ P. Then ↓^{i}(c) is the i-view of c and it is defined as:

↓^{i}(c) =↓(c ∩ E_{i}).

We note that ↓^{i}(c) is also a configuration. It is the “best” configuration that the agent i is aware of at c. We say that ↓^{i}(c) is an i-local configuration. Let C_{F}^{i} = {↓^{i}(c) | c ∈ C_{F} } be the set of i-local configurations. For Q ⊆ P and c ∈ C_{F}, we let ↓^{Q}(c) denote the set ⋃{↓^{i}(c) | i ∈ Q}. Once again, ↓^{Q}(c) is a configuration. It represents the collective knowledge of the processes in Q about the configuration c.

The following basic properties of traces follow directly from the definitions.

Proposition 3.1 Let F = (E, ≤, λ) be an infinite trace. The following statements hold.

(i) Let ≤_{i} = ≤ ∩(E_{i} × E_{i}). Then (E_{i}, ≤_{i}) is a linear order isomorphic to ω if E_{i} is infinite and isomorphic to a finite initial segment of ω if E_{i} is finite.

(ii) (C_{F}^{i} , ⊆) is a linear order. In fact (C_{F}^{i} − {∅}, ⊆) is isomorphic to (E_{i}, ≤_{i}). (iii) Suppose ↓^{i}(c) ≠ ∅ where c ∈ C_{F}. Then there exists e ∈ E_{i} such that ↓^{i}(c) =↓e.

In fact e is the ≤_{i}-maximum event in (c ∩ E_{i}). (iv) Suppose Q ⊆ Q′ ⊆ P and c ∈ C_{F}. Then ↓^{Q}(c) =↓^{Q}(↓^{Q′}(c)). In particular,

for a single process i, ↓^{i}(c) =↓^{i}(↓^{i}(c)).

We can now present the semantics of TrPTL. A model is a pair M = (F, {V_{i}}_{i∈p}) where F = (E, ≤, λ) ∈ T R^{ω} and V_{i} : C_{F}^{i} → 2^{AP} is a valuation function which assigns a set of atomic propositions to i-local configurations for each process i. Let c ∈ C_{F} and α ∈ Φ. Then M, c ⊧ α denotes that α is satisfied at c in M and it is defined inductively as follows:

• M, c ⊧ p(i) for p ∈ AP iff p ∈ V_{i} (↓^{i}(c)).

• M, c ⊧ ¬α iff M, c |̸= α.

• M, c ⊧ α ∨ β iff M, c ⊧ α or M, c ⊧ β • M, c ⊧ ⟨a⟩_{i}α iff there exists e ∈ E_{i} − c such that λ(e) = a and M, ↓e ⊧ α.

Moreover, for every e′ ∈ E_{i}, e′ < e iff e′ ∈ c.

• M, c ⊧ α U_{i}β iff there exists c′ ∈ C_{F} such that c ⊆ c′ and M, ↓^{i}(c′) ⊧ β. Moreover, for every c′′ ∈ C_{F}, if ↓^{i}(c) ⊆↓^{i}(c′′) ⊂↓^{i}(c′) then M, ↓^{i}(c′′) ⊧ α.

Thus TrPTL is an action based agent-wise generalization of LTL. Indeed both in terms of its syntax and semantics, LTL corresponds to the case where there is only one agent and where this agent can execute only one action at any time. With P = {1} and Σ_{1} = {a_{0}} one then writes p instead of p(1), Oα instead of ⟨a_{0}⟩α and α Uβ instead of α U_{i}β. The semantics of TrPTL when specialized down to this case yields the usual LTL semantics. In the next section we will say more about the relationship between TrPTL and LTL.

Returning to TrPTL, the assertion p(i) says that the i-view of c satisfies the atomic proposition p. Observe that we could well have p(i) satisfied at c but not p(j) (with i ≠ j). It is interesting to note that all atomic assertions (that we know of) concerning distributed behaviours are local in nature. Indeed, it is well-known that global atomic propositions will at once lead to an undecidable logic in the current setting [LPRT, Pen].

Suppose M = (F, {V_{i}}) is a model and c ⟶^{a}_{F} c′ with j ∉ loc(a). Then M, c ⊧ p(j) iff M, c′ ⊧ p(j). In this sense the valuation functions are local. There are, of course, a number of equivalent ways of formulating this idea which we will not get into here.

The assertion ⟨a⟩_{i}α says that the agent i will next participate in an a-event. Moreover, at the resulting i-view, the assertion α will hold. The assertion α U_{i}β says that there is a future i-view (including the present i-view) at which β will hold and for all the intermediate i-views (if any) starting from the current i-view, the assertion α will hold.

Before considering examples of TrPTL specifications, we will introduce some notation. We let α, β with or without subscripts range over Φ. Abusing notation, we will use loc to denote the map which associates a set of locations with each formula.

• loc(p(i)) = loc(⟨a⟩_{i}α) = loc(α U_{i}β) = {i}.

• loc(¬α) = loc(α).

• loc(α ∨ β) = loc(α) ∪ loc(β).

In what follows, Φ^{i} = {α | loc(α) = {i}} is the set of i-type formulas. A basic observation concerning the semantics of TrPTL can be phrased as follows:

Proposition 3.2 Let M = (F, {V_{i}}) be a model, c ∈ C_{F} and α a formula such that loc(α) ⊆ Q. Then M, c ⊧ α iff M, ↓^{Q}(c) ⊧ α.

A corollary to this result is that in case α ∈ Φ^{i} then M, c ⊧ α iff M, ↓^{i}(c) ⊧ α. As a result, the formulas in Φ^{i} can be used in exactly the same manner as one would use LTL (in the setting of sequences) to express properties of the agent i. Boolean combinations of such local assertion can be used to capture various interaction patterns between the agents implied by the logical connectives as well as the coordination enforced by the distributed alphabet Σ̃.

For writing specifications, apart from the usual derived connectives of propositional calculus such as ∧, ⇒ and ≡, the following operators are also available

• ⊤ =^{△} p_{1}(1) ∨ ¬p_{1}(1) denotes the constant “True”, where AP = {p_{1}, p_{2}, …}. We use ⊥ = ¬⊤ to denote “False”. .

• ◇_{i}α =^{△} ⊤ U_{i}α is a local version of the ◇ modality of LTL.

• □_{i}α =^{△} ¬◇_{i}¬α is a local version of the □ modality of LTL..

• Let X ⊆ Σ_{i} and \overline{X} = Σ_{i} − X. Then α U_{i}^{X}β =^{△} (α ∧ ⋀_{a∈\overline{X}}[a]_{i}⊥) U_{i}β. In

other words α U_{i}^{X}β is fulfilled using (at most) actions taken from X. We set

◇_{i}^{X}α =^{△} ⊤ U_{i}^{X}α and □_{i}^{X}α =^{△} ¬◇_{i}^{X}¬α.

• α(i) =^{△} α U_{i}α (or equivalently ⊥ U_{i}α). α(i) is to be read as “α at i”. If M = (F, {V_{i}}) is a model and c ∈ C_{F} then M, c ⊧ α(i) iff M, ↓^{i}(c) ⊧ α. It could of course be the case that loc(α) ≠ {i}.

A simple but important observation is that every formula is a boolean combination of formulas taken from ⋃_{i∈P} Φ^{i}. In TrPTL we can say that a specific global configuration is reachable from the initial configuration. Let {α_{i}}_{i∈P} be a family with α_{i} ∈ Φ^{i} for each i. Then we can define a derived connective ◇(α_{1}, α_{2}, …, α_{K}) which has the following semantics at the empty configuration. Let M = (F, {V_{i}}) be a model. Then M, ∅ ⊧ ◇(α_{1}, α_{2}, …, α_{k}) iff there exists c ∈ C_{F} such that M, c ⊧ α_{1} ∧ α_{2} ∧ ⋯ ∧ α_{K}.

To define this derived connective set Σ′_{1} = Σ_{1} and, for 1 < i ≤ K, set Σ′_{i} = Σ_{i} − ∪{Σ_{j} | 1 ≤ j < i}. Then ◇(α_{1}, α_{2}, …, α_{K}) is the formula:

◇_{1}^{Σ′_{1}}(α_{1} ∧ ◇_{2}^{Σ′_{2}}(α_{2} ∧ ◇_{3}^{Σ′_{3}}(α_{3} ∧ ⋯ ◇_{K}^{Σ′_{K}} α_{K})) ⋯).

The idea is that the sequence of actions leading up to the required configuration can be reordered so that one first performs all the actions in Σ_{1}, then all the actions in Σ_{2} − Σ_{1} etc. Hence, if now is an atomic proposition, the formula ◇(now(1), now(2), …, now(K)) is satisfied at the empty configuration iff there is a reachable configuration at which all the agents assert now.

Dually, safety properties that hold at the initial configuration can also be expressed. For example, let crt(i) be the atomic assertion declaring that the agent i is currently in its critical section. Then it is possible to write a formula φ_{ME} which asserts that at all reachable configurations at most one agent is in its critical section, thereby guaranteeing that the system satisfies the mutual exclusion property. We omit the details of how to specify φ_{ME}.

On the other hand, it seems difficult to express nested global and safety properties in TrPTL. This is mainly due to the local nature of the modalities which results in information about the past sneaking into the semantics even though there are no explicit past operators in the logic. In particular, TrPTL admits formulas that are satisfiable but not root-satisfiable.

A formula α is said to be root-satisfiable iff there exists a model M such that M, ∅ ⊧ α. On the other hand, α is said to be satisfiable iff there exists a model M = (F, {V_{i}}) and c ∈ C_{F} such that M, c ⊧ α. It turns out that these two notions are not equivalent. Consider the distributed alphabet Σ̃_{0} = {Σ_{1}, Σ_{2}} with Σ_{1} = {a, d} and Σ_{2} = {b, d}. Then it is not difficult to verify that the formula p(2)(1) ∧ □_{2}¬p(2) is satisfiable but not root-satisfiable. (Recall that p(2)(1) abbreviates ⊥ U_{1}p(2)). One can however transform every formula α into a formula α′ such that α is satisfiable iff α′ is root satisfiable.

This follows from the observation that every α can be expressed as a boolean combination of formulas taken from the set ⋃_{i∈P} Φ^{i}. Hence the given formula α can be assumed to be of the form α = ⋁_{j=1}^{m}(α_{j1} ∧α_{j2} ∧⋯∧α_{jK}) where α_{ji} ∈ Φ^{i} for each j ∈ {1, 2, …, m} and each i ∈ P. Now convert α to the formula α′ where α′ = ⋁_{j=1}^{m} ◇(α_{j1}, α_{j2}, ⋯, α_{jK}). (Recall the derived modality ◇(α_{1}, α_{2}, …, α_{K}) introduced earlier.) From the semantics of ◇(α_{1}, α_{2}, …, α_{K}) it follows that α is satisfiable iff α′ is root-satisfiable.

Hence, in principle, it suffices to consider only root-satisfiability in developing a decision procedure for TrPTL. There is of course a blow-up involved in converting satisfiable formulas to root-satisfiable formulas. If one wants to avoid this blow-up then the decision procedure for checking root-satisfiability can be suitably modified to yield a direct decision procedure for checking satisfiability as done in [Thi1]. In any case, it is root satisfiability which is of importance from the standpoint of model checking. Hence here we shall only develop a procedure for deciding if a given formula of TrPTL is root-satisfiable.

As a first step we augment the syntax of our logic by one more construct.

• If α is a formula, so is O_{i}α. In the model M = (F, {V_{i}}), at the configuration c ∈ C_{F}, M, c ⊧ O_{i}α iff M, c ⊧ ⟨a⟩_{i}α for some a ∈ Σ_{i}. We also define loc(O_{i}α) = {i}.

Thus O_{i}α ≡ ⋁_{a∈Σ_{i}}⟨a⟩_{i}α is a valid formula and O_{i} is expressible in the former syntax. It will be however more efficient to admit O_{i} as a first class modality.

Fix a formula α_{0}. Our aim is to effectively associate an A2-automaton A_{α_{0}} with α_{0} such that α_{0} is root-satisfiable iff L_{T r}(A_{α_{0}}) ≠ ∅. Since the emptiness problem for A2-automata is decidable (Theorem 2.4), this will yield the desired decision procedure. Let CL′(α_{0}) be the least set of formulas containing α_{0} which satisfies:

• ¬β ∈ CL′(α_{0}) implies β ∈ CL′(α_{0}).

• α ∨ β ∈ CL′(α_{0}) implies α, β ∈ CL′(α_{0}).

• ⟨a⟩_{i}α ∈ CL′(α_{0}) implies α ∈ CL′(α_{0}).

• O_{i}α ∈ CL′(α_{0}) implies α ∈ CL′(α_{0}).

• α U_{i}β ∈ CL′(α_{0}) implies α, β ∈ CL′(α_{0}). In addition, O_{i}(α U_{i}β) ∈ CL′(α_{0}).

We then define CL(α_{0}) to be the set CL′(α_{0}) ∪ {¬β | β ∈ CL′(α_{0})}.

Thus CL(α_{0}), sometimes called the Fisher-Ladner closure of α_{0}, is closed under negation with the convention that ¬¬β is identified with β. From now we shall write CL instead of CL(α_{0}).

A ⊆ CL is called an i-type atom iff it satisfies:

• ∀α ∈ CL. α ∈ A iff ¬α ∉ A.

• ∀α ∨ β ∈ CL. α ∨ β ∈ A iff α ∈ A or β ∈ A.

• ∀α U_{i}β ∈ CL. α U_{i}β ∈ A iff β ∈ A or (α ∈ A and O_{i}(α U_{i}β) ∈ A).

• If ⟨a⟩_{i}α, ⟨b⟩_{i}β ∈ A_{i} then a = b.

AT_{i} denotes the set of i-type atoms. We now need to define the notion of a formula in CL being a member of a collection of atoms. Let α ∈ CL and {A_{i}}_{i∈Q} be a family of atoms with loc(α) ⊆ Q and A_{i} ∈ AT_{i} for each i ∈ Q. Then the predicate α ∈ {A_{i}}_{i∈Q} is defined inductively as:

• If loc(α) = {j} then α ∈ {A_{i}}_{i∈Q} iff α ∈ A_{j}.

• If α = ¬β then α ∈ {A_{i}}_{i∈Q} iff β ∉ {A_{i}}_{i∈Q}.

• If α = α_{1} ∨ α_{2} then α_{1} ∨ α_{2} ∈ {A_{i}}_{i∈Q} iff α_{1} ∈ {A_{i}}_{i∈Q} or α_{2} ∈ {A_{i}}_{i∈Q}.

The construction of the A2-automaton A_{α_{0}} is guided by the construction due to Vardi and Wolper for LTL [VW]. However in the much richer setting of traces it turns out that one must make crucial use of the latest information that the agents have about each other when defining the transitions of A_{α_{0}}. It has been shown by Mukund and Sohoni [MS] that this information can be kept track of by a deterministic A2-automaton whose size depends only on Σ̃. (Actually the automaton described in [MS] operates over finite traces but it is a trivial task to convert it into A2-automaton having the desired properties). To bring out the relevant properties of this automaton, let F ∈ T R^{ω} with F = (E, ≤, λ). For each subset Q of processes, the function latest_{F,Q} : C_{F} × P → Q is given by latest_{F,Q}(c, j) = ℓ iff ℓ is the least member of Q (under the usual ordering over the integers) with the property ↓^{j}(↓^{q}(c)) ⊆ ↓^{j}(↓^{ℓ}(c)) for every q ∈ Q. In other words, among the agents in Q, ℓ has the best information about j at c, with ties being broken by the usual ordering over integers.

Theorem 3.3 ([MS]) There exists an effectively constructible deterministic A2automaton A_{Γ} = (T S, T ) with T S = ({Γ_{i}}, {⇒_{a}}, Γ_{in}) such that:

(i) L_{T r}(A_{Γ}) = T R^{ω}. (ii) For each Q = {i_{1}, i_{2}, …, i_{n}}, there exists an effectively computable function

gossip_{Q} : Γ_{i_{1}} × Γ_{i_{2}} × ⋯ × Γ_{i_{n}} × P → Q such that for every F ∈ T R^{ω}, every c ∈ C_{F} and every j ∈ P, latest_{F,Q}(c, j) = gossip_{Q}(γ(i_{1}), …, γ(i_{n}), j) where ρ_{F} (c) = γ and ρ_{F} is the unique (accepting) run of A_{Γ} over F.

Henceforth, we refer to A_{Γ} as the gossip automaton. Each process in the gossip automaton has 2^{O(K^{2} log K)} local states, where K = |P|. Moreover the function g_{Q} can be computed in time which is polynomial in the size of K.

Each i-state of the automaton A_{α_{0}} will consist of an i-type atom together with an appropriate i-state of the gossip automaton. Two additional component will be used to check for liveness requirements. One component will take values from the set N_{i} = {0, 1, 2, …, |U_{i}|} where U_{i} = {α U_{i}β | α U_{i}β ∈ CL}. This component will be used to ensure that all “until” requirements are met. The other component will take values from the set {on,off}. This will be used to detect when an agent has quit.

The automaton A_{α_{0}} can now be defined.

Definition 3.4 A_{α_{0}} = (T S, T ), where T S = ({S_{i}}, {→_{a}}, S_{in}) and T = {(F_{i}^{ω}, F_{i})} are defined as follows:

(i) For each i, S_{i} = AT_{i}×Γ_{i}×N_{i}× {on,off}. Recall that Γ_{i} is the set of i-states of the gossip automaton and N_{i} = {0, 1, 2, …, |U_{i}|} with U_{i} = {α U_{i}β | α U_{i}β ∈ CL}.

(ii) Let s_{a}, s′_{a} ∈ S_{a} with s_{a}(i) = (A_{i}, γ_{i}, n_{i}, v_{i}) and s′_{a}(i) = (A′_{i}, γ′_{i}, n′_{i}, v′_{i}) for each i ∈ loc(a). Then (s_{a}, s′_{a}) ∈ →_{a} iff the following conditions are met.

(1) (γ_{a}, γ′_{a}) ∈ ⇒_{a} (recall that {⇒_{a}} is the family of transition relations of the gossip automaton) where γ_{a}, γ′_{a} ∈ Γ_{a} such that γ_{a}(i) = γ_{i} and γ′_{a}(i) = γ′_{i} for each i ∈ loc(a).

(2) ∀i, j ∈ loc(a), A′_{i} = A′_{j}.

(3) ∀i ∈ loc(a) ∀⟨a⟩_{i}α ∈ CL. ⟨a⟩_{i}α ∈ A_{i} iff α ∈ A′_{i}.

(4) ∀i ∈ loc(a) ∀O_{i}α ∈ CL. O_{i}α ∈ A iff α ∈ A′_{i}.

(5) ∀i ∈ loc(a)∀⟨b⟩_{i}β ∈ CL. If ⟨b⟩_{i}β ∈ A_{i} then b = a.

(6) Suppose j ∉ loc(a) and β ∈ CL with loc(β) = {j}. Further suppose that loc(a) = {i_{1}, i_{2}, …, i_{n}}. Then β ∈ A′_{i} iff β ∈ A_{ℓ} where ℓ = gossip_{loc(a)}(γ_{i_{1}}, γ_{i_{2}}, …, γ_{i_{n}}, j).

(7) Let i ∈ loc(a), U_{i} = {α_{1} U_{i}β_{1}, α_{2} U_{i}β_{2}, …, α_{n_{i}} U_{i}β_{n_{i}}}. Then u′_{i} and u_{i} are related to each other via:

u′_{i} = \{ \begin{matrix}(u_{i}+1) mod (n_{i}+1), & if u_{i} = 0 or β_{u_{i}} ∈ A_{i} or α_{u_{i}} U_{i}β_{u_{i}} ∉ A_{i} \\ u_{i}, & otherwise \end{matrix}

(8) For each i ∈ loc(a), v_{i} = on. Moreover, if v′_{i} = off then ⟨a⟩_{i}α ∉ A′_{i} for

every i ∈ loc(a) and every ⟨a⟩_{i}α ∈ CL. (iii) Let s ∈ S_{P} with s(i) = (A_{i}, γ_{i}, u_{i}, v_{i}) for every i. Then s ∈ S_{in} iff α_{0} ∈

{A_{i}}_{i∈P} and γ ∈ Γ_{in} where γ ∈ Γ_{P} satisfies γ(i) = γ_{i} for every i. Furthermore, u_{i} = 0 for every i. Finally, for every i, v_{i} = off implies that ⟨a⟩_{i}α ∉ A_{i} for every ⟨a⟩_{i}α ∈ CL.

(iv) For each i, F_{i}^{ω} ⊆ S_{i} is given by F_{i}^{ω} = {(A_{i}, γ_{i}, u_{i}, v_{i}) | u_{i} = 0 and v_{i} = on} and F_{i} ⊆ S_{i} is given by F_{i} = {(A_{i}, γ_{i}, u_{i}, v_{i}) | v_{i} = off}.

The automaton A_{α_{0}} extends the automata theoretic construction for LTL described in [VW] to the setting of TrPTL. The main new feature is the use of the gossip automaton in step (ii)(6) when dealing with formulas located at agents not taking part in the current action. A detailed explanation of A_{α_{0}} can be found in [Thi1].

This construction differs from the original construction for TrPTL presented in [Thi1] in a number of ways. Each S_{i} in [Thi1] was defined to be AT_{1} × AT_{2} × ⋯ × AT_{K} × Ũ_{i} × {act_{i}^{+}, act_{i}^{−}, stop_{i}} with Ũ_{i} as the set of subsets of U_{i}. The acceptance condition used was A1. Using A2, we need just two elements {on, off} to record when an agent has quit. Using the counter N_{i} instead of Ũ_{i} leads to a more compact description of A_{α_{0}}. The significant improvement, namely, replacing AT_{1} × AT_{2} × ⋯ × AT_{K} by just AT_{i} is due to Narayan Kumar [Nar]. The arguments described in [Thi1] go through in the present setting with minor modifications. These arguments lead to the next set of results.

Theorem 3.5

(i) α_{0} is root-satisfiable iff L_{T r}(A_{α_{0}}) ≠ ∅. (ii) The number of local states of A_{α_{0}} is bounded by 2^{O(max(n,m^{2} log m))} where

n = |α_{0}| and m is the number of agents mentioned in α_{0}. Clearly, m ≤ n. It follows that the root-satisfiability problem (and in fact the satisfiability problem) for TrPTL is solvable in time 2^{O(max(n,m^{2} log m)·m)}.

The number of local states of each process in A_{α_{0}} is determined by two quantities: the length of α_{0} and the size of the gossip automaton A_{Γ}. As far as the size of A_{Γ} is concerned, it is easy to verify that we need to consider only those agents in P that are mentioned in loc(α_{0}), rather than all agents in the system.

The model checking problem for TrPTL can be phrased as follows. A finite state distributed program over Σ̃ is a pair P r = (A_{P r}, V_{P r}) where A_{P r} = (({S_{i}^{P r}}, {⇒_{a}^{P r}}, S_{in}^{P r}), {(S_{i}, S_{i})}) is an A2-automaton modelling the state space of P r and V_{P r} : S → 2^{AP} is an interpretation of the atomic propositions over the local states of the program. (In this context, one assumes AP to be a finite set.)

Let ρ be a run of A_{P r} over F = (E, ≤, λ). Then ρ induces the model M_{ρ} via V_{P r} as follows: M_{ρ} = (F, {V_{i}^{ρ}}) where for each i and each c ∈ C_{F}, V_{i}^{ρ}(↓^{i}(c)) = V_{P r}(s_{i}) ∩ P, where s = ρ(c) and s_{i} = s(i). Viewing a formula α_{0} as a specification, we say that P r meets the specification α_{0}—denoted P r ⊧ α_{0}— if for every F ∈ T r^{ω} and for every run ρ of A_{P r} over F, it is the case that M_{ρ}, ∅ ⊧ α_{0}.

The model checking problem is to determine whether P r ⊧ α_{0}. This problem can be solved by “intersecting” the program automaton A_{P r} with the formula automaton A_{¬α_{0}} to yield an automaton A such that L_{T r}(A) = L_{T r}(A_{P r}) ∩ L_{T r}(A_{¬α_{0}}). It turns out that L_{T r}(A) = ∅ iff P r ⊧ α_{0}. It is easy to construct A. The only point to care of is that the i-local states of A should consist of only those pairs (s_{i}, s′_{i}) (where s_{i} is an i-local state of A_{P r} and s′_{i} = (A′_{i}, γ′_{i}, n′_{i}, v′_{i}) is an i-local state of A_{¬α_{0}}) such that V_{P r}(s_{i}) ∩ AP = A_{i} ∩ AP. The details can be found in [Thi1].

It turns out that this model checking problem has time complexity O(|A_{P r}| · 2^{O(max(n,m^{2} log m)·m)}) where |A_{P r}| is the size of the global state space of the A2-automaton modelling the behaviour of the given program P r and, as before, n = |α_{0}| and m is the number of agents mentioned in α_{0}, where α_{0} is the specification formula.

We now turn to two interesting sublogics of TrPTL. The first is the sublogic TrPTL^{con}, which consists of the so called connected formulas of TrPTL. We define Φ_{TrPTL}^{con} (from now on written as Φ^{con}) to be the least subset of Φ satisfying the following conditions:

(i) p(i) ∈ Φ^{con} for every p ∈ P and every i ∈ P. (ii) If α, β ∈ Φ^{con}, so are ¬α and α ∨ β. (iii) If α ∈ Φ^{con} and a ∈ Σ_{i} such that loc(α) ⊆ loc(a) then ⟨a⟩_{i}α ∈ Φ^{con}. (iv) If α, β ∈ Φ^{con} with loc(α) = loc(β) = {i} then α U_{i}β ∈ Φ^{con}. Actually one

need only demand that loc(α), loc(β) ⊆ ⋂{loc(a) | a ∈ Σ_{i}} but this leads to notational complications that we wish to avoid here.

(v) If α ∈ Φ^{con} and loc(α) = {i} then O_{i}α ∈ Φ^{con}. (Once again one needs to just demand that α ⊆ ⋂{loc(a) | a ∈ Σ_{i}}.)

Connected formulas were first identified by Niebert and used by Huhn [Huh]. They have also been independently identified by Ramanujam [Ram]. Thanks to the syntactic restrictions imposed on the next state and until formulas, past information is not allowed to creep in. Indeed one can prove the following:

Proposition 3.6 Let α ∈ Φ^{con}. Then α is satisfiable iff α is root-satisfiable.

Yet another pleasing feature of TrPTL^{con} is that the gossip automaton can be eliminated in the construction of the automaton A_{α_{0}} whenever α_{0} ∈ Φ^{con}. In fact one can do a bit more.

Let α_{0} ∈ Φ^{con} and let CL_{i} = CL ∩ Φ^{i} for each i (recall that CL is an abbreviation for CL(α_{0})). We redefine an i-type atom to be a subset A of CL_{i} such that:

• ∀β ∈ CL_{i} β ∈ A iff ¬β ∉ A.

• ∀α ∨ β ∈ CL_{i}. α ∨ β ∈ A iff α ∈ A or β ∈ A.

• ∀α U_{i}β ∈ CL_{i} α U_{i}β ∈ A iff β ∈ A or α ∈ A and O_{i}(α U_{i}β) ∈ A.

As before (but with the new definition in operation!), AT_{i} is the set of i-type atoms.

Let α ∈ CL with loc(α) ⊆ Q. The notion of α belonging to a family of atoms {A_{i}}_{i∈Q}, with A_{i} ∈ AT_{i} for each i ∈ Q, is defined inductively in the obvious way—if loc(α) = {i} then α ∈ {A_{i}}_{i∈Q} iff α ∈ A_{i} etc. etc. The construction of A_{α_{0}} is as specified in Definition 3.4 with the following modifications:

(i) S_{i} = AT_{i} × N_{i}× {on,off} for each i ∈ P. Thus the gossip automaton is eliminated and AT_{i} is the set of i-type atoms of the new kind.

(ii) (1) This condition is obviously dropped. (2) Interestingly enough, this condition is also dropped.

(3) This condition is modified to ∀⟨a⟩_{i}α ∈ CL_{i}.⟨a⟩_{i}α ∈ A_{i} iff α ∈ {A′_{j}}_{j∈loc(a)}.

In addition, condition (ii)(6) is dropped, while conditions (ii)(4), (ii)(5), (ii)(7) and (ii)(8) remain unchanged. Parts (iii) and (iv) are modified to eliminate all references to the gossip automaton. After these alterations, it is not difficult to prove the following result.

Theorem 3.7 Let α_{0} ∈ Φ^{con} and A_{α_{0}} be constructed as detailed above.

(i) α_{0} is satisfiable iff L_{T r}(A_{α_{0}}) ≠ ∅. (ii) The satisfiability problem for TrPTL^{con} is solvable in time 2^{O(|α_{0}|)}.

Once again, a suitably modified statement can be made about the associated model checking problem. At present we do not know whether or not TrPTL is strictly more expressive than TrPTL^{con}. We shall formulate this question more rigorously in the next section.

Yet another sublogic of TrPTL is called product TrPTL and is denoted as TrPTL^{⊗}. Let Φ^{⊗}, the set of formulas of TrPTL^{⊗}, be the least subset of Φ which satisfies:

(i) p(i) ∈ Φ^{⊗} for every p ∈ P and every i ∈ P. (ii) If α, β ∈ Φ^{⊗} then so are ¬α and α ∨ β. (iii) If α ∈ Φ^{⊗} with loc(α) = {i} and a ∈ Σ_{i} then ⟨a⟩_{i}α ∈ Φ^{⊗}. (iv) If α, β ∈ Φ^{⊗} with loc(α) = loc(β) = {i} then α U_{i}β ∈ Φ^{⊗}.

Clearly Φ^{⊗} ⊆ Φ^{con} ⊆ Φ. In case α_{0} ∈ Φ^{⊗}, the automaton A_{α_{0}} can be simplified even further (than the case when α_{0} ∈ Φ^{con}). A_{α_{0}} essentially consists of a synchronized product of Büchi automata. A detailed treatment of TrPTL^{⊗} is provided in [Thi2]. The interest in this subsystem lies in the fact that the accompanying program model is particularly simple and commonplace. Namely, it consists of a fixed set of finite state transition systems that coordinate their behaviour by performing common actions together. Here we shall just sketch the construction for A_{α_{0}}.

A product Büchi automaton over Σ̃ is a structure A = ({T S_{i}}_{i∈P}, S_{in}, T ) where T S_{i} = (S_{i}, →_{i}) for each i with →_{i} ⊆ S_{i} × Σ_{i} × S_{i} as the local transition relation of the agent i. Everything else is as in the definition of an A2-automaton. Thus the key difference is that each agent comes with its own local transition relation. From these agent transition relations, one can derive the action indexed transition relations {→_{a}} as follows: (s_{a}, s′_{a}) ∈ →_{a} iff s_{a}(i) ⟶^{a} s′_{a}(i) for every i ∈ loc(a). Thus product Büchi automata are a (strict) subclass of the class of A2-automata.

Given α_{0} ∈ Φ^{⊗}, the construction of A_{α_{0}} proceeds as in the case where α_{0} ∈ Φ^{con}. The only difference is, we must define the transition relations {→_{i}}_{i∈P} instead of the transition relations {→_{a}}_{a∈Σ}. This can be done as follows:

Let s_{i}, s′_{i} ∈ S_{i} with s_{i} = (A_{i}, u_{i}, v_{i}) and s′_{i} = (A′_{i}, u′_{i}, v′_{i}). Let a ∈ Σ_{i}. Then s_{i} ⟶^{a_{i}} s′_{i} iff the following conditions are satisfied:

(i) ∀⟨a⟩_{i}α ∈ CL. ⟨a⟩_{i}α ∈ A_{i} iff α ∈ A′_{i}. (ii) ∀O_{i}α ∈ CL. O_{i}α ∈ A iff α ∈ A′_{i}. (iii) If ⟨b⟩_{i}α ∈ A_{i} then b = a. (iv) u_{i} and u′_{i} are related to each other just as in part (ii)(7) of Definition 3.4.

(v) v_{i} and v′_{i} satisfy part (ii)(8) of Definition 3.4.

As shown in [Thi2] one can establish the following result for TrPTL^{⊗}.

Theorem 3.8 Let α_{0} ∈ Φ^{⊗} and A_{α_{0}} be constructed as above.

(i) α_{0} is satisfiable iff L_{T r}(A_{α_{0}}) ≠ ∅. (ii) The satisfiability problem for TrPTL^{⊗} can be solved in time 2^{O(|α_{0}|)}.

Once again, one can make suitably modified statements about the accompanying model checking problem. As mentioned earlier, the program model in this setting consists of a fixed set (one for each i) finite state transition systems.

We conclude this section with a quick look at some related logics. Katz and Peled introduced the logic ISTL [KP] which can be easily viewed as a temporal logic over traces. However, it has branching time modalities which permit quantification over the so called observations of a trace. ISTL uses global atomic propositions rather than local atomic propositions. Penczek has also studied a number of temporal logics (including a version of ISTL) with branching time modalities and global atomic propositions [Pen]. His logics are interpreted directly over the space of configurations of a trace resulting in a variety of axiomatizations and undecidability results. We feel that local atomic propositions (as used in TrPTL) are crucial for obtaining tractable partial order based temporal logics. Niebert has considered a μ-calculus version of TrPTL [Nie] and has obtained a decidability result using a variant of asynchronous Büchi automata. Since this logic uses “local” fixed points, it is not clear at present what is the expressive power of this logic. The four linear time temporal logics studied by Ramanujam in a closely related setting [Ram] can be easily captured as four sublogics of TrPTL through purely syntactic restrictions. Two of the resulting sublogics are TrPTL^{⊗} and TrPTL^{con}. It is not clear at present whether the other two logics admit a simpler treatment in terms of asynchronous Büchi automata (than the one for TrPTL).

The temporal logic of causality (TLC) proposed by Alur, Peled and Penczek is basically a temporal logic over traces [APP]. The concurrent structures used in [APP] as frames for TLC can be easily represented as traces over an appropriately chosen trace alphabet. The interesting feature of TLC is that its branching time modalities are interpreted over causal paths. In a trace (E, ≤, λ), the sequence e_{0}e_{1} ⋯ ∈ E^{∞} is a causal path if e_{0} ⋖ e_{1} ⋖ e_{2} · · ·. This logic is almost certainly not expressible within the first order theory of traces although it admits an elementary time (in fact essentially exponential time) decision procedure.

Finally, Ebinger has also proposed a linear time temporal logic to be interpreted over traces [Ebi]. An interesting property of this logic is that when its frames are restricted to be finite traces then it is exactly equivalent to the first order theory of finite traces. Unfortunately the decidability of this logic is settled using a translation into the first order theory of infinite traces. Hence the decision procedure has non-elementary time complexity.

4 Expressiveness Issues

Our main aim here is to show that TrPTL is expressible within the first order theory of traces. In order to simplify the presentation, we shall eliminate atomic propositions and instead use the single constant ⊤ standing for “True” (and ⊥ = ¬⊤ standing for “False”). The resulting logic will also be called TrPTL accompanied by the notations and terminology developed in the previous section. The function loc which assigns a set of processes to a formula works exactly as before except that we start with loc(⊤) = ∅. As will be seen later, this will entail minor changes in the definition of the syntax of TrPTL^{con} and TrPTL^{⊗}. For now, we repeat that the syntax of Φ, the set of formulas of TrPTL is now given by:

Φ ::= ⊤ | ¬α | α ∨ β | ⟨a⟩_{i}α | α U_{i}β.

As before, for ⟨a⟩_{i}α to be a formula we require a ∈ Σ_{i}. Local atomic propositions can be coded up into the actions and hence their elimination does not result in loss of expressive power.

A model is just an infinite trace F ∈ T R^{ω}. We set F, c ⊧ ⊤ for every c ∈ C_{F}. The rest of the semantics is as before. L_{α}, the ω-trace language defined by the formula α is given by, L_{α} = {F | F ∈ T R^{ω} and F, ∅ ⊧ α}. We say that L ⊆ T R^{ω} is TrPTL-definable iff there exists α ∈ Φ such that L = L_{α}.

First we shall compare the expressive powers of TrPTL, TrPTL^{con} and TrPTL^{⊗}. In order to do so, we must define the syntax of the two sublogics in the present setting. For TrPTL^{con} the only changes that are required are:

• ⊤ ∈ Φ^{con}.

• If α, β ∈ Φ^{con} such that loc(α), loc(β) ⊆ {i} then α U_{i}β ∈ Φ^{con}.

For TrPTL^{⊗}, the only changes that are required are

• ⊤ ∈ Φ^{⊗}.

• If α ∈ Φ^{⊗} such that loc(α) ⊆ {i} and if a ∈ Σ_{i} then ⟨a⟩_{i}α ∈ Φ^{⊗}.

• If α, β ∈ Φ^{⊗} with loc(α), loc(β) ⊆ {i} then α U_{i}β ∈ Φ^{⊗}.

The notion of L ⊆ T R^{ω} being TrPTL^{con}-definable or TrPTL^{⊗}-definable is formulated in the obvious way. Since Φ^{⊗} ⊆ Φ^{con} ⊆ Φ it is clear that TrPTL is at least as expressive as T rP T L^{con} which in turn is at least as expressive as T rP T L^{⊗}. As mentioned earlier we do not know at present if TrPTL is strictly more expressive than T rP T L^{con}, though we conjecture that this the case.

We do know however that TrPTL^{con} is strictly more expressive than TrPTL^{⊗}. To illustrate this it will be convenient to extend the notion of definability to subsets of Σ^{ω}. We say that L ⊆ Σ^{ω} is TrPTL-definable iff L is I-consistent and {str(σ) | σ ∈ L} is TrPTL-definable. This notion is defined for TrPTL^{con} and TrPTL^{⊗} in the obvious way. Hence in order to show that TrPTL^{con} is more expressive than TrPTL^{⊗} it suffices to exhibit some L ⊆ Σ^{ω} which is I-consistent and is TrPTL^{con}-definable but not TrPTL^{⊗}-definable.

Let Γ̃ = {Γ_{1}, Γ_{2}} with Γ_{1} = {a, a′, d} and Γ_{2} = {b, b′, d}. Let Γ = {a, a′, b, b′, d}. Consider L ⊆ Γ^{ω} given by:

L = (d(ab + ba + a′b′ + b′a′))^{ω}.

It turns out that L is not TrPTL^{⊗}-definable. Clearly L is I-consistent. As shown in [Thi2], for L to be TrPTL^{⊗}-definable, it must be a so-called (synchronized) product language. As a result, it would have to possess the following property:

(PR) Suppose σ ∈ Γ^{ω}. Then σ ∈ L iff there exist σ_{1}, σ_{2} ∈ L such that σ ↾Γ_{1} = σ_{1} ↾Γ_{1} and σ ↾Γ_{2} = σ_{2} ↾Γ_{2}.

Now let σ = (dab′)^{ω}, σ_{1} = (dab)^{ω} and σ_{2} = (da′b′)^{ω} . Clearly σ ↾Γ_{1} = σ_{1} ↾Γ_{1} and σ ↾Γ_{2} = σ_{2} ↾Γ_{2}. Since σ_{1}, σ_{2} ∈ L, this implies that σ ∈ L which it is not. Hence L cannot be a product language and therefore is not TrPTL^{⊗}-definable. On the other hand, it is a simple exercise to come up with a formula α ∈ Φ^{con} such that {str(σ) | σ ∈ L} = L_{α}.

We now turn to F O(Σ̃), the first order theory of infinite traces over Σ̃. One starts with a countable set of individual variables X = {x_{0}, x_{1}, …} with x, y, z with or without subscripts ranging over X. For each a ∈ Σ there is a unary predicate symbol R_{a}. There is also a binary predicate symbol ≤.

R_{a}(x) and x ≤ y are atomic formulas. If φ and φ′ are formulas, so are ¬φ, φ ∨ φ′ and (∃x)φ. The structures for this first order theory are elements of T R^{ω}. Let F ∈ T R^{ω} with F = (E, ≤, λ) and let I : X → E be an interpretation. Then F ⊧_{I}^{F O}R_{a}(x) iff λ(I(x)) = a and F ⊧_{I}^{F O} x ≤ y iff I(x) ≤ I(y). The remaining semantic definitions go along the expected lines. Each sentence φ (i.e., a formula with no free occurrences of variables) defines the ω-trace language L_{φ} = {F | F ⊧^{F O} φ}.

We say that L ⊆ T R^{ω} is F O-definable iff there exists a sentence φ in F O(Σ̃) such that L = L_{φ}. As before we will say that L ⊆ Σ^{ω} is F O-definable iff L is I-consistent and {str(σ) | σ ∈ L} is F O-definable.

Using the fact that LTL has the same expressive power as the first order theory of sequences, one can show that L ⊆ Σ^{ω} is F O-definable iff it is Iconsistent and LTL-definable [EM]. It will be worthwhile to pin down the notion of LTL-definability. In the current setting, remembering that (Σ, I) is the trace alphabet induced by Σ̃, we define the syntax of the logic LTL(Σ) as follows:

LTL(Σ) ::= ⊤ | ¬α | α ∨ β | ⟨a⟩α | α Uβ.

A model is a infinite word σ. For σ ∈ Σ^{ω} and n ∈ ω, the notion of α ∈ LTL(Σ) being satisfied at stage n is denoted by σ, n ⊧ α. This satisfaction relation is defined in the usual manner. The only point of interest might be that σ, n ⊧ ⟨a⟩α iff σ(n+1) = a and σ, n+1 ⊧ α. We say that L ⊆ Σ^{ω} is LTL-definable iff there exists α ∈ LTL(Σ) such L = L_{α} where L_{α} = {σ ∈ Σ^{ω} | σ, 0 ⊧ α}.

The result in [EM] relating F O-definable subsets of T R^{ω} and LTL-definable subsets of Σ^{ω} can now be phrased as follows.

Proposition 4.1 Let L ⊆ Σ^{ω}. Then, the following statements are equivalent.

(i) L is I-consistent and LTL-definable. (ii) {str(σ) | σ ∈ L} is an F O-definable subset of T R^{ω}.

We now wish to concentrate on showing that TrPTL is expressible within the first order theory of infinite traces.

To show this, we will freely use the standard derived connectives of Propositional Calculus, together with universal quantification and abbreviations such as x = y for (x ≤ y) ∧ (y ≤ x), x ≤ y ≤ z for (x ≤ y) ∧ (y ≤ z) etc.

An event e is an i-event iff λ(e) ∈ Σ_{i}. With this in mind, we let x ∈ E_{i} stand for the formula ⋁_{a∈Σ_{i}} R_{a}(x). The key to the result we are after is the observation that configurations of a trace can be described using predicates of bounded dimension. In what follows we let Q, Q′, Q′′ range over the non-empty subsets of P. For Q = {i_{1}, i_{2}, …, i_{n}}, the formula config({x_{i}}_{i∈Q}) is defined as:

config({x_{i}}_{i∈Q}) = (φ_{1} ∧ φ_{2} ∧ φ_{3}), where
φ_{1} = ⋀_{i∈Q} x_{i} ∈ E_{i},
φ_{2} = ⋀_{i,j} ⋀_{a}(R_{a}(x_{i}) ∧ R_{a}(x_{j})) ⇒ x_{i} = x_{j},
φ_{3} = ⋀_{i,j}(∀y) (y ∈ E_{j} ∧ y ≤ x_{i}) ⇒ y ≤ x_{j}.

We can now write down a formula describing prime configurations—recall that a prime configuration is one of the form ↓e, where e ∈ E. Let loc(a) ⊆ Q. Then the formula prime_{a}({x_{i}}_{i∈Q}) is defined as

config({x_{i}}_{i∈Q}) ∧ ⋀_{i∈loc(a)} ⋀_{j∈Q−loc(a)} R_{a}(x_{i}) ∧ (x_{j} ≤ x_{i}).

A careful examination of this formula along with the basic properties of traces at once leads to the next result.

Proposition 4.2 Let F = (E, ≤, λ) ∈ T R^{ω} and let I : X → E be an interpretation. Then F ⊧_{I}^{F O} prime_{a}({x_{i}}_{i∈Q}) iff there exists an a-event e such that for each j ∈ Q, I(x_{j}) is the ≤_{j}-maximum event in ↓e ∩ E_{j} and for each j ∉ Q, ↓e ∩ E_{j} = ∅.

For each α ∈ Φ we now define the sentence Sat(∅, α) and the set of formulas {Sat({x_{i}}_{i∈Q}, α) | {x_{i}}_{i∈Q} ⊆ X and ∅ ≠ Q ⊆ P} through simultaneous induction as follows:

• Sat(∅, ⊤) = Sat({x_{i}}_{i∈Q}, ⊤) = (∃x) x = x.

• Sat(∅, ¬α) = ¬Sat(∅, α).

Sat({x_{i}}_{i∈Q}, ¬α) = ¬Sat({x_{i}}_{i∈Q}, α).

• Sat(∅, α ∨ β) = Sat(∅, α) ∨ Sat(∅, β).

Sat({x_{i}}_{i∈Q}, α ∨ β) = Sat({x_{i}}_{i∈Q}, α) ∨ Sat({x_{i}}_{i∈Q}, β).

• Sat(∅, ⟨a⟩_{j}α) = ⋁_{Q⊇loc(a}(∃x_{i_{1}}, ∃x_{i_{2}}, …, ∃x_{i_{n}}) φ_{1} ∧ φ_{2} ∧ φ_{3} where Q = {i_{1}, i_{2}, …, i_{n}} and

φ_{1} = prime_{a}({x_{i}}_{i∈Q}),
φ_{2} = Sat({x_{i}}_{i∈Q}, α),
φ_{3} = (∀y) (y ∈ E_{j} ∧ y ≤ x_{j}) ⇒ y = x_{j}.

Sat({x_{i}}_{i∈Q}, ⟨a⟩_{j}α) is defined according to two cases.

Case 1 j ∉ Q: Sat({x_{i}}_{i∈Q}, ⟨a⟩_{j}α) = Sat(∅, ⟨a⟩_{j}α).

Case 2 j ∈ Q Sat({x_{i}}_{i∈Q}, ⟨a⟩_{j}α) = ⋁_{Q′⊇loc(a)}(∃y_{k_{1}}, ∃y_{k_{2}}, … ∃y_{k_{n}}) φ_{1} ∧ φ_{2} ∧ φ_{3} where Q′ = {k_{1}, k_{2}, …, k_{n}} and {y_{k}}_{k∈Q′} is disjoint from {x_{i}}_{i∈Q} and

φ_{1} = prime_{a}({y_{k}}_{k∈Q′}),
φ_{2} = Sat({y_{k}}_{k∈Q′}, α),
φ_{3} = ∀y (y ∈ E_{j} ⇒ (y < y_{j} ⇔ y ≤ x_{j})).

• Sat(∅, α U_{j}β) = Sat(∅, β) ∨ (Sat(∅, α) ∧ Sat(∅, ⋁_{a∈Σ_{j}}⟨a⟩_{j}α U_{j}β).

Sat({x_{i}}_{i∈Q}, α U_{j}β) is defined according to two cases.

Case 1 j ∉ Q: Sat({x_{i}}_{i∈Q}, α U_{j}β) = Sat(∅, α U_{j}β).

Case 2 j ∈ Q: Sat({x_{i}}_{i∈Q}, α U_{j}β) = ⋁_{a∈Σ_{j}} ⋁_{Q′⊇loc(a)}(∃y_{k_{1}}, ∃y_{k_{2}}, … ∃y_{k_{n}}) φ_{1} ∧ φ_{2} ∧ φ_{3} ∧ φ_{4} where Q′ = {k_{1}, k_{2}, …, k_{n}} and {y_{k}}_{k∈Q′} is disjoint from {x_{i}}_{i∈Q} and

φ_{1} = prime_{a}({y_{k}}_{k∈Q′}),
φ_{2} = x_{j} ≤ y_{j},
φ_{3} = Sat({y_{k}}_{k∈Q′}, β),
φ_{4} = ∀z(z ∈ E_{j} ∧ x_{j} ≤ z < y_{j}) ⇒ φ′_{4}.

where φ′_{4} = ⋁_{a∈Σ_{j}} ⋁_{Q′′⊇loc(a)}(∃z_{ℓ_{1}}, ∃z_{ℓ_{2}}, …, ∃z_{ℓ_{m}}) φ′_{41} ∧ φ′_{42} ∧ φ′_{43} with Q′′ = {ℓ_{1}, ℓ_{2}, …, ℓ_{m}} and {z_{ℓ}}_{ℓ∈Q′′} disjoint from both {x_{i}}_{i∈Q} and {y_{k}}_{k∈Q′} and

φ′_{41} = prime_{a}({z_{ℓ}}_{ℓ∈Q′′}),
φ′_{42} = (z = z_{j}),
φ′_{43} = Sat({z_{ℓ}}_{ℓ∈Q′′}, α).

Let f be the map which sends each formula in Φ to a sentence in F O(Σ̃) via f(α) = Sat(∅, α). Using the previous proposition and the semantics of TrPTL, it is not difficult to prove the following:

Theorem 4.3

(i) For every F ∈ T R^{ω}, F, ∅ ⊧ α iff F ⊧^{F O} f(α). (ii) If L ⊆ T R^{ω} is TrPTL definable then it is also F O(Σ̃)-definable.

As mentioned earlier we do not know at present if TrPTL is expressively complete—i.e., whether every L ⊆ T R^{ω} which is FO(Σ̃)-definable is also TrPTLdefinable. Clearly from Proposition 4.1 it follows that the expressive completeness of TrPTL can be characterized as follows:

Corollary 4.4 The following statements are equivalent:

(i) TrPTL is expressively complete. (ii) For every L ⊆ Σ^{ω}, if L is I-consistent and L is LTL-definable then L is

TrPTL definable.

We believe that TrPTL is not expressively complete. This leads to the following question: What is the linear time temporal logic of infinite traces? Such a logic should possess the following properties:

(TR1) It should be expressively complete. (TR2) It should admit a decision procedure (preferably in terms of asynchronous

Büchi automata) whose time complexity is 2^{p(n,m)} where n is the size of the input formula, m = |Σ| and p is a (low degree) polynomial in n and m.

(TR3) It should be possible to transparently express global liveness and safety properties in the logic.

It is worth noting that TrPTL and most of the decidable temporal logics over traces mentioned earlier such as [Nie] and [APP] cannot express all global invariant properties. The somewhat awkward semantics of the logic in [Ebi] also makes it event-based and hence not suitable for expressing invariant properties. However we believe that it should be possible to define a logic with a variant of the until operator defined in [Ebi] which will be able to capture global liveness and safety properties in a straightforward manner.

Any linear time temporal logic over traces which fulfills the properties (PR1)– (PR3) will be a very useful specification tool. In particular it will exactly capture properties that are expressible by I-consistent formulas in LTL—(α ∈ LTL(Σ) is I-consistent iff L_{α} is I-consistent). This is important because it is such properties which can be verified efficiently using partial order based verification methods [GW, Val].

5 Conclusion

In this paper we have considered linear time temporal logics over traces. Our emphasis has been on TrPTL and its two sublogics TrPTL^{con}, TrPTL^{⊗}. The choice of these logics has been mainly motivated by the fact that they are expressible within the first order theory of traces and the fact that they can be studied using asynchronous Büchi automata.

Our formulation of asynchronous Büchi automata in terms of the acceptance condition A2 appears to be particularly suited for logical studies. The present constructions are much more compact and transparent than the ones in [Thi1] which used A1 as the acceptance condition. We feel that, in the future, alternating versions of our automata will play an important role in the study of temporal logics over traces.

As we have mentioned a number of times, an important open problem is to pin down a linear time temporal logic for traces (assuming it exists!) which will fulfill the properties set out in the previous section. A solution to this problem will at once open up the possibility of investigating branching time temporal logics where path quantification is over traces.

References

[AHU] A.V. Aho, J.E. Hopcroft and J.D. Ullman: The Design and Analysis of Algorithms, Addison-Wesley, Reading (1974).

[APP] R. Alur, D. Peled and W. Penczek: Model-Checking of Causality Properties, Proc. 10th IEEE LICS (1994).

[Die] V. Diekert: Combinatorics on traces, LNCS 454 (1990).

[DM] V. Diekert and A. Muscholl: Deterministic Asynchronous Automata for Infinite Traces, Acta Inf., 31 (1993) 379-397.

[DR] V. Diekert, G. Rozenberg (Eds.): The Book of Traces, World Scientific, Singapore (1995).

[Ebi] W. Ebinger: Charakterisierunǵ von Sprachklassenunendlicher Spuren durch Logiken, Ph.D. Thesis, Institut für Informatik, Universität Stuttgart, Stuttgart, Germany (1994).

[EM] W. Ebinger and A. Muscholl: Logical Definability on Infinite Traces, Proc. ICALP ’93, LNCS 700 (1993) 335–346.

[GP] P. Gastin and A. Petit: Asynchronous Cellular Automata for Infinite Traces, Proc. ICALP ’92, LNCS 623 (1992) 583–594.

[GW] P. Godefroid and P. Wolper: A Partial Approach to Model Checking, Inform. and Comput., 110 (1994) 305–326.

[Huh] M. Huhn: On Semantic and Logical Refinement of Actions, Technical Report, Institut für Informatik, Universität Hildesheim, Germany (1996).

[KP] S. Katz and D. Peled: Interleaving Set Temporal Logic, Theor. Comput. Sci., 75 (3) (1992) 21–43.

[KMS] N. Klarlund, M. Mukund and M. Sohoni: Determinizing Büchi asynchronous automata, Proc. FST&TCS 1995, LNCS 1026 (1995) 456–470.

[LPRT] K. Lodaya, R. Parikh, R. Ramanujam and P.S. Thiagarajan: A logical study of distributed transition systems, Inform. and Comput., 119 (1995) 91–118.

[MP] Z. Manna and A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems (Specification), Springer-Verlag, Berlin (1991).

[Maz] A. Mazurkiewicz: Concurrent Program Schemes and their Interpretations, Report DAIMI-PB-78, Computer Science Department, Aarhus University, Denmark (1978).

[MS] M. Mukund and M. Sohoni: Keeping track of the latest gossip: Bounded time-stamps suffice, Proc. FST&TCS ’93, LNCS 761 (1993) 388–399.

[Mus] A. Muscholl: On the complementation of Büchi asynchronous cellular automata, Proc. ICALP ’94, LNCS 820 (1994) 142–153.

[Nar] K. Narayan Kumar: An Improved Decision Procedure for TrPTL, Unpublished Manuscript, Tata Institute of Fundamental Research, Bombay, India (1994).

[Nie] P. Niebert: A ν-Calculus with Local Views for Systems of Sequential Agents, Proc. MFCS’95, LNCS 969 (1995) 563–573.

[NPW] M. Nielsen, G.D. Plotkin and G. Winskel: Petri Nets, Event Structures and Domains I, Theor. Comput. Sci., 13 (1980) 86–108.

[Pen] W. Penczek: Temporal Logics for Trace Systems: On Automated Verification, Int. J. Found. of Comput. Sci., 4(1) (1993) 31-68.

[Pnu] A. Pnueli: The Temporal Logic of Programs, Proc. 18th IEEE FOCS (1977) 46–57.

[Ram] R. Ramanujam: Locally Linear Time Temporal Logic, To appear in Proc. 11th IEEE LICS (1996).

[Tho] W. Thomas: Automata on infinite objects, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, North-Holland, Amsterdam (1990) 133–191.

[Thi1] P.S. Thiagarajan: A Trace Based Extension of Linear Time Temporal Logic, Proc. 9th IEEE LICS (1994) 438–447. Full version available as: TrPTL: A Trace Based Extension of Linear Time Temporal Logic, Report TCS-93-6, School of Mathematics, SPIC Science Foundation, Madras, India (1993).

[Thi2] P.S. Thiagarajan: A Trace Consistent Subset of PTL, Proc. CONCUR’95, LNCS 962 (1995) 438-452. Full version available as: PTL over Product State Spaces, Report TCS-95-4, School of Mathematics, SPIC Science Foundation, Madras, India (1995).

[Val] A. Valmari: Stubborn Sets for Reduced State Space Generation, LNCS 483 (1990) 491–515.

[VW] M. Vardi, P. Wolper: An automata theoretic approach to automatic program verification, Proc. 1st IEEE LICS (1986) 332–345.

[WN] G. Winskel and M. Nielsen: Models for Concurrency, In: S. Abramsky and D. Gabbay (Eds.), Handbook of Logic in Computer Science, Vol 3, Oxford University Press, Oxford (1994).

[Zie] W. Zielonka: Notes on finite asynchronous automata, R.A.I.R.O.—Inf. Théor. et Appl., 21 (1987) 99–135.

[Zuc] L. Zuck: Past Temporal Logic, Ph.D. Thesis, Weizmann Institute, Rehovot, Israel (1986).