BRICS RS-99-26 J. G. Henriksen: An Expressive Extension of TLC BRICS

Basic Research in Computer Science

An Expressive Extension of TLC

Jesper G. Henriksen BRICS Report Series RS-99-26 ISSN 0909-0878 September 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Jesper G. Henriksen.

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/99/26/

An Expressive Extension of TLC

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

              gulmann@brics.dk

Spetember 27, 1999

Abstract

A temporal logic of causality (TLC) was introduced by Alur, Penczek and Peled in [1]. It is basically a linear time temporal logic interpreted over Mazurkiewicz traces which allows quantification over causal chains. Through this device one can directly formulate causality properties of distributed systems. In this paper we consider an extension of TLC by strengthening the chain quantification operators. We show that our logic TLC^{∗} adds to the expressive power of TLC. We do so by defining an Ehrenfeucht-Fraïssé game to capture the expressive power of TLC. We then exhibit a property and by means of this game prove that the chosen property is not definable in TLC. We then show that the same property is definable in TLC^{∗}. We prove in fact the stronger result that TLC^{∗} is expressively stronger than TLC exactly when the dependency relation associated with the underlying trace alphabet is not transitive.

1 Introduction

One traditional approach to automatic program verification is model checking LTL [13] specifications. In this context, the model checking problem is to decide whether or not all computation sequences of the system at hand satisfy the required properties formulated as an assertion of LTL. Several software packages exploiting the rich theory of LTL are now available to carry out the automated verification task for quite large finite-state systems, e.g. [2, 9].

∗Part of this work was done at Lehrstuhl für Informatik VII, RWTH Aachen, Germany † Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Usually computations of a distributed system will constitute interleavings of the occurrences of causally independent actions. Often, the computation sequences can be naturally grouped together into equivalence classes of sequences corresponding to different interleavings of the same partially ordered computation stretch. For a large class of interesting properties expressed by linear time temporal logics, it turns out that either all members of an equivalence class satisfy a certain property or none do. For such properties the computional resources needed for the verification task can be substantially reduced by means of the so-called partial-order methods for verification [8, 12, 18].

Such equivalence classes can be canonically represented by restricted labelled partial orders known as Mazurkiewicz traces [5, 10]. These objects — apart from alleviating the state-explosion problems of verification — also allow direct formulations of properties expressing concurrency and causality. A number of linear time temporal logics to be interpreted directly over Mazurkiewicz traces (e.g. [1, 4, 11, 14, 15, 16, 17]) has been proposed in the literature starting with TrPTL [15].

Among these, we consider here a temporal logic of causality (TLC) introduced in [1] to express serializability (of partially ordered computations) in a direct fashion. The operators of TLC are essentially the branching-time operators of CTL [3] interpreted over causal chains of traces. However, the expressive power of this logic has remained an interesting open problem. Indeed, not much is known about the relative expressive powers of the various temporal logics over traces.

What is known is that a linear time temporal LTrL, patterned after LTL, was introduced [17] and proven expressively equivalent to the first-order theory of traces [6]. LTrL has a simple and natural formulation with very restricted past operators, but was shown non-elementary in [19]. Recently, it was shown that the restricted past operators of LTrL can be replaced by certain new future operators while maintaining expressive completeness. In other work, Niebert introduced a fixed point based linear time temporal logic [11]. This logic has an elementary-time decision procesure and is equal in expressive power to the monadic second-order theory of traces.

However, the expressive powers of most other logics put forth (e.g. [1, 14, 15]) still have an unresolved relationship to each other and, in particular, to first-order logic. Most notably, it is still a challenging open problem whether or not TrPTL or TLC is expressively weaker than first-order logic. With virtually no other seperation result known, this paper is a contribution towards understanding the relative expressive power of such logics.

A weakness of TLC is that it doesn’t facilitate direct reasoning about causal relationships between the individual events on the causal chains. In this paper we remedy this deficiency and extend TLC by strengthening quantification over causal chains. This extended logic, which we call TLC^{∗}, will enjoy a similarity to CTL^{∗} [3] that TLC has to CTL. The main result of this paper is that our extension TLC^{∗} is expressively stronger than TLC for general trace alphabets whereas they express the same class of properties over trace alphabets with a transitive dependency relation. We prove this result with the aid of an Ehrenfeucht-Fraïssé game for traces that we develop. To our knowledge this is the first instance of the use of such games to obtain seperation results for temporal logics defined over partial orders. We believe that this approach is fruitful and that similar techniques may lead to other seperation results within this area.

In the next section we briefly recall Mazurkiewicz traces and a few related notions. In Section 3 we introduce TLC and TLC^{∗}, the main objects of study in this paper. We give a very simple and natural example of a property easily captured in TLC^{∗} but not in TLC. In Section 4 we define an Ehrenfeucht-Fraïssé game and prove its correspondence to TLC. We use this correspondence in Section 5 to exhibit a property which we prove is undefinable in TLC. In Section 6 we show that the said property can be defined within TLC^{∗}. Finally, we put all the pieces together to arrive at the main result. We conclude by a quick overview of the relative expressive powers of logics over traces.

2 Preliminaries

A (Mazurkiewicz) trace alphabet is a pair (Σ, I), where Σ, the alphabet, is a finite set and I ⊆ Σ×Σ is an irreflexive and symmetric independence relation. Usually, Σ consists of the actions performed by a distributed system while I captures a static notion of causal independence between actions. For the rest of the section we fix a trace alphabet (Σ, I). We define D = (Σ × Σ) − I to be the dependency relation which is then reflexive and symmetric.

Let T = (E, ≤, λ) be a Σ-labelled poset. In other words, (E, ≤) is a poset and λ : E → Σ is a labelling function. For e ∈ E we define ↓e = {x ∈ E | x ≤ e}. We also let ⋖ be the covering relation given by x ⋖ y iff x < y and for all z ∈ E, x ≤ z ≤ y implies x = z or z = y. Moreover, we let the concurrency relation be defined as x co y iff x ≰ y and y ≰ x. A Mazurkiewicz trace (over (Σ, I)) is then 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 let T R(Σ, I) denote the class of traces over (Σ, I). As usual, a trace language L is a subset of traces, i.e. L ⊆ T R(Σ, I). Throughout the paper we will not distinguish between isomorphic elements in T R(Σ, I). We will refer to members of E as events. It will be convenient to assume the existence of a unique least event ⊥ ∈ E corresponding to a system initialization event carrying no label, i.e. λ(⊥) is undefined and ⊥ < e for every e ∈ E − {⊥}.

It’s not hard to show that the traces introduced above as restricted labelled partial orders can be equivalently represented as congruence classes of strings corresponding to the same partially ordered computations (and vice versa; see e.g. [16]). We will sometimes abuse notation and let a string in Σ^{∗} denote its corresponding trace in (Σ, I) whenever no confusion arises. This is enforced by using conventional parentheses for string languages and square brackets for trace languages.

In setting the scene for defining the semantics of formulas of TLC^{∗} we first introduce some notation for sequences. The length of a finite sequence ρ will be denoted by |ρ|. In case ρ is infinite we set |ρ| = ω. Let ρ = (e_{0}, e_{1}, …, e_{n}, …) and 0 ≤ k < |ρ|. We set ρ_{k} = (e_{k}, e_{k+1}, …, e_{n}, …).

Let T = (E, ≤, λ) be a trace over (Σ, I). A future causal chain rooted at e ∈ E is a (finite or infinite) sequence ρ = (e_{0}, e_{1}, …, e_{n}, …) with e = e_{0}, e_{i} ∈ E such that e_{i−1} ⋖ e_{i} for every i ≥ 1. The labelling function λ : E → Σ is extended to causal chains in the obvious way by: λ(ρ) = (λ(e_{0})λ(e_{1}) ⋯ λ(e_{n}) ⋯). We say that a future causal chain ρ is maximal in case ρ is either infinite or it is finite and there exists no e′ ∈ E such that e_{|ρ|} ⋖ e′. A past causal chain rooted at e ∈ E is a (finite) sequence ρ = (e_{n}, …, e_{1}, e_{0}) with e = e_{0}, e_{i} ∈ E such that e_{i}⋖e_{i−1} for every 1 ≤ i ≤ n.

3 Syntax and Semantics

In this section we will define the syntax and semantics of the temporal logics over traces to be considered in this paper. We start by introducing TLC^{∗} and continue by giving an explicit definition of the sublogic TLC. We will not define first-order logic over traces (FO), but we refer the reader to e.g. [6, 16, 17].

TLC^{∗} consists of three different syntactic entities; event formulas (Φ_{ev}), future chain formulas (Φ_{ch}^{+}) and past chain formulas (Φ_{ch}^{−}) defined by mutual induction as described below:

Φ_{ev} ::= p_{a} | ∼α | α_{1} ∨ α_{2} | co(α) | E(ϕ) | E^{−}(ψ), with a ∈ Σ.
Φ_{ch}^{+} ::= α | ∼ϕ | ϕ_{1} ∨ ϕ_{2} | Xϕ | ϕ_{1}Uϕ_{2}.
Φ_{ch}^{−} ::= α | ∼ψ | ψ_{1} ∨ ψ_{2} | X^{−}ψ | ψ_{1}U^{−}ψ_{2} ,

where α, ϕ and ψ with or without subscripts here and throughout the rest of the paper are formulas of Φ_{ev}, Φ_{ch}^{+} and Φ_{ch}^{−}, respectively. The formulas of TLC^{∗}(Σ, I) are the set of event formulas Φ_{ev} as defined above^{1}.

The semantics of formulas of TLC^{∗} is divided into two parts; event formulas and chain formulas. Let T ∈ T R(Σ, I) and e ∈ E. The notion of an event formula α being satified at an event e of T is defined inductively in the following manner.

• T, e ⊧ p_{a} iff λ(e) = a.

• T, e ⊧ ∼α iff T, e |̸= α.

• T, e ⊧ α_{1} ∨ α_{2} iff T, e ⊧ α_{1} or T, e ⊧ α_{2}.

• T, e ⊧ co(α) iff there exists an e′ ∈ E with e co e′ and T, e′ ⊧ α.

• T, e ⊧ E(ϕ) iff there exists a future causal chain ρ rooted at e with T, ρ ⊧ ϕ.

• T, e ⊧ E^{−}(ψ) iff there exists a past causal chain ρ rooted at e with T, ρ ⊧ ψ.

1Another logic was in [1] termed “TLC^{∗}”, but as that logic denoted TLC interpreted over linearizations it is unrelated to our logic which seems naturally to earn the name “TLC^{∗}”.

As usual, tt = p_{a} ∨ ∼p_{a} and ff = ∼tt. Suppose ρ = (e_{0}, e_{1}, …, e_{n}, …) is a future causal chain. The notion of T, ρ ⊧ ϕ for a future chain formula ϕ is defined inductively below.

• T, ρ ⊧ α iff T, e_{0} ⊧ α.

• T, ρ ⊧ ∼ϕ iff T, ρ |̸= ϕ.

• T, ρ ⊧ ϕ_{1} ∨ ϕ_{2} iff T, ρ ⊧ ϕ_{1} or T, ρ ⊧ ϕ_{2}.

• T, ρ ⊧ Xϕ iff T, ρ_{1} ⊧ ϕ.

• T, ρ ⊧ ϕ_{1}Uϕ_{2} iff there exists a 0 ≤ k < |ρ| such that T, ρ_{k} ⊧ ϕ_{2}. Moreover, T, ρ_{m} ⊧ ϕ_{1} for each 0 ≤ m < k.

The notion of T, ρ ⊧ ψ for a past causal chain ρ and past chain formula ψ is defined in the straightforward manner. The well-known future chain operators are derived as F ϕ = ttUϕ and Gϕ = ∼F ∼ϕ.

Suppose T ∈ T R(Σ, I) and α ∈ TLC^{∗}(Σ, I). Then T satisfies α iff T, ⊥ ⊧ α, denoted T ⊧ α. The language defined by α is: L(α) = {T ∈ T R(Σ, I) | T ⊧ α}. We say that L ⊆ T R(Σ, I) is definable in TLC^{∗} if there exists some α ∈ TLC^{∗}(Σ, I) such that L(α) = L. By slight abuse of notation, the class of trace languages over (Σ, I) definable in TLC^{∗} will also be denoted by TLC^{∗}(Σ, I).

The formulas of TLC(Σ, I) — introduced in [1] with a slightly different syntax — is then the set of formulas of TLC^{∗}(Σ, I) where each of the chain operators X, U, G, X^{−}, U^{−} is immediately preceded by a chain quantifier E. As TLC will play a prominent role in this paper we will bring out its definition in more detail. More precisely, the set of formulas is given as:

TLC(Σ, I) ::= p_{a} | ∼α | α ∨ β | EX(α) | EU(α, β) |
EG(α) | EX^{−}(α) | EU^{−}(α, β) | co(α),

where a ∈ Σ. The semantics is inherited directly from TLC^{∗} in the obvious manner, so notions of definability etc. are carried over directly. It can be shown that our extension TLC^{∗} remains decidable. In work to appear we construct an elementary-time decision procedure for TLC^{∗} by means of Büchi automata.

Hence while the formulas of TLC are basically the well-known operators of the branching-time logic CTL [3] augmented with symmetrical past operators and concurrency information, the operators of TLC^{∗} are basically the well-known operators of CTL^{∗}[3] similarly extended with past quantifiers in a restricted fashion as well as concurrency information. The crucial difference is that while CTL and CTL^{∗} are branching-time logics interpreted over Kripke structures, TLC and TLC^{∗} are linear time temporal logics on traces interpreted over the underlying Hasse diagrams of the partial orders.

One of the weaknesses of TLC is that it doesn’t directly facilitate reasoning about causal relationships of the individual events of the causal chains at hand. As a consequence, a number of interesting properties are not (either easily or at all) expressible within TLC. Section 5 provides a formal proof of this claim, but we will in the following bring out another such property which is very natural.

Suppose that a and b are actions representing the acquiring and releasing, respectively, of some resource. A relevant property of this system is then whether or not there exists some causal chain in the execution of the system — presumably containing other system actions than {a, b} — such that the a’s and b’s alternate strictly until the task is perhaps eventually completed. Via the future chain formula ϕ_{xy} = p_{x} → X(∼(p_{x} ∨ p_{y})U(p_{y})) we can easily express this property in TLC^{∗} by E(G(ϕ_{ab} ∧ ϕ_{ba})). The point is here that TLC^{∗} allows us to investigate each causal chain in mention by a causal chain formula, which is then confined to this very chain. This is not possible in TLC, as the existential quantifications interpreted at some fixed event of the chain would potentially consider all causal chains originating at this event — not just the one presently being investigated.

We conclude with two important notions relating to TLC. Firstly, let α be a formula of TLC(Σ, I). The operator depth of α is defined inductively as follows:

• od(p_{a}) = 0.

• od(∼α) = od(α) and od(α ∨ β) = max(od(α), od(β)).

• od(EX(α)) = od(EG(α)) = od(EX^{−}(α)) = od(co(α)) = 1 + od(α).

• od(EU(α, β)) = od(EU^{−}(α, β)) = 1 + max(od(α), od(β)).

The set of formulas of operator depth k is denoted by OD(k).

Given T_{0}, T_{1} ∈ T R(Σ, I) and e_{i} events of T_{i} we define that (T_{0}, e_{0}) ≡_{n} (T_{1}, e_{1}) if for any formula α ∈ TLC(Σ, I) with od(α) ≤ n, T_{0}, e_{0} ⊧ α iff T_{1}, e_{1} ⊧ α, i.e. both structures agree on all subformulas of operator depth at most n ≥ 0. It is then not hard to see that (T_{0}, e_{0}) ≡_{0} (T_{1}, e_{1}) iff e_{0} and e_{1} are identically labelled, i.e. either λ(e_{0}) = λ(e_{1}) or e_{0} = e_{1} = ⊥.

4 An Ehrenfeucht-Fraïssé Game for TLC

In this section we will present an Ehrenfeucht-Fraïssé game to capture the expressive power of TLC. The game is played directly on the poset representation of (finite or infinite) Mazurkiewicz traces and it is similar in spirit to the Ehrenfeucht-Fraïssé game for LTL introduced by Etessami and Wilke [7]. We extend their approach to the richer setting of traces by highlighting current causal chains in the until-based moves and adding past- and co-moves.

The EF-TLC game is a game played between two persons, Spoiler and Preserver, on a pair of traces (T_{0}, T_{1}). The game is played over k rounds starting from an initial game state (e_{0}, e_{1}) and after each round the current game state is a pair of events (e′_{0}, e′_{1}) with e′_{i} ∈ E_{i}. Each round starts with the game in some specific initial game state (e_{0}, e_{1}) and Spoiler chooses one of the moves defined below and the game proceeds accordingly:

EX-Move: This move can only be played by Spoiler if there exists an e′_{0} ∈ E_{0} such that e_{0} ⋖ e′_{0} or there exists an e′_{1} ∈ E_{1} such that e_{1} ⋖ e′_{1}. Spoiler then wins the game in case there either exists no e′_{0} ∈ E_{0} such that e_{0} ⋖ e′_{0} or no e′_{1} ∈ E_{1} such that e_{1} ⋖ e′_{1}. Otherwise (in which case both e_{0} and e_{1} has ⋖-successors) the game proceeds as follows:

1. Spoiler chooses i ∈ {0, 1}, and an event e′_{i} ∈ E_{i} such that e_{i} ⋖ e′_{i}.

2. Preserver responds by choosing an event e′_{1−i} ∈ E_{1−i} such that e_{1−i} ⋖ e′_{1−i}.

3. The new game state is now (e′_{0}, e′_{1}).

EU-Move:

1. Spoiler chooses i ∈ {0, 1}, and an event e′_{i} ∈ E_{i} such that e_{i} ≤ e′_{i} and he highlights a future causal chain (e_{i} = f_{i}^{0}, f_{i}^{1}, …, f_{i}^{n} = e′_{i}) with n ≥ 0.

2. Preserver responds by choosing an event e′_{1−i} ∈ E_{1−i} with e_{1−i} ≤ e′_{1−i} such that if e_{i} = e′_{i} then e_{1−i} = e′_{1−i}. Furthermore she highlights a future causal chain (e_{1−i} = f_{1−i}^{0}, f_{1−i}^{1}, …, f_{1−i}^{m} = e′_{1−i}) with m ≥ 0.

3. Spoiler now chooses one of the following two steps:

• Spoiler sets the game state to (e′_{0}, e′_{1}).

• Spoiler chooses an event f_{1−i} ∈ {f_{1−i}^{0}, f_{1−i}^{1} … f_{1−i}^{m}}. Preserver responds with an event f_{i} ∈ {f_{i}^{0}, f_{i}^{1} … f_{i}^{n}} and the game continues in the state (f_{0}, f_{1}).

EG-Move:

1. Spoiler chooses i ∈ {0, 1}, and highlights a maximal future causal chain (e_{i} = f_{i}^{0}, f_{i}^{1}, …, f_{i}^{n}, …) with f_{i}^{j} ∈ E_{i} and n ≥ 0.

2. Preserver responds by highlighting a maximal future causal chain (e_{1−i} = f_{1−i}^{0}, f_{1−i}^{1}, …, f_{1−i}^{m}, …) with f_{i}^{j} ∈ E_{1−i} and m ≥ 0.

3. Spoiler chooses an event f_{1−i} ∈ {f_{1−i}^{0}, f_{1−i}^{1} … f_{1−i}^{m}}. Preserver responds with an event f_{i} ∈ {f_{i}^{0}, f_{i}^{1} … f_{i}^{n}} and the game continues in the state (f_{0}, f_{1}).

co-Move: This move can only be played by Spoiler if there exists an e′_{0} ∈ E_{0} such that e_{0} co e′_{0} or there exists an e′_{1} ∈ E_{1} such that e_{1} co e′_{1}. Spoiler then wins the game in case there either exists no e′_{0} ∈ E_{0} such that e_{0} co e′_{0} or no e′_{1} ∈ E_{1} such that e_{1} co e′_{1}. Otherwise (in which case both e_{0} and e_{1} have concurrent events) the game proceeds as follows:

1. Spoiler chooses i ∈ {0, 1}, and an event e′_{i} ∈ E_{i} such that e_{i} co e′_{i} in T_{i}.

2. Preserver responds by choosing an event e′_{1−i} ∈ E_{1−i} such that e_{1−i} co e′_{1−i} in T_{1−i}.

3. The new game state is now (e′_{0}, e′_{1}).

EX^{−}-Move: This move can only be played by Spoiler if e_{0} ≠ ⊥ or e_{1} ≠ ⊥. Spoiler then wins the game in case e_{0} = ⊥ or e_{1} = ⊥. Otherwise (in which case neither e_{0} nor e_{1} is ⊥) the game proceeds as follows:

1. Spoiler chooses i ∈ {0, 1}, and an event e′_{i} ∈ E_{i} such that e′_{i} ⋖ e_{i}.

2. Preserver responds by choosing an event e′_{1−i} ∈ E_{1−i} such that e′_{1−i} ⋖ e_{1−i}.

3. The new game state is now (e′_{0}, e′_{1}).

EU^{−}-Move:

1. Spoiler chooses i ∈ {0, 1}, and an event e′_{i} ∈ E_{i} such that e′_{i} ≤ e_{i} and he highlights a past causal chain (e′_{i} = f_{i}^{n}, f_{i}^{n−1}, …, f_{i}^{0} = e_{i}) with n ≥ 0.

2. Preserver responds by choosing an event e′_{1−i} ∈ E_{1−i} with e′_{1−i} ≤ e_{1−i} such that if e_{i} = e′_{i} then e_{1−i} = e′_{1−i}. Furthermore she highlights a past causal chain (e′_{1−i} = f_{1−i}^{m}, f_{1−i}^{m−1}, …, f_{1−i}^{0} = e_{1−i}) with m ≥ 0.

3. Spoiler now chooses one of the following two steps:

• Spoiler sets the game state to (e′_{0}, e′_{1}).

• Spoiler chooses an event f_{1−i} ∈ {f_{1−i}^{0}, f_{1−i}^{1} … f_{1−i}^{m}}. Preserver responds with an event f_{i} ∈ {f_{i}^{0}, f_{i}^{1} … f_{i}^{n}} and the game continues in the state (f_{0}, f_{1}).

In the 0-round game Spoiler wins if (T_{0}, e_{0}) ≢_{0} (T_{1}, e_{1}) and otherwise Preserver wins. In the (k + 1)-round game Spoiler wins if (T_{0}, e_{0}) ≢_{0} (T_{1}, e_{1}). If it is the case that (T_{0}, e_{0}) ≡_{0} (T_{1}, e_{1}), a round is played according to the above moves. This round either results in a win for Spoiler (e.g. by the EX-move) or a new game state (e′_{0}, e′_{1}). In the latter case, a k-round game is then played starting from the initial game state (e′_{0}, e′_{1}).

We say that Preserver has a winning strategy in the k-round game on (T_{0}, e_{0}) and (T_{1}, e_{1}), denoted (T_{0}, e_{0}) ∼_{k} (T_{1}, e_{1}), if she can win the k-round game on the structures T_{0} and T_{1} starting in the initial game state (e_{0}, e_{1}) no matter which moves are performed by Spoiler. If not, we say that Spoiler has a winning strategy. We refer to [7] for basic intuitions about the game.

Our interest in the game lies in the following fact.

Proposition 4.1 For every k ≥ 0, (T_{0}, e_{0}) ∼_{k} (T_{1}, e_{1}) iff (T_{0}, e_{0}) ≡_{k} (T_{1}, e_{1}).

Proof: We prove that (T_{0}, e_{0}) ∼_{k} (T_{1}, e_{1}) iff (T_{0}, e_{0}) ≡_{k} (T_{1}, e_{1}) by induction on k. The base case where k = 0 follows trivially from the definition.

For the inductive step suppose that the claim is true for k. We first prove the direction from left to right. Suppose that (T_{0}, e_{0})∼_{k+1}(T_{1}, e_{1}). Let α ∈ TLC(Σ, I) with od(α) = k + 1. We must show that T_{0}, e_{0} ⊧ α iff T_{1}, e_{1} ⊧ α. It suffices to prove the statement when the top-level connective of α is a chain-operator because by boolean combinations (T_{0}, e_{0}) and (T_{1}, e_{1}) would then agree on all formulas of operator depth k + 1. We will only consider the case where the top-level chain-operator is EU. The other cases follow similarly.

Suppose now α = EU(β, β′). Assume without loss of generality that T_{0}, e_{0} ⊧ α, i.e. there exists a future causal chain ρ^{0} = (f_{0}^{0}, f_{0}^{1}, …, f_{0}^{n}) with e_{0} = f_{0}^{0} and f_{0}^{n} = e′_{0} such that T_{0}, f_{0}^{j} ⊧ β for each 0 ≤ j < n and T_{0}, e′_{0} ⊧ β′. Hence we let Spoiler play the EU-move on T_{0} and make him highlight ρ^{0} on T_{0}. Preserver now uses her winning strategy and highlights ρ^{1} = (f_{1}^{0}, f_{1}^{1}, …, f_{1}^{m}) with e_{1} = f_{1}^{0} and f_{1}^{m} = e′_{1}. Two subcases now arise.

Assume first that Spoiler sets the new game state to (e′_{0}, e′_{1}). As e′_{1} was chosen from Preserver’s winning strategy we have that (T_{0}, e′_{0})∼_{k}(T_{1}, e′_{1}) which by induction hypothesis implies that (T_{0}, e′_{0})≡_{k}(T_{1}, e′_{1}). Thus T_{1}, e′_{1} ⊧ β′. Now, assume that Spoiler instead picked an event f_{1} on ρ^{1}. By Preserver’s winning strategy she could pick an event f_{0} on ρ^{0} (This is possible due to the requirement that if e_{0} = e′_{0} then e_{1} = e′_{1}). Again by the winning strategy we have that (T_{0}, f_{0})∼_{k}(T_{1}, f_{1}) and by induction hypothesis that T_{1}, f_{1} ⊧ β. Hence T_{1}, f_{1} ⊧ EU(β, β′), which concludes this direction of the proof.

We prove the direction from right to left by contraposition, so suppose that (T_{0}, e_{0}) ≁_{k+1} (T_{1}, e_{1}). We will then exhibit a formula α ∈ TLC(Σ, I) with od(α) = k + 1 such that T_{0}, e_{0} ⊧ α but T_{1}, e_{1} |̸= α. Again, we will only prove the case where Spoiler’s first move of his winning strategy is either the EU-move. The other cases either follows in analogous or easier manners.

Suppose Spoiler plays the EU-move on T_{0} (without loss of generality), i.e. he chooses a future causal chain ρ^{0} = (f_{0}^{0}, f_{0}^{1}, …, f_{0}^{n}) with e_{0} = f_{0}^{0} and f_{0}^{n} = e′_{0}. It is not hard to show by induction that there are only a finite number of semantically inequivalent formulas α with od(α) ≤ k and T_{0}, e ⊧ α for any e ∈ E_{0}. Hence, each formula β_{0}^{j} = ⋀{α ∈ OD(k) | T_{0}, f_{0}^{j} ⊧ α} ∧ ⋀{∼α ∈ OD(k) | T_{0}, f_{0}^{j} |̸= α} is well-defined and equivalent to a formula of operator depth k for each 0 ≤ j < n, so letting β_{e′_{0}} = β_{0}^{n} we have that α = EU(⋁_{0≤j<n} β_{0}^{j}, β_{e′_{0}}) is a TLC-formula with od(α) = k + 1 and by definition T_{0}, e_{0} ⊧ α. We will argue that T_{1}, e_{1} |̸= α.

Suppose that T_{1}, e_{1} ⊧ α. Then there exists a future causal chain ρ^{1} = (f_{1}^{0}, f_{1}^{1}, …, f_{1}^{m}) with e_{1} = f_{1}^{0} and f_{1}^{m} = e′_{1} such that T_{1}, f_{1}^{l} ⊧ ⋁_{0≤j<n} β_{0}^{j} for each 0 ≤ l < m and T_{1}, e′_{1} ⊧ β_{e′_{0}}.

Assume first that Spoiler chooses to set the new game state to (e′_{0}, e′_{1}) by following his winning strategy. As T_{1}, e′_{1} ⊧ β_{e′_{0}} it must be the case that for each γ ∈ OD(k), T_{0}, e′_{0} ⊧ γ iff T_{1}, e′_{1} ⊧ γ. By induction hypothesis (T_{0}, e′_{0})∼_{k}(T_{1}, e′_{1}) which contradicts that Spoiler has a winning strategy because Preserver could initially have played ρ^{1} as above and continued according to (T_{0}, e′_{0})∼_{k}(T_{1}, e′_{1}).

Now assume that Spoiler instead by his winning strategy picks an event f_{1} on ρ^{1}. Then T_{1}, f_{1} ⊧ β_{0}^{j} for some 0 ≤ j < n as T_{1}, f_{1} ⊧ ⋁_{0≤j<n} β_{0}^{j}. Again by induction hypothesis we know that (T_{0}, f_{0}^{j})∼_{k}(T_{1}, f_{1}) which again contradicts that Spoiler has a winning strategy because Preserver could respond by picking f_{0}^{j} ∈ E_{0} and continue from the game state (f_{0}^{j}, f_{1}) according to (T_{0}, f_{0}^{j})∼_{k}(T_{1}, f_{1}).

Hence T_{1}, e_{1} |̸= α as required. □

5 An Undefinability Result

In this section we will give an example of a natural property which we, by means of the game characterization of the previous section, will show is not definable in TLC. Let (Σ, I) be a trace alphabet with {a, b, c} ⊆ Σ such that a D c and c D b but a I b. Consider L = [abcabc]^{∗} ⊆ T R(Σ, I).

Lemma 5.1 L is not definable in TLC(Σ, I).

Proof: Let k ≥ 0 be given and consider T_{0}^{k} = [abc]^{4k} and T_{1}^{k} = [abc]^{4k+1}. It suffices to show that (T_{0}^{k}, ⊥)∼_{k}(T_{1}^{k}, ⊥). By Proposition 4.1 it then follows that (T_{0}^{k}, ⊥)≡_{k}(T_{1}^{k}, ⊥). Suppose L would be definable by a TLC-formula α of operator depth n. In particular then (T_{0}^{n}, ⊥)≡_{n}(T_{1}^{n}, ⊥). However, by definition it must be the case that T_{0}^{n} ∈ L and T_{1}^{n} ∉ L, contradicting that T_{0}^{n} and T_{1}^{n} satisfy the same set of formulas of operator depth at most n. Hence, L cannot be expressed by any formula of TLC assuming (T_{0}^{k}, ⊥)∼_{k}(T_{1}^{k}, ⊥) holds for any k ≥ 0. The remainder of the proof will be devoted to showing that it is the case that (T_{0}^{k}, ⊥)∼_{k}(T_{1}^{k}, ⊥). To bring this out we need a few definitions.

[figure: a; a; a; a; a; a; ⊥; c; c; …; c; c; c; c; …; c; c; b; b; b; b; b; b; |; ∥; 2k; ∥; 2k; |; 1; a; a; a; a; a; a; a; ⊥; c; c; …; c; c; c; c; …; c; c; c; b; b; b; b; b; b; b]

Figure 1: T_{0}^{k} (top) and T_{1}^{k} (bottom) on which the game is played.

As depicted in Figure 1 the game is played on T_{0}^{k} and T_{1}^{k} consisting of 4k and 4k + 1 copies of the trace factor [abc], respectively. The section of e_{i} for i ∈ {0, 1} is then defined to be the number of the enclosing [abc]-factor in T_{k}^{i} counting from left and starting with 1. We denote this number by sect(e_{i}). In case e_{i} = ⊥ we set sect(e_{i}) = 0. Furthermore, we say that e_{0} and e_{1} are position equivalent, in case either (e_{0}, e_{1}) = (⊥, ⊥) or λ(e_{0}) = λ(e_{1}). From the definition of T_{0} and T_{1} it follows that e_{0} and e_{1} are position equivalent in case e_{0} and e_{1} denote the same local positions in two (possibly distinct) sections of T_{0} and T_{1}, respectively. The unique event of section s ≥ 1 labelled with letter x ∈ {a, b, c} in T_{i}^{k} will be denoted e_{i}^{x,s}. For example, the fourth b-labelled event of T_{0}^{k} is denoted e_{0}^{b,4}.

We will then show that Preserver has a strategy such that after k′ ≤ k rounds played on (T_{0}^{k}, T_{1}^{k}) with current game state (e_{0}, e_{1}), the following invariant holds:

(i) e_{0} and e_{1} are position equivalent.

(ii) sect(e_{0}) = sect(e_{1}) or sect(e_{0}) = sect(e_{1}) − 1.

(iii) sect(e_{0}) = sect(e_{1}) implies sect(e_{0}) ≤ 2(k + k′).

(iv) sect(e_{0}) = sect(e_{1}) − 1 implies sect(e_{0}) ≥ 2(k − k′) + 1.

We prove that the invariant holds by induction on k′. It is trivial to observe, that in the base case we have that (e_{0}, e_{1}) = (⊥, ⊥), sect(e_{0}) = sect(e_{1}) = 0 and k′ = 0 thus satisfying (i),(ii), (iii) and (iv) above.

For the inductive step, assume that the statement holds for k′ < k. From (i) it follows that (T_{0}, e_{0}) ≡_{0} (T_{1}, e_{1}), so a next round is played. We then show that the Preserver can move so as to maintain the invariant for the next game state (e′_{0}, e′_{1}) by case analysis on the next move chosen by Spoiler. We only consider the case for the EU-move. The other moves follow analogously. From (ii) we know that sect(e_{0}) = sect(e_{1}) or sect(e_{0}) = sect(e_{1}) − 1, so two subcases arise. \underline{Subcase I: sect(e_{0}) = sect(e_{1}).} Suppose Spoiler chooses to play the EU-move on T_{0}^{k} and highlights a future causal chain ρ^{0} = (e_{0} = e_{0}^{x_{0},s_{0}}, e_{0}^{x_{1},s_{1}}, …, e_{0}^{x_{n},s_{n}} = e′_{0}). By assumption sect(e_{0}) ≤ 2(k + k′).

Suppose first that s_{n} ≤ 2(k + k′ + 1). Then Preserver can just copy the move and respond with ρ^{1} = (e_{1} = e_{1}^{x_{0},s_{0}}, e_{1}^{x_{1},s_{1}}, …, e_{1}^{x_{n},s_{n}} = e′_{1}). If Spoiler chooses to set the new game state to (e′_{0}, e′_{1}), sect(e′_{0}) = sect(e′_{1}) ≤ 2(k+k′+1) and the invariant is maintained. If Spoiler instead chooses to pick an event e_{1}^{x_{i},s_{i}}, Preserver would respond by picking e_{0}^{x_{i},s_{i}} and the invariant is maintained in a similar manner.

Suppose then that s_{n} > 2(k + k′ + 1). Preserver must then “insert” an additional occurrence of a section into ρ^{0} at section 2(k + k′ + 1). To bring this out, let l be the least index such that s_{l} = 2(k + k′ + 1), which exists by assumption. Preserver then responds with

ρ^{1} = (e_{1}^{x_{0},s_{0}}, …, e_{1}^{x_{l},s_{l}}, e_{1}^{x_{l+1},s_{l+1}}, e_{1}^{x_{l},s_{l}+1}, e_{1}^{x_{l+1},s_{l+1}+1}, e_{1}^{x_{l+2},s_{l+2}+1}, …, e_{1}^{x_{n},s_{n}+1})

with e′_{1} = e_{1}^{x_{n},s_{n}+1}. If Spoiler chooses to set the new game state to (e′_{0}, e′_{1}), sect(e′_{0}) = s_{n} = sect(e′_{1}) − 1. However, the invariant is maintained as sect(e′_{0}) ≥ 2(k + k′ + 1) ≥ 2(k − (k′ + 1)) + 1. If Spoiler instead chooses to pick an event on ρ^{1}, Preserver responds dependent upon its index. If Spoiler picks one of the first l + 2 events e_{1}^{x_{i},s_{i}}, Preserver responds with e_{0}^{x_{i},s_{i}}. As sect(e_{0}^{x_{i},s_{i}}) = s_{i} = sect(e_{1}^{x_{i},s_{i}}) ≤ 2(k + k′ + 1) the invariant is maintained. If Spoiler picks one of the remaining events e_{1}^{x_{i},s_{i}+1}, Preserver responds with e_{0}^{x_{i},s_{i}} in which case sect(e_{0}^{x_{i},s_{i}}) = s_{i} = sect(e_{1}^{x_{i},s_{i}+1}) − 1 and the invariant is maintained as sect(e_{0}^{x_{i},s_{i}}) ≥ 2(k + k′ + 1) > 2(k − (k′ + 1)) + 1.

Suppose spoiler chooses to play the EU-move on T_{1}^{k} and highlights a future causal chain ρ^{1} = (e_{1} = e_{1}^{x_{0},s_{0}}, e_{1}^{x_{1},s_{1}}, …, e_{1}^{x_{n},s_{n}} = e′_{1}). By assumption sect(e_{0}) ≤ 2(k + k′). If s_{n} ≤ 2(k + k′ + 1) then Preserver can, as above, just copy the move and maintain the invariant, so suppose that s_{n} > 2(k +k′ +1).

Preserver must then “chop” a duplicate occurrence off ρ^{1} around the sections 2(k + k′) + 1, 2(k + k′) + 2 = 2(k + k′ + 1), 2(k + k′) + 3 which exist by construction. Any causal chain passing through these three sections must pass (at least) two identical ac-labelled or bc-labelled stretches. Now, let l be the least index such that s_{l} = 2(k + k′) + 1 and consider the sequence σ = (x_{l}, x_{l+2}, x_{l+4}) with λ(σ) ∈ {a, b}^{3}. Remove from σ the first occurrence x_{i} where there exists an j > i with x_{j} in σ and x_{i} = x_{j}. Let σ′ = (x_{p}, x_{q}) denote the resulting sequence where p, q ∈ {l, l + 2, l + 4}. Preserver then plays the chain ρ^{0}:

(e_{0}^{x_{0},s_{0}}, …, e_{0}^{x_{l−1},s_{l−1}}, e_{0}^{x_{p},s_{l}}, e_{0}^{c,s_{l+1}}, e_{0}^{x_{q},s_{l+2}}, e_{0}^{c,s_{l+3}}, e_{0}^{x_{l+5},s_{l+5}−1}, …, e_{0}^{x_{n},s_{n}−1})

with e′_{0} = e_{0}^{x_{n},s_{n}−1}. If Spoiler chooses to set the new game state to (e′_{0}, e′_{1}) then sect(e′_{0}) = s_{n} = sect(e′_{1}) − 1 so the invariant is maintained because s_{n} > 2(k + k′ + 1) > 2(k − (k′ + 1)) + 1. If Spoiler chooses to pick an event on ρ^{0}, Preserver responds according to one of several cases. If Spoiler picks one of the first l events e_{0}^{x_{i},s_{i}} then Preserver picks e_{1}^{x_{i},s_{i}} and the invariant is maintained as usual. If Spoiler picks either e_{0}^{c,s_{l+1}} or e_{0}^{c,s_{l+3}} then Preserver picks either e_{1}^{c,s_{l+1}} or e_{1}^{c,s_{l+3}}, respectively. As the sections are both s_{l+1} or both s_{l+3} and s_{l+1} < s_{l+3} = s_{l} + 1 = 2(k + k′ + 1) the invariant follows. If Spoiler picks an event, e_{0}^{x_{m},s} say, in {e_{0}^{x_{p},s_{l}}, e_{0}^{x_{q},s_{l+2}}} before the removed occurrence in σ then m ∈ {l, l + 2} and Preserver responds by e_{1}^{x_{m},s}. Then sect(e_{0}^{x_{m},s}) = s = sect(e_{1}^{x_{m},s}) ≤ s_{l+2} = 2(k + k′ + 1). Similarly, if e_{0}^{x_{m},s} occurs after the removed occurrence then m ∈ {l+2, l+4} and Preserver picks e_{1}^{x_{m},s+1}. Then sect(e_{0}^{x_{m},s}) = s = sect(e_{1}^{x^{m},s+1}) − 1 ≥ 2(k + k′) > 2(k − (k′ + 1)) + 1 and in both cases the invariant is maintained. Finally, if Spoiler picks one of the remaining events e_{0}^{x_{i},s_{i}−1} with i ≥ l + 5 then Preserver responds with e_{1}^{x_{i},s_{i}}. As sect(e_{0}^{x_{i},s_{i}−1}) = sect(e_{1}^{x_{i},s_{i}}) − 1 ≥ 2(k − (k′ + 1)) + 1 the invariant is also maintained in this case.

\underline{Subcase II: sect(e_{0}) = sect(e_{1}) − 1.} Here the futures of e_{0} in T_{0}^{k} and e_{1} in T_{1}^{k} both consist of 4k −sect(e_{0}) factors of [abc] and are identical with respect to future moves. Hence Preserver can just “copy” the move made by Spoiler. with the obvious correspondence. □

6 The Expressiveness of TLC^{∗}

Let (Σ, I) be any trace alphabet with {a, b, c} ⊆ Σ such that a D c and c D b but a I b. Consider L = [abcabc]^{∗} ⊆ T R(Σ, I) from the previous section.

Lemma 6.1 L is definable in TLC^{∗}(Σ, I).

Proof: Our proof will in fact show that the future fragment of TLC with only one future chain quantifier of TLC^{∗} suffices to express L. First define

α_{[abc]^{∗}} = AG( ⋀_{d∈Σ−{a,b,c}} ∼p_{d}) ∧ EX(p_{a} ∧ EX(p_{c})) ∧ EX(p_{b} ∧ EX(p_{c})) ∧
AG(p_{c} ∧ EX(tt) → EX(p_{a} ∧ EX(p_{c})) ∧ EX(p_{b} ∧ EX(p_{c})).

It is easy to see that T ⊧ α_{[abc]^{∗}} iff T ∈ [abc]^{∗}. We will then use existence of “zig-zagging” future causal chains to restrict to [abcabc]^{∗} ⊂ [abc]^{∗} below. Define the future chain formula ϕ_{(acbc)^{∗}} as follows.

ϕ_{(acbc)^{∗}} = p_{a} ∧ G(p_{a} → X(p_{c} ∧ X(p_{b} ∧ X(p_{c} ∧ (∼Xtt ∨ Xp_{a}))))).

It’s easy to see that T, e ⊧ E(ϕ_{(acbc)^{∗}}) iff there exists a future causal chain ρ rooted at e such that λ(ρ) ∈ (acbc)^{∗} ⊆ Σ^{∗}. The statement of the lemma now follows by taking α_{L} = α_{[abc]^{∗}} ∧ (∼EXtt ∨ EX(E(ϕ_{(acbc)^{∗}}))). □

Putting all the pieces together, we can now state and prove the main result of the paper.

Theorem 6.2 Let (Σ, I) be any trace alphabet. Then

1. TLC(Σ, I) = TLC^{∗}(Σ, I) if D is transitive.

2. TLC(Σ, I) ⊂ TLC^{∗}(Σ, I) if D is not transitive.

Proof: Obviously TLC(Σ, I) ⊆ TLC^{∗}(Σ, I), so (2) follows easily from Lemma 5.1 and Lemma 6.1 as (a, c), (c, b) ∈ D but (a, b) ∉ D witness that D is not transitive. Hence it suffices to prove (1).

Let (Σ, I) be a trace alphabet with D transitive, i.e. the graph (Σ, D) is a disjoint union of cliques {C_{i}}_{i=1}^{n}. Thus any trace T ∈ T R(Σ, I) consists of disjoint C_{i}-labelled causal chains only initially connected by ⊥. We can then define three mutually inductive translations || · ||_{ev}, || · ||_{ch}^{+} and || · ||_{ch}^{−} converting event formulas, future chain formulas and past chain formulas, respectively, of TLC^{∗}(Σ, I) to formulas of TLC(Σ, I) as follows.

• ||p_{a}||_{ev} = p_{a} and the boolean connectives are as expected.

• ||co(α)||_{ev} = co(||α||_{ev}).

• ||E(ϕ)||_{ev} = ||ϕ||_{ch}^{+} and ||E^{−}(ϕ)||_{ev} = ||ϕ||_{ch}^{−}.

• ||α||_{ch}^{+} = ||α||_{ch}^{−} = ||α||_{ev} and the boolean connectives are as expected.

• ||Xϕ||_{ch}^{+} = EX(||ϕ||_{ch}^{+}) and ||X^{−}ϕ||_{ch}^{−} = EX^{−}(||ϕ||_{ch}^{−}).

• ||ϕUψ||_{ch}^{+} = EU(||ϕ||_{ch}^{+}, ||ψ||_{ch}^{+}) and ||ϕU^{−}ψ||_{ch}^{−} = EU(||ϕ||_{ch}^{−}, ||ψ||_{ch}^{−}).

By nested inductions one can show that for each α ∈ TLC^{∗}(Σ, I), T, e ⊧ α iff T, e ⊧ ||α||_{ev}. As ||α||_{ev} ∈ TLC(Σ, I) the required conclusion follows. □

One can show that TLC^{∗}(Σ, I) can be expressed within MSO(Σ, I). Moreover, it’s not hard to see that FO(Σ, I), TLC(Σ, I) and TLC^{∗}(Σ, I) are all expressively equivalent in the sequential case where I = ∅. Hence, we obtain the following corollary.

Corollary 6.3

1. TLC^{∗}(Σ, ∅) ⊂ MSO(Σ, ∅).

2. TLC^{∗}(Σ, I) ⊈ FO(Σ, I) if D is not transitive.

Proof: The proof of (1) follows from TLC^{∗}(Σ, ∅) = FO(Σ, ∅) and the wellknown classical fact that FO(Σ, ∅) ⊂ MSO(Σ, ∅).

For the proof of (2), let (Σ, I) be given and suppose D is not transitive. As before, we can then define L = [abcabc]^{∗}. By a standard argument one can show that ((abc + bac)(abc + bac))^{∗}, the set of linearizations of L, is not a first-order definable language of strings over Σ. From [6] it then follows that L is not definable in FO(Σ, I). Lemma 6.1 now yields the required conclusion. □

We conclude by summarizing what is currently known about the relative expressive powers of the various linear time temporal logics over traces. A quick overview is displayed in Figure 2. 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, while cut lines denote negation.

Theorem 6.2 and Corollary 6.3 have been applied to place TLC^{∗} in Figure 2. Like most other logics, its relationship to the first-order logic of traces needs to be pinned down exactly. Also, one might try to capture the expressive power of TLC^{∗} as (fragments of) either FO^{2}(TC), two-variable first-order

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

Figure 2: Overview of relative expressive powers

logic of traces augmented with the transitive-closure operator, or MSO with set quantifications restricted to causal chains. This constitutes an interesting open problem to be investigated in future work.

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 (LICS’95), 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] Clarke, E. M., Emerson, E. A., Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2) (1986) 244– 263

[4] Diekert, V., Gastin, P.: An expressively complete temporal logic without past tense operators for Mazurkiewicz traces. Proceedings of the 13th Annual Conference of the European Association for Computer Science Logic (CSL’99), Lecture Notes in Computer Science 1683, Springer-Verlag (1999)

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

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

[7] Etessami, K., Wilke, Th.: An until hierarchy for temporal logic. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press (1996) 108–117

[8] Godefroid, P.: Partial-order methods for the verification of concurrent systems. Lecture Notes in Computer Science 1032, Springer-Verlag (1996)

[9] 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)

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

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

[12] 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

[13] 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

[14] 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

[15] 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 [16] Thiagarajan, P. S., Henriksen, J. G.: Distributed versions of linear time

temporal logic: A trace perspective. In Reisig and Rozenberg (Eds.), Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science 1491, Springer-Verlag (1998) 643–681

[17] 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

[18] Valmari, A.: A stubborn attack on state explosion. Formal Methods in Systems Design 1 (1992) 285–313

[19] 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 1443, Springer-Verlag (1998) 140–151

Recent BRICS Report Series Publications

RS-99-26 Jesper G. Henriksen. An Expressive Extension of TLC. September 1999. 20 pp. To appear in Thiagarajan and Yap, editors, Fifth Asian Computing Science Conference, ASIAN ’99 Proceedings, LNCS, 1998.

RS-99-25 Gerth Stølting Brodal and Christian N. S. Pedersen. Finding Maximal Quasiperiodicities in Strings. September 1999. 20 pp.

RS-99-24 Luca Aceto, Willem Jan Fokkink, and Chris Verhoef. Conservative Extension in Structural Operational Semantics. September 1999. 23 pp. To appear in the Bulletin of the EATCS.

RS-99-23 Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. August 1999. 14 pp. To appear in Gordon and Pitts, editors, 3rd Workshop on Higher Order Operational Techniques in Semantics, HOOTS ’99 Proceedings, ENTCS, 1999.

RS-99-22 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers. August 1999. 22 pp.

RS-99-21 Olivier Danvy. An Extensional Characterization of Lambda-Lifting and Lambda-Dropping. August 1999. 13 pp. Extended version of an article to appear in Fourth Fuji International Symposium on Functional and Logic Programming, FLOPS ’99 Proceedings (Tsukuba, Japan, November 11–13, 1999). This report supersedes the earlier report BRICS RS-98-2.

RS-99-20 Ulrich Kohlenbach. A Note on Spector’s Quantifier-Free Rule of Extensionality. August 1999. 5 pp. To appear in Archive for Mathematical Logic.

RS-99-19 Marcin Jurdziński and Mogens Nielsen. Hereditary History Preserving Bisimilarity is Undecidable. June 1999. 18 pp.

RS-99-18 M. Oliver Möller and Harald Rueß. Solving Bit-Vector Equations of Fixed and Non-Fixed Size. June 1999. 18 pp. Revised version of an article appearing under the title Solving Bit-Vector Equations in Gopalakrishnan and Windley, editors, Formal Methods in Computer-Aided Design: Second International Conference, FMCAD ’98 Proceedings, LNCS 1522, 1998, pages 36–48.