BRICS RS-96-62 Thiagarajan & Walukiewicz: Linear Time Temporal Logic for Mazurkiewicz Traces

BRICS

Basic Research in Computer Science

An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces

P. S. Thiagarajan Igor Walukiewicz

BRICS Report Series RS-96-62 ISSN 0909-0878 December 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, 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 publications in the BRICS Report Series. 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 World Wide Web and anonymous FTP:

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

This document in subdirectory RS/96/62/

An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces^{1}

P. S. Thiagarajan SPIC Mathematical Institute

92 G.N.Chetty Road Madras 600017

India pst@smi.ernet.in

I. Walukiewicz^{2} Institute of Informatics, Warsaw University Banacha 2, 02-097 Warsaw Poland igw@mimuw.edu.pl

Abstract

A basic result concerning LT L, the propositional temporal logic of linear time, is that it is expressively complete; it is equal in expressive power to the first order theory of sequences. We present here a smooth extension of this result to the class of partial orders known as Mazurkiewicz traces. These partial orders arise in a variety of contexts in concurrency theory and they provide the conceptual basis for many of the partial order reduction methods that have been developed in connection with LT L-specifications.

We show that LTrL, our linear time temporal logic, is equal in expressive power to the first order theory of traces when interpreted over (finite and) infinite traces. This result fills a prominent gap in the existing logical theory of infinite traces. LTrL also provides a syntactic characterisation of the so called trace consistent (robust) LT L-specifications. These are specifications expressed as LT L formulas that do not distinguish between different linearisations of the same trace and hence are amenable to partial order reduction methods.

1 Introduction

A basic result concerning LT L, the propositional temporal logic of linear time, is that it is expressively complete; it is equal in expressive power to the first order theory of sequences [10, 6, 23]. Here we present a natural extension of this result to the class of labelled partial orders known as Mazurkiewicz traces.

To motivate this extension, we first note that as suggested by Pnueli [16], LT L is often interpreted over the runs of a distributed system. It is well known that these runs can be grouped together into equivalence classes using the causal independence of actions performed by different agents at separate locations; two runs are equated just in case they constitute two different linearisations of the same partially ordered stretch of behaviour. Thus each equivalence class corresponds to – all possible – linearisations of a partial order. In many settings, the partial orders that arise in this fashion are Mazurkiewicz traces. It is also often the case that the property expressed by an LT L formula is insensitive to the choice of linearisations in the sense that either all members of an equivalence class of runs satisfy the formula or none do. For verifying such properties it suffices to check that it holds for just one member of each equivalence class. The resulting savings in the verification process can be often substantial. This is the insight that underlies many of the so-called partial order reduction techniques [9, 14, 22].

1This work was done at BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation, Computer Science Department, Aarhus University, Denmark.

2The author was partially supported by Polish KBN grant No. 8 T11C 002 11.

There is an alternative way to exploit the non-sequential nature of the behaviour of distributed systems and the resulting partial order based reduction methods. It consists of developing temporal logics that can be directly interpreted over partial orders corresponding to the equivalence classes of runs of a distributed system. This is one of the main motivations for studying linear time temporal logics that are interpreted over traces. Yet another motivation is that traces are intimately related to basic objects in concurrency theory such as Petri nets and event structures [13].

Starting with [18] a number of such logics have been proposed in the literature [1, 3, 12, 17]. The study of these logics has so far left open two important expressiveness issues, one theoretical and the other pragmatic. From a theoretical standpoint, it has not been possible so far to exhibit a temporal logic patterned after LT L that has the same expressive power as the first order theory of infinite traces. This has been been an annoying gap in an otherwise smooth generalisation of the theory of ω-sequences to the theory of infinite traces [8, 4]. From a pragmatic standpoint, the “local” nature of the semantics of the logics that have been proposed so far makes it impossible to express arbitrary global liveness and safety properties. (More material on these issues can be found in [11].)

The temporal logic that we propose here, denoted LT rL, fulfils both these criteria. It is expressively complete for both finite and infinite traces. And we can transparently formulate within LT rL, global liveness and safety properties of all kinds. The existence of such a temporal logic is not guaranteed in advance since the class of partial orders as a whole does not admit an expressively complete temporal logic [7]. The only comparable previous result concerning traces is due to Ebinger [3]. His logic, denoted TLPO, has both previous state and Since modalities. These past modalities are used extensively in the proof of the fact that TLPO is expressively complete when interpreted over finite traces. This proof does not extend to infinite traces. In contrast, LT rL uses just a very restricted past state modality and as stated already, it is expressively complete over the domain of infinite traces.

One consequence of our main result is that LT rL captures exactly the so called trace consistent (robust) LT L-definable properties [19, 15]. These are properties that are naturally amenable to partial order reduction methods. A second consequence is that the satisfiability problem for LTrL is decidable. The decision procedure we obtain is non-elementary.

At present, we do not have an elementary decision procedure for LTrL and this is a limitation shared by TLPO. Proving the existence of such a procedure seems to be a challenging problem and its outcome will strongly influence the applicability of our logic as a specification formalism.

In the next section we introduce traces. The first order theory of traces as well as the syntax and semantics of LT rL are presented in section 3. This leads to the formulation of the main result and its corollaries. The major ingredients of the proof of the main result are: An observation in [4] that makes crucial use of [6], a decomposition result for infinite traces, an easy version of the Feferman-Vaught theorem for generalised products [5] and a new normal form linearisation of traces. Indeed, it is the use of the Feferman-Vaught result and the new normal form that takes us past the key technical hurdles. The proof is presented in section 4.

2 Traces

A (Mazurkiewicz) trace alphabet is a pair (Σ, I) where Σ is a finite set of actions and I ⊆ Σ × Σ is an irreflexive and symmetric independence relation. D = (Σ × Σ) − I is called the dependency relation. Through the rest of the paper we fix a trace alphabet (Σ, I) and we will often refer to it implicitly. We let a, b range over Σ.

We shall view (Mazurkiewicz) trace as a restricted Σ-labelled poset. Let (E, ≤, λ) 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 ∀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′ ⇒ λ(e)Dλ(e′). (T3) ∀e, e′ ∈ E. λ(e)Dλ(e′) ⇒ 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^{inf}(Σ, I) be the set of infinite traces over (Σ, I) and set T R(Σ, I) = T R^{fin}(Σ, I) ∪ T R^{inf}(Σ, I). Often we will write T R^{fin} instead of T R^{fin}(Σ, I) etc.

Let T = (E, ≤, λ) be a trace. A configuration 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 →_{T}^{a} 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 →_{T}^{a} c′ and c →_{T}^{a} c′′ then c′ = c′′.

3 The Main Result

The first order theory of traces is formulated by assuming a countable set of individual variables V ar = {x, y, z, … }; a family of unary predicates {R_{a}}_{a∈Σ}; a binary predicate ≤. Then F O(Σ, I), the set of formulas in the first order theory of traces (over (Σ, I)), is given by the syntax:

F O(Σ, I) ::= R_{a}(x) | x ≤ y |∼ φ | φ ∨ φ′ | (∃x)φ

Thus the syntax does not explicitly involve I. However, it is reflected in ≤ that will be interpreted as the partial order relation associated with a trace which does indeed respect the independence relation I.

Given a trace T = (E, ≤, λ) and an associated valuation V : Var → E, the relation T ⊧_{V}^{F O} φ will denote that T is a model of φ ∈ F O(Σ, I). This notion is defined in the expected manner. In particular, T ⊧_{V}^{F O} R_{a}(x) iff λ(V (x)) = a and T ⊧_{V}^{F O} x ≤ y iff V (x) ≤ V (y). As usual, a sentence is a formula with no free variables. L_{φ} will denote the set of models of the sentence φ: L_{φ} = {T | T ∈ T R and T ⊧^{F O} φ}

We will say that L ⊆ T R is F O-definable iff there exists a sentence φ ∈ F O(Σ, I) such that L = L_{φ}.

The set of formulas of our linear time temporal logic of traces (LTrL) is defined as follows:

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

Thus the next state modality is indexed by actions. There is also a very restricted version of the previous state modality. Indeed the number of past formulas is bounded by the size of Σ. For achieving the present aims, there is no need for atomic propositions. It is worth mentioning that if atomic propositions are to be introduced then the valuations must be required to respect the independence relation in a suitable fashion. The logic will become undecidable otherwise [11]. In the current framework, a model of LTrL is just a trace T = (E, ≤, λ). The relation T, c ⊧ α will denote that α ∈ LTrL(Σ, I) is satisfied at the configuration c ∈ C_{T}. This notion is defined via:

• T, c ⊧ \underline{tt}. Furthermore ∼ and ∨ are interpreted in the usual way.

• T, c ⊧ ⟨a⟩α iff ∃c′ ∈ C_{T}. c →_{T}^{a} c′ and T, c′ ⊧ α.

• T, c ⊧ αUβ iff ∃c′ ∈ C_{T}. c ⊆ c′ and T, c′ ⊧ β and ∀c′′ ∈ C_{T}. c ⊆ c′′ ⊂ c′ implies T, c′′ ⊧ α.

• T, c ⊧ ⟨a^{−1}⟩\underline{tt} iff ∃c′ ∈ C_{T}. c′ →_{T}^{a} c.

The derived “sometime” and “always” modalities have pleasant semantics. More precisely, with

◇α ⇔^{Δ} \underline{tt} Uα and □α ⇔^{Δ}∼ ◇ ∼ α, we have: T, c ⊧ □α iff ∀c′ ∈ C_{T}. c ⊆ c′ implies T, c′ ⊧ α. Thus

arbitrary liveness and safety properties interpreted over the global states of a distributed system can be formulated in LTrL. With each formula α ∈ LTrL(Σ, I), we can associate a set of traces as follows: L_{α} = {T ∈ T R | T, ∅ ⊨ α}. We say that L ⊆ T R is LTrL-definable iff there exists a formula α ∈ LTrL(Σ, I) such that L = L_{α}. Our main result can now be stated.

Theorem 1 Let L ⊆ T R^{inf}. Then L is F O-definable iff L is LT rL-definable.

Indeed this result goes through in case L ⊆ T R^{fin} or L ⊆ T R. We note that in case I = ∅, Theorem 1 is just the expressiveness result of [6] in a different and slightly weakened (because of the past modalities) form. As the first order theory of traces is decidable [4] and our translations are constructive we immediately obtain:

Corollary 2 The satisfiability problem for LTrL is decidable.

To bring out one more consequence of Theorem 1, we shall define LT L(Σ), linear time temporal logic interpreted over Σ-sequences. We will use Σ^{∗} and Σ^{ω} to denote the set of finite and infinite sequences over Σ respectively. We will use Σ^{∞} for Σ^{∗} ∪ Σ^{ω}.

The syntax of LT L(Σ) is given by:

LT L(Σ) ::= \underline{tt} |∼ α̂ | α̂ ∨ β̂ | ⟨a⟩α̂ | α̂ U β̂.

For σ ∈ Σ^{∞}, let prf(σ) denote the set of finite prefixes of σ and let τ ⊑ τ′ denote that τ is a prefix of τ′. Then σ, τ ⊧ α̂ will stand for α̂ being satisfied at the prefix τ of σ. This notion is defined in the usual way.

• σ, τ ⊧ \underline{tt}. The connectives ∼ and ∨ are interpreted in the standard fashion.

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

• σ, τ ⊧ α̂Uβ̂ iff ∃τ′ ∈ prf(σ) such that τ ⊑ τ′ and σ, τ′ ⊧ β̂. Moreover for every τ′′ ∈ prf(σ), if τ ⊑ τ′′ ⊏ τ′ then σ, τ′′ ⊧ α̂.

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

(i) ρ(ϵ) = ∅ (ϵ is the null string)

(ii) ∀τa ∈ prf(σ) with τ ∈ Σ^{∗}, ρ(τ) →_{T}^{a} ρ(τa)

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

The function ρ will be called a run map of the linearisation σ. Note that the run map of a linearisation is unique. In what follows we shall let lin(T) to be the set of linearisations of the trace T. The notion of linearisation induces the well-known equivalence relation ≈_{I}⊆ Σ^{∞} × Σ^{∞} via: σ ≈_{I} σ′ iff there exists a trace T, such that, σ, σ′ ∈ lin(T). A formula α̂ is said to be trace consistent if σ, ε ⊨ α̂ and σ ≈_{I} σ′ implies σ′, ε ⊨ α̂; for every σ, σ′ ∈ Σ^{∞}. As mentioned earlier, specifications that are formulated as trace consistent formulas can be often verified efficiently using partial order reduction techniques. LTrL provides a characterisation of trace consistent LTL formulas in the following sense.

Corollary 3 For every formula α ∈ LTrL(Σ, I) there is a trace consistent formula α̂ ∈ LT L(Σ), s.t. ⋃{lin(T)|T, ∅ ⊨ α} = {σ|σ, ε ⊨ α̂}. For every trace consistent LTL(Σ) formula α̂ there is a LTrL(Σ, I) formula α such that {σ|σ, ε ⊨ α̂} = ⋃{lin(T)| T, ∅ ⊨ α}.

4 The Proof

The structure of the proof of Theorem 1 can be brought out by breaking it up into the following steps.

Lemma 4 Let α ∈ LT rL(Σ, I). Then there exists φ ∈ F O(Σ, I) such that for every T ∈ T R^{inf}: T, ∅ ⊧ α iff T ⊧^{F O} φ.

Proof The key observation underlying the proof is that a configuration can be described in F O(Σ, I) in terms of its maximal elements. There can be no more than |Σ| maximal elements in a configuration.

In F O(Σ, I) the variables range over events, but we can use a finite set of variables to represent a configuration. Intuitively a set of variables X represents in a given valuation V : Var → E the configuration c_{V}^{X} = {e | ∃z ∈ X. e ≤ V (z)}.

For every set of variables X and every formula α of LTrL we will construct a formula φ_{α}^{X} of F O(Σ, I) with free variables in the set X. This formula will have the property that for every valuation V : Var → E:

T ⊨_{V}^{F O} φ_{α}^{X} iff T, c_{V}^{X} ⊨ α  (1)

In particular taking X = ∅ we will obtain the thesis of the lemma.

The construction proceeds by induction on α. If α = \underline{tt} then for every X we put φ_{α}^{X} = ∀ z. (z ≤ z). The cases for disjunction and negation are also obvious.

Suppose α = ⟨a⟩β. Let X = {x_{1}, …, x_{k}} (this set may be empty). We let φ_{α}^{X} to be:

∃y. R_{a}(y) ∧ φ_{β}^{X∪{y}} ∧ ( ⋀_{i=1,...,k} y ≰ x_{i})

∧ (∀z. z < y ⇒ ⋁_{i=1,...,k} z ≤ x_{i})

Suppose α = βUγ. First, for two sets of variables Y, Z we define the formulas

Below(Y, Z) = ⋀_{y∈Y} ⋁_{z∈Z} y ≤ z
SBelow(Y, Z) = Below(Y, Z) ∧ ¬ Below(Z, Y)

Intuitively formula Below(X, Y) says that all the events in the configuration represented by Y belong to a configuration represented by Z. The formula SBelow(X, Y) says the same plus the fact that the configurations are not equal. With the help of this formula we define φ_{α}^{X} for X ≠ ∅ by:

∃Z. Below(X, Z) ∧ φ_{γ}^{Z} ∧
∀Y. (Below(X, Y) ∧ SBelow(Y, Z)) ⇒ φ_{β}^{Y}

The quantifier ∃Z is an abbreviation of ∃z_{1}, …, ∃z_{|Σ|}. Similarly for ∀Y. We let φ_{α}^{∅} to be:

φ_{γ}^{∅} ∨ ∃Z. φ_{γ}^{Z} ∧ φ_{β}^{∅} ∧ ∀Y. SBelow(Y, Z) ⇒ φ_{β}^{Y}

Finally, if α = ⟨a^{−1}⟩\underline{tt} then the formula φ_{α}^{X} is

⋁_{x∈X} (R_{a}(x) ∧ ⋀_{x′∈X} x ≠ x′ ⇒ x ≰ x′)

By induction on α one can show that the condition (1) is satisfied. □

The other direction is much more difficult. Our goal is:

Lemma 5 Let φ ∈ F O(Σ, I). Then there exists α ∈ LT rL(Σ, I) such that for every T ∈ T R^{inf}: T ⊧^{F O} φ iff T, ∅ ⊧ α.

The line of the proof is as follows. First we will define a decomposition of traces into traces with special properties. Next we will show the above lemma for each of these special traces. Finally we will put the obtained formulas together using properties of our decomposition.

4.1 Decomposition of traces

Our decomposition is done in two steps. First a trace is split into finite and infinite part. Then the infinite part turns out to be a disjoint union of infinite traces and we separate the components of this part.

Let T = (E, ≤, λ) be a trace. Then alph(T) = {λ(e) | e ∈ E}. Denote ΣT^{fin} = {a | λ^{−1}(a) is a finite set}. The trace T is called perpetual if it is non-empty and ΣT^{fin} = ∅. Hence every perpetual trace is infinite but converse is not always true. The trace T is called directed iff every two events e_{1}, e_{2} ∈ E have an upper bound under ≤, i.e., there exists e, such that, e_{1} ≤ e and e_{2} ≤ e.

We now define the Σ-labelled posets fin(T) and inf(T) via:

fin(T) = (E_{fin}, ≤_{fin}, λ_{fin}) and inf(T) = (E_{inf}, ≤_{inf}, λ_{inf})

where E_{fin} = {e | ∃e′. e ≤ e′ and λ(e′) ∈ ΣT^{fin}} and E_{inf} = E − E_{fin}. Furthermore, ≤_{fin} (≤_{inf}) is ≤ restricted to E_{fin} × E_{fin} (E_{inf} × E_{inf}) and λ_{fin} (λ_{inf}) is λ restricted to E_{fin} (E_{inf}). The following observation follows easily from the definitions.

Proposition 6 For every trace T, fin(T) is a finite trace. Further, inf(T) is a perpetual trace iff T is an infinite trace.

Next we decompose inf(T).

Proposition 7 Let T = (E, ≤, λ) be a perpetual trace. Then there exists a unique family of traces {T_{i} = (E_{i}, ≤_{i}, λ_{i})}_{i=1}^{m} with m ≤ |Σ| such that the following conditions are satisfied:

(i) Each T_{i} is a perpetual directed trace.

(ii) For each i, j ∈ {1, …, m}, if i ≠ j then E_{i} ∩ E_{j} = ∅ and alph(T_{i}) × alph(T_{j}) ⊆ I.

(iii) E = ∪_{i=1}^{m} E_{i}, ≤= ∪_{i=1}^{m} ≤_{i} and λ = ∪_{i=1}^{m} λ_{i}.

Proof Let T = (E, ≤ λ) be a perpetual trace and let D_{T} = (alph(T) × alph(T)) ∩ D. Define a binary relation ↔⊆ E × E via:

e ↔ e′ iff ∃e′′. e ≤ e′′ and e′ ≤ e′′.  (2)

We wish to show that ↔ is an equivalence relation. For this we will need three observations.

Observation 7.1 Suppose (a, b) ∈ D_{T} and e ∈ E with λ(e) = a. Then there exists e′ ≥ e with λ(e′) = b.

To see this, note that as T is perpetual, there must exist infinitely many events labelled by b. For each such event e_{b} we have e_{b} ≤ e or e ≤ e_{b} by condition T3 in the definition of a trace.

It cannot be the case that all these events are ≤-smaller than e; this would contradict the condition (T1) of the definition of a trace. Hence there is an event e′ labelled by b that is not ≤-smaller than e. By the condition (T3) we have: e ≤ e′.

Observation 7.2 Let e, e′ ∈ E with e < e′. Then (λ(e), λ(e′)) ∈ D_{T}^{∗}.

As might be expected, D_{T}^{∗} is the (reflexive and) transitive closure of the relation D_{T}. Let us prove Observation 7.2. Call a path from e to e′ in T a sequence e = e_{0} ⋖ e_{1} ⋖ ⋯ ⋖ e_{n} = e′. Clearly such a path must exist because e < e′. This follows from T 1 in the definition of a trace. Again, by condition T 2 in the definition of a trace, we have (λ(e_{i}), λ(e_{i+1})) ∈ D_{T} for 0 ≤ i < n.

Observation 7.3 For every e, e′ ∈ E we have: e ↔ e′ iff (λ(e), λ(e′)) ∈ D_{T}^{∗}

If this observation holds then ↔ is an equivalence relation because D_{T}^{∗} is an equivalence relation. To establish the observation first assume that e′′ ∈ E with e ≤ e′′ and e′ ≤ e′′ so that e ↔ e′. From Observation 7.2 and the fact that D_{T}^{∗} is an equivalence relation, we at once have (λ(e), λ(e′)) ∈ D_{T}^{∗}. So next assume that (λ(e), λ(e′)) ∈ D_{T}^{∗} with λ(e) = a and λ(e′) = b. If a = b then e ↔ e′ follows at once from condition T 3 in the definition of a trace. So assume a ≠ b. Let a_{0}, a_{1}, …, a_{n} be a sequence such that a = a_{0}, a_{n} = b and (a_{i}, a_{i+1}) ∈ D_{T} for 0 ≤ i < n. By repeated applications of Observation 7.1 we can find a sequence of events e_{0}, e_{1}, …, e_{n} in E such that e = e_{0}, λ(e_{i}) = a_{i} and e_{i} ≤ e_{i+1} for 0 ≤ i < n. Since λ(e_{n}) = b = λ(e′) we must have e′ ≤ e_{n} or e_{n} ≤ e′. In either case, e ↔ e′ as required.

To finish the proof of the proposition, let {eq_{1}, eq_{2}, …, eq_{m}} be the set of D_{T}^{∗} - equivalence classes of alph(T). Define T_{i} = (T |eq_{i}, ≤ |eq_{i}, λ|eq_{i}) where |eq_{i} denotes the restriction to the events labelled with the letters in eq_{i}. Conditions (i) and (ii) follow from Observation 7.3. Condition (iii) follows directly from the definition of the traces T_{i}. □

Definition 8 (Shape) The shape of a perpetual trace T is the family {alph(T_{i})}_{i=1}^{m} where {T_{i}}_{i=1}^{m} is the decomposition described above. (In other words the shape of T is the D_{T}^{∗} - equivalence classes of alph(T))

A family {Σ_{i}}_{i=1}^{m} is a shape in an alphabet (Σ, I) if it is the shape of some perpetual trace over this alphabet.

4.2 Decomposing formulas in FO

Here we show a couple of composition lemmas which will allow us to reason about the properties of the whole trace in terms of the properties of its components. Before doing this, let us recall, for the sake of completeness, an easy case of composition theorem of Feferman and Vaught [5]. The reader familiar with this topic can proceed directly to Lemma 10.

Let us fix some finite relational signature Sig = {R_{1}, …, R_{l}}. Given two structures

A = ⟨A, R_{1}^{A}, …, R_{l}^{A}⟩ B = ⟨B, R_{1}^{B}, …, R_{l}^{B}⟩

of this signature we define their disjoint union as the structure A⊕B of the signature Sig ∪{in_{1}, in_{2}}:

A ⊕ B =

⟨A ⊕ B, R_{1}^{A} ⊕ R_{1}^{B}, …, R_{l}^{A} ⊕ R_{l}^{B}, in_{1}^{A⊕B}, in_{2}^{A⊕B}⟩

here A ⊕ B and R_{i}^{A} ⊕ R_{i}^{B} stand for disjoint sums of the appropriate sets and in_{1}^{A⊕B}(a) holds if a ∈ A. Similarly in_{2}^{A⊕B}(b) holds if b ∈ B.

Theorem 9 (Composition thm. for disjoint sum) Let Sig be a finite relational signature. Let φ be a sentence of F O(Sig ∪{in_{1}, in_{2}}). There exists a finite collection of pairs (ψ_{1}, ψ′_{1}), …, (ψ_{k}, ψ′_{k}) of F O(Sig) sentences, such that, for every two structures A, B of the signature Sig we have:

A ⊕ B ⊨ φ iff there exists i ∈ {1, 2, …, k} with A ⊨ ψ_{i} and B ⊨ ψ′_{i}.

Proof The proof is a standard application of Ehrenfeucht-Fraïssé games. For description of the games see for example [2]. We denote the n-move game on structures A and B by G_{n}(A, B). Let us denote by qd(θ) the quantifier depth of the sentence θ. We define an n-theory of a structure C as the set of sentences Th_{n}(C) = {θ : qd(θ) ≤ n and C ⊨ θ}. We have the following characterisation of n-theories in terms of Ehrenfeucht-Fraïssé games

Observation 9.1 Two structures A, B have the same n-theories iff Duplicator has a winning strategy in the n-move Ehrenfeucht-Fraïssé game. Every n-theory is equivalent to a single sentence, i.e., for every n-theory Γ there exist a sentence θ_{Γ} such that for every structure A: Th_{n}(A) = Γ iff A ⊨ θ_{Γ}.

The proof of this observation relies on the fact that the signatures are finite and relational.

The next observation is that the n-theory of A ⊕ B is determined by the n-theories of A and B. Indeed suppose that Th_{n}(A) = Th_{n}(A′) and Th_{n}(B) = Th_{n}(B′). By Observation 9.1 it is enough to show that Duplicator has a winning strategy in the n-move game G_{n}(A ⊕ B, A′ ⊕ B′). By assumption Duplicator has winning strategies in the games G_{n}(A, A′) and G_{n}(B, B′). The strategy in G_{n}(A ⊕ B, A′ ⊕ B′) is to copy moves of Spoiler in this game to G_{n}(A, A′) or G_{n}(B, B′) and consult the strategies there. For example if Spoiler puts a pebble on some element of the A component of A ⊕ B then we put Spoilers pebble on the same element in the game G_{n}(A, A′). The winning strategy of Duplicator in this game puts a pebble on some element of A′ and we copy this move by putting a pebble on the same element of the A′ component of A′ ⊕ B′. It should be clear that such a strategy is winning for Duplicator.

After these preliminary remarks we are ready to prove the theorem. Let φ be a F O(Sig ∪{in_{1}, in_{2}}) sentence. Let n be the quantifier depth of φ. Let (Γ_{1}, Γ′_{1}), …, (Γ_{k}, Γ′_{k}) be all pairs of n-theories such that:

if Th_{n}(A) = Γ_{i} and Th_{n}(B) = Γ′_{i} then φ ∈ Th_{n}(A ⊕ B)

The number of such pairs is finite because it can be proved by simple induction on n that there are finitely many n-theories. From Observation 9.1 we know that for every Γ_{i} there exists a formula ψ_{i}, such that, for every structure A: Th_{n}(A) = Γ_{i} iff A ⊨ ψ_{i}. Similarly for every Γ′_{i} we can find ψ′_{i}. We claim that (ψ_{1}, ψ′_{1}), … (ψ_{k}, ψ′_{k}) satisfies the thesis of the theorem.

For left to right implication suppose that A⊕B ⊨ φ. Then φ ∈ Th_{n}(A⊕B). Hence there exists i, s.t. Th_{n}(A) = Γ_{i} and Th_{n}(B) = Γ′_{i}. So A ⊨ ψ_{i} and B ⊨ ψ′_{i}. The proof of the reverse implication is similar. □

Let us now come back to decomposing traces. First we show that we can separate finite and infinite part.

Lemma 10 Let φ ∈ F O(Σ, I). Then there exists a finite collection of pairs (ψ_{1}, ψ′_{1}), (ψ_{2}, ψ′_{2}), …, (ψ_{k}, ψ′_{k}), such that, ψ_{i}, ψ′_{i} ∈ F O(Σ, I), for each i, and for every T ∈ T R^{inf}: T ⊧^{F O} φ iff there is i ∈ {1, 2, …, k} with fin(T) ⊧^{F O} ψ_{i} and inf(T) ⊧^{F O} ψ′_{i}.

Proof Let φ ∈ F O(Σ, I) be given. We claim that there exists a formula φ′, such that, for every infinite trace T:

T ⊨ φ iff fin(T) ⊕ inf(T) ⊨ φ′  (3)

For this we show that in fin(T) ⊕ inf(T) we can recover the ordering from T by means of a first order formula. Recall that fin(T)⊕inf(T) is a structure of a signature {R_{a}}_{a∈Σ}∪{≤, in_{1}, in_{2}}. The carriers of T and fin(T) ⊕ inf(T) are the same. Also the interpretations of the relations {R_{a}}_{a∈Σ} are the same. The interpretation of ≤ relation in fin(T) ⊕ inf(T) is the (disjoint) union of ≤_{fin} and ≤_{inf} where fin(T) = (E_{fin}, ≤_{fin}, λ_{fin}) and inf(T) = (E_{inf}, ≤_{inf}, λ_{inf}). Consider the formula:

θ(x, y) =(in_{1}(x) ∧ in_{1}(y) ∧ x ≤ y)
∨ (in_{2}(x) ∧ in_{2}(y) ∧ x ≤ y)
∨ (in_{1}(x) ∧ in_{2}(y) ∧ ∃z_{1}∃z_{2}. in_{1}(z_{1})
∧ in_{2}(z_{2}) ∧ D(z_{1}, z_{2}) ∧ x ≤ z_{1} ∧ z_{2} ≤ y)

where D(z_{1}, z_{2}) is a formula stating that the labels of z_{1} and z_{2} are dependent. It is not difficult to check that for all nodes x, y of T we have: T ⊨ x ≤ y iff fin(T) ⊕ inf(T) ⊨ θ(x, y). Hence taking φ and replacing all subformulas of the form x ≤ y by θ(x, y) we obtain a formula φ′ satisfying the condition (3). The thesis of the lemma follows directly from Theorem 9. □

Next we further break up the assertions concerning inf(T) to mimic the decomposition described in Proposition 7.

Lemma 11 Let φ ∈ F O(Σ, I) and sh = {Σ_{i}}_{i=1}^{m} be a shape of (Σ, I). Then there exists a finite array of formulas

(θ_{1}^{1}, …, θ_{m}^{1}), (θ_{1}^{2}, …, θ_{m}^{2}), …, (θ_{1}^{n}, …, θ_{m}^{n})

such that the following conditions are satisfied:

(i) θ_{i}^{j} ∈ F O(Σ_{i}, I) for every i ∈ {1, 2, …, m} and every j ∈ {1, 2, …, n}. (Observe that the formulas with different subscripts have disjoint alphabets.)

(ii) Suppose T ∈ T R^{inf}, and inf(T) is of shape sh. Let {T_{i}}_{i=1}^{m} be a decomposition of inf(T) as in Proposition 7. We have that inf(T) ⊧^{F O} φ iff there exists j ∈ {1, 2, …, n}, s.t., T_{i} ⊧^{F O} θ_{i}^{j} for all i = 1, …, m.

This lemma follows easily from Proposition 7 and another easy application of Theorem 9.

4.3 Translation for components

Here we present a translation of F O(Σ, I) formulas that works for finite traces as well as for perpetual directed traces.

Lemma 12 Let φ ∈ F O(Σ, I). Then there exists a formula α ∈ LT rL(Σ, I) such that for every finite or perpetual directed T ∈ T R we have: T ⊧^{F O} φ iff T, ∅ ⊧ α.

This lemma constitutes the heart of the proof of Theorem 1. The main ingredients involved in establishing the lemma are an observation made in [4] and a new normal form linearisation of traces. The first step is:

Lemma 13 Let φ ∈ F O(Σ, I). Then there exists a trace consistent α̂ ∈ LT L(Σ) such that for every T ∈ T R, T ⊧^{F O} φ iff σ, ε ⊧ α̂ for some linearisation σ of T.

Proof As observed in a slightly different setting in [4], this lemma follows easily from [6]. To see this, let F O(Σ) be the first order theory whose syntax is exactly that of F O(Σ, I) but whose structures are elements of Σ^{∞} with the usual semantics (see for instance [20]). In what follows, the semantic relation of satisfiability associated with the sentences of F O(Σ) will be denoted ⊧^{f_{0}}. A simple but basic observation essentially due to Wolfgang Thomas [21] can be stated as:

Observation 13.1 For every sentence φ ∈ F O(Σ, I) there exists a sentence φ̂ ∈ F O(Σ) such that for every trace T, T ⊧^{F O} φ iff u ⊧^{fo} φ̂ for every u ∈ lin(T).

Recall that lin(T) is the set of linearisations of T. Now let T = (E, ≤, λ) be a trace, u ∈ lin(T) and ρ : prf(u) → C_{T} the associated run map. Suppose that e ∈ E and λ(e) = a. Then there exists a unique τa ∈ prf(u) such that e ∉ ρ(τ) and e ∈ ρ(τa). Let us call this τa the occurrence of e in u. It is not difficult to show that e < e′ in T with e, e′ ∈ E iff there exists τ_{0}a_{0}, τ_{1}a_{1}, …, τ_{n}a_{n} ∈ prf(u) such that the following conditions are satisfied.

• τ_{0}a_{0} is the occurrence of e and τ_{n}a_{n} is the occurrence e′ in u.

• τ_{0}a_{0} ⊑ τ_{1}a_{1} ⊑ … ⊑ τ_{n}a_{n}.

• 1 ≤ n ≤ |Σ| and a_{i} D a_{i+1} for 0 ≤ i < n.

All these conditions can be expressed in F O(Σ) and this easily leads to Observation 13.1. Now, by the expressiveness result of [6, 23], for each sentence φ̂ ∈ F O(Σ) there exists α̂ ∈

LT L(Σ) such that:

{u ∈ Σ^{∞} | u ⊧^{fo} φ̂} = {u ∈ Σ^{∞} | u, ε ⊧ α̂}.

The lemma now follows at once from the definition of trace consistent formulas. □

We now wish to exhibit a normal linearisation of traces that can be described within LT rL(Σ, I). As a result, we will be able to translate each LT L(Σ)-formula α̂ into LT rL(Σ, I)-formula α with the property that a trace T satisfies α at a normal configuration iff α̂ is satisfied at the corresponding prefix of the normal linearisation of T. Through the rest of the section we fix a strict linear order ≺⊆ Σ × Σ. For ∅ ≠ Σ′ ⊆ Σ, min(Σ′) will denote the least element of Σ′ under ≺.

Let T = (E, ≤, λ) ∈ T R be a trace. Then the relation co ⊆ E ×E is defined as: e co e′ iff e ≰ e′ and e′ ≰ e. Further, for e, e′ ∈ E we set Σ_{ee′} = λ(↑e−↑e′). (For X ⊆ E, λ(X) = {λ(x) | x ∈ X}.)

Definition 14 Let T = (E, ≤, λ) be a trace. Then lex_{T} ⊆ E × E is defined as: e lex_{T} e′ iff e < e′ or e co e′ and min(Σ_{ee′}) ≺ min(Σ_{e′e}).

Suppose T = (E, ≤, λ) is a trace and e, e′ ∈ E with e co e′. Then it is easy to show that Σ_{ee′} ∩ Σ_{e′e} = ∅ and that both Σ_{ee′} and Σ_{e′e} are nonempty. Hence lex_{T} is well-defined.

Lemma 15 Let T = (E, ≤, λ) ∈ T R be a trace. Then (E, lex_{T}) is a strict linear order.

Proof Let e, e′ ∈ E with e ≠ e′. It is straightforward to verify that e lex_{T} e′ or e′ lex_{T} e but not both. So what needs to be shown is that lex_{T} is transitive.

Let e_{1}, e_{2}, e_{3} ∈ E with e_{1} lex_{T} e_{2} and e_{2} lex_{T} e_{3}. To show e_{1} lex_{T} e_{3}, first note that e_{1}, e_{2} and e_{3} must be pairwise distinct. For distinct i, j ∈ {1, 2, 3} we fix (if it exists) an event e_{ij} ∈ ↑e_{i} − ↑e_{j} labelled with the ≺-smallest action among those occurring in ↑e_{i} − ↑e_{j}. We need to examine several, quite easy, cases.

Suppose e_{1} < e_{2}. Then ↑e_{2} − ↑e_{3} ⊆ ↑e_{1} − ↑e_{3} and ↑e_{3} − ↑e_{1} ⊆ ↑e_{3} − ↑e_{2}. As lex_{T} (e_{2}, e_{3}) we get lex_{T} (e_{1}, e_{3}).

The case when e_{2} ≤ e_{3} is done similarly. If e_{1} ≤ e_{3} then lex_{T} (e_{1}, e_{3}) and we are done.

Suppose e_{1} co e_{2} and e_{2} co e_{3} and e_{1} ≰ e_{3}. We claim that e_{1} co e_{3}. If it were e_{3} ≤ e_{1} then ↑e_{1} − ↑e_{2} ⊆ ↑e_{3} − ↑e_{2} and ↑e_{2} − ↑e_{3} ⊆ ↑e_{2} − ↑e_{1}. Hence λ(e_{32}) ⪯ λ(e_{12}) and λ(e_{21}) ⪯ λ(e_{23}). We also know that λ(e_{12}) ≺ λ(e_{21}). This gives us λ(e_{32}) ≺ λ(e_{23}), a contradiction.

Hence we are left with the case when e_{1}, e_{2}, e_{3} are pairwise in co relation. From lex_{T} (e_{1}, e_{2}) and lex_{T} (e_{2}, e_{3}) we get λ(e_{12}) ≺ λ(e_{21}) and λ(e_{23}) ≺ λ(e_{32}).

First we claim that:

λ(e_{13}) ⪯ λ(e_{12}).  (4)

Suppose e_{12} ∉ ↑e_{3}. Then e_{12} ∈ ↑e_{1} − ↑e_{3} and (4) follows. So assume that e_{12} ∈ ↑e_{3}. Then e_{12} ∈ ↑e_{3} − ↑e_{2}. Since e_{2} lex_{T} e_{3} we have:

λ(e_{23}) ≺ λ(e_{32}) ⪯ λ(e_{12}).  (5)

Now we must consider two cases. Suppose e_{23} ∈ ↑e_{1}. Then e_{23} ∈ ↑e_{1} − ↑e_{3} and hence λ(e_{13}) ⪯ λ(e_{23}) which then leads to (4). Suppose on the other hand e_{23} ∉ ↑e_{1}. Then e_{23} ∈ ↑e_{2} − ↑e_{1} which leads to λ(e_{12}) ≺ λ(e_{21}) ⪯ λ(e_{23}). But from (5) above we now have the contradiction: λ(e_{12}) ≺ λ(e_{12}). Hence (4) must hold.

To finish the proof there are two cases to consider. Suppose e_{31} ∈ ↑e_{2}. Then e_{31} ∈ ↑e_{2} − ↑e_{1} and from λ(e_{12}) ≺ λ(e_{21}) ⪯ λ(e_{31}) and (4) we can deduce λ(e_{13}) ≺ λ(e_{31}). So suppose that e_{31} ∉ ↑e_{2}. Then e_{31} ∈ ↑e_{3} − ↑e_{2} and consequently λ(e_{23}) ≺ λ(e_{32}) ⪯ λ(e_{31}). If e_{23} ∈ ↑e_{1} then e_{23} ∈ ↑e_{1} − ↑e_{3} and hence λ(e_{13}) ⪯ λ(e_{23}) ≺ λ(e_{31}) as desired. If on the other hand, e_{23} ∉ ↑e_{1} then e_{23} ∈ ↑e_{2} − ↑e_{1} and hence λ(e_{12}) ≺ λ(e_{21}) ⪯ λ(e_{23}). This in turn leads to λ(e_{12}) ≺ λ(e_{31}). From (4) we can again conclude that λ(e_{13}) ≺ λ(e_{31}).

□

We shall introduce the notion of normal configurations that in turn will enable us to define normal linearisations of traces. Let T = (E, ≤, λ) ∈ T R and c ∈ C_{T}. Then c is a normal configuration iff for every e ∈ c and every e′ ∈ E, if e′ lex_{T} e then e′ ∈ c.

Now, let σ be a linearisation of T with ρ as the run map of σ (as defined in Section 3). Then σ is a normal linearisation of T iff ρ(τ) is a normal configuration for every τ ∈ prf(σ). It is easy to see that there can be at most one normal linearisation of a trace. Some traces do not have normal linearisations. One of the reasons why we focus on directed perpetual traces is:

Lemma 16 If T is finite or a directed perpetual trace then there exists a unique normal linearisation of T.

Proof Let c be a configuration of a trace T = (E, ≤, λ). We say that the event e ∈ E is enabled at c iff e ∉ c and c ∪ {e} is a configuration. (This notion plays an important role in the proof of the next lemma too). It is easy to see that e is enabled at c iff e is a minimal element of E − c under ≤. Next we note that if c is a normal configuration of the trace T and e is the least enabled event at c under lex_{T} (among all the enabled events at c), then c ∪ {e} is also a normal configuration. From the fact that the empty configuration is always normal, it now follows that if T is a finite trace then it admits a unique normal linearisation.

One can apply the same reasoning in case of directed perpetual traces but it may be not clear that the obtained sequence contains all the events of the trace. To show that it is indeed the case it is enough to show that for every event e the set {e′ | e′ lex_{T} e} is finite.

Let {a_{1}, …, a_{k}} = alph(T) . Take an event e_{1} ≥ e labelled with a_{1}. Such an event exists because T is directed and perpetual. Then inductively for every i = 2, …, k take e_{i} ≥ e_{i−1} labelled by a_{i}. We claim that if e′ lex_{T} e then e′ ≤ e_{k}. If e′ ≤ e then it is obvious. If e′ co e then let a_{j} be the label of e′. Clearly e′ ≤ e_{j}. Hence e′ ≤ e_{k}. We are done, as the set ↓ e_{k} is finite. □

The crucial feature of lex_{T} is that normal configurations are definable in LTrL.

Lemma 17 There exists an LTrL(Σ, I) formula NRC such that for every T ∈ T R and every c ∈ C_{T}: T, c ⊧ NRC iff c is a normal configuration.

Proof We will say that the event e is at the top of the configuration c iff c ∩ ↑e = {e}. In other words, e is a maximal element of c under ≤. We let top(c) be the set of elements that are on the top of c.

Observation 17.1 Let T = (E, ≤, λ) be a trace and c ∈ C_{T}. Then c is not a normal configuration iff there exist events e, e′ and e_{1} satisfying the following conditions:

(i) e ∈ top(c), e′ is enabled at c and e_{1} ∈ ↑e′ − ↑e,

(ii) ∀e_{2} ∈ E, if e_{2} ∈ ↑e − ↑e′ then λ(e_{1}) ≺ λ(e_{2}).

To see that this holds assume first that c is not a normal configuration. Then there exists e_{3} ∈ c and e′_{3} ∉ c such that e′_{3} lex_{T} e_{3}. Let e ∈ top(c) such that e_{3} ≤ e and let e′ be enabled at c such that e′ ≤ e′_{3}. By the transitivity of lex_{T} we now have e′ lex_{T} e. Let x = min(Σ_{e′e}) and e_{1} ∈ ↑e′ − ↑e such that λ(e_{1}) = x. Now suppose e_{2} ∈ ↑e − ↑e′. By the definition of lex_{T}, we have x ≺ λ(e_{2}).

Next suppose there exist e, e′ and e_{1} fulfilling the conditions specified by Observation 17.1. Let e_{2} ∈ ↑e − ↑e′. Then λ(e_{1}) ≺ λ(e_{2}). Hence min(Σ_{e′e}) ⪯ λ(e_{1}) ≺ min(Σ_{ee′}). Thus e′ lex_{T} e and c is not normal.

We need to define an intermediate formula before getting to NRC. In what follows, for a, b, d ∈ Σ let Γ_{ab}^{d} = {S | S ⊆ Σ and a ∈ S but b, d ∉ S}. We will use this notion only in contexts where a ≠ b and a ≠ d.

For a, b, d ∈ Σ, define the formula μ_{ab}^{d} to be ∼ \underline{tt} in case a = b or a = d. Otherwise,

μ_{ab}^{d} = ⟨b^{−1}⟩\underline{tt} ∧ ⋁_{S∈Γ_{ab}^{d}} α_{S}

where

α_{S} = ( ⋀_{x∈S}⟨x^{−1}⟩\underline{tt}) U (⟨d^{−1}⟩\underline{tt} ∧ ⋀_{x∈S}⟨x^{−1}⟩\underline{tt}

∧ ⋀_{y∈(Σ−S)−\{d\}} ∼ ⟨y^{−1}⟩\underline{tt}).

Observation 17.2 Let T = (E, ≤, λ) be a trace and c ∈ C_{T}. Then T, c ⊧ μ_{ab}^{d} iff there exist events e, e′, e_{1} such that the following conditions are satisfied:

(i) λ(e) = a, λ(e′) = b and λ(e_{1}) = d.

(ii) e, e′ ∈ top(c) with e ≠ e′ and e_{1} ∈ ↑e′ − ↑e.

To see that this must hold first suppose that T, c ⊧ μ_{ab}^{d}. Then a ≠ b and a ≠ d. Let S ∈ Γ_{ab}^{d} such that T, c ⊧ ⟨b^{−1}⟩\underline{tt} ∧ α_{S}. Then there exists c′ such that c ⊆ c′ and

T, c′ ⊧ ⟨d^{−1}⟩\underline{tt} ∧ ⋀_{x∈S}⟨x^{−1}⟩\underline{tt} ∧ ⋀_{y∈(Σ−S)−\{d\}} ∼< y^{−1} > \underline{tt}.  (1)

Furthermore, for every configuration c′′ such that c ⊆ c′′ ⊂ c′, we have

T, c′′ ⊧ ⋀_{x∈S}⟨x^{−1}⟩\underline{tt}.  (2)

Let e, e′ ∈ top(c) such that λ(e) = a and λ(e′) = b. Clearly, a ≠ b implies e ≠ e′.

Now suppose b = d. Then by setting e_{1} = e′, we at once get the desired conclusion. This follows from the fact that a ≠ b because b ∉ S and hence λ(e) ≠ λ(e′). But then e, e′ ∈ top(c) and thus e′ ∈ ↑e′ − ↑e.

So assume that b ≠ d. Then T, c′ ⊧∼ ⟨b^{−1}⟩\underline{tt} because b ∈ (Σ − S) − \{d\}.

Let e_{1} ∈ top(c′) such that λ(e_{1}) = d. Such an e_{1} must exist because T, c′ ⊧ ⟨d^{−1}⟩\underline{tt}. We now wish to argue that e, e′ and e_{1} have the desired properties.

Let S = \{a^{1}, a^{2}, …, a^{k}\}. Note that a ∈ S. Since T, c ⊧ ⋀_{x∈S}⟨x^{−1}⟩\underline{tt}, we can fix e^{1}, e^{2}, … e^{k} ∈ top(c) such that λ(e^{j}) = a^{j} for each j ∈ {1, 2, …, k}. Clearly e ∈ {e^{1}, …, e^{j}}. We will first argue that e^{j} co e_{1} for every j which will lead to e co e_{1}. So fix j ∈ {1, 2, …, k} and suppose that e^{j} co e_{1} does not hold. Since e_{1} ∈ top(c′) and c ⊆ c′ and e^{j} ∈ top(c) we can rule out e_{1} < e^{j}. So it must be the case that e^{j} < e_{1}. But this implies that there exists a finite chain e^{j} = z_{0} ⋖ z_{1} ⋖ ⋯ ⋖ z_{n} = e_{1}. Since λ(e_{1}) = d ∉ S we have λ(e^{j}) ≠ d and n ≥ 1. Let i be the least integer in {0, 1, …, n − 1} such that λ(z_{i}) = a^{j} and λ(z_{i+1}) ≠ a^{j}. Let λ(z_{i+1}) = â. Clearly a^{j} D â. Now consider the configuration ĉ = c ∪ ↓ z_{i+1}. It is easy to check that c ⊆ ĉ ⊆ c′. Hence T, ĉ ⊧ ⋀_{x∈S}⟨x^{−1}⟩\underline{tt} which then implies T, ĉ ⊧ ⟨(a^{j})^{−1}⟩\underline{tt}. But z_{i+1} ∈ top(ĉ) and hence T, ĉ ⊧ ⟨(â)^{−1}⟩\underline{tt}. This is a contradiction because two distinct labels at the top of a configuration can not be in the dependence relation. Thus e^{j} co e_{1} and consequently e co e_{1}.

Next we must show that e′ ≤ e_{1}. Since T, c ⊧ ⟨b^{−1}⟩\underline{tt} and T, c′ ⊧∼ ⟨b^{−1}⟩\underline{tt} (recall that we are considering the case b ≠ d) we know that e′ ∉ top(c′). Hence there exists e′′ ∈ top(c′) such that e′ < e′′. If e′′ = e_{1}, we are done. Otherwise e′ < e′′ for some e′′ ∈ top(c′) with λ(e′′) = a^{j} for some a^{j} ∈ S. We will now argue that this is impossible.

Suppose e′ < e′′ and λ(e′′) = a^{j} ∈ S with e′′ ∈ top(c′). Then from e^{j} ∈ top(c) and b ∉ S, we get a^{j} I b. Consequently a^{j} ≠ b. Clearly there exists a non-null path e′ = z_{0} ⋖ z_{1} ⋖ ⋯ ⋖ z_{n} = e′′ . Let i be the largest integer in {1, 2, …, n} such that z_{i} = a^{j} and z_{i−1} ≠ a^{j}. Let λ(z_{i−1}) = â and ĉ = c ∪ ↓ z_{i−1}. It is easy to check that c ⊆ ĉ ⊂ c′ and hence T, ĉ ⊧ ⟨(a^{j})^{−1}⟩\underline{tt}. But z_{j−1} ∈ top(ĉ) and hence T, ĉ ⊧ ⟨(â)^{−1}⟩\underline{tt}. We now have a contradiction because â ≠ a^{j} and â D a^{j}.

To prove the right to left implication of Observation 17.2 assume that the event e, e′ and e_{1} exist which fulfil the properties specified in the observation. Let c′ = c ∪ ↓ e_{1}. Then e_{1} ∈ top(c′) and hence T, c′ ⊧ ⟨d^{−1}⟩\underline{tt}. Let S = \{λ(e′′) | e′′ ∈ top(c′) and e′′ ≠ e_{1}\}. First we assert a ∈ S. This is because e ∈ top(c) and e co e_{1}. Hence e ∈ top(c′) as well because c′ = c ∪ ↓ e_{1}. By the definition of S we are assured that d ∉ S. Hence a ≠ d. Next suppose b ∈ S. Then there exists e′′ ∈ top(c′) such that e′′ ≠ e_{1} and λ(e′′) = b. But then e′′ ∈ c ∪ ↓ e_{1} and since e′′ ≠ e_{1} implies e′′ co e_{1}, we must have e′′ ∈ c. In fact e′′ ∈ top(c) because e′′ ∈ top(c′) and c ⊆ c′. But this implies e′′ = e′ which contradicts e′ ≤ e_{1}. Thus b ∉ S and consequently b ≠ a.

Clearly, by the choice of S, we have

T, c′ ⊧ ⟨d^{−1}⟩\underline{tt} ∧ ⋀_{x∈S}⟨x^{−1}⟩\underline{tt} ∧ ⋀_{y∈(Σ−S)−\{d\}} ∼ ⟨y^{−1}⟩\underline{tt}.

It is also clear that T, c ⊧ ⟨b^{−1}⟩\underline{tt}. So suppose c ⊆ c′′ ⊂ c′ and â ∈ S. Then there exists e′′ ∈ top(c′) such that λ(e′′) = â. But then c′ = c ∪ ↓ e_{1} and d ∉ S at once leads to â ∈ top(c′′) as well. Hence T, c′′ ⊧ ⟨(â^{−1}⟩\underline{tt}. We now have T, c ⊧ μ_{ab}^{d}.

Now we define the desired formula NRC as:

NRC =∼ ⋁_{(a,b)∈I}⟨b⟩ (⋁_{d∈Σ} (μ_{ab}^{d} ∧ ⋀_{d′≺d} ∼ μ_{ba}^{d′})) .

To see that NRC has the required property assume first that T = (E, ≤, λ) is a trace and ĉ ∈ C_{T} is a configuration that is not normal. Then by Observation 17.1, there exist event e, e′ and e_{1} such that e ∈ top(ĉ), e′ is enabled at ĉ and e_{1} ∈ ↑e′ − ↑e. Further, if e_{2} ∈ ↑e − ↑e′ then λ(e_{1}) ≺ λ(e_{2}). Let λ(e) = a, λ(e′) = b and λ(e_{1}) = d. If e ≤ e′ then this would lead to e ≤ e_{1} contradicting e co e_{1}. Hence e co e′ as well. Consequently a ≠ b and a ≠ d. Now consider the configuration c = ĉ ∪ {e′}. Clearly c fulfils the requirements of Observation 17.2 and hence T, c ⊧ μ_{ab}^{d}. Now suppose T, c ⊧ μ_{ba}^{d′} for some d′ ≺ d. Then by the definition of the formula μ_{ba}^{d′} we are assured that b ≠ d′. Further, we already have b ≠ a. Now again by Observation 17.2, there exists e_{2} such that e_{2} ∈ ↑e − ↑e′ with λ(e_{2}) ≺ λ(e_{1}). But this contradicts the criteria justifying the choice of e, e′ and e_{1}. Hence T, ĉ ⊧∼ NRC.

Next suppose T, ĉ ⊧∼ NRC. Then there exists (a, b) ∈ I and d ∈ Σ such that T, ĉ ⊧ ⟨b⟩ (μ_{ab}^{d} ∧ ⋀_{d′≺d} ∼ μ_{ba}^{d′}). Clearly a ≠ b and a ≠ d. Hence there exists an event e ∈ top(ĉ) and an event e′ which is enabled at ĉ such that λ(e) = a and λ(e′) = b. Moreover with c = ĉ∪ {e′}, we have T, c ⊧ μ_{ab}^{d} ∧⋀_{d′≺d} ∼ μ_{ba}^{d′}. Because T, c ⊧ μ_{ab}^{d} there exists an event e_{1} such that λ(e_{1}) = d and e_{1} ∈ ↑e′ − ↑e. This follows from Observation 17.2. Now suppose there exists e_{2} ∈ ↑e − ↑e′ such that λ(e_{2}) = d′ ≺ d. If d′ ≠ b then, by Observation 17.2, we have T, c′ ⊧ μ_{ba}^{d′}; a contradiction. Hence it must be the case that d′ = b so that μ_{ba}^{d′} =∼ \underline{tt}. But this is again a contradiction, because λ(e_{2}) = d′ = b implies that e′ ≤ e_{2} or e_{2} ≤ e′ whereas we are supposed to have e_{2} co e′. Thus min(Σ_{e′e}) ⪯ d ≺ min(Σ_{ee′}). This leads to e′ lex_{T} e, which then guarantees that ĉ is not a normal configuration. □

Using NRC, we now define the map ∥.∥ : LT L(Σ) →LT rL(Σ, I) via:

∥\underline{tt}∥ = \underline{tt} ∥ ∼ α̂∥ =∼ ∥α̂∥ ∥α̂ ∨ β̂∥ = ∥α̂∥ ∨ ∥β̂∥
∥⟨a⟩α̂∥ = ⟨a⟩(NRC ∧ ∥α̂∥)
∥α̂ U β̂∥ = (NRC ⊃ ∥α̂∥) U (NRC ∧ ∥β̂∥)

Lemma 18 Let α̂ be a formula of LTL(Σ). For every finite or perpetual directed trace T and its normal linearisation σ_{0} we have: σ_{0}, ε ⊧ α̂ iff T, ∅ ⊧ ∥α̂∥.

The lemma can be obtained without much work by structural induction of α̂ using the property of NRC.

We claim that Lemma 12 follows from Lemma 18 and the previous results. To see this, let φ ∈ F O(Σ, I) and T be a finite or perpetual directed trace. Then by Lemma 13, there exists α̂ ∈ LT L(Σ), such that, T ⊧ φ iff σ_{0}, ε ⊧ α̂; where σ_{0} is the normal linearisation of T. By Lemma 18: T ⊧ φ iff T, ∅ ⊧ ∥α̂∥. Thus with each φ ∈ F O(Σ, I) we can associate the formula ∥α̂∥.

4.4 Composing formulas in LTrL

Lemma 19 Let φ ∈ F O(Σ, I). Then there exists a formula α ∈ LT rL(Σ, I) such that for every T ∈ T R^{inf}, inf(T) ⊧^{F O} φ iff inf(T), ∅ ⊧ α.

Proof Let us fix a F O(Σ, I) formula φ. First, for every shape sh = {Σ_{i}}_{i=1}^{m} of (Σ, I) we will construct a LTrL formula α_{sh} with the property:

for every trace T with inf(T) of shape sh:

inf(T) ⊨^{F O} φ iff inf(T), ∅ ⊨ α_{sh} (6)

Let us fix a shape sh = {Σ_{i}}_{i=1}^{m}. By Lemma 11, for the shape sh we have an array of F O(Σ, I) formulas:

(θ_{1}^{1}, …, θ_{m}^{1}), (θ_{1}^{2}, …, θ_{m}^{2}), …, (θ_{1}^{n}, …, θ_{m}^{n})  (7)

such that for every trace T, if inf(T) is of the shape sh and {T_{i}}_{i=1}^{m} is the decomposition of inf(T) as in Proposition 7 then:

inf(T) ⊨^{F O} φ iff there is j ∈ {1, 2, … n} such that for all i ∈ {1, 2, …, m}, T_{i}, ∅ ⊨ θ_{i}^{j}

Moreover each θ_{i}^{j} is over the alphabet Σ_{i}.

By Lemma 12, for every θ_{i}^{j} we can find a LTrL formula α_{i}^{j} such that for every perpetual directed trace T′ over the alphabet Σ_{i} we have: T′ ⊧^{F O} θ_{i}^{j} iff T′, ∅ ⊨ α_{i}^{j}. Hence, for a decomposition {T_{i} = (E_{i}, ≤_{i}, λ_{i})}_{i=1}^{m} as above and for every j = 1, …, n we have: T_{i} ⊨^{F O} θ_{i}^{j} iff T_{i}, ∅ ⊨ α_{i}^{j}. Now Σ_{i} × Σ_{j} ⊆ I whenever i ≠ j and i, j ∈ {1, 2, …, m}. Hence, we are assured that c ⊆ E is a configuration of inf(T) iff c_{i} = c ∩ E_{i} is a configuration of T_{i} for each i. It is easy to establish by structural induction that for every formula γ_{i} over Σ_{i} (i.e. γ_{i} mentioning at most the letters in Σ_{i}) and for every configuration c of inf(T), we have inf(T), c ⊧ γ_{i} iff T_{i}, c_{i} ⊧ γ_{i}. Since each α_{i}^{j} is over the alphabet Σ_{i} we have: inf(T), ∅ ⊧ α_{1}^{j} ∧ α_{2}^{j} ⋯ ∧ α_{m}^{j} iff T_{i} ⊧ α_{i}^{j} for each i.

Let us denote α_{1}^{j} ∧ ⋯ ∧ α_{n}^{j} by β^{j} and let

α_{sh} = β^{1} ∨ ⋯ ∨ β^{n}

It should be clear that α_{sh} satisfies the property (6). Next we observe that we can write a formula ν_{sh} in LT rL such that inf(T), ∅ ⊧ ν_{sh} iff inf(T) is of shape sh. Let sh = {Σ_{i}}_{i=1}^{m} and

Σ_{sh} = ⋃_{i=1}^{m} Σ_{i}.

Then

ν_{sh} = ( ⋀_{a∈Σ_{sh}} ◇⟨a⟩\underline{tt}) ∧ ( ⋀_{a∉Σ_{sh}} □ ∼ ⟨a⟩\underline{tt}) .

Clearly (Σ, I) admits only finitely many shapes. Let SH be the set of all shapes. Then consider the formula:

α = ⋀_{sh∈SH}(ν_{sh} ⊃ α_{sh}).

It is not difficult to show now that α satisfies the property required by the lemma. □

Lemma 20 Let α_{0}, α_{1} ∈ LT rL(Σ, I). Then there exists a formula α ∈ LT rL(Σ, I) such that for every T ∈ T R^{inf}, T, ∅ ⊧ α iff fin(T), ∅ ⊧ α_{0} and inf(T), ∅ ⊧ α_{1}.

Proof First we define a LTrL formula Border that holds precisely in the configuration of T consisting of all the events in fin(T):

Border = (⋀_{a∈Σ} < a^{−1} > \underline{tt} ⊃ □ ∼< a > \underline{tt}) ∧

⋀_{b∈Σ} □(< b > \underline{tt} ⊃< b > ◇ < b > \underline{tt}).

Next we define F IN to be the formula ◇Border. We have that for every trace T: T, c ⊨ F IN iff c ⊆ fin(T) and T, c ⊨ BORDER iff c = E_{fin}; where E_{fin} is the set of events of fin(T).

Now, with each formula α ∈ LT rL we associate the formula fin(α) inductively as follows.

fin(\underline{tt}) = \underline{tt} fin(∼ α) =∼ fin(α)

\begin{matrix}fin((α ∨ β)) = & fin(α) ∨ fin(β) \\ fin(⟨a⟩α) = & ⟨a⟩(F IN ∧ fin(α)) \\ fin(αUβ) = & fin(α) U (F IN ∧ fin(β)) \end{matrix}

Also, with each formula β we associate the formula inf(β) given by: inf(β) = ◇(Border ∧ β). Now, let T = (E, ≤, λ) ∈ T R^{inf} and fin(T) = (E_{fin}, ≤_{fin}, λ_{fin}) and inf(T) = (E_{inf}, ≤_{inf}, λ_{inf}). It follows from the definitions that c ⊆ E_{fin} is a configuration of fin(T) iff c is a configuration of T. Hence using the properties of the translation map fin defined above we can establish by structural induction on α that T, c ⊧ fin(α) iff fin(T), c ⊧ α for each configuration c of fin(T).

Next we note that c ⊆ E_{inf} is a configuration of inf(T) iff E_{fin} ∪c is a configuration of T. Again, by using the property of the map inf, we can show by structural induction, that

T, E_{fin} ∪ c ⊧ inf(β) iff inf(T), c ⊧ β

for each configuration c of inf(T). It now follows at once that for every T ∈ T R^{inf}, T, ∅ ⊧ fin(α_{0}) ∧ inf(α_{1}) iff fin(T), ∅ ⊧ α_{0} and inf(T), ∅ ⊧ α_{1}.

□

Clearly Lemmas 10, 12, and 20 together yield Lemma 5 and we are done.

Using the intermediate lemmas that have been established to prove the main result, it is an easy exercise to derive Corollary 3.

References

[1] R. Alur, D. Peled, and W. Penczek. Model-checking of causality properties. In LICS ’95, pages 90–100, 1995.

[2] H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer-Verlag, 1995.

[3] W. Ebinger. Charakterisierung von Sprachklassen unendlicher Spuren durch Logiken. PhD thesis, Institut für Informatik, Universität Stuttgart, 1994.

[4] W. Ebinger and A. Muscholl. Logical definability on infinite traces. In ICALP ’93, volume 700, pages 335–346, 1993.

[5] S. Feferman and R. Vaught. The first order properties of products of algebraic systems. Fundamenta Mathematicae, 47:57–103, 1959.

[6] A. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In 7th Ann. ACM Symp. on Principles of Programming Languages, pages 163–173, 1980.

[7] D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic : Mathematical Foundations and Computational Aspects, volume 1. Clarendon Press, Oxford, G.B., 1994.

[8] P. Gastin and A. Petit. Asynchronous cellurar automata for infinite traces. In ICALP ’92, volume 623 of LNCS, pages 583–594, 1992.

[9] P. Godefroid. Partial-order methods for the verification of concurrent systems, volume 1032 of LNCS. Springer-Verlag, 1996.

[10] H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, 1968.

[11] M. Mukund and P.S. Thiagarajan. Linear time temporal logics over traces. In MFCS’96, volume 1113 of LNCS, pages 62–92, 1996.

[12] P. Niebert. A ν-calculus with local views for sequential agents. In MFCS ’95, volume 969 of LNCS, pages 563–573, 1995.

[13] M. Nielsen and G. Winskel. Trace structures and other models for concurrency. In V. Diekert and G. Rozenberg, editors, The Book of Traces, pages 271–305. World Scientific, Singapore, 1995.

[14] D. Peled. Partial order reduction : model checking using representatives. In MFCS’9, volume 1113 of LNCS, pages 93–112, 1996.

[15] D. Peled, T. Wilke and P. Wolper. An Algorithmic Approach for Checking Closure Properties of ω-Regular Languages. In CONCUR’96, volume 1119 of LNCS, Springer-Verlag, (1996) 596-610.

[16] A. Pnueli. The temporal logic of programs. In 18th Symposium on Foundations of Computer Science, pages 46–57, 1977.

[17] R. Ramanujam. Locally linear time temporal logic. In LICS ’96, pages 118–128, 1996.

[18] P. S. Thiagarajan. A trace based extension of linear time temporal logic. In LICS ’94, pages 438–447, 1994.

[19] P. S. Thiagarajan. A trace consistent subset of P T L. In CONCUR ’95, volume 962 of LNCS, Springer-Verlag, (1995) 438-452.

[20] W. Thomas. Automata on infinite objects. In J. van Leeuven, editor, Handbook of Theoretical Computer Science Vol.B, pages 133–192. Elsevier, 1990.

[21] W. Thomas. On logical definability of trace languages. In V. Diekert, editor, Workshop of the ESPRIT Basic Research Action No: 3166, volume Report TUM-19002, Technical University of Munich,, pages 172–182, 1990.

[22] A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1:297–322, 1992.

[23] L. Zuck. Past temporal logic. PhD thesis, Weizmann Institute of Science, Israel, 1986.

Recent Publications in the BRICS Report Series

RS-96-62 P. S. Thiagarajan and Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. December 1996. 19 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-96-61 Sergei Soloviev. Proof of a Conjecture of S. Mac Lane. December 1996. 53 pp. Extended abstract appears in Pitt, Rydeheard and Johnstone, editors, Category Theory and Computer Science: 6th International Conference, CTCS ’95 Proceedings, LNCS 953, 1995, pages 59�80.

RS-96-60 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal in 1995. December 1996. 5 pp. Appears in Margaria and Steffen, editors, Tools and Algorithms for The Construction and Analysis of Systems: 2nd International Workshop, TACAS ’96 Proceedings, LNCS 1055, 1996, pages 431�434.

RS-96-59 Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. December 1996. 12 pp. Appears in 16th IEEE Real-Time Systems Symposium, RTSS ’95 Proceedings, 1995.

RS-96-58 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal � a Tool Suite for Automatic Veri�cation of Real�Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, DIMACS Workshop on Veri�cation and Control of Hybrid Systems, HYBRID ’96 Proceedings, LNCS 1066, 1996, pages 232�243.

RS-96-57 Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, DIMACS Workshop on Veri�cation and Control of Hybrid Systems, HYBRID ’96 Proceedings, LNCS 1066, 1996, pages 575�586.