BRICS RS-98-8 Thiagarajan & Henriksen: Distributed Versions of Linear Time Temporal Logic BRICS

Basic Research in Computer Science

Distributed Versions of Linear Time Temporal Logic: A Trace Perspective

P. S. Thiagarajan Jesper G. Henriksen

BRICS Report Series RS-98-8 ISSN 0909-0878 April 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/8/

Distributed Versions of Linear Time Temporal Logic: A Trace Perspective^{∗}

P. S. Thiagarajan^{†} SPIC Mathematical Institute, Chennai, India

                  pst@smi.ernet.in

Jesper Gulmann Henriksen BRICS^{‡}, Department of Computer Science, University of Aarhus, Denmark

                  gulmann@brics.dk

April 28, 1998

1 Introduction

Linear time Temporal Logic (LTL) as proposed by Pnueli [37] has become a well established tool for specifying the dynamic behaviour of distributed systems. A basic feature of LTL is that its formulas are interpreted over sequences. Typically, such a sequence will model a computation of a system; a sequence of states visited by the system or a sequence of actions executed by the system during the course of the computation. A system is said to satisfy a specification expressed as an LTL formula in case every computation of the system is a model of the formula. A rich theory of LTL is now available using which one can effectively verify whether a finite state system meets its specification [51]. Indeed, the verfication task can be automated (for instance using the software packages SPIN [21] and FormalCheck [2]) to handle large systems of practical interest.

∗

Appears as a chapter of “Lectures on Petri Nets I: Basic Models”,

Lecture Notes in Computer Science 1491, Springer-Verlag (1998), pp. 643-681.

†This work has been supported by BRICS and IFCPAR Project 1502-1.

‡

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

In many applications the computations of a distributed system will constitute interleavings of the occurrences of causally independent actions. Consequently, the computations can be naturally grouped together into equivalence classes where two computations are equated in case they are two different interleavings of the same partially ordered stretch of behaviour. It turns out that many of the properties expressed as LTL-formulas happen to have the so called “all-or-none” property. Either all members of an equivalence class of computations will have the desired property or none will do (“leads to deadlock” is one such property). For verifying such properties one has to check the property for just one member of each equivalence class. This is the insight underlying many of the partial-order based verification methods [17, 35, 50]. As may be guessed, the importance of these methods lies in the fact that via these methods the computational resources required for the verification task can often be dramatically reduced.

It is often the case that the equivalence classes of computations generated by a distributed system constitute objects called Mazurkiewicz traces. They can be canonically represented as restricted labelled partial orders. This opens up an alternative way of exploiting the non-sequential nature of the computations of a distributed systems and the attendant partial-order based methods. It consists of developing linear time temporal logics that can be directly interpreted over Mazurkiewicz traces. In these logics, every specification is guaranteed to have the “all-or-none” property and hence can take advantage of the partial-order based reduction methods during the verification process. The study of these logics also exposes the richness of the partial-order settings from a logical standpoint and the complications that can arise as a consequence.

Our aim here is to present an overview of linear time temporal logics whose models can be viewed as Mazurkiewicz traces. The presentation is, in principle, self-contained though previous exposure to temporal logics [12] and automata over infinite objects [49] will be very helpful. We have provided net-theoretic examples whenever possible in order to emphasize the broad scope of applicability of the material.

In the next section we introduce linear time temporal logic and sketch the automata-theoretic solutions to the satisfiability problem (does a formula have a model?) and the model checking problem (do all computations of a system constitute models of a given specification formula?). In Section 3 we introduce Mazurkiewicz traces viewed as equivalence classes of sequences. This leads to the precise formualtion of the notion “all-or-none” LTL properties.

Next we introduce a well-understood class of trace languages called product languages. The automata that recognize these languages are called product automata and they incorporate a simple and yet useful method of forming distributed systems. The system consists of a network of sequential agents, each with its own alphabet of actions. In the interesting instances the alphabets are not pair-wise disjoint. One then imposes a synchronization regime under which the agents are forced to carry out common actions together. After presenting a theory of product languages and automata, we formulate in Section 5 a simple version of a trace-based version of LTL called product LTL. The formulas of this logic have a natural semantics in terms of the computations generated by a network of sequential agents as introduced in the previous section. Using the theory of product automata we then provide solutions to the satisfiability and model checking problems for product LTL.

In Section 6 we introduce the representation of Mazurkiewicz traces as restricted labelled partial orders. We then provide a rapid introduction to the theory of trace languages and automata that we call asynchronous automata for recognizing trace languages. In the subsequent section we introduce the logic TrPTL which is a trace-based logic with much richer possibilities than product LTL. We then provide solutions to the satisfiability and model checking problems for TrPTL using asynchronous automata. This is followed by a brief survey of other trace-based linear time temporal logics available in the literature. Section 8 is devoted to considering various expressiveness issues associated with our temporal logics. We conclude in the final section with remarks about branching time temporal logics based on traces.

2 Linear Time Temporal Logic

In our formulation of linear time temporal logics it will be convenient to treat actions as first class objects both at the syntactic and semantic levels. As a first step we shall consider a version of LTL (linear time temporal logic) in which the next-state modality is indexed by actions.

Through the rest of the paper we fix a finite non-empty alphabet of actions Σ. We let a, b range over Σ and refer to members of Σ as actions. Σ^{∗} is the set of finite words and Σ^{ω} is the set of infinite words generated by Σ with ω = {0, 1, 2, …}. We set Σ^{∞} = Σ^{∗} ∪ Σ^{ω} and denote the null word by ε. We let σ, σ′ range over Σ^{ω} and τ, τ′, τ′′ range over Σ^{∗}. Finally ⪯ is the usual prefix ordering defined over Σ^{∗} and for u ∈ Σ^{∞}, we let prf(u) be the set of finite prefixes of u.

Next we fix a finite non-empty set of atomic propositions P = {p_{1}, p_{2}, …} and let p, q range over P. The set of formulas of LTL(Σ) is then given by the syntax:

LTL(Σ) ::= p | ∼α | α ∨ β | ⟨a⟩α | α U β.

Through the rest of this section α, β will range over LTL(Σ).

A model of LTL(Σ) is a pair M = (σ, V) where σ ∈ Σ^{ω} and V : prf(σ) → 2^{P} is a valuation function. Let M = (σ, V) be a model, τ ∈ prf(σ) and α be a formula. Then M, τ ⊧ α will stand for α being satisfied at τ in M. This notion is defined inductively in the expected manner.

• M, τ ⊧ p iff p ∈ V (τ).

• M, τ ⊧ ∼α iff M, τ |̸= α.

• M, τ ⊧ α ∨ β iff M, τ ⊧ α or M, τ ⊧ β.

• M, τ ⊧ ⟨a⟩α iff τa ∈ prf(σ) and M, τa ⊧ α.

• M, τ ⊧ α U β iff there exists τ′ such that ττ′ ∈ prf(σ) and M, ττ′ ⊧ β. Moreover for every τ′′ such that ε ⪯ τ′′ ≺ τ′, it is the case that M, ττ′′ ⊧ α.

Along with the usual propositional connectives ∧, ⊃ and ≡ we will also use the propositional constants, ⊤ ⟺^{Δ} p_{1}∨ ∼ p_{1} and ⊥ ⟺^{Δ} ∼ ⊤. Some useful derived modalities are:

• Oα ⟺^{Δ} ⋁_{a∈Σ}⟨a⟩α.

• ◇α ⟺^{Δ} ⊤Uα.

• □α ⟺^{Δ} ∼◇ ∼α.

Let M = (σ, V) be a model and τ ∈ prf(σ). Then it is easy to check the following assertions.

• M, τ ⊧ Oα iff M, τ′ ⊧ α where τ′ ∈ prf(σ) is such that |τ′| = |τ| + 1.

• M, τ ⊧ ◇α iff there exists a τ′ ∈ Σ^{∗} with ττ′ ∈ prf(σ) such that M, ττ′ ⊧ α.

• M, τ ⊧ □α iff for each τ′ ∈ Σ^{∗}, ττ′ ∈ prf(σ) implies M, ττ′ ⊧ α.

Note that Oα is the usual next-state operator of LTL.

We say that a formula α ∈ LTL(Σ) is satisfiable iff there exist a model M = (σ, V) and τ ∈ prf(σ) such that M, τ ⊧ α. This logic does not refer to the past either in the syntax or in the semantics. Hence the formula α is satisfiable iff there exists a model M such that M, ε ⊧ α. This is easy to check. The satisfiability problem for LTL is to develop a decision procedure which will determine whether a given formula α is satisfiable. We will later in this section describe such a decision procedure.

We now wish to formulate the model checking problem for LTL(Σ). A finite-state program over Σ is a structure P r = (S, ⟶, S_{in}, V_{P r}) where:

• S is a finite set of states.

• ⟶ ⊆ S × Σ × S is a transition relation.

• S_{in} ⊆ S is a set of initial states of the program.

• V_{P r} : S → 2^{P} assigns a subset of P to each state of the program.

The members of P capture a finite set of basic assertions concerning the program which can usually be “read off” by examining the states of P r and this is described by V_{P r}. It will often be the case that the set of initial states is a singleton.

It is easy to arrange matters so that at each reachable state of the program at least one transition can be performed. We will assume that this is indeed the case for all program models we consider in this paper. Further we will say “program” instead “finite-state program” from now on.

A computation of the program P r is a pair (σ, ρ) where σ ∈ Σ^{ω} and ρ : prf(σ) → S is a map which satisfies:

• ρ(ε) ∈ S_{in}.

• ρ(τ) ⟶^{a} ρ(τa) for each τa ∈ prf(σ).

Let (σ, ρ) be a computation of the program Pr. Then this computation canonically induces the model M_{σ,ρ} = (σ, V_{ρ}) where V_{ρ} is given by: V_{ρ}(τ) = V_{P r}(ρ(τ)) for each τ ∈ prf(σ).

Let P r be a program and α be a formula of LTL(Σ). We say that P r meets the specification α — denoted P r ⊧ α — if for every computation (σ, ρ) of P r, it is the case that M, ε ⊧ α where M is the model induced by the computation (σ, ρ). The model checking problem is to decide for a given program P r and a given formula α whether or not P r ⊧ α. We will sketch a solution to the model checking problem later in this section.

Let N = (B, E, F, c_{in}) be a finite elementary net system. In other words, it is an elementary net system in which both B, the set of conditions and E, the set of events are finite sets. We can associate the program P r_{N} = (S, ⟶, S_{in}, V_{P r}) with N as follows:

• Σ = E and P = B.

• S is the least subset of 2^{B} and ⟶ is the least subset of S × Σ × S satisfying:

– c_{in} ∈ S.

– Suppose c ∈ S and e ∈ E such that ^{•}e ⊆ c and e^{•} ∩ c = ∅. Then c′ ∈ S and (c, e, c′) ∈ ⟶ where c′ = (c −^{•}e) ∪ e^{•}.

• S_{in} = {c_{in}}.

• V_{P r}(c) = c for every c ∈ S.

Thus the so called case graph is the underlying transition system of the program. The conditions serve as the atomic propositions.

For c ⊆ B, let α_{c} be the formula ⋀_{b∈c} b. Now consider the specification □ ∼ α_{c} for some c ⊆ B. Then P r_{N} |̸= □ ∼ α_{c} iff c is a reachable state (i.e. c ∈ S) in N. Next suppose e and e′ are two events. Then P r_{N} ⊧ □◇⟨e⟩⊤ ⊃ □◇⟨e′⟩⊤ captures the fact that in N, along every computation, if e occurs infinitely often then so does e′. A rich variety of liveness and safety properties can be expressed in LTL(Σ). For a substantial collection of examples the reader should see [26].

It turns out that both the satisfiability and model checking problems for LTL can be solved elegantly using Büchi automata [51]. We start with a brief introduction to these automata. A Büchi automaton over Σ is a tuple B = (Q, ⟶, Q_{in}, F) where:

• Q is a finite non-empty set of states.

• ⟶ ⊆ Q × Σ × Q is a transition relation.

• Q_{in} ⊆ Q is a set of initial states.

• F ⊆ Q is a set of accepting states.

Let σ ∈ Σ^{ω}. Then a run of B over σ is a map ρ : prf(σ) ⟶ Q such that:

• ρ(ε) ∈ Q_{in}.

• ρ(τ) ⟶^{a} ρ(τa) for each τa ∈ prf(σ).

The run ρ is accepting iff inf(ρ) ∩ F ≠ ∅ where inf(ρ) ⊆ Q is given by q ∈ inf(ρ) iff ρ(τ) = q for infinitely many τ ∈ prf(σ). Finally L(B), the language of ω-words accepted by B, is:

L(B) = {σ | ∃ an accepting run of B over σ}.

The languages recognized by Büchi automata are called the ω-regular languages. For an excellent survey of regular languages and automata over infinite objects, the reader is referred to [49].

It is easy to solve the emptiness problem for Büchi automata; to determine whether or not the language accepted by a Büchi automaton is empty. This can be done in time linear in the size of the automaton where the size of a Büchi automaton is the number of states of the automaton [49].

We will now show how one can effectively construct for each α ∈ LTL(Σ), a Büchi automaton B_{α} such that the language of ω-words accepted by B_{α} is non-empty iff α is satisfiable. This is an action-based version of the elegant solution presented in [51] for LTL.

Through the rest of the section we fix a formula α_{0}. To construct B_{α_{0}} we first define the (Fischer-Ladner) closure of α_{0}. For convenience we will assume that the derived next-state modality modality O is included in the syntax of LTL(Σ). We take cl(α_{0}) to be the least set of formulas that satisfies:

• α_{0} ∈ cl(α_{0}).

• If ∼β ∈ cl(α_{0}) then β ∈ cl(α_{0}).

• If α ∨ β ∈ cl(α_{0}) then α, β ∈ cl(α_{0}).

• If ⟨a⟩α ∈ cl(α_{0}) then α ∈ cl(α_{0}).

• If α U β ∈ cl(α_{0}) then α, β ∈ cl(α_{0}). In addition, O(α U β) ∈ cl(α_{0}).

Now CL(α_{0}), the closure of α_{0}, is defined to be:

CL(α_{0}) = cl(α_{0}) ∪ {∼β | β ∈ cl(α_{0})}.

In what follows ∼∼ β will be identified with β. Moreover, throughout the section, all the formulas that we encounter will be assumed to be members of CL(α_{0}). For convenience, we shall often write CL instead of CL(α_{0}).

A ⊆ CL is called an atom iff it satisfies :

• β ∈ A iff ∼β ∉ A.

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

• α U β ∈ A iff β ∈ A or α, O(α U β) ∈ A.

• If ⟨a⟩α ∈ A and ⟨b⟩β ∈ A then a = b.

AT (α_{0}) is the set of atoms and again we shall often write AT instead of AT (α_{0}). Finally we set U_{α_{0}}, the set of until requirements of α_{0}, to be the given by U_{α_{0}} = {α U β | α U β ∈ CL}. We will often write U_{0} instead of U_{α_{0}}.

The Büchi automaton B_{α_{0}} (from now on denoted as B) is now defined as B = (Q, ⟶, Q_{in}, F), where the various components of B are specified as follows.

• Q = AT × 2^{U_{0}} is the set of states.

• The transition relation ⟶ ⊆ Q × Σ × Q is given by (A, x) ⟶^{a} (B, y) iff the following requirements are met:

– For every ⟨a⟩α ∈ CL, ⟨a⟩α ∈ A iff α ∈ B and for every O(α) ∈ CL, O(α) ∈ A iff α ∈ B.

– if ⟨b⟩β ∈ A then b = a.

– if x ≠ ∅ then y = {α U β | α U β ∈ x and β ∉ B}. If x = ∅ then y = {α U β | α U β ∈ B and β ∉ B}.

• Q_{in} ⊆ Q is given by (A, x) ∈ Q_{in} iff α_{0} ∈ A and x = ∅.

• F ⊆ Q is given by (A, x) ∈ F iff x = ∅.

It is easy to show that L(B) ≠ ∅ iff α_{0} is satisfiable. It is also easy to check that the size of B is at most exponential in the size of α_{0}. As observed earlier the emptiness problem for a Büchi automaton can be solved in time linear in the size of the automaton. Thus we arrive at:

Theorem 2.1 The satisfiability problem for LTL(Σ) is decidable in exponential time.

Turning now to the model checking problem we first recall that the intersection problem for Büchi automata can be easily solved. In other words, let B_{1}, B_{2} be two Büchi automata both operating over Σ. Then one can effectively construct a Büchi automaton B over the same alphabet such that the language accepted by B is the intersection of the languages accepted by B_{1} and B_{2}. Moreover, the size of B can be assumed to be bounded by 2n_{1}n_{2} where n_{1} is the size of B_{1} and n_{2} is the size of B_{2} [49].

Now let P r = (S, ⟶, S_{in}, V_{P r}) be a program. We associate the Büchi automaton B_{P r} = (S, ⇝, S_{in}, S) over the alphabet Σ × 2^{P} with P r where ⇝ is given by: (s, (a, R), s′) ∈ ⇝ iff (s, a, s′) ∈ ⟶ and V_{P r}(s) = R.

Let α be a specification. Then we construct the Büchi automaton B_{∼α} corresponding to the negation of α. Let B_{∼α} = (Q, ⟹, Q_{in}, F). Recall that each state in Q is of the form (A, x) where A is an atom. We now convert this automaton into the automaton B̂ = (Q, ⇛, Q_{in}, F) over the alphabet Σ × 2^{P} by defining ⇛ as: ((A, x), (a, R), (B, y)) ∈ ⇛ iff ((A, x), a, (B, y)) ∈ ⟹ and A ∩ P = R. Finally, let B be the Büchi automaton which accepts the intersection of the languages accepted by B_{P r} and B̂. It is straightforward to check that P r ⊧ α iff the language accepted by B is empty. An easy analysis of the size of B leads to:

Theorem 2.2 The model checking problem for LTL(Σ) is decidable in time O(|P r| · 2^{|α|}).

In what follows, automata-theoretic constructions and expressiveness issues will play a considerable role. These topics can be treated in a simpler fashion if we eliminate atomic propositions. Most of the material we present can easily accomodate atomic propositions with some notational overhead. Hence from now on, we will not — except for some passing remarks — deal with atomic propositions. To be specific, the syntax of LTL(Σ) will be assumed to be:

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

Notice that a model is now just a member of Σ^{ω} with the semantics being the obvious one (⊤ is always true). The set of models of a formula constitute a language of infinite words. More precisely, each α induces the language L_{α} given by:

L_{α} = {σ | σ, ε ⊧ α}.

A program is now just a finite-state transition system P r = (S, ⟶, S_{in}) over Σ. Each such program P r has the language L_{P r} associated with it. This is just the language accepted by the Büchi automaton (S, ⟶, S_{in}, S). It is also easy to see that P r ⊧ α iff L_{P r} ⊆ L_{α} iff L_{P r} ∩ L_{∼α} = ∅.

3 Mazurkiewicz Traces and Trace Consistent Properties

Here we wish to introduce the notion of traces from the standpoint of sequences. This will enable us to define the notion of a trace consistent property. This notion plays an important role in partial order based reducion methods. As pointed out in the introduction, it also provides the motivation for studying trace based linear time temporal logics.

A (Mazurkiewicz) trace alphabet is a pair (Σ, 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 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.

For the rest of the section we fix a trace alphabet (Σ, I) and assume the terminology developed in the previous section for objects derived from Σ. We define D = (Σ × Σ) − I to be the dependency relation. Note that D is reflexive and symmetric. A set p ⊆ Σ is called a D-clique iff p × p ⊆ D. 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. However the definition of ≈_{I} in terms of permutations can not be directly transported to infinite words, which is why we work with the definition presented here.

The equivalence classes generated by ≈_{I} are called (Mazurkiewicz) traces. A set of traces is called a trace language. The theory of traces is well developed and documented—see [6, 7] for basic material as well as a substantial number of references to related work.

A variety of models of distributed systems naturally have a trace alphabet associated with them [55]. It also turns out that many interesting properties of distributed systems respect the equivalence relation induced by these trace alphabets. This has important consequences for the practical verification of such properties.

The key notion in this context is that of a trace consistent property. To bring this out, we start with a trace alphabet (Σ, I) and recall the remarks concerning the abolition of atomic propositions at the end of Section 2. Let L ⊆ Σ^{ω}. We say that L is trace consistent in case σ ∈ L and σ ≈_{I} σ′ implies σ′ ∈ L; for every σ, σ′ ∈ Σ^{ω}. In other words, either all members of a trace are in L or none of them are. We say that the formula α in LTL(Σ) is trace consistent in case L_{α} is trace consistent. It is not hard to see that there is a one-to-one correspondence between trace languages and trace consistent languages of strings.

Now suppose P r is a program over Σ which has a trace alphabet (Σ, I) associated with it in some natural manner. Suppose further that L_{P r}, the linear time behaviour of P r, is trace consistent (we will see a number of models of distributed programs that possess these features in the material to follow). Now consider a specification α which happens to be trace consistent. Then, as remarked at the end of Section 2, verifying P r ⊧ α boils down to verifying L_{P r} ⊆ L_{α}. Instead of checking L_{P r} ⊆ L_{α} we can choose to check L′ ⊆ L_{α} where L′ is designed to be such that L′ ⊆ L_{P r} and for every σ ∈ L_{P r}, [σ] ∩ L′ ≠ ∅. The key point is, the finite representation of L′ can be often substantially smaller than the representation of P r. This is the insight underlying many of the so called partial-order methods deployed in the model checking world [17, 35, 50].

As pointed out in the introduction this is also the main motivation for considering the trace-based linear time temporal logics that we will encounter later. We shall conclude this section with some examples.

Recall the material on elementary net systems introduced in Section 2. Suppose N = (B, E, F, c_{in}) is an elementary net system. Each such system induces the independence relation I_{N} given by:

I_{N} = {(e_{1}, e_{2}) | (^{•}e_{1} ∪ e_{1}^{•}) ∩ (^{•}e_{2} ∪ e_{2}^{•}) = ∅}.

Let e ∈ E and consider the formula □◇⟨e⟩⊤. The property captured by this formula says that (along every computation) the event e occurs infinitely often. It is easy to see that this is a trace consistent property with respect to the trace alphabet (E, I_{N}). Next consider the net system of Figure 1.

Consider the formula β = □◇(⟨e⟩⊤ ∧ ⟨e′⟩⊤). Suppose σ = (e_{1}e_{2}ee′)^{ω} and σ′ = (e_{1}e′e_{2}e)^{ω}. Then σ, ε ⊧ β and σ ≈_{I_{N}} σ′ but σ′, ε |̸= β. Thus this property is not trace consistent with respect to the trace alphabet induced by this net system.

4 Product Languages and Automata

We will now exhibit a restricted but useful class of distributed behaviours that we call product behaviours. Such behaviours are generated by a network of sequential agents that coordinate their activities by performing common actions together. It will turn out that product behaviours are naturally trace consistent. They also constitute a clean and yet non-trivial subset of the class of trace behaviours considered later.

[figure: ·; ·; e_{1}; e_{2}; e′; e]

Figure 1: Example elementary net system

We first study product Büchi automata. We then formulate in Section 5 the product version of LTL(Σ). We will then use product Büchi automata to solve the satisfiability and model checking problems for the product version of LTL(Σ). The technical details — which we suppress here — can be found in [47]. The key notion underlying product behaviours is that of a distributed alphabet. It can be viewed as an “implementation” of a trace alphabet. As a result, distributed alphabets play a fundamental role in the automatatheoretic aspects of trace languages [15, 58]. This will become more clear when the material in Section 6 is encountered.

A distributed alphabet is a family {Σ_{p}}_{p∈P} where P is a finite non-empty set of agents (also referred to as processes in the sequel) and Σ_{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}}.

Through the rest of the section we fix a distributed alphabet {Σ_{p}}_{p∈P} and set Σ = Σ_{P}. It will be convenient to assume that P = {1, 2, …, K}. Further, the ith component of a K-tuple x = (x_{1}, x_{2}, …, x_{K}) will be written as x[i]. In other words, x[i] = x_{i}.

A product Büchi automaton over Σ̃ is a structure A = ({A_{i}}_{i=1}^{K}, Q_{in}) where A_{i} = (Q_{i}, ⟶_{i}, F_{i}, F_{i}^{ω}) for each i such that :

• Q_{i} is a finite set of i-local states.

• ⟶_{i} ⊆ Q_{i} × Σ_{i} × Q_{i} is the transition relation of the ith component.

• F_{i} ⊆ Q_{i} is a set of finitary accepting states.

• F_{i}^{ω} ⊆ Q_{i} is a set of infinitary accepting states.

• Q_{in} ⊆ Q_{1} × Q_{2} × ⋯ × Q_{K} is a set of global initial states.

We use two types of accepting states for the components in order to be able to handle both finite and infinite behaviours. Even if one is interested only in global infinite behaviours, finite behaviours at the component level must be treated; a component might quit after engaging in a finite number of actions while a part of the network runs forever. We use global initial states to obtain the required expressive power. In general, the automaton will not be able to branch off into different parts of the state space, starting from a single global initial state. This will be brought out through a simple example after we define the language behaviour of product automata. The same example will also illustrate why using the cartesian product of local initial state sets as global initial states will result in a loss of expressive power.

Let A = ({A_{i}}_{i=1}^{K}, Q_{in}) be a product Büchi automaton over Σ̃. From now on we will say just “product automata”. Also, we shall often suppress the mention of Σ̃. We will also write {A_{i}} instead of {A_{i}}_{i=1}^{K}. Let A_{i} = (Q_{i}, ⟶_{i}, F_{i}, F_{i}^{ω}). Then we set Q_{G}^{A} = Q_{1} × Q_{2} × … × Q_{K}. When A is clear from the context, we will write Q_{G} instead of Q_{G}^{A}. The global transition relation of A is denoted as ⟶_{A} and it is the subset of Q_{G} × Σ × Q_{G} given by:

q ⟶^{a}_{A} q′ iff ∀ i ∈ loc(a) : q[i] ⟶^{a}_{i} q′[i] and ∀ i ∉ loc(a) : q[i] = q′[i].

Let σ ∈ Σ^{∞}. A run of A over σ is a map ρ : Prf(σ) ⟶ Q_{G} which satisfies:

• ρ(ε) ∈ Q_{in}.

• ∀ τa ∈ prf(σ). ρ(τ) ⟶^{a}_{A} ρ(τa).

A simple but useful property of runs is the following. Suppose ρ is a run of the product automaton A over σ. Further suppose that τ, τ′ ∈ Prf(σ) such that τ ↾ i = τ′ ↾ i for some i. Then ρ(τ)[i] = ρ(τ′)[i].

Let ρ be a run of the product automaton A over σ. Then ρ is accepting iff for each i, the following condition is satisfied:

• If σ ↾ i is finite then ρ(τ)[i] ∈ F_{i} where τ ∈ prf(σ) such that τ ↾ i = σ ↾ i.

• If σ ↾ i is infinite then ρ(τa)[i] ∈ F_{i}^{ω} for infinitely many τa ∈ prf(σ) with a ∈ Σ_{i}.

If σ ↾i is finite then clearly there exists τ ∈ prf(σ) such that τ ↾ i = σ ↾ i. Now the above property of runs assures us that the notion of an accepting run is well-defined. In case σ ↾ i is infinite the acceptance condition can also be phrased as:

• ρ(τ)[i] ∈ F_{i}^{ω} for infinitely many τ ∈ prf(σ).

This once again follows easily from the definition of a run. We now define L(A), the language accepted by the product automaton A as,

L(A) = {σ | ∃ an accepting run of A over σ}.

Now consider the alphabet ({a, d}, {d, b}) and the language L = {ad, bd}. Figure 2 shows a product automaton over this alphabet which accepts L. It

q_{1}  q_{4}  p_{1}  p_{4}
↓a  ↓d  ↓b  ↓d
q_{2}  q_{5}  p_{2}  p_{5}
↓d  ↓d
q_{3}  p_{3}
A_{1}  A_{2}

F_{1} = {q_{3}, q_{5}} F̂_{1} = ∅ = F̂_{2} F_{2} = {p_{3}, p_{5}}

Q_{in} = {(q_{1}, p_{4}), (q_{4}, p_{1})}

Figure 2: Product automaton accepting L = {ad, bd}

is easy to verify that no product automaton over this alphabet with a single global initial state can accept L. It is also easy to verify that no product automaton whose set of initial states is a cartesian product of component initial state sets can accept this language.

A crucial property of product automata is that they accept ≈-consistent languages.

Lemma 4.1 Let A = ({A_{i}}, Q_{in}) be a product automaton over Σ̃. Then L(A) is trace consistent.

The class of languages accepted by product automata can now be characterized. To this end we define the K-ary operation ⊗ : 2^{Σ_{1}^{∞}} × 2^{Σ_{2}^{∞}} × ⋯ × 2^{Σ_{K}^{∞}} → 2^{Σ^{∞}} via ⊗(L_{1}, …, L_{K}) = {σ | σ ↾ i ∈ L_{i} for each i}.

In what follows we will write L = L_{1} ⊗ L_{2} ⋯ ⊗ L_{K} to denote the fact ⊗(L_{1}, …, L_{K}) = L. We say that L ⊆ Σ^{∞} is a direct product language over Σ̃ iff ∃ L_{i} ⊆ Σ_{i}^{∞} for each i such that L = L_{1} ⊗ L_{2} ⊗ ⋯ ⊗ L_{K}. Here are two useful properties of direct product languages. In stating this result and elsewhere we will say “product language” instead of “product language over Σ̃” etc.

Proposition 4.2

1. Let L be a direct product language and σ ∈ Σ^{∞}. Then σ ∈ L iff for each i there exists σ_{i} ∈ L such that σ ↾ i = σ_{i} ↾ i.

2. Let L ⊆ Σ^{∞}. Then L is a direct product language iff L = L̂_{1} ⊗ L̂_{2} ⊗ ⋯ ⊗ L̂_{K} where L̂_{i} = {σ ↾ i | σ ∈ L} for each i.

As usual, for an alphabet Σ and L ⊆ Σ^{∞} we say that L is regular iff L ∩ Σ^{∗} is a regular subset of Σ^{∗} and L ⊆ Σ^{ω} is an ω-regular subset of Σ^{ω} as described in Section 2. We can now define the class of languages accepted by product automata.

Definition 4.3

• R_{0}^{⊗}(Σ̃) is the subset of 2^{Σ^{∞}} given by L ∈ R_{0}^{⊗}(Σ̃) iff L = L_{1} ⊗L_{2} ⊗⋯⊗ L_{K} with each L_{i} a regular subset of Σ_{i}^{∞}.

• R^{⊗}(Σ̃) is the least subset of 2^{Σ^{∞}} which contains R_{0}^{⊗} and is closed under finite unions.

The class R^{⊗}(Σ̃) defined above will be called the regular product languages over Σ̃. As usual, we shall often write R_{0}^{⊗} instead of R_{0}^{⊗}(Σ̃) and write R^{⊗} instead of R^{⊗}(Σ̃). An interesting observation concerning R^{⊗} is the following:

Proposition 4.4 R^{⊗} is closed under boolean operations.

It turns out that R^{⊗} is precisely the class of languages accepted by product automata.

Theorem 4.5 ([47]) Let L ⊆ Σ^{∞}. Then L ∈ R^{⊗} iff there exists a product automaton A such that L = L(A).

We shall be using product automata to settle the decidability and model checking problems for the logic LTL^{⊗} to be introduced in the next section. In anticipation of this, we shall put down two more results concerning product automata. While doing so and elsewhere the size of the product automaton A will be understood to be |Q_{G}|.

Theorem 4.6 Let A be a product automaton. Then the question L(A) =^{?} ∅ can be settled in time O(2^{2K} · n^{2}) where n is the size of A.

Theorem 4.7 Let A^{1} and A^{2} be two product automata. Then one can effectively construct a product automaton A such that L(A) = L(A^{1}) ∩ L(A^{2}) and moreover n = O(2^{K} · n_{1} · n_{2}) where n is the size of A and n_{ℓ} is the size of A^{ℓ} for ℓ = 1, 2.

5 A Product Version of LTL

We now wish to design a product version of LTL denoted LTL^{⊗}(Σ̃). The set of formulas and their locations are given by:

• ⊤ is a formula and loc(⊤) = ∅.

• Suppose α and β are formulas. Then so are ∼α and α∨β. Furthermore, loc(∼α) = loc(α) and loc(α ∨ β) = loc(α) ∪ loc(β).

• Suppose a ∈ Σ_{i} and α is a formula with loc(α) ⊆ {i}. Then ⟨a⟩_{i}α is a formula and loc(⟨a⟩_{i}α) = {i}.

• Suppose α and β are formulas such that loc(α), loc(β) ⊆ {i}. Then αU_{i}β is a formula. Moreover, loc(αU_{i}β) = {i}.

We note that each formula in LTL^{⊗}(Σ̃) is a boolean combination of formulas taken from the set ⋃_{i∈Loc} LTL_{i}^{⊗}(Σ̃) where, for each i,

LTL_{i}^{⊗}(Σ̃) = {α | α ∈ LTL^{⊗}(Σ̃) and loc(α) ⊆ {i} }.

Stated differently, the syntax of LTL_{i}^{⊗}(Σ̃) is given inductively by:

• ⊤ ∈ LTL_{i}^{⊗}(Σ̃).

• If α and β are in LTL_{i}^{⊗}(Σ̃) then ∼α and α ∨ β are in LTL_{i}^{⊗}(Σ̃).

• If α is in LTL_{i}^{⊗}(Σ̃) and a ∈ Σ_{i} then ⟨a⟩_{i}α is in LTL_{i}^{⊗}(Σ̃).

• If α and β are in LTL_{i}^{⊗}(Σ̃) then αU_{i}β is in LTL_{i}^{⊗}(Σ̃).

Once again, we have chosen to avoid dealing with atomic propositions for the sake of convenience. They can be introduced in a local fashion as done in [47]. The decidability result to be presented will go through with minor notational overheads.

As before, we will often suppress the mention of Σ̃. We will also often write τ_{i}, τ′_{i} and τ′′_{i} instead of τ ↾ i , τ′ ↾ i and τ′′ ↾ i, respectively with τ, τ′, τ′′ ∈ Σ^{∗}.

A model is a sequence σ ∈ Σ^{∞} and the semantics of this logic is given, as before, with τ ∈ prf(σ).

• σ, τ ⊧ ⊤.

• σ, τ ⊧ ∼α iff σ, τ |̸= α.

• σ, τ ⊧ α ∨ β iff σ, τ ⊧ α or σ, τ ⊧ β.

• σ, τ ⊧ ⟨a⟩_{i}α iff there exists τ′ ∈ prf(σ) such that σ, τ′ ⊧ α and τ′_{i} = τ_{i}a. (recall that τ′_{i} = τ′ ↾i.)

• σ, τ ⊧ αU_{i}β iff there exists τ′ such that ττ′ ∈ prf(σ) and σ, ττ′ ⊧ β. Further, for every τ′′ ∈ prf(τ′), if ε ⪯ τ′′_{i} ≺ τ′_{i} then σ, ττ′′ ⊧ α.

As before we derive some useful modalities:

• O_{i}α ⟺^{Δ} ⋁_{a∈Σ_{i}}⟨a⟩_{i}α.

• ◇_{i}α ⟺^{Δ} ⊤U_{i}α.

• □_{i}α ⟺^{Δ} ∼◇_{i} ∼α.

Let M = σ be a model and τ ∈ prf(σ). The following assertions can now easily be checked.

• σ, τ ⊧ O_{i}α iff there exists τ′ ∈ prf(σ) such that σ, τ′ ⊧ α and |τ′_{i}| = |τ_{i}| + 1.

• σ, τ ⊧ ◇_{i}α iff there exists τ′ with ττ′ ∈ prf(σ) such that σ, ττ′ ⊧ α.

• σ, τ ⊧ □_{i}α iff for each τ′, ττ′ ∈ prf(σ) implies σ, ττ′ ⊧ α.

Note that O_{i}α is the i-local version of the usual next-state operator of LTL.

We will say that a formula α ∈ LTL^{⊗}(Σ̃) is satisfiable if there exist σ ∈ Σ^{∞} and τ ∈ prf(σ) such that σ, τ ⊧ α. The language defined by α is given by

L_{α} = {σ ∈ Σ^{∞} | σ, ε ⊧ α}.

We will show the satisfiability problem for LTL^{⊗}(Σ̃) is solvable in deterministic exponential time. This will be achieved by effectively constructing a product automaton A_{α} for each α ∈ LTL^{⊗}(Σ̃) such that the language accepted by A_{α} is non-empty iff α is satisfiable. Our construction is a generalization of the one for LTL in Section 2. The solution to the satisfiability problem will at once lead to a solution to the model checking problem for programs modelled as a product of sequential agents.

Through the rest of the section we fix a formula α_{0} ∈ LTL^{⊗}(Σ̃). As before we will for convenience assume that the derived local next-state modality O_{i} is included in the syntax of LTL^{⊗}. In order to construct A_{α_{0}} we first define the (Fischer-Ladner) closure of α_{0}. As a first step let cl(α_{0}) be the least set of formulas satisfying:

• α_{0} ∈ cl(α_{0}).

• ∼α ∈ cl(α_{0}) implies α ∈ cl(α_{0}).

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

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

• αU_{i}β ∈ cl(α_{0}) implies α, β ∈ cl(α_{0}). In addition, O_{i}(αU_{i}β) ∈ cl(α_{0}). We will now take the closure of α_{0} to be CL(α_{0}) = cl(α_{0})∪{∼α | α ∈ cl(α_{0})}. From now on we shall identify ∼∼α with α. Set CL_{i}(α_{0}) = CL(α_{0}) ∩ LTL_{i}^{⊗} for each i. We will often write CL instead of CL(α_{0}) and CL_{i} instead of CL_{i}(α_{0}). All formulas considered from now on will be assumed to belong to CL unless otherwise stated.

An i-type atom is a subset A ⊆ CL_{i} which satisfies:

• ⊤ ∈ A.

• α ∈ A iff ∼α ∉ A.

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

• αU_{i}β ∈ A iff β ∈ A or α, O_{i}(αU_{i}β) ∈ A. The set of i-type atoms is denoted AT_{i}. We next define, for each α ∈ CL(α_{0}) and (A_{1}, …, A_{K}) ∈ AT_{1}×…×AT_{K}, the predicate Member(α, (A_{1}, …, A_{K})). For convenience this predicate will be denoted as α ∈ (A_{1}, …, A_{K}) and is given inductively by:

• Let α ∈ CL_{i}. Then α ∈ (A_{1}, …, A_{K}) iff α ∈ A_{i}.

• Let α = ∼β. Then α ∈ (A_{1}, …, A_{K}) iff β ∉ (A_{1}, …, A_{K}).

• Let α = β ∨ γ. Then α ∈ (A_{1}, …, A_{K}) iff β ∈ (A_{1}, …, A_{K}) or γ ∈ (A_{1}, …, A_{K}).

Finally, we set U_{i} = {αU_{i}β | αU_{i}β ∈ CL_{i}(α_{0})} for each i. The product automaton A_{α_{0}} associated with α_{0} is now defined to be A_{α_{0}} = ({A_{i}}, Q_{in}) where, for each i, A_{i} = (Q_{i}, ⟶_{i}, F_{i}, F_{i}^{ω}) is specified as follows:

• Q_{i} = AT_{i} × {off, on} × 2^{U_{i}}

• ⟶_{i} ⊆ Q_{i} × Σ_{i} × Q_{i} is given by, (A, x, u) ⟶^{a}_{i} (B, y, v) iff the following conditions are met.

1. x = on and for all ⟨a⟩_{i}α ∈ CL_{i}(α_{0}), ⟨a⟩_{i}α ∈ A iff α ∈ B and for all O_{i}α ∈ CL_{i}(α_{0}), O_{i}α ∈ A iff α ∈ B. Moreover, if ⟨b⟩_{i}β ∈ A then b = a.

2. If u ≠ ∅ then v = {αU_{i}β | αU_{i}β ∈ u and β ∉ B}. If u = ∅ then v = {αU_{i}β | αU_{i}β ∈ B and β ∉ B}.

• F_{i} ⊆ Q_{i} is given by: (A, x, u) ∈ F_{i} iff x = off and for all ⟨a⟩_{i}α ∈ CL_{i}(α_{0}), ⟨a⟩_{i}α ∉ A and for all O_{i}α ∈ CL_{i}(α_{0}), O_{i}α ∉ A.

• F_{i}^{ω} ⊆ Q_{i} is given by: (A, x, u) ∈ F_{i}^{ω} iff u = ∅.

• Q_{in} ⊆ Q_{1}×Q_{2}×…×Q_{K} is given by: ((A_{1}, x_{1}, u_{1}), …, (A_{K}, x_{K}, u_{K})) ∈ Q_{in} iff α_{0} ∈ (A_{1}, …, A_{K}) and u_{i} = ∅ for every i.

It is not difficult to now establish the next result by an application of Theorem 4.6.

Theorem 5.1 α_{0} is satisfiable iff L(A_{α_{0}}) ≠ ∅. Hence the satisfiability problem for LTL^{⊗} is decidable in exponential time.

We now turn to the model checking problem for LTL^{⊗}. A product program (over Σ̃) is a structure P r = ({P r_{i}}_{i=1}^{K}, Q_{in}^{P r}) where, for each i, P r_{i} = (Q_{i}, ⟶_{i}) with Q_{i} a finite set and ⟶_{i} ⊆ Q_{i} × Σ_{i} × Q_{i}. Since we have agreed to drop atomic propositions there is no need for (local) interpretations for the atomic propositions. Let us further assume for convenience that Q_{in}^{P r} is a singleton with q_{in} as its sole member and with q_{in}[i] = q_{in}^{i} for each i. With each such program we can associate the product automaton A_{P r} = ({A_{i}}_{i=1}^{K}, {q_{in}}) where A_{i} = (Q_{i}, ⟶_{i}, Q_{i}, Q_{i}) for each i.

Now let P r be a product program and α_{0} be a formula of LTL^{⊗}. As in the case for LTL, we say that P r meets the specification α_{0} — again denoted P r ⊧ α_{0} — iff σ, ε ⊧ α_{0} for every σ ∈ L(A_{P r}). Once again, using Theorem 4.7 it is not difficult to prove the following.

Theorem 5.2 The model checking problem for LTL^{⊗} is decidable in time O(|P r| · 2^{|α_{0}|}).

We wish to observe that each product program can be represented as a Σlabelled 1-safe net system. To see this let P r = ({P r_{i}}_{i=1}^{K}, {q_{in}}) be a product program. Let’s assume without loss of generality that the family of local states {Q_{i}} is pairwise disjoint. We set Q = ⋃_{i∈P} Q_{i} and define an a-state to be a map q_{a} : loc(a) → Q which satisfies q_{a}(i) ∈ Q_{i} for each i in loc(a). (A more elaborate development of these notions will appear in the next section).

[figure: ·; ·; ·; e_{2}; e_{1}; e; e′_{1}; e′_{2}; e_{3}; e_{3}; e_{4}; e_{4}; P r_{1}; P r_{2}; P r_{3}]

Figure 3: 1-safe net with three components

An a-event is a pair of a-states (q_{a}, q′_{a}) which satisfies q_{a}(i) ⟶^{a}_{i} q′_{a}(i) for each i in loc(a). We let E_{a} be the set of a-events. We can now define the Σ-labelled 1-safe net system representing P r to be N = (B, E, F, c_{in}, ϕ) where:

• B = Q

• E = ⋃_{a∈Σ} E_{a}

• Let q_{i} ∈ Q_{i} and e = (q_{a}, q′_{a}) ∈ E_{a}. Then (q_{i}, e) ∈ F iff i ∈ loc(a) and q_{a}(i) = q_{i}. Similarly (e, q_{i}) ∈ F iff i ∈ loc(a) and q′_{a}(i) = q_{i}.

• Let e ∈ E. Then ϕ(e) = a iff e is an a-event.

On the other hand each 1-safe net system which is covered by a set of Scomponents can be viewed as a (deterministic) product program; the alphabet of each component is its set of events. If necessary, S-complementation can be performed to ensure that the system is covered by a set of S-components. We do not wish to enter into details here. Instead we show on Figure 3 an example of a 1-safe net system composed out of three components.

Let P r denote the associated product program over the distributed alphabet {{e_{1}, e_{2}, e_{3}}, {e_{3}, e_{4}}, {e′_{1}, e′_{2}, e_{4}}}. Then it is easy to check that

P r ⊧ □_{1}O_{1}⊤ ⊃ □_{3}O_{3}⊤.

This property says that along every computation, if the first component executes infinitely often then so does the third component. The point to note is that the first component and the third component do not have any common events and hence there is no direct communication between them. Nevertheless through the power of the boolean connectives alone the logic can make assertions about the way components that are ”far apart” are required to influence each other’s behaviour.

6 Trace Languages and Automata

Traces have many equivalent representations. Here we shall view them as restricted Σ-labelled partial orders. Abusing terminology we shall call these objects also traces. We will then argue that these objects are in a rather precise sense the same as the objects called traces defined in Section 3 in terms of equivalence classes of sequences.

Let T be a Σ-labelled poset. In other words, (E, ≤) is a poset and λ : E → Σ is a labelling function. For Y ⊆ E we define ↓Y = {x | ∃y ∈ Y : x ≤ y} and ↑ Y = {x | ∃y ∈ Y : y ≤ x}. In case Y = {y} is a singleton we shall write ↓y (↑ y) instead of ↓{y} (↑ {y}). We also let ⋖ be the relation: x ⋖ y iff x < y and for all z ∈ E, x ≤ z ≤ y implies x = z or z = y.

A trace (over (Σ, I)) is a Σ-labelled poset T = (E, ≤, λ) satisfying:

(T1) ∀e ∈ E. ↓e is a finite set (T2) ∀e, e′ ∈ E. e ⋖ e′ implies λ(e) D λ(e′). (T3) ∀e, e′ ∈ E. λ(e) D λ(e′) implies e ≤ e′ or e′ ≤ e.

We shall refer to members of E as events. The trace T = (E, ≤, λ) is said to be finite if E is a finite set. Otherwise it is an infinite trace. Note that E is always a countable set. T is said to be non-empty in case E ≠ ∅. We let T R^{fin}(Σ, I) be the set of finite traces and T R^{ω}(Σ, I) be the set of infinite traces over (Σ, I) and set T R(Σ, I) = T R^{fin}(Σ, I) ∪ T R^{ω}(Σ, I). Often we will write T R^{fin} instead of T R^{fin}(Σ, I) etc. As before, a subset of traces L_{T r} ⊆ T R will be called a trace language.

Let T = (E, ≤, λ) be a trace. The finite prefixes of T, to be called configurations, will play a crucial role in what follows. A configuration of T is a finite subset c ⊆ E such that c = ↓ c. We let C_{T} be the set of configurations of T and let c, c′, c′′ range over C_{T}. Note that ∅, the empty set, is a configuration and ↓ e is a configuration for every e ∈ E. Finally, the transition relation ⟶_{T} ⊆ C_{T} × Σ × C_{T} is given by: c ⟶^{a}_{T} c′ iff there exists e ∈ E such that λ(e) = a and e ∉ c and c′ = c ∪ {e}. It is easy to see that if

c ⟶^{a}_{T} c′ and c ⟶^{a}_{T} c′′ then c′ = c′′.

Note that we have now introduced two different notions of traces; one in terms of equivalence classes of strings as in Section 3 and the other in terms of Σ-labelled partial orders as in this section. We now sketch briefly the constructions that show that Σ^{∞}/≈_{I} and T R(Σ, I) represent the same class of objects. We shall construct representation maps str : Σ^{∞}/ ≈_{I}→ 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 [55] for relating traces and event structures.

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

Recall that for σ ∈ Σ^{∞}, [σ] stands for the ≈_{I}-equivalence class containing σ. 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′.

Next, let T = (E, ≤, λ) ∈ T R(Σ, I). Then σ ∈ Σ^{∞} is a linearization of T iff there exists a map ρ : prf(σ) → C_{T}, such that the following conditions are met:

• ρ(ε) = ∅.

• ∀τa ∈ prf(σ) with τ ∈ Σ^{∗}, ρ(τ) ⟶^{a}_{T} ρ(τa).

• ∀e ∈ E ∃τ ∈ prf(σ). e ∈ ρ(τ).

The function ρ will be called a run map of the linearization σ. Note that the run map of a linearization is unique. In what follows, we shall let lin(T) to be the set of linearizations of the trace T.

We can now define the map trs : T R(Σ, I) → Σ^{∞}/ ≈_{I} as: trs(T) = lin(T). One can now show that for every σ ∈ Σ^{∞}, trs(str(σ)) = [σ] and for every T ∈ T R(Σ, I), str(trs(T)) = T. This justify our claim that Σ^{∞}/ ≈_{I} and T R(Σ, I) are indeed two equivalent ways of talking about the same class of objects.

We note that every trace consistent subset L of Σ^{∞} defines a trace language L_{T r} given by L_{T r} = {str(σ) | σ ∈ L} which has the property trs(L_{T r}) = L. In this sense every product language defines a trace language. We say that a trace language L_{T r} is regular iff trs(L_{T r}) is a regular subset of Σ^{∞}. As we will see later not every (regular) trace language is a (regular) product language. Hence in order to recognize regular trace languages one will have to use strengthened versions of product automata. Such automata called asynchronous automata were formulated by Zielonka for recognizing regular languages of finite traces. These were then generalized for handling infinite traces by Gastin and Petit [15]. We will use a combination of these two types of automata for solving the satisfiability and model checking problems for the trace-based temporal logic called TrPTL to be considered in the next section.

Let Σ̃ be a distributed alphabet with P as the associated set of agents. In an asynchronous automaton, each process p ∈ P is equipped with a finite non-empty set of local p-states, denoted S_{p}. It will be convenient to develop some notations for talking about “more global” states before defining these automata.

First 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.

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.

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 follows: Suppose s and s′ are two global states and s_{a} and s′_{a} are the two corresponding astates. In other words, s_{a}(i) = s(i) and s′_{a}(i) = s′(i) for each i in loc(a). Then

s ⟶^{a}_{T S} s′ iff (s_{a}, s′_{a}) ∈ ⟶_{a} and s(j) = s′(j) for every j ∉ 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.

An asynchronous automaton over Σ̃ is then a distributed transition system equipped with a set of global accepting states. More precisely, it is a structure A = ({S_{p}}, {⟶_{a}}, S_{in}, F) where

• F ⊆ S_{P} is a set of accepting global states.

A trace run of A over the finite trace T = (E, ≤, λ) is a map ρ : C_{T} → S_{P} such that ρ(∅) ∈ S_{in} and for every (c, a, c′) ∈ ⟶_{T}, ρ(c) ⟶^{a}_{T S} ρ(c′). We say that ρ is an accepting run whenever ρ(E) ∈ F. The language of finite traces accepted by A is given by

L_{T r}(A) = { T ∈ T R^{fin} | ∃ an accepting run of A over T }.

In the present setting Zielonka’s fundamental result can now be formulated as

Theorem 6.1 ([58]) L ⊆ T R^{fin}(Σ, I) is regular iff L = L_{T r}(A) for some asynchronous automaton A over some Σ̃ where Σ̃ is a distributed alphabet whose induced trace alphabet is (Σ, I). Further, one may assume A to be deterministic and one may assume Σ̃ to be the distributed alphabet induced by the maximal D-cliques of (Σ, I).

This result has been generalized to the set of ω-regular trace languages by Gastin and Petit [15] in terms of asynchronous automata with Büchi acceptance conditions. Since we will treat both finite and infinite traces on an equal footing we will present a class of automata capable of accepting both finite and infinite traces. Hence our automata are essentially distributed transition systems augmented with both finite and infinite accepting states.

An asynchronous Büchi automaton over Σ̃ is a structure

A = ({S_{p}}, {⟶_{a}}, S_{in}, {(F_{p}, F_{p}^{ω})}),

where:

• ({S_{p}}, {⟶_{a}}, S_{in}) is a distributed transition system.

• F_{p} ⊆ S_{p} is a set of local finitary accepting states of process p.

• F_{p}^{ω} ⊆ S_{p} is a set of local infinitary accepting states of process p.

For convenience we will from now on denote this class of automata just “asynchronous automata”.

To define acceptance we must now compute Inf_{p}(ρ), the set of p-states that are encountered infinitely often along ρ. When incorporating both finite and infinite behaviour in this richer domain we have to take care in defining the set of infinitely occuring states of process p. The obvious definition, namely Inf_{p}(ρ) = {s_{p} | ρ(c)(p) = s_{p} for infinitely many c ∈ C_{T} }, 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 T = (E, ≤, λ) where |E_{p}| = 1 and E_{q} is infinite — i.e., all the infinite words in trs(T) 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 T′ = (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}(ρ) so as to detect whether or not process p is making progress. The appropriate formulation is as follows:

• E_{p} is finite: Inf_{p}(ρ) = {s_{p}}, where ρ(↓E_{p}) = s and s_{p} = s(p).

• 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}}.

A trace run of an asynchronous automaton over the (possibly infinite) trace T = (E, ≤, λ) ∈ T R is now defined in the obvious way. A run ρ of A over the (possibly infinite) trace T = (E, ≤, λ) is accepting iff for each process p the following conditions are met:

• If E_{p} is finite then Inf_{p}(ρ) ∩ F_{p} ≠ ∅.

• If E_{p} is infinite then Inf_{p}(ρ) ∩ F_{p}^{ω} ≠ ∅.

We then have the following characterization extending Theorem 6.1.

Theorem 6.2 A trace language L ⊆ T R(Σ, I) is regular iff L = L_{T r}(A) for an asynchronous automaton over Σ̃ where Σ̃ is a distributed alphabet whose induced trace alphabet is (Σ, I).

It should be noted however that deterministic automata no longer suffice for accepting all regular languages.

We say that A is in standard form if

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

• For each (s_{a}, t_{a}) ∈ ⟶_{a} and p ∈ loc(a) we have that s_{a}(p) ∉ F_{p}.

Thus, A is in standard form if the p-states in F_{p} are all “dead” and disjoint from F_{p}^{ω}. It is easy to convert every asynchronous automaton into standard form. All our asynchronous automata will be in standard form.

We conclude with a result concerning the emptiness problem for asynchronous automata.

Proposition 6.3 ([30]) Let A be an asynchronous automaton in standard form. The emptiness problem is decidable in time O(n^{2|P|}), where n is the largest of the local state spaces, S_{p}.

We have defined here the languages defined by asynchronous automata in terms of traces. We note that these automata can be viewed — and this is the conventional approach — as automata running over Σ-sequences. Using the global transition relations of these automata one can easily define the string languages accepted by these automata. These languages will be naturally trace consistent w.r.t. the trace alphabets induced by the associated distributed alphabets. The resulting trace languages will be precisely the trace languages accepted by these automata according to the definitions we have provided here.

7 TrPTL

We present here the linear time temporal logic over traces called TrPTL. This is the first such logic patterned after PTL (i.e. LTL) formulated for traces. For a detailed treatment of this logic the reader is referred to [44, 45].

As before, 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 Σ̃. In order to better illustrate the main features of the logic we will first include atomic propositions. They will be dropped once we return to considering the technical aspects of the logic. We fix a finite non-empty set of atomic propositions P with p, q ranging over P. Then Φ_{TrPTL(Σ̃)}, the set of formulas of TrPTL(Σ̃), is defined inductively via:

• For p ∈ P 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}β.

Throughout this section, 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 T ∈ T R^{ω} with T = (E, ≤, λ). Recall that E_{i} = {e | e ∈ E and λ(e) ∈ Σ_{i}}. Let c ∈ C_{T} 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_{T}^{i} = {↓^{i}(c) | c ∈ C_{T} } be the set of i-local configurations. For Q ⊆ P and c ∈ C_{T}, 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 7.1 Let T = (E, ≤, λ) be an infinite trace. The following statements hold.

1. 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.

2. (C_{T}^{i} , ⊆) is a linear order. In fact (C_{T}^{i} −{∅}, ⊆) is isomorphic to (E_{i}, ≤_{i}).

3. Suppose ↓^{i}(c) ≠ ∅ where c ∈ C_{T}. Then there exists e ∈ E_{i} such that ↓^{i}(c) = ↓e. In fact e is the ≤_{i}-maximum event in (c ∩ E_{i}).

4. Suppose Q ⊆ Q′ ⊆ P and c ∈ C_{T}. 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 = (T, {V_{i}}_{i∈p}) where T = (E, ≤, λ) ∈ T R^{ω} and V_{i} : C_{T}^{i} → 2^{P} is a valuation function which assigns a set of atomic propositions to i-local configurations for each process i. Let c ∈ C_{T} 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 ∈ P 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_{T} such that c ⊆ c′ and M, ↓^{i}(c′) ⊧ β. Moreover, for every c′′ ∈ C_{T}, if ↓^{i}(c) ⊆ ↓^{i}(c′′) ⊂ ↓^{i}(c′) then M, ↓^{i}(c′′) ⊧ α.

Thus TrPTL is an action based multi-agent version of LTL. Indeed both in terms of its syntax and semantics, LTL(Σ) corresponds to the case where there is only one agent. The semantics of TrPTL when specialized down to this case yields the previous LTL(Σ) semantics.

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 [25, 36].

Suppose M = (T, {V_{i}}) is a model and c ⟶^{a}_{T} 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 aevent. 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. We note that unlike LTL^{⊗}, a TrPTL formula of the form ⟨a⟩_{i}α could have j ∈ loc(α) with j ≠ i. A similar remark applies to the indexed until-operators.

A basic observation concerning the semantics of TrPTL can be phrased as follows:

Proposition 7.2 Let M = (T, {V_{i}}) be a model, c ∈ C_{T} 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 ⊧ α if and only if M, ↓^{i}(c) ⊧ α. As a result, the formulas in Φ^{i} can be used in exactly the same manner as one would use LTL^{⊗} to express properties of the agent i. Boolean combinations of such local assertions 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 that we already introduced in Section 2 for LTL, the following operators are also available:

• ⊤ ⟺^{Δ} p_{1}(1) ∨ ∼ p_{1}(1) denotes the constant “True”, where P = {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 = (T, {V_{i}}) is a model and c ∈ C_{T} 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 = (T, {V_{i}}) be a model. Then M, ∅ ⊧ ◇(α_{1}, α_{2}, …, α_{k}) iff there exists c ∈ C_{T} 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. It is also the case that due to the local nature of the modalities, information about the past sneaks into the semantics even though there are no explicit past operators in the logic.

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 = (T, {V_{i}}) and c ∈ C_{T} 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 rootsatisfiable. (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 rootsatisfiability can be suitably modified to yield a direct decision procedure for checking satisfiability as done in [44]. 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 = (T, {V_{i}}), at the configuration c ∈ C_{T}, M, c ⊧ O_{i}α iff M, c ⊧ ⟨a⟩_{i}α for some a ∈ Σ_{i}. We also define loc(O_{i}α) = {i}.

Secondly, we will from now on drop the atomic propositions and instead work with the constant ⊤ and its negation ⊥ as done earlier. The semantic definitions are assumed to be suitably modified.

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 as we did in Section 2.

Fix a formula α_{0}. Our aim is to effectively associate an asynchronous automaton A_{α_{0}} with α_{0} such that α_{0} is root-satisfiable iff L_{T r}(A_{α_{0}}) ≠ ∅. Since the emptiness problem for asynchronous automata is decidable (Proposition 6.3), 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 β. Moreover, throughout the remainder of the section all formulas that we encounter will be assumed to be members of CL(α_{0}). From now we shall write CL instead of CL(α_{0}).

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

• ⊤ ∈ A.

• α ∈ A iff ∼α ∉ A.

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

• α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. We’ll define the predicate Member(α,{A_{i}}_{i∈Q}), which for convenience will be denoted by α ∈ {A_{i}}_{i∈Q}. It 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 asynchronous automaton A_{α_{0}} is guided by the construction developed for LTL in Section 2. 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 [29] that this information can be kept track of by a deterministic asynchronous automaton whose size depends only on Σ̃. (Actually the automaton described in [29] operates over finite traces but it is a trivial task to convert it into an asynchronous automaton having the desired properties). To bring out the relevant properties of this automaton, let T ∈ T R^{ω} with T = (E, ≤, λ). For each subset Q of processes, the function latest_{T,Q} : C_{T} × P → Q is given by latest_{T,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 7.3 ([29]) There exists an effectively constructible deterministic asynchronous automaton A_{Γ} = ({Γ_{i}}, {⟹_{a}}, Γ_{in}, {(F_{i}, F_{i}^{ω})}) such that:

1. L_{T r}(A_{Γ}) = T R^{ω}.

2. 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 T ∈ T R^{ω}, every c ∈ C_{T} and every j ∈ P, latest_{T,Q}(c, j) = gossip_{Q}(γ(i_{1}), …, γ(i_{n}), j) where ρ_{T} (c) = γ and ρ_{T} is the unique (accepting) run of A_{Γ} over T.

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 gossip_{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 components 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 as:

A_{α_{0}} = ({S_{i}}, {⟶_{a}}, S_{in}, {(F_{i}, F_{i}^{ω})}),

where:

• 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}.

• 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.

– (γ_{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).

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

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

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

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

– 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).

– 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}

– 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.

• 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.

• 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}.

This construction is an optimized version of the original construction for TrPTL presented in [44, 45]. Note that A_{α_{0}} is indeed in standard form. Arguments similar to those presented in [44, 45] lead to the next set of results.

Theorem 7.4

1. α_{0} is root-satisfiable iff L_{T r}(A_{α_{0}}) ≠ ∅.

2. 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 P r over Σ̃ is an asynchronous automaton A_{P r} = ({S_{i}^{P r}}, {⟹_{a}^{P r}}, S_{in}^{P r}, {(S_{i}^{P r}, S_{i}^{P r})}) modelling the state space of P r.

Viewing a formula α_{0} as a specification, we say that P r meets the specification α_{0} — denoted P r ⊧ α_{0} — if for every T ∈ T R^{ω}, if A_{P r} has a run over T then T, ∅ ⊧ α_{0}.

The model checking problem for TrPTL 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}}). As before, L_{T r}(A) = ∅ iff P r ⊧ α_{0}.

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 asynchronous 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 take a brief look at some related agent-based linear time temporal logics over traces. The first one is the sublogic of TrPTL denoted 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:

• ⊤ ∈ Φ^{con} and as before Loc(⊤) = ∅

• If α, β ∈ Φ^{con}, so are ∼α and α ∨ β.

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

• 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.

• 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 [22]. They have also been independently identified by Ramanujam [38]. 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 7.5 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 prove the following.

Theorem 7.6 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}, but it is clear that LTL^{⊗} is a strict sublogic of TrPTL^{con}. We shall deal with the relative strengths of these logics in the next section. Two of the four logics considered by Ramanujam [38] in a closely related setting turn out to be LTL^{⊗} and TrPTL^{con}. We conjecture that the other two logics are also expressible within TrPTL.

Katz and Peled introduced the logic ISTL [24] whose semantics has a trace-theoretic flavour. In a subsequent paper by Peled and Pnueli [34] on ISTL, the connection to traces was made more directly. Indeed this is one of the first instances of the explicit use of traces in a temporal logical setting that we know of. 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 [36]. 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 several μ-calculus versions of TrPTL [31, 32] and has obtained various decidability results using a variant of asynchronous Büchi automata.

The temporal logic of causality (TLC) proposed by Alur, Peled and Penczek is basically a temporal logic over traces [1]. The concurrent structures used in [1] 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 admits an essentially exponential time decision procedure for checking satisfiablity in terms of a variant of Büchi automata called Street automata.

8 Expressiveness Issues

Our aim here is to discuss some expressiveness issues concerning trace-based linear time temporal logics. To set the stage we first quickly review the classical case of sequences.

The monadic second-order theory of infinite sequences over Σ is denoted MSO(Σ). Its vocabulary consists of a family of unary predicates {R_{a}}_{a∈Σ}, one for each a ∈ Σ; a binary predicate ≤; a binary predicate ∈; a countable supply of individual variables Var = {x, y, z, …}; a countable supply of set variables (i.e. monadic predicate variables) SVar = {X, Y, Z, …}. The formulas of MSO(Σ) are then built up by:

• R_{a}(x), x ≤ y and x ∈ X are atomic formulas.

• If ϕ and ϕ′ are formulas then so are ∼ϕ, ϕ ∨ ϕ′, (∃x)ϕ and (∃X)ϕ.

A structure for MSO(Σ) is a ω-sequence σ ∈ Σ^{ω}. Let I be an interpretation of the variables with I : Var ⟶ ω and I : SVar ⟶ 2^{ω}. Then the notion of σ being a model of ϕ under the interpretation I, denoted σ ⊧_{I} ϕ, is defined in the expected manner. In particular, σ ⊧_{I} R_{a}(x) iff σ(I(x)) = a (note that σ ∈ Σ^{ω} is viewed as σ : ω ⟶ Σ); σ ⊧_{I} x ≤ y iff I(x) ≤ I(y) (here ≤ is the usual ordering over ω); σ ⊧_{I} x ∈ X iff I(x) ∈ I(X).

As usual, a sentence is a formula with no free variables. Each sentence ϕ defines an ω-language, denoted L_{ϕ}, where:

L_{ϕ} = {σ | σ ⊧ ϕ}.

We say that L ⊆ Σ^{ω} is MSO(Σ)-definable iff there exists a sentence ϕ ∈ MSO(Σ) such that L = L_{ϕ}. A celebrated result of Büchi [4] shows that the class of languages expressible by sentences in MSO(Σ) coincides with the class of languages recognized by Büchi automata over Σ. This class is the ω-regular languages over Σ.

The first-order theory of infinite sequences over Σ is denoted FO(Σ) and is obtained from MSO(Σ) by abolishing the monadic second-order quantifications from the logic. The semantics and notions of first-order definability are carried over in the obvious manner.

A fundamental result in the theory of temporal logic is Kamp’s Theorem [23] which was later strengthened in [14] to establish that LTL(Σ) is expressively equivalent to the FO(Σ). The surprise here being that LTL(Σ) admits only a bounded number of operators (one unary and one binary as we have formulated it) whereas infinitely many operators of increasing arities can be defined in FO(Σ). Secondly, as we saw in Section 2, the satisfiability problem for LTL(Σ) can be solved in deterministic exponential time. The satisfiability problem for FO(Σ) on the other hand, even when the sentences are interpreted over finite words, is known to be non-elementary hard [43]. It is quite easy to see that FO(Σ) — and hence LTL(Σ) — is strictly less expressive than MSO(Σ) in the sense that there is a language which is MSO(Σ)- definable but not FO(Σ)-definable. (Indeed this is the sense in which we shall compare the expressive power of various logics in what follows.) For instance, as pointed out by Wolper in a state-based setting [56], the language L ⊆ {a, b}^{ω} given by “a is executed at every even position” is not definable in this logic. On the other hand, it is easy to come up with a formula of MSO(Σ) defining L.

The expressive power of LTL can be extended to obtain the expressive power of MSO while still guaranteeing an exponential time decidable satisfiability problem as demonstrated first in [57]. Here we sketch how the regular programs over Σ can be used to achieve this goal [19].

The syntax of regular programs over Σ is given by:

Prg(Σ) ::= a | π_{0} + π_{1} | π_{0}; π_{1} | π^{∗}.

With each program we associate a set of finite words via the map || · || : Prg(Σ) ⟶ 2^{Σ^{∗}}. This map is defined in the standard fashion:

• ||a|| = {a}.

• ||π_{0} + π_{1}|| = ||π_{0}|| ∪ ||π_{1}||.

• ||π_{0}; π_{1}|| = {τ_{0}τ_{1} | τ_{0} ∈ ||π_{0}|| and τ_{1} ∈ ||π_{1}||}.

• ||π^{∗}|| = ⋃_{i∈ω} ||π^{i}||, where

– ||π^{0}|| = {ε} and

– ||π^{i+1}|| = {τ_{0}τ_{1} | τ_{0} ∈ ||π|| and τ_{1} ∈ ||π^{i}||} for every i ∈ ω.

The set of formulas of DLTL(Σ) is given by the following syntax.

DLTL(Σ) ::= ⊤ | ∼α | α ∨ β | α U^{π}β, π ∈ Prg(Σ)

A model is a ω-sequence σ ∈ Σ^{ω}. For τ ∈ prf(σ) we define σ, τ ⊧ α just as we did for LTL(Σ) in the case of the first three clauses. As for the last one,

• σ, τ ⊧ α U^{π}β iff there exists τ′ ∈ ||π|| such that ττ′ ∈ prf(σ) and σ, ττ′ ⊧ β. Moreover, for every τ′′ such that ε ⪯ τ′′ ≺ τ′, it is the case that σ, ττ′′ ⊧ α.

Thus DLTL(Σ) adds to LTL(Σ) by strengthening the until-operator. To satisfy α U^{π}β, one must satisfy α Uβ along some finite stretch of behaviour which is required to be in the (linear time) behaviour of the program π. We associate with a formula α of DLTL(Σ) the ω-language L_{α} in the obvious manner.

A useful derived operator of DLTL is:

• ⟨π⟩α ⟺^{Δ} ⊤ U^{π}α.

By replacing the until-modality of DLTL with the above derived operator we obtain the sublogic DLTL^{−}(Σ), which is essentially Propositional Dynamic Logic [13] equipped with a linear time semantics. It turns out that DLTL(Σ) and DLTL^{−}(Σ) both have the same expressive power as MSO(Σ).

Theorem 8.1 Let L ⊆ Σ^{ω}. Then the following statements are equivalent.

1. L is ω-regular (i.e. definable in MSO(Σ)).

2. L is DLTL(Σ)-definable.

3. L is DLTL^{−}(Σ)-definable.

Both the satisfiablity and model checking problems for DLTL(Σ) are decidable with the same time complexity as for LTL(Σ).

Let (Σ, I) be trace alphabet. Then MSO(Σ, I), the monadic second-order theory of infinite traces (over Σ, I), has the same syntax as MSO(Σ). The structures are elements of T R^{ω}(Σ, I). Let T ∈ T R^{ω}(Σ, I) with T = (E, ≤, λ) and let I : X → E be an interpretation. Then T ⊧_{I}^{MSO}R_{a}(x) iff λ(I(x)) = a and T ⊧_{I}^{MSO} x ≤ y iff I(x) ≤ I(y). Hence, the essential difference is that the binary predicate symbols is now interpreted as the causal partial order of the trace. 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_{φ} = {T | T ⊧^{MSO} φ}.

We say that L ⊆ T R^{ω} is MSO-definable iff there exists a sentence φ in MSO(Σ, I) such that L = L_{φ}. It is known that MSO-definable languages are precisely the regular trace languages; i.e. those recognized by asynchronous automata [11].

FO(Σ, I), the first-order theory of traces, is defined in the obvious way. Clearly it will be strictly weaker than MSO(Σ, I). For more information the reader is referred to [7]. Naturally both these theories can be made to handle finite traces as well.

Through the rest of this section we fix a distributed alphabet Σ̃ and let (Σ, I) be the induced trace alphabet. By MSO(Σ̃) we shall mean the theory MSO(Σ, I) and similarly for FO(Σ̃), the first-order fragment of MSO(Σ̃). In what follows we shall often supress the mention of Σ̃ as well as the induced (Σ, I).

We first consider the logic LTL^{⊗}. Recall that product languages are trace consistent and hence they induce trace languages via the map str. The resulting trace languages will be called product trace languages. As might be expected, the regular product trace languages are the ones obtained from regular product languages via the map str. It is easy to show that not every (regular) trace language is a product trace language [47]. It is also easy to see that LTL^{⊗}-definable trace languages constitute a strict subclass of regular product trace languages. It has been shown that a product version of DLTL denoted DLTL^{⊗} captures exactly the class of regular product trace languages [20]. We also claim that it is an easy exercise to formulate a product version of MSO(Σ̃) and show that it captures exactly the regular product trace languages. Let us denote this product version of MSO(Σ̃) as MSO^{⊗}(Σ̃) and its first-order fragment as FO^{⊗}(Σ̃). It is easy to show — using Kamp’s theorem — that LTL^{⊗}(Σ̃) has exactly the same expressive power as FO^{⊗}(Σ̃).

We also know that LTL^{⊗} is strictly weaker than TrPTL. First note that each formula (say α of TrPTL) defines a trace language L_{α} via :

L_{α} = { T | T, ∅ ⊧ α}.

Hence we can compare the relative expressive powers of LTL^{⊗} and TrPTL. It is known that ([30, 47]):

LTL^{⊗} ⊂ TrPTL^{con} ⊆ TrPTL.

It is still open whether TrPTL^{con} is equal to TrPTL in expressive power.

It is not difficult to show that TrPTL is no more expressive than the firstorder theory of traces but it is not known whether the converse also holds. It would be nice to have a linear time temporal logic over traces patterned after LTL which has the same expressive power as the first-order theory of traces. The motivation is provided by the next result [11]:

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

1. L is trace consistent and LTL(Σ)-definable.

2. {str(σ) | σ ∈ L} is FO(Σ, I)-definable.

Egged on by this result, recently a different kind of trace-based linear time temporal logic called LTrL has been proposed [48]. This logic works directly with a trace alphabet (i.e. it is not based on agents). It is interpreted over the configurations of a trace and its syntax is given by:

LTrL(Σ, I) ::= ⊤ | ∼α | α ∨ β | ⟨a⟩α | α U β | ⟨a^{−1}⟩⊤.

Thus the syntax is very close to LTL except for the addition of a very restricted past-operator. In fact, just a constant number of past-operators are present in the logic; one for each action.

A model of LTrL(Σ, I) is a trace T = (E, ≤, λ). Let c ∈ C_{T} be a configuration of T. Then T, c ⊧ α will stand for α being satisfied at c in T. This notion is defined inductively as follows:

• T, c ⊧ ⊤.

• T, c ⊧ ∼α and T, c ⊧ α ∨ β are defined in the expected manner.

• T, c ⊧ ⟨a⟩α iff there exists c′ ∈ C_{T} with c ⟶^{a}_{T} c′ with T, c′ ⊧ α.

• T, c ⊧ α U β iff there exists c′ ∈ C_{T} with c ⊆ c′ such that T, c′ ⊧ β. Moreover, for every c′′ ∈ C_{T}, c ⊆ c′′ ⊂ c′ implies T, c′′ ⊧ α.

• T, c ⊧ ⟨a^{−1}⟩α iff there exists c′ ∈ C_{T} with c′ ⟶^{a}_{T} c.

The major result concerning LTrL is the following:

Theorem 8.3 ([48]) Let L ⊆ T R^{ω}(Σ, I). Then the following statements are equivalent.

1. L is FO(Σ, I)-definable.

2. L is LTrL(Σ, I)-definable.

Thus — except for the addition of the restricted past-operators — LTrL is a generalization of Kamp’s Theorem to the much richer setting of traces. Meyer and Petit have shown that the past-operators can be eliminated without loss of expressive power when the logic is interpreted over finite traces [28]. A similar result for infinite traces is not known at present. Unfortunately this logic does not have a matching time complexity in relation to LTL. Recently Walukiewicz has shown that the satisfiability problem for LTrL is non-elementary hard [53]. A related result concerns the logic TLPO formulated by Ebinger [10]. This is also a linear time temporal logic interpreted over traces but with full-fledged past-operators. TLPO is claimed to be expressively complete when interpreted over finite traces but nothing is known

[figure: MSO = νTrPTL; TLC; FO = LTrL; TrPTL; MSO^{⊗} = DLTL^{⊗}; _{TrPTL_{con}}; FO^{⊗} = LTL^{⊗}]

Figure 4: Relative expressive power of the logics

about the complexity of the satisfiability problem nor about its expressive power in relation to infinite traces.

At present we do not know much about the relationship between TLC and the logics we have mentioned so far, except that it is strictly weaker than the monadic second-order theory of traces.

In an interesting recent development Niebert [32] has formulated a fixed point based linear time temporal logic for traces in the setting of distributed alphabets. This logic is denoted as νTrPTL. It is equal in expressive power to the monadic second-order theory of traces and it has decision procedure of essentially exponential time complexity. However, the formulas of this logic are required to satisfy what appears to be awkward syntactic restrictions and it is not clear how one could express global properties of interest in this formalism.

The relative strengths of the various linear time temporal logics over traces mentioned in this section are displayed in Figure 4. A dotted (solid) arrow from A to B indicates that B is at least as expressive as (strictly more expressive than) A. Squiggled lines denote that the logics are incomparable to each other.

To conclude this section, a lot is known about linear time temporal logics for traces but at present we still do not have — unlike the case of sequences — pleasing counterparts to the first-order and monadic second-order theories of traces.

9 Conclusion

In this paper we have attempted an overview of linear time temporal logics interpreted over traces. We have mainly concentrated on the satisfiability and model checking problems as well as expressiveness issues. The problem of axiomatizing these logics seems to be a non-trivial task. Some partial results may be found in [39]. In [34] the authors present proof rules for the logic ISTL with a trace semantics together with a relative expressive completeness result. Reisig has also developed a kit of proof rules for a version of UNITY logic [40, 41]. The models of this logic are the non-sequential processes of a net system and the proof rules are mainly designed to help reason about distributed algorithms modelled using net systems.

At present not much is known about corresponding logics in a branching time setting. Most of the attempts in this direction have lead to logics whose satisfiablity problems are undecidable [5, 25, 36]. It is however the case that the model checking problem often remains tractable [5, 36]. We do not know at present whether the properties expressible in such logics have any type of “all-or-none” flavour and if so whether one can develop some reduction techniques for verifying such properties. Some preliminary attempts in this direction have been made in [16, 54].

References

[1] Alur, R., Peled, D., Penczek, W.: Model checking of causality properties. Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1995) 90–100

[2] Bell Labs Design Automation: FormalCheck^{tm}. Further information can

    be obtained at http://www.bell-labs.com/formalcheck/

[3] Bracho, F., Droste, M., Kuske, D.: Representation of computations in concurrent automata by dependence orders. Theoretical Computer Science 174(1-2) (1997) 67–96

[4] Büchi, J. R.: On a decision method in restricted second order arithmetic. Proceedings of the International Congress on Logic, Methodology and Philosophy of Science, Stanford University Press (1960) 1–11

[5] Cheng, A.: Petri nets, traces, and local model checking. Proceedings of the 4th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science 936, Springer-Verlag (1995) 322–337 [6] Diekert, V.: Combinatorics of traces. Lecture Notes in Computer Science

454, Springer-Verlag (1990)

[7] Diekert, V., Rozenberg, G. (eds.): The book of traces. World Scientific (1995)

[8] Droste, M.: Recognizable languages in concurrency monoids. Theoretical Computer Science 150(1) (1995) 77–109

[9] Droste, M., Gastin, P.: Asynchronous cellular automata for pomsets without auto-concurrency. Proceedings of the 7th International Conference on Concurrency Theory, Lecture Notes in Computer Science 1119, Springer-Verlag (1996) 627–638

[10] Ebinger, W.: Charakterisierung von sprachklassen unendlicher spuren durch logiken. Dissertation, Institut für Informatik, Universität Stuttgart (1994)

[11] Ebinger, W., Muscholl, A.: Logical definability on infinite traces. Theoretical Computer Science 154(1) (1996) 67–84

[12] Emerson, A. E.: Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, Elsevier Science Publishers (1990) 996–1072

[13] Fischer, M. J., Ladner, R. E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2) (1979) 194– 211

[14] Gabbay, A., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. Proceedings of the 7th Annual Symposium on Principles of Programming Languages, ACM (1980) 163–173

[15] Gastin, P., Petit, A.: Asynchronous cellular automata for infinite traces. Proceedings of the 19th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science 623, Springer-Verlag (1992) 583–594

[16] Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial-order approach to branching time model checking. Proceedings of the 3rd Israeli Symposium on Theory of Computing and Systems, IEEE Computer Society Press (1995) 130–139 [17] Godefroid, P.: Partial-order methods for the verification of concur-

rent systems. Lecture Notes in Computer Science 1032, Springer-Verlag (1996)

[18] Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear time temporal logic. Proceedings of the 15th IFIP WG 6.1 International Workshop on Protocol Specification, Testing, and Verification, North-Holland (1995)

[19] Henriksen, J. G., Thiagarajan, P. S.: Dynamic linear time temporal logic. Journal of Pure and Applied Logic, Elsevier (to appear)

[20] Henriksen, J. G., Thiagarajan, P. S.: A product version of dynamic linear time temporal logic. Proceedings of the 8th International Conference on Concurrency Theory, Lecture Notes in Computer Science 1243, Springer-Verlag (1997) 45–58

[21] Holzmann, G. J.: An overview of the SPIN model checker. In “On-the-fly Model Checking Tutorial”, BRICS Autumn School on Verification, Note NS-96-6, BRICS, Department of Computer Science, University of Aarhus (1996)

[22] Huhn, M.: On semantic and logical refinement of actions. Technical Report, Institut für Informatik, Universität Hildesheim, Germany (1996)

[23] Kamp, H. R.: Tense logic and the theory of linear order. Ph.D. thesis, University of California (1968)

[24] Katz, S., Peled, D.: Interleaving set temporal logic. Theoretical Computer Science 73(3) (1992) 21–43

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

[26] Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems (specification), Springer-Verlag (1991)

[27] Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Technical report DAIMI PB-78, Department of Computer Science, University of Aarhus, Denmark (1977)

[28] Meyer, R., Petit, A.: Expressive completeness of LTrL on finite traces: an algebraic proof. Proceedings of the 15th Annual Symposium on Theoretical Aspects of Computer Science 1373, Lecture Notes in Computer Science, Springer-Verlag (1998) 533–543

[29] Mukund, M., Sohoni, M.: Keeping track of the latest gossip in a distributed system. Distributed Computing 10(3) (1997) 117-127

[30] Mukund, M., Thiagarajan, P. S.: Linear time temporal logics over Mazurkiewicz traces. Proceedings of the 21st International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 1113, Springer-Verlag (1996) 62–92

[31] Niebert, P.: A ν-calculus with local views for systems of sequential agents. Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 969, Springer-Verlag (1995) 563–573

[32] Niebert, P.: A temporal logic for the specification and validation of distributed behaviour. Ph.D. thesis, University of Hildesheim (1997)

[33] Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part I. Theoretical Computer Science 13(1) (1981) 85–108

[34] Peled, D., Pnueli, A.: Proving partial order properties. Theoretical Computer Science 126(2) (1994) 143–182

[35] Peled, D.: Partial order reduction: model checking using representatives. Proceedings of the 21st International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 1113, Springer-Verlag (1996) 93–112

[36] Penczek, W.: Temporal logics for trace systems: on automated verification. International Journal of the Foundations of Computer Science 4(1) (1993) 31–68

[37] Pnueli, A.: The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science, IEEE Computer Society Press (1977) 46–57

[38] Ramanujam, R.: Locally linear time temporal logic. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1996) 118–127 [39] Ramanujam, R.: Rules for trace consistent reasoning. Proceedings of the

3rd Asian Computing Science Conference, Lecture Notes in Computer Science 1345, Springer-Verlag (1997) 57–71

[40] Reisig, W.: Temporal logic and causality in concurrent systems. Proceedings of CONCURRENCY’88, Lecture Notes in Computer Science 335, Springer-Verlag (1988) 121–139

[41] Reisig, W.: Petri net models for distributed algorithms. In Computer Science Today — Recent Trends and Developments, Lecture Notes in Computer Science 1000, Springer-Verlag (1995) 441–454

[42] Sistla, A. P., Clarke, E.: The complexity of propositional linear temporal logics. Journal of the ACM 32(3) (1985) 733–749

[43] Stockmeyer, L. J.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, MIT, Cambridge, Massachusetts (1974)

[44] Thiagarajan, P. S.: A trace based extension of linear time temporal logic. Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1994) 438–447

[45] Thiagarajan, P. S.: TrPTL: a trace based extension of linear time temporal logic. Technical report TCS-93-6, School of Mathematics, SPIC Science Foundation, Madras (1993)

[46] Thiagarajan, P. S.: A trace consistent subset of PTL. Proceedings of the 6th International Conference on Concurrency Theory, Lecture Notes in Computer Science 962, Springer-Verlag (1995) 438–452

[47] Thiagarajan, P. S.: PTL over product state spaces. Technical report TCS-95-4, School of Mathematics, SPIC Science Foundation, Madras (1995)

[48] Thiagarajan, P. S., Walukiewicz, I.: An expressively complete linear time temporal logic for Mazurkiewicz traces. Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1997) 183–194

[49] Thomas, W.: Automata on infinite objects. In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, Elsevier Science Publishers (1990) 133–191

[50] Valmari, A.: A stubborn attack on state explosion. Formal Methods in Systems Design 1 (1992) 285–313 [51] Vardi, M. Y., Wolper, P.: An automata-theoretic approach to automatic

program verification. Proceedings of the 1st Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1986) 332-345

[52] Vardi, M. Y.: An automata-theoretic approach to linear time temporal logic. In Logics for Concurrency - Structure vs. Automata, Lecture Notes in Computer Science 1043, Springer-Verlag (1996) 238–266

[53] Walukiewicz, I.: Difficult configurations — on the complexity of LTrL (extended abstract). Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, Springer-Verlag (to appear)

[54] Willems, B., Wolper, P.: Partial-order methods for model checking: from linear time to branching time. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1996) 294–303

[55] Winskel, G., Nielsen, M.: Models for concurrency. In Handbook of Logic and the Foundations of Computer Science, volume 4, Oxford University Press (1995) 1–148

[56] Wolper, P.: Temporal logic can be more expressive. Proceedings of the 22nd Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society Press (1981) 340–348

[57] Wolper, P., Vardi, M. Y., Sistla, A. P.: Reasoning about infinite computation paths. Proceedings of the 24th Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society Press (1983) 185–194.

[58] Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O. Informatique Théorique et Applications 21 (1987) 99–135

Recent BRICS Report Series Publications

RS-98-8 P. S. Thiagarajan and Jesper G. Henriksen. Distributed Versions of Linear Time Temporal Logic: A Trace Perspective. April 1998. 49 pp. Appears as a chapter of Reisig and Rozenberg, editors, Lectures on Petri Nets I: Basic Models, LNCS 1491, 1998, pages 643–681.

RS-98-7 Stephen Alstrup, Thore Husfeldt, and Theis Rauhe. Marked Ancestor Problems (Preliminary Version). April 1998. 36 pp.

RS-98-6 Kim Sunesen. Further Results on Partial Order Equivalences on Infinite Systems. March 1998. 48 pp.

RS-98-5 Olivier Danvy. Formatting Strings in ML. March 1998. 3 pp. This report is superseded by the later report BRICS RS-98-12.

RS-98-4 Mogens Nielsen and Thomas S. Hune. Timed Bisimulation and Open Maps. February 1998. 27 pp. Appears in Brim, Gruska and Zlatuška, editors, Mathematical Foundations of Computer Science: 23rd International Symposium, MFCS ’98 Proceedings, LNCS 1450, 1998, pages 378–387.

RS-98-3 Christian N. S. Pedersen, Rune B. Lyngsø, and Jotun Hein. Comparison of Coding DNA. January 1998. 20 pp. Appears in Farach-Colton, editor, Combinatorial Pattern Matching: 9th Annual Symposium, CPM ’98 Proceedings, LNCS 1448, 1998, pages 153–173.

RS-98-2 Olivier Danvy. An Extensional Characterization of Lambda-Lifting and Lambda-Dropping. January 1998.

RS-98-1 Olivier Danvy. A Simple Solution to Type Specialization (Extended Abstract). January 1998. 7 pp. Appears in Larsen, Skyum and Winskel, editors, 25th International Colloquium on Automata, Languages, and Programming, ICALP ’98 Proceedings, LNCS 1433, 1998, pages 908–917.

RS-97-53 Olivier Danvy. Online Type-Directed Partial Evaluation. December 1997. 31 pp. Extended version of an article to appear in Third Fuji International Symposium on Functional and Logic Programming, FLOPS ’98 Proceedings (Kyoto, Japan, April 2– 4, 1998), pages 271–295, World Scientific, 1998.

RS-97-52 Paola Quaglia. On the Finitary Characterization of π-Congruences. December 1997. 59 pp.