Automata, Languages and Programming, 29th International Colloquium, Proceedings: P. Widmayer, F.T. Ruiz, R. Morales, M. Hennessy, S. Eidenbenz, R. Conejo(eds.) Springer Lecture Notes in Computer Science 2382 (2002), 938–949.

An Elementary Expressively Complete Temporal Logic for Mazurkiewicz Traces^{⋆}

Paul Gastin^{1} and Madhavan Mukund^{2}

1 LIAFA, Université Paris 7, 2, place Jussieu, F-75251 Paris Cedex 05

         Fax: 33 1 44 27 68 49 — Paul.Gastin@liafa.jussieu.fr

2 Chennai Mathematical Institute, 92 G N Chetty Road, Chennai 600 017, India

               Fax: 91 44 823 3671 — madhavan@cmi.ac.in

Abstract. In contrast to the classical setting of sequences, no temporal logic has yet been identified over Mazurkiewicz traces that is equivalent to first-order logic over traces and yet admits an elementary decision procedure. In this paper, we describe a local temporal logic over traces that is expressively complete and whose satisfiability problem is in Pspace. Contrary to the situation for sequences, past modalities are essential for such a logic. A somewhat unexpected corollary is that first-order logic with three variables is expressively complete for traces. Keywords Temporal logics, Mazurkiewicz traces, concurrency

1 Introduction

Linear-time temporal logic (LTL) [15] has established itself as a useful formalism for specifying the interleaved behaviour of reactive systems. To combat the combinatorial blow-up involved in describing computations of concurrent systems in terms of interleavings, there has been a lot of interest in using temporal logic more directly on labelled partial orders.

Mazurkiewicz traces [12] are labelled partial orders generated by dependence alphabets of the form (Σ, D), where D is a dependence relation over Σ. If (a, b) ∉ D, a and b are deemed to be independent actions that may occur concurrently. Traces are a natural formalism for describing the behaviour of static networks of communicating finite-state agents [26].

LTL over Σ-labelled sequences is equivalent to FO_{Σ}(<), the first-order logic over Σ-labelled linear orders [11] and thus defines the class of aperiodic languages over Σ. Though FO_{Σ}(<) permits assertions about both the past and the future, future modalities suffice for establishing the expressive completeness of LTL with respect to FO_{Σ}(<) [9]. From a practical point of view, a finite-state program may be checked against an LTL specification relatively efficiently [2, 19, 20].

Though a number of LTL-like temporal logics have been proposed for reasoning directly about Mazurkiewicz traces, it has proved elusive to define a tractable logic that is expressively complete with respect to FO_{Σ}(<), the first order logic

⋆ Work done while the second author was visiting LIAFA, Université Paris 7. Partial support of CEFIPRA-IFCPAR Project 2102-1 (ACSMV) is gratefully acknowledged.

over traces. The first expressively complete temporal logic over traces was described in [17]. The result was refined in [3, 5] to show expressive completeness without past modalities, using an extension of the proof technique developed for LTL in [24, 25]. Formulae in both these logics are defined at global configurations (maximal antichains). Unfortunately, reasoning at the level of global configurations makes the complexity of deciding satisfiability non-elementary [21].

Computational tractability seems to require interpreting formulae at local states—effectively at individual events. This approach was followed (sometimes indirectly) in early temporal logics over traces [1, 13, 16, 18]. While model-checking is relatively efficient for these logics, they are not known to be expressively complete. In fact, the logic TLC described in [1] is not even first-order definable.

Recently, an expressively complete local temporal logic has been defined for the subclass of Mazurkiewicz traces where the dependence graph of the underlying alphabet has a series-parallel structure [4]. Unfortunately, this logic cannot be expressively complete over all traces—the logic uses only future modalities and, unlike LTL over sequences, there exist two first-order inequivalent traces that cannot be distinguished using only future modalities [23].

In this paper, we define a new local temporal logic over traces that is expressively complete and whose satisfiability problem is in Pspace. The observation in [23] about the shortcoming of future modalities necessitates the introduction of past modalities in our logic. As in [3, 4], we show expressive completeness using an extension to traces of the proof technique introduced in [24, 25] for LTL over sequences. However, the earlier proofs exploit the fact that the past cannot affect the truth of a formula. The introduction of past modalities in our logic requires the use of new techniques for “relativizing” formulae placed in new past contexts. The satisfiability problem for our logic is settled using two-way alternating automata, extending techniques from [1, 4].

A corollary of our main result is that FO_{(Σ,D)}^{3}(<), the subclass of first-order logic formulae with at most three variables, is expressively complete over traces, extending the same result for sequences. This is somewhat surprising—intuition suggests that we require variables proportional to the width of a trace. (This result has been independently established by Walukiewicz [22].)

The paper is organized as follows. We begin with some preliminaries about traces. In Section 3 we define our new temporal logic. Section 4 describes a syntactic partition of traces that is used in Section 5 to establish expressive completeness. The decision procedure for satisfiability is sketched in Section 6. We conclude with a discussion of open questions. Many proofs have had to be omitted in this extended abstract.

2 Preliminaries

We briefly recall some notions about Mazurkiewicz traces (see [6] for background). A dependence alphabet is a pair (Σ, D) where the alphabet Σ is a finite set of actions and the dependence relation D ⊆ Σ ×Σ is reflexive and symmetric. The independence relation I is the complement of D. For A ⊆ Σ, the set of letters independent of A is denoted by I(A) = {b ∈ Σ | (a, b) ∈ I for all a ∈ A} and the set of letters depending on (some action in) A is denoted by D(A) = Σ \ I(A).

A Mazurkiewicz trace is a labelled partial order t = [V, ≤, λ] where V is a set of vertices labelled by λ : V → Σ and ≤ is a partial order over V satisfying the following conditions: For all x ∈ V, the downward set ↓x = {y ∈ V | y ≤ x} is finite, (λ(x), λ(y)) ∈ D implies x ≤ y or y ≤ x, and x⋖y implies (λ(x), λ(y)) ∈ D, where ⋖ = < \ <^{2} is the immediate successor relation in t.

The alphabet of a trace t is the set alph(t) = λ(V) ⊆ Σ and its alphabet at infinity, alphinf(t), is the set of letters occurring infinitely often in t. The set of all traces is denoted by ℝ(Σ, D) or simply by ℝ. A trace t is called finite if V is finite. For t = [V, ≤, λ] ∈ ℝ, we define min(t) ⊆ V as the set of all minimal vertices of t. We can also read min(t) ⊆ Σ as the set of labels of the minimal vertices of t. It will be clear from the context what we actually mean.

Let t_{i} = [V_{i}, ≤_{i}, λ_{i}], i ∈ {1, 2}, be a pair of traces such that V_{1} ∩ V_{2} = ∅ and alphinf(t_{1}) × alph(t_{2}) ⊆ I. We define the concatenation of t_{1} and t_{2} to be t_{1} · t_{2} = [V, ≤, λ] where V = V_{1} ∪ V_{2}, λ = λ_{1} ∪ λ_{2} and ≤ is the transitive closure of ≤_{1} ∪ ≤_{2} ∪ (V_{1} × V_{2} ∩ λ^{−1}(D)). The set of finite traces is then a monoid, denoted 𝕄(Σ, D) or simply 𝕄, with the empty trace 1 = (∅, ∅, ∅) as unit.

Here is some useful notation for subclasses of traces. For C ⊆ Σ, let ℝ_{C} = {t ∈ ℝ | alph(t) ⊆ C} and 𝕄_{C} = 𝕄 ∩ ℝ_{C}. Also, (alphinf = C) = {t ∈ ℝ | alphinf(t) = C} and (min = C) = {t ∈ ℝ | min(t) = C}. For A, C ⊆ Σ, we set ℝ_{C}^{A} = ℝ_{C} ∩ (alphinf = A). Observe that 𝕄_{C} = ℝ_{C}^{∅}.

The first order logic over traces FO_{Σ}(<) is given by the syntax:

φ ::= P_{a}(x) | x < y | ¬φ | φ ∨ φ | ∃xφ,

where a ∈ Σ and x, y ∈ Var are first order variables. For a trace t = [V, ≤, λ] and a valuation σ : Var → V, t, σ ⊧ φ denotes that t satisfies φ under σ. We interpret each predicate P_{a} by the set {x ∈ V | λ(x) = a} and the relation < as the strict partial order relation of t. The semantics then lifts to all formulas as usual. Since the meaning of a closed formula (sentence) φ is independent of the valuation σ, we can associate with each sentence φ the language L(φ) = {t ∈ ℝ | t ⊧ φ}. A trace language L ⊆ ℝ is said to be expressible in FO_{Σ}(<) if there is a sentence φ ∈ FO_{Σ}(<) such that L = L(φ). For n > 0, FO_{Σ}^{n}(<) denotes the set of formulae with at most n distinct variables (possibly bound and reused several times).

We use the algebraic notion of recognizability (see e.g. [14]). Let h : 𝕄 → S be a morphism to a finite monoid S. For t, u ∈ ℝ, we say that t and u are h-similar, denoted t ∼_{h} u, if either t, u ∈ 𝕄 and h(t) = h(u) or t and u have infinite factorizations in non-empty finite traces t = t_{1}t_{2} ⋯, u = u_{1}u_{2} ⋯ with h(t_{i}) = h(u_{i}) for all i. The transitive closure ≈_{h} of ∼_{h} is an equivalence relation. Since S is finite, this equivalence relation is of finite index with at most |S|^{2} +|S| equivalence classes. A trace language L ⊆ ℝ is recognized by h if it is saturated by ≈_{h} (or equivalently by ∼_{h}), i.e., t ∈ L implies [t]_{≈_{h}} ⊆ L for all t ∈ ℝ.

Let L ⊆ ℝ be recognized by a morphism h : 𝕄 → S. For B ⊆ Σ, L ∩ 𝕄_{B} and L ∩ ℝ_{B} are recognized by h↾_{𝕄_{B}} the restriction of h to 𝕄_{B}.

A finite monoid S is aperiodic if there is an n ≥ 0 such that s^{n} = s^{n+1} for all s ∈ S. A trace language L ⊆ ℝ is aperiodic if it is recognized by some morphism to a finite and aperiodic monoid.

Theorem 1 ([8, 7]). A language L ⊆ ℝ(Σ, D) is expressible in FO_{Σ}(<) if and only if it is aperiodic.

3 Local temporal logic

Our local temporal logic over traces consists of two types of formulae: internal formulae, evaluated at arbitrary events within a trace, and initial formulae, asserting properties of minimal events of the trace. Internal formulae only talk about the structure within a connected portion of a trace. Initial formulae permit us to combine local assertions across disjoint components and form “global” assertions about the structure of the trace.

The set LocTL_{Σ}^{i} of internal formulae over the alphabet Σ is defined as follows:

φ ::= a ∈ Σ | ¬φ | φ ∨ φ | EX φ | φ U_{C} φ, C ⊆ Σ | EY φ | φ S_{C} φ, C ⊆ Σ

Let t = [V, ≤, λ] ∈ ℝ be a finite or infinite trace and let x ∈ V be some vertex of t. We write t, x ⊧ φ to denote that trace t at node x satisfies the formula φ ∈ LocTL_{Σ}^{i}. This is defined inductively as follows:

t, x ⊧ a  if λ(x) = a
t, x ⊧ ¬φ  if t, x |̸= φ
t, x ⊧ φ ∨ ψ if t, x ⊧ φ or t, x ⊧ ψ
t, x ⊧ EX φ if ∃y. x ⋖ y and t, y ⊧ φ
t, x ⊧ EY φ if ∃y. y ⋖ x and t, y ⊧ φ
t, x ⊧ φ U_{C} ψ if ∃z ≥ x. [t, z ⊧ ψ and ∀y. (x ≤ y < z) ⇒ t, y ⊧ φ and ∀y. (λ(y) ∈ C and y ≤ z) ⇒ y ≤ x]
t, x ⊧ φ S_{C} ψ if ∃z ≤ x. [t, z ⊧ ψ and ∀y. (z < y ≤ x) ⇒ t, y ⊧ φ and ∀y. (λ(y) ∈ C and y ≤ x) ⇒ y ≤ z]

The modalities EX and EY are existential extensions of the next state and previous state operators X and Y of LTL. The modality U_{C} extends the “universal” until operator U defined in [4] with an alphabetic filter that restricts the actions performed while fulfilling an until requirement. If t, x ⊧ φ U_{C} ψ then no C-actions are performed when going from x to the node satisfying ψ. Since the filter also applies to events that are concurrent to x, the modality U_{C} no longer looks purely at the future of an event. Similarly, S_{C} is a filtered extension of the LTL since operator. The intuitive meanings of U_{C} and S_{C} are depicted below.

[figure: φ U_{C} ψ; ψ; ¬C; φ ∧ ¬C; ψ; φ S_{C} ψ; ¬C; φ ∧ ¬C]

Past modalities are essential, as indicated by the following example from [23], where the dependence relation is a − b − c − d. These two traces are not first-order equivalent but are bisimilar at the level of events and thus cannot be distinguished by pure future modalities. However, the two traces below can be distinguished using the filtered until, which is not pure future.

\begin{aligned}a & → & b & → & c & → & b & → & c & ⋯ \\ & & ↑ \\ d & → & c \end{aligned}  \begin{aligned}d & → & c & → & b & → & c & → & b & ⋯ \\ & & ↑ \\ a & → & b \end{aligned}

For the same alphabet, one can also show that the language ad(bc)^{∗} ⊆ 𝕄 of finite traces is first order but cannot be expressed by pure future modalities.

As usual, we can derive useful operators. Using unfiltered versions of until and since, φU ψ = φU_{∅} ψ and φS ψ = φS_{∅} ψ, we recover the classical modalities eventually in the future F φ = ⊤ U φ, eventually in the past F^{−1} φ = ⊤ S φ, always in the future G φ = ¬ F ¬φ, and always in the past G^{−1} φ = ¬ F^{−1} ¬φ. We also use some filtered versions of these modalities: F_{b} φ = ⊤ U_{b} φ (eventually in the future but above the same b’s), G_{b} φ = ¬ F_{b} ¬φ (for all future vertices that are above the same b’s). The existence of a successor (resp. a predecessor) above the same b’s can be written as follows:

EX_{b} φ = ⋁_{d≠b} EX(d ∧ φ) ∧ ⊤ U_{b} d = ⋁_{c} c ∧ EX(¬b ∧ φ ∧ ⊤ S_{b} c),
EY_{b} φ = ⋁_{c} EY(c ∧ φ) ∧ ⊤ S_{b} c = ⋁_{d≠b} d ∧ EY(φ ∧ ⊤ U_{b} d).

Finally, F^{∞} a = F a ∧ G(a ⇒ EX F a) expresses the existence of infinitely many vertices labelled with a above the current vertex. The filtered version of this formula, F_{b}^{∞} a = F_{b} a ∧ G_{b}(a ⇒ EX_{b} F_{b} a), requires in addition that the vertices labelled with a are above the same b’s.

For A ⊆ Σ, let A denote the internal formula ⋁_{a∈A} a. An alphabetic since is a formula of the form A S_{C} a for A, C ⊆ Σ and a ∈ Σ.

We turn now to initial formulae. These are boolean combinations of formulae EM φ asserting that some minimal vertex in the trace satisfies the internal formula φ. Formally, the set LocTL_{Σ} of initial formulae over Σ is given by:

α ::= ⊥ | EM φ, φ ∈ LocTL_{Σ}^{i} | ¬α | α ∨ α

The semantics is defined as follows:

t ⊧ EM φ if ∃x. (x ∈ min(t) and t, x ⊧ φ)
t ⊧ ¬α if t |̸= α
t ⊧ α ∨ β if t ⊧ α or t ⊧ β

An initial formula α ∈ LocTL_{Σ} defines the trace language L(α) = {t ∈ ℝ | t ⊧ α}. We can then express various alphabetic properties using initial formulae: L(EM a) = {t ∈ ℝ | a ∈ min(t)}, L(EM F a) = {t ∈ ℝ | a ∈ alph(t)}, and L(EM F^{∞} a) = {t ∈ ℝ | a ∈ alphinf(t)}. Therefore, for C ⊆ Σ, trace languages such as (alphinf = C) and (min = C) are expressible in LocTL_{Σ}.

The following result is immediate from the definition of LocTL_{Σ}.

Proposition 2. If a trace language is expressible in LocTL_{Σ}, then it is expressible in FO_{Σ}^{3}(<).

4 Decomposition of traces

The proof of our main result is a case analysis based on partitioning the set of traces according to the structure of the trace. Fix a letter b ∈ Σ and set B = Σ \ {b}. Using the notation introduced in the middle of Section 2, let Γ^{A} = {t ∈ ℝ_{B}^{A} | min(t) ⊆ D(b)}, Γ = Γ^{∅}, and Ω_{A} = {t ∈ ℝ_{I(A)} | min(t) ⊆ {b}}.

Each trace t ∈ ℝ has a unique factorization t = t_{0}bt_{1}bt_{2} ⋯ with t_{0} ∈ ℝ_{B} and t_{i} ∈ ℝ_{B} ∩ (min ⊆ D(b)) for all i > 0. We obtain the following partition of ℝ.

ℝ = 𝕄_{B}(bΓ)^{∞} ⊎ ( ⋃_{A≠∅} ℝ_{B}^{A}Ω_{A}) ⊎ ( ⋃_{A≠∅} 𝕄_{B}(bΓ)^{∗}bΓ^{A}Ω_{A})

If all t_{i} are finite, then we are in the first block. If t_{0} ∉ 𝕄, then we are in the second block. Otherwise, we are in the last block. Note that 𝕄_{B}(bΓ)^{∗} = 𝕄. The three possibilities are depicted below.

(1) [figure: 𝕄_{B}; b; b; b; Γ; Γ; ⋯] (2) [figure: ℝ_{B}^{A}; b; Ω_{A}]

(3) [figure: 𝕄_{B}; b; b; b; b; Γ; ⋯; Γ; Γ^{A}; b; Ω_{A}]

The following two results will allow us to use this decomposition effectively in proving the expressive completeness of our logic.

Lemma 3. All these sets are expressible in LocTL_{Σ}. More precisely,

1. The sets 𝕄_{B}(bΓ)^{∗} and 𝕄_{B}(bΓ)^{ω} are expressible in LocTL_{Σ}.

2. ℝ_{B}^{A} · Ω_{A} = L(α) where

α = ( ⋀_{a∈A} EM(¬b ∧ F_{b}^{∞} a)) ∧ ( ⋀_{a∉A} ¬ EM(¬b ∧ F_{b}^{∞} a)).

3. 𝕄_{B}(bΓ)^{∗}bΓ^{A}Ω_{A} = 𝕄bΓ^{A}Ω_{A} = L(β) where

β = ⋁_{C⊆Σ}((alphinf = C) ∧ EM F(b ∧ ⋀_{c∈C} F^{∞} c ∧ ⋀_{a∈A} F_{b}^{∞} a ∧ ⋀_{a∉A} ¬ F_{b}^{∞} a)).

Note that “the” b in 𝕄bΓ^{A}Ω_{A} is characterized by the formula b ∧ F_{b}^{∞} a, where a is any letter in A.

Lemma 4. Let A ⊆ Σ and let L ⊆ ℝ be a trace language recognized by a morphism h from 𝕄 into a finite monoid S. Then,

(1) L ∩ 𝕄_{B}(bΓ)^{∞} = ⋃ ; finite(L_{1} ∩ 𝕄_{B}) · (L_{2} ∩ (bΓ)^{∞})
(2) L ∩ ℝ_{B}^{A}Ω_{A}  = ⋃ ; finite(L_{1} ∩ ℝ_{B}^{A}) · (L_{2} ∩ Ω_{A})
(3) L ∩ 𝕄bΓ^{A}Ω_{A} = ⋃ ; finite(L_{1} ∩ 𝕄_{B})(L_{2} ∩ (bΓ)^{∗})b(L_{3} ∩ Γ^{A})(L_{4} ∩ Ω_{A})

where the trace languages L_{i} ⊆ ℝ are recognized by h.

5 Expressive completeness

We now show that our temporal logic for traces is expressively complete with respect to FO_{Σ}(<). In light of Theorem 1, it suffices to establish the following.

Theorem 5. Every aperiodic trace language L ⊆ ℝ is expressible in LocTL_{Σ}.

From Proposition 2 and Theorems 1 and 5, we deduce immediately

Corollary 6. Let L ⊆ ℝ be a trace language. The following are equivalent

1. L is aperiodic,
3. L is expressible in FO_{Σ}^{3}(<),

2. L is expressible in LocTL_{Σ},
4. L is expressible in FO_{Σ}(<).

In the rest of this section, we sketch a proof of Theorem 5. We start with a trace language L ⊆ ℝ recognized by a morphism h from 𝕄 to a finite aperiodic monoid S. We use induction on |Σ|.

The base case is when Σ = {a}, a singleton. Then L is either a finite set or the union of a finite set and a set of the form a^{n}a^{∗}, n ≥ 0. In both cases, L is expressible in LocTL_{Σ}. For instance, {a^{ω}} and {a^{2}} correspond to the formulae EM G EX ⊤ and EM EX ¬ EX ⊤. Also, a^{3}a^{∗} ∪ {a^{ω}} is expressed by EM EX EX ⊤.

For the induction step, with |Σ| > 1, we fix a letter b ∈ Σ and use the decomposition introduced in Section 4. Therefore, we have

L = (L ∩ 𝕄_{B}(bΓ)^{∞}) ⊎ (L ∩ ⋃_{A≠∅} ℝ_{B}^{A}Ω_{A}) ⊎ (L ∩ ⋃_{A≠∅} 𝕄_{B}(bΓ)^{∗}bΓ^{A}Ω_{A}).

We show separately that the three languages above are expressible in LocTL_{Σ}. From Lemma 4, it suffices to establish the following.

Proposition 7. Recall that B = Σ \ {b}. Let A ⊆ Σ be non-empty and let L ⊆ ℝ be a trace language recognized by h. Then,

(1) (L ∩ ℝ_{B}) · (min ⊆ {b}) is expressible in LocTL_{Σ}.

(2) 𝕄_{B} · (L ∩ (bΓ)^{∞}) is expressible in LocTL_{Σ}.

(3) L ∩ 𝕄_{B}(bΓ)^{∞} is expressible in LocTL_{Σ}.

(4) ℝ_{B}^{A} · (L ∩ Ω_{A}) is expressible in LocTL_{Σ}.

(5) L ∩ ℝ_{B}^{A}Ω_{A} is expressible in LocTL_{Σ}.

(6) 𝕄_{B}(L ∩ (bΓ)^{∗})bΓ^{A}Ω_{A} is expressible in LocTL_{Σ}.

(7) 𝕄b(L ∩ Γ^{A})Ω_{A} is expressible in LocTL_{Σ}.

(8) 𝕄bΓ^{A}(L ∩ Ω_{A}) is expressible in LocTL_{Σ}.

(9) L ∩ 𝕄bΓ^{A}Ω_{A} is expressible in LocTL_{Σ}.

In all cases, we use the induction hypothesis to derive a formula for the factor over a smaller alphabet and then relativize this formula to the full class. As a representative example, we sketch the proof of Proposition 7(1,2,3).

Proof of Proposition 7(1). The language L ∩ ℝ_{B} is recognized by h ↾_{𝕄_{B}} (Section 2). By the induction hypothesis, it is expressible in LocTL_{B}: L ∩ ℝ_{B} = L_{B}(α) = {t ∈ ℝ_{B} | t ⊧ α} for some α ∈ LocTL_{B}. Let α̃ ∈ LocTL_{Σ} be the formula given by Lemma 8 below. We have (L ∩ ℝ_{B}) · (min ⊆ {b}) = L_{Σ}(α̃). ⊓ ⊔

Lemma 8. Let α ∈ LocTL_{B}. There exists a formula α̃ ∈ LocTL_{Σ} such that for all t = t_{1}t_{2} with t_{1} ∈ ℝ_{B} and min(t_{2}) ⊆ {b}, t_{1} ⊧ α iff t ⊧ α̃.

Proof. We show simultaneously a similar result for internal formulae: for all φ ∈ LocTL_{B}^{i}, there exists a formula φ̃ ∈ LocTL_{Σ}^{i} such that for all t = t_{1}t_{2} with t_{1} ∈ ℝ_{B} and min(t_{2}) ⊆ {b}, and for all x ∈ t_{1}, t_{1}, x ⊧ φ iff t, x ⊧ φ̃. We use structural induction on α and φ. We have { \atop α ∨ β} = α̃ ∨ β̃, ˜¬α = ¬α̃, { \atop EM φ} = EM(¬b∧φ̃), { \atop φ ∨ ψ} = φ̃∨ψ̃, ˜¬φ = ¬φ̃, ã = a, { \atop EX φ} = EX_{b} φ̃, { \atop EY φ} = EY φ̃,

{ \atop φ U_{C} ψ} = φ̃ U_{C∪\{b\}} ψ̃, and { \atop φ S_{C} ψ} = φ̃ S_{C} ψ̃. ⊓ ⊔

To prove Proposition 7(2), we use a reduction to the word case. Let LTL_{T} (XU) denote LTL over T -labelled sequences with the strong until modality XU—for t = t_{1}t_{2} ⋯ ∈ T^{∞}, t ⊧ f XU g if there exists j > 1 such that t_{j}t_{j+1} ⋯ ⊧ g and t_{k}t_{k+1} ⋯ ⊧ f for all 1 < k < j. From the theory of LTL over sequences, we know that every aperiodic word language K ∈ T^{∞} is expressible in LTL_{T} (XU).

We fix T = h(bΓ) and define σ : (bΓ)^{∞} → T^{∞} by σ(x) = h(bx_{1})h(bx_{2}) ⋯ if x = bx_{1}bx_{2} ⋯ with x_{i} ∈ Γ for i ≥ 1. The map σ is well-defined since each trace x ∈ (bΓ)^{∞} has a unique factorization x = bx_{1}bx_{2} ⋯ with x_{i} ∈ Γ for i ≥ 1.

We begin with the following result.

Lemma 9. Let L ⊆ ℝ be recognized by h. Then, L ∩ (bΓ)^{∞} = σ^{−1}(K) for some K expressible in LTL_{T} (XU).

Proof. Let K = σ(L ∩ (bΓ)^{∞}). We first show that L ∩ (bΓ)^{∞} = σ^{−1}(K). The inclusion ⊆ is clear. Conversely, let x = bx_{1}bx_{2} ⋯ ∈ L∩(bΓ)^{∞} and y ∈ σ^{−1}(σ(x)). Then, y = by_{1}by_{2} ⋯ ∈ (bΓ)^{∞} with h(bx_{i}) = h(by_{i}) for all i. Therefore, y ∼_{h} x and x ∈ L implies y ∈ L.

Next, we show that K is recognized by the evaluation morphism e : T^{∗} → S defined by e(u) = u for all u ∈ T.

Let s, t ∈ T^{∞} with s ∼_{e} t and s ∈ K. Write s = s_{1}s_{2} ⋯ ∈ T^{∞} and t = t_{1}t_{2} ⋯ ∈ T^{∞}. Since T = h(bΓ) we find x = bx_{1}bx_{2} ⋯ ∈ L with x_{i} ∈ Γ and h(bx_{i}) = s_{i} for all i > 1; and y = by_{1}by_{2} ⋯ with y_{i} ∈ Γ and h(by_{i}) = t_{i} for all i > 1. From s ∼_{e} t we deduce that x ∼_{h} y. Since x ∈ L, y ∈ L and t = σ(y) ∈ K.

Since S is aperiodic, K ⊆ T^{∞} is an aperiodic language over T and is thus expressible in LTL_{T} (XU)—this is the only place where we use S aperiodic. ⊓ ⊔

The next step is to show that if K ⊆ T^{∞} is expressible in LTL_{T} (XU) then σ^{−1}(K) is expressible in LocTL_{Σ}.

Lemma 10. Let f ∈ LTL_{T} (XU). There exists f̃ ∈ LocTL_{Σ}^{i} such that for all t = t_{1}t′ with t_{1} ∈ 𝕄 and t′ ∈ (bΓ)^{∞} \ {1}, we have σ(t′) ⊧ f iff t, min(t′) ⊧ f̃.

Proof Sketch. We use a structural induction on f. Clearly, ˜¬f = ¬f̃ and { \atop f ∨ g} = f̃∨ g̃. We claim that { \atop f XU g} = EX((¬b ∨ f̃) U (b ∧ g̃)).

Let t′ = t_{2}t_{3} ⋯ with t_{i} ∈ bΓ for all i > 1 and let x = min(t′).

Assume that σ(t′) ⊧ f XU g and let j > 2 be such that σ(t_{j}t_{j+1} ⋯) ⊧ g and σ(t_{k}t_{k+1} ⋯) ⊧ f for 2 < k < j. Let x′ ∈ t with x ⋖ x′ and z = min(t_{j}). We have x′ ≤ z, λ(z) = b and t, z ⊧ g̃, by induction. Suppose y ∈ t with x′ ≤ y < z. Either λ(y) ≠ b and t, y ⊧ ¬b, or there exists 2 < k < j with y = min(t_{k}) and, by induction, t, y ⊧ f̃. Therefore, t, x′ ⊧ (¬b ∨ f̃) U (b ∧ g̃) and t, x ⊧ EX((¬b ∨ f̃) U (b ∧ g̃)).

Conversely, assume that t, x ⊧ EX((¬b ∨ f̃) U (b ∧ g̃)). Let x′, z ∈ t with x ⋖ x′ ≤ z, t, z ⊧ b ∧ g̃ and t, y ⊧ ¬b ∨ f̃ for all x′ ≤ y < z. Since λ(z) = b, there exists j > 2 with z = min(t_{j}) and by induction, we get σ(t_{j}t_{j+1} ⋯) ⊧ g. Now, let 2 < k < j and y = min(t_{k}). We have x′ ≤ y < z and since λ(y) = b we get t, y ⊧ f̃ and σ(t_{k}t_{k+1} ⋯) ⊧ f by induction. Therefore, σ(t′) ⊧ f XU g.

It remains to deal with a formula of the form f = s ∈ T. For all r ∈ S, the trace language h_{B}^{−1}(r) ⊆ 𝕄_{B} is aperiodic and, by induction on |Σ|, h_{B}^{−1}(r) = L_{B}(α_{r}) for some formula α_{r} ∈ LocTL_{B}. Let α̃_{r} ∈ LocTL_{Σ}^{i} be the formula obtained using Lemma 11. We claim that s̃ = ⋁_{h(b)·r=s} α̃_{r}.

We write t′ = bt_{2}t_{3} with t_{2} ∈ Γ and t_{3} ∈ (bΓ)^{∞}. Let r = h(t_{2}). Then, t_{2} ⊧ α_{r} and by Lemma 11 we obtain t, min(t′) ⊧ α̃_{r}. Now, if σ(t′) ⊧ s then s = h(bt_{2}) = h(b)r and we get t, min(t′) ⊧ s̃.

Conversely, assume that t, min(t′) ⊧ α̃_{r} for some r with s = h(b)r. By Lemma 11 we get t_{2} ⊧ α_{r} and h(t_{2}) = r. Hence, h(bt_{2}) = s and σ(t′) ⊧ s. ⊓ ⊔

Lemma 11. For all α ∈ LocTL_{B}, there is a formula α̃ ∈ LocTL_{Σ}^{i} such that for all t = t_{1}bt_{2}t_{3} ∈ ℝ with t_{1} ∈ 𝕄, t_{2} ∈ ℝ_{B}, min(t_{2}) ⊆ D(b) and min(t_{3}) ⊆ {b} we have t_{2} ⊧ α iff t, min(bt_{2}t_{3}) ⊧ α̃.

[figure: t_{1}; b; t_{2}; b; t_{3}]

Proof. We simultaneously establish an equivalent result for internal formulae: for all φ ∈ LocTL_{B}^{i}, there exists a formula φ̃ ∈ LocTL_{Σ}^{i} such that for all t = t_{1}bt_{2}t_{3} ∈ ℝ with t_{1} ∈ 𝕄, t_{2} ∈ ℝ_{B}, min(t_{2}) ⊆ D(b) and min(t_{3}) ⊆ {b} and for all x ∈ t_{2}, we have t_{2}, x ⊧ φ iff t, x ⊧ φ̃.

We proceed by structural induction on α and φ. As always, we have ˜¬α = ¬α̃, { \atop α ∨ β} = α̃ ∨ β̃, ˜¬φ = ¬φ̃, and { \atop φ ∨ ψ} = φ̃ ∨ ψ̃. Now, { \atop EM φ} = EX(¬b ∧ φ̃), ã = a, { \atop EX φ} = EX_{b} φ̃, { \atop EY φ} = EY_{b}(¬b ∧ φ̃),

\begin{matrix}{ \atop φ U_{C} ψ} = & ⋁_{E⊆Σ}φ̃ U_{(C∩E)∪\{b\}} (ψ̃ ∧ E S b) \\ { \atop φ S_{C} ψ} = & ⋁_{E⊆Σ}(E S b) ∧ (φ̃ S_{(C∩E)∪\{b\}} (ψ̃ ∧ ¬b)). \end{matrix}

We prove the formula for U_{C}. Let x ∈ t_{2} with t_{2}, x ⊧ φ U_{C} ψ. Let z ∈ t_{2} be such that x ≤ z, t_{2}, z ⊧ ψ, t_{2}, y ⊧ φ for all x ≤ y < z, and for all y ∈ t_{2}, y ≤ z and λ(y) ∈ C implies y ≤ x. By induction, t, z ⊧ ψ̃ and t, y ⊧ φ̃ for all x ≤ y < z.

Let E = alph(↓_{t_{2}} z) = alph({y ∈ t_{2} | y ≤ z}). Clearly, t, z ⊧ E S b. Let y ∈ t with y ≤ z. If λ(y) = b, then y ≤ min(bt_{2}t_{3}) ≤ x. If λ(y) ∈ C ∩ E, then there exists y′ ∈ t_{2} such that λ(y′) = λ(y) ∈ C and y ≤ y′. From y′ ≤ z, we deduce y′ ≤ x and then y ≤ y′ ≤ x.

Conversely, let x ∈ t_{2} and E ⊆ Σ with t, x ⊧ φ̃ U_{(C∩E)∪{b}} (ψ̃ ∧ E S b). Let z ∈ t with x ≤ z, t, z ⊧ ψ̃ ∧ E S b, t, y ⊧ φ̃ for all x ≤ y < z, and for all y ≤ z, λ(y) ∈ (C ∩ E) ∪ {b} implies y ≤ x. If z ∈ t_{3} then y = min(t_{3}) satisfies λ(y) = b, y ≤ z and y ≰ x, a contradiction. Therefore, z ∈ t_{2} and by induction, we get t_{2}, z ⊧ ψ and t_{2}, y ⊧ φ for all x ≤ y < z. Now, let y ∈ t_{2} with y ≤ z and λ(y) ∈ C. Since t, z ⊧ E S b we deduce that alph(↓_{t_{2}} z) ⊆ E. Therefore, λ(y) ∈ C ∩ E and we obtain y ≤ x. ⊓ ⊔

Proof of Proposition 7(2). By Lemma 9, L ∩ (bΓ)^{∞} = σ^{−1}(L_{T} (f)) for some f ∈ LTL_{T} (XU). Let f̃ ∈ LocTL_{Σ}^{i} be given by Lemma 10 and define the formula γ = EM(b ∧ f̃) ∨ EM(¬b ∧ F_{b} EX(b ∧ f̃)). We claim that

𝕄_{B} · (L ∩ (bΓ)^{∞} \ {1}) = 𝕄_{B} · (bΓ)^{∞} ∩ L(γ).

Indeed, let t = t_{1}t′ with t_{1} ∈ 𝕄_{B}, t′ ∈ L ∩ (bΓ)^{∞} \ {1} and let x = min(t′). We have σ(t′) ⊧ f and by Lemma 10 we get t, x ⊧ f̃. Now, if x ∈ min(t) we have t ⊧ EM(b ∧ f̃) and otherwise we have t ⊧ EM(¬b ∧ F_{b} EX(b ∧ f̃)).

Conversely, let t = t_{1}t′ with t_{1} ∈ 𝕄_{B}, t′ ∈ (bΓ)^{∞} and assume that t ⊧ γ. Necessarily, b ∈ alph(t) and therefore t′ ≠ 1. From t ⊧ γ we deduce that t, x ⊧ b ∧ f̃ with x = min(t′). By Lemma 10 we get σ(t′) ⊧ f. Therefore, t′ ∈ σ^{−1}(L_{T} (f)) ⊆ L and t belongs to the left-hand side.

Since 𝕄_{B} · (bΓ)^{∞} and 𝕄_{B} are both expressible in LocTL_{Σ}, we deduce that 𝕄_{B} · (L ∩ (bΓ)^{∞}) is expressible in LocTL_{Σ}. ⊓ ⊔

Proof of Proposition 7(3). From Lemma 4, L ∩ 𝕄_{B}(bΓ)^{∞} is a finite union of languages of the form (L_{1} ∩𝕄_{B})·(L_{2} ∩(bΓ)^{∞}) where the trace languages L_{i} ⊆ ℝ are recognized by h. Now, since the product 𝕄_{B}(bΓ)^{∞} is unambiguous, we have

(L_{1} ∩ 𝕄_{B}) · (L_{2} ∩ (bΓ)^{∞}) = (L_{1} ∩ 𝕄_{B}) · (bΓ)^{∞} ∩ 𝕄_{B} · (L_{2} ∩ (bΓ)^{∞})
(L_{1} ∩ 𝕄_{B}) · (bΓ)^{∞} = (𝕄_{B} · (bΓ)^{∞}) ∩ ((L_{1} ∩ ℝ_{B}) · (min ⊆ {b})).

We conclude using Lemma 3 and Proposition 7(1,2). ⊓ ⊔

We can prove Proposition 7(1-3) using no EY and only sinces of the form A S_{C} a (“alphabetic” sinces). If L ⊆ 𝕄 then L = L ∩ 𝕄_{B}(bΓ)^{∗}, so we only need to consider the first case in the decomposition. From this, we have the following.

Theorem 12. Let L ⊆ 𝕄 be a trace language recognized by h. Then, L is expressible in LocTL_{Σ} without using EY and with alphabetic sinces only.

6 Satisfiability

To decide satisfiability, we work with alternating automata over sequentializations of traces. The states of the alternating automaton consist of subformulas of the main formula together with bookkeeping information about the letters traversed while satisfying until and since requirements. The basic technique we use was introduced in [1] and refined in [4]. The additional complication for our logic is that we have to deal with past requirements, both explicitly in the operators EY and S_{C}, and implicitly, because of the alphabetic filters in U_{C} and S_{C}. We thus need two-way alternating automata. Nevertheless, checking emptiness for this class remains within Pspace [10] for each fixed dependence alphabet (Σ, D). Due to space constraints, we omit all details of the construction.

7 Open problems

As we have seen in Section 3, the introduction of past modalities is unavoidable when constructing an expressively complete local temporal logic over traces. A natural question is whether unfiltered versions of U_{C} and S_{C} are sufficient for expressive completeness. We also do not know whether the temporal logic based only on EX and U_{C} is expressively complete. Another alternative is to keep the unfiltered until and to use a concurrency modality asserting the existence of a concurrent vertex satisfying some formula. Also, we have seen in Theorem 12 that no EY are required for finite traces and that alphabetic sinces are sufficient. We do not know whether the same restriction applies to infinite traces.

References

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

2. C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. formal Methods in System Design, 1:275–288, 1992.

3. V. Diekert and P. Gastin. LTL is expressively complete for Mazurkiewicz traces. In Proceedings of ICALP 2000, number 1853 in LNCS, pages 211–222. Springer Verlag, 2000.

4. V. Diekert and P. Gastin. Local temporal logic is expressively complete for cograph dependence alphabets. In Proceedings of LPAR’01, number 2250 in LNAI, pages 55–69. Springer Verlag, 2001.

5. V. Diekert and P. Gastin. LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences, 2002. To appear.

6. V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.

7. W. Ebinger and A. Muscholl. Logical definability on infinite traces. Theoretical Computer Science, 154:67–84, 1996.

8. W. Ebinger. Charakterisierung von Sprachklassen unendlicher Spuren durch Logiken. Dissertation, Institut für Informatik, Universität Stuttgart, 1994.

9. D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proceedings of PoPL’80, pages 163–173, Las Vegas, Nev., 1980.

10. T. Jiang and B. Ravikumar. A note on the space complexity of some decision problems for finite automata. Information Processing Letters, 40:25–31, 1991.

11. J.A.W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, California, 1968.

12. A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.

13. P. Niebert. A ν-calculus with local views for sequential agents. In Proceedings of MFCS’95, number 969 in LNCS, pages 563–573. Springer Verlag, 1995.

14. D. Perrin and J.-E. Pin. Infinite words. Technical report, LITP, Avril 1997.

15. A. Pnueli. The temporal logics of programs. In Proceedings of the 18th IEEE FOCS, 1977, pages 46–57, 1977.

16. R. Ramanujam. Locally linear time temporal logic. In Proceedings of LICS’96, pages 118–128, 1996.

17. P.S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. In Proceedings of LICS’97, pages 183–194, 1997.

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

19. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of LICS’86, pages 322–331, 1986.

20. M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, number 1043 in LNCS, pages 238–266. Springer Verlag, 1996.

21. I. Walukiewicz. Difficult configurations – on the complexity of LTrL. In Proceedings of ICALP’98, number 1443 in LNCS, pages 140–151. Springer Verlag, 1998.

22. I. Walukiewicz. Private communication, 2001.

23. I. Walukiewicz. Local logics for traces. Journal of Automata, Languages and Combinatorics, 2002. To appear.

24. Th. Wilke. Classifying discrete temporal properties. Habilitationsschrift (postdoctoral thesis), April 1998.

25. Th. Wilke. Classifying discrete temporal properties. In Proceedings of STACS’99, number 1563 in LNCS, pages 32–46. Springer Verlag, 1999.

26. W. Zielonka. Notes on finite asynchronous automata. R.A.I.R.O. — Informatique Théorique et Applications, 21:99–135, 1987.