Mathematical Foundations of Computer Science 2003, 28th International Symposium Proceedings: Branislav Rovan, Peter Vojtás (eds.) Springer Lecture Notes in Computer Science 2747 (2003), 429–438.

Local LTL with past constants is expressively complete for Mazurkiewicz traces^{⋆}

Paul Gastin^{1}, Madhavan Mukund^{2}, and K. Narayan Kumar^{2}

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

                 Paul.Gastin@liafa.jussieu.fr

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

                  {madhavan,kumar}@cmi.ac.in

Abstract. To obtain an expressively complete linear-time temporal logic (LTL) over Mazurkiewicz traces that is computationally tractable, we need to intepret formulas locally, at individual events in a trace, rather than globally, at configurations. Such local logics necessarily require past modalities, in contrast to the classical setting of LTL over sequences. Earlier attempts at defining expressively complete local logics have used very general past modalities as well as filters (side-conditions) that “look sideways” and talk of concurrent events. In this paper, we show that it is possible to use unfiltered future modalities in conjunction with past constants and still obtain a logic that is expressively complete over traces. Keywords Temporal logics, Mazurkiewicz traces, concurrency

1 Introduction

Linear-time temporal logic (LTL) [17] 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 [13] 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 [24].

LTL over Σ-labelled sequences is equivalent to FO_{Σ}(<), the first-order logic over Σ-labelled linear orders [12] 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_{Σ}(<) [8]. From a practical point of view, a finite-state program may be checked against an LTL specification relatively efficiently.

⋆ Partial support of CEFIPRA-IFCPAR Project 2102-1 (ACSMV) is gratefully acknowledged.

The first expressively complete temporal logic over traces was described in [6] for finite traces and in [19] for infinite traces. The result was refined in [4] to show expressive completeness without past modalities, using an extension of the proof technique developed for LTL in [23]. Formulas 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 formulas at local states—effectively at individual events.

Recently, in [10], a local temporal logic has been defined over traces and shown to be expressively complete and tractable (the satisfiability problem is in Pspace). This logic uses both future and past modalities (similar to the until and since operators of LTL) which are further equipped with filters (side-conditions). It was also shown that for finite traces, a restricted form of past modalities suffices, but only in conjunction with filtered future modalities. Another proposal is presented in [1] and this logic also uses the since operator.

LTL without any past operators is expressively complete over words but this cannot be the case for traces: there exist two first-order inequivalent traces that cannot be distinguished using only future modalities [22].

In this paper, we show that a very limited ability to talk about the past is sufficient to obtain expressive completeness over traces. Our logic uses unfiltered future modalities and a finite number of past constants. (In particular, there is no nesting of past operators and for that matter even future formulas cannot be nested into past formulas.) As in [3, 4, 10], we show expressive completeness using an extension to traces of the proof technique introduced in [23] for LTL over sequences. From the recent general result proved in [9], it follows that the satisfiability problem for this new logic is also in Pspace.

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. Many proofs have had to be omitted in this extended abstract. A full version of the paper is available in [11].

2 Preliminaries

We briefly recall some notions about Mazurkiewicz traces (see [5] 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_{1} = [V_{1}, ≤_{1}, λ_{1}] and t_{2} = [V_{2}, ≤_{2}, λ_{2}] be a pair of traces such that alphinf(t_{1}) × alph(t_{2}) ⊆ I. We then define the concatenation of t_{1} and t_{2} to be t_{1} ·t_{2} = [V, ≤, λ] where V = V_{1} ∪V_{2} (assuming wlog that V_{1} ∩V_{2} = ∅), λ = λ_{1} ∪λ_{2} and ≤ is the transitive closure of the relation ≤_{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(x) ⊆ C} and 𝕄_{C} = 𝕄 ∩ ℝ_{C}. Also, (alph = C) = {t ∈ ℝ | alph(t) = C}, (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 theory of traces FO_{Σ}(<) is given by the syntax:

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

where a ∈ Σ and x, y ∈ Var are first order variables. Given 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 ⊧ φ}. We say that a trace language L ⊆ ℝ is expressible in FO_{Σ}(<) if there exists a sentence φ ∈ FO_{Σ}(<) such that L = L(φ). We denote by FO_{(Σ,D)}(<) the set of trace languages L ⊆ ℝ(Σ, D) that are expressible in FO_{Σ}(<). For n > 0, FO_{Σ}^{n}(<) denotes the set of formulas with at most n distinct variables (note that each variable may be bound and reused several times).

We use the algebraic notion of recognizability. 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. First-order definability coincides with aperiodicity for traces.

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

3 Local temporal logic

We denote by LocTL_{Σ}^{i} the set of (internal) formulas over the alphabet Σ. They are given by the following syntax:

φ ::= a ∈ Σ | ¬φ | φ ∨ φ | EX φ | φ U φ | ¬a S b, a, b ∈ Σ

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 ⊧ φ U ψ if ∃z ≥ x. [t, z ⊧ ψ and ∀y. (x ≤ y < z) ⇒ t, y ⊧ φ]
t, x ⊧ ¬a S b if ∃z ≤ x. [λ(z) = b and ∀y. (z < y ≤ x) ⇒ λ(y) ≠ a]

[figure: φ U ψ; ψ; φ; b; ¬a S b; ¬a]

The modality U is the “universal” until operator defined in [3]. The modality S is the corresponding since operator. Note that we only use the operator S in the very restricted form of a fixed number of past constants.

Past modalities are essential, as indicated by the following example from [22], 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 purely future modalities.

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

As usual, we can derive useful operators such as universal next AX φ = ¬ EX ¬φ, eventually in the future F φ = ⊤ U φ and always in the future G φ = ¬ F ¬φ. The modality F^{∞} a = F a ∧ G(a ⇒ EX F a) expresses the existence of infinitely many vertices labelled with a above the current vertex.

Traces as models of formulas: We now turn our attention to defining when a trace satisfies a formula. For LTL over sequences, lifting satisfaction at positions to satisfaction by a word is quite simple: a word models a formula if its initial position models the formula. Since a trace, in general, does not have a unique initial position, we need to use initial formulas as introduced in [3]. These are boolean combinations of formulas EM φ, each of which asserts the existence of a minimal vertex in a trace satisfying the internal formula φ. More precisely, the set LocTL_{Σ} of initial formulas over the alphabet Σ is defined as follows:

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

The semantics of EM is given by:

t ⊧ EM φ if ∃x. (x ∈ min(t) and t, x ⊧ φ)

An initial formula α ∈ LocTL_{Σ} defines the trace language L(α) = {t ∈ ℝ | t ⊧ α}. We can then express various alphabetic properties using initial formulas: 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 (alph = C), (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}(<).

We now show that the “filtered” modalities EX_{b} and F_{b} from [10], with the following semantics, are both expressible in LocTL_{Σ}^{i}.

t, x ⊧ EX_{b} φ if ∃y. [x ⋖ y and t, y ⊧ φ and ∀z. (z ≤ y ∧ λ(z) = b) ⇒ z ≤ x]
t, x ⊧ F_{b} φ if ∃y. [x ≤ y and t, y ⊧ φ and ∀z. (z ≤ y ∧ λ(z) = b) ⇒ z ≤ x]

Proposition 3. For any trace t over some alphabet Σ, any position x in t and any formula φ of LocTL_{Σ}^{i}

t, x ⊧ EX_{b} φ ⟺ t, x ⊧ (b ∧ EX(φ ∧ ¬b)) ∨ ⋁_{a≠b}(a ∧ EX(φ ∧ ¬(¬a S b)))

Let the formula Safe_{b} = (b ∧ AX ¬b) ∨ ⋁_{a≠b}(a ∧ AX ¬(¬a S b)). Further, let F_{b}^{0} φ = Safe_{b} U φ and F_{b}^{k+1} φ = Safe_{b} U EX_{b}(F_{b}^{k} φ).

Proposition 4. For any trace t ∈ ℝ(Σ, D), any position x in t and any formula φ of LocTL_{Σ}^{i}

t, x ⊧ F_{b} φ ⟺ t, x ⊧ ⋁_{k≤|Σ|} F_{b}^{k} φ

Now we establish some important lemmas that are critical in proving the expressive completeness of LocTL_{Σ}.

Lemma 5. Let A ⊆ Σ and b ∈ Σ with b ∉ A. For all φ ∈ LocTL_{A}^{i}, there is a formula φ̃ ∈ LocTL_{A∪{b}}^{i} such that for all t = t_{1}bt_{2}t_{3} ∈ ℝ with t_{1} ∈ ℝ, t_{2} ∈ ℝ_{A}, min(t_{2}) ⊆ D(b) and min(t_{3}) ⊆ {b} and for all x ∈ bt_{2} we have bt_{2}, x ⊧ φ iff t, x ⊧ φ̃.

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

Proof Sketch. We have ã = a, ˜¬φ = ¬φ̃, { \atop φ ∨ ψ} = φ̃ ∨ ψ̃, { \atop EX φ} = EX_{b} φ̃, { \atop φ U ψ} =

⋁_{d∈A∪\{b\}}((φ̃ U (d ∧ ψ̃)) ∧ F_{b}(d ∧ ψ̃)) and { \atop ¬c S d} = (¬c S d) ∧ ¬(¬d S b). ⊓ ⊔

Lemma 6. Let A ⊆ Σ and b ∈ Σ with b ∉ A. For all α ∈ LocTL_{A}, there exists a formula \overline{α} ∈ LocTL_{A∪\{b\}}^{i} such that for all t = t_{1}bt_{2}t_{3} ∈ ℝ with t_{1} ∈ ℝ, t_{2} ∈ ℝ_{A}, min(t_{2}) ⊆ D(b) and min(t_{3}) ⊆ {b}, we have t_{2} ⊧ α if and only if t, min(bt_{2}t_{3}) ⊧ \overline{α}.

Proof Sketch. We have \overline{¬α} = ¬\overline{α}, \overline{α ∨ β} = \overline{α} ∨ \overline{β} and \overline{EM φ} = EX(φ̃ ∧ ¬b) where φ̃ is the formula given by Lemma 5. ⊓ ⊔

Lemma 7. Let A ⊆ Σ and b ∈ Σ with b ∉ A. For all α ∈ LocTL_{A}, there exists a formula α̃ ∈ LocTL_{A∪{b}} such that for all t = t_{1}t_{2} with t_{1} ∈ ℝ_{A} and min(t_{2}) ⊆ {b}, we have t_{1} ⊧ α if and only if t ⊧ α̃.

Proof Sketch. Let { \atop φ ∨ ψ} = φ̃ ∨ ψ̃, ˜¬φ = ¬φ̃, { \atop EX φ} = EX(φ̃ ∧ ¬(¬b S b)), { \atop φ U ψ} = φ̃ U (ψ̃ ∧ ¬(¬b S b)) and { \atop ¬c S d} = ¬c S d. Then, for all t = t_{1}t_{2} with t_{1} ∈ ℝ_{A}, min(t_{2}) ⊆ {b} and for all x ∈ t_{1}, we have t_{1}, x ⊧ φ if and only if t, x ⊧ φ̃. Finally, let { \atop EM φ} = EM(φ̃ ∧ ¬b). ⊓ ⊔

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 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 finite or infinite factorization t = t_{0}bt_{1}bt_{2} ⋯ with t_{0} ∈ ℝ_{B} and t_{i} ∈ ℝ_{B} ∩ (min ⊆ D(b)) for all i > 0. In particular, we have

(min = {b}) = (bΓ)^{+} ⊎ (bΓ)^{ω} ⊎ ⋃_{∅≠A⊆B}(bΓ)^{∗}bΓ^{A}Ω_{A}

The following two results will allow us to use this decomposition effectively in proving the expressive completeness of our logic. For this, we use F_{b}^{∞} a = F_{b} a ∧ ¬ F_{b}(a ∧ ¬ EX_{b} F_{b} a).

Lemma 8. Let t = t_{0}t′ with t_{0}, t′ ∈ ℝ and min(t′) = {b}. Then,

1. t′ ∈ (bΓ)^{∞} \ {1} if and only if t, min(t′) ⊧ β with

β = ⋁_{C}( ⋀_{c∈C} F^{∞} c ∧ ⋀_{c∉C} ¬ F^{∞} c)

where C ranges over connected subsets of Σ such that b ∈ C if C ≠ ∅.

2. t′ ∈ (bΓ)^{∗}bΓ^{A}Ω_{A} if and only if t, min(t′) ⊧ γ with

γ = ⋁_{C⊆Σ}( ⋀_{c∉C} ¬ F^{∞} c) ∧ 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 9. Let A ⊆ Σ and let L ⊆ ℝ be a trace language recognized by a morphism h from 𝕄 into a finite monoid S. Then,

L ∩ (bΓ)^{∗}bΓ^{A}Ω_{A} = ⋃ ; finite(L_{1} ∩ (bΓ)^{∗})b(L_{2} ∩ Γ^{A})(L_{3} ∩ Ω_{A})

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

5 Expressive Completeness

If T is a finite alphabet, we define the linear temporal logic LTL_{T} (XU) by the syntax: f ::= u ∈ T | f XU f | ¬f | f ∨ f.

The length of a finite or infinite word w = w_{1}w_{2} ⋯ ∈ T^{∞} is |w| ∈ ℕ ∪ {ω}. For a word w = w_{1}w_{2} ⋯ ∈ T^{∞} the semantics of LTL_{T} (XU) is given by

w ⊧ u  if |w| > 0 and w_{1} = u
w ⊧ f XU g if ∃j ∈ ℕ with 1 < j ≤ |w| + 1 and
w_{j}w_{j+1} ⋯ ⊧ g and w_{k}w_{k+1} ⋯ ⊧ f, ∀1 < k < j.

Note that if w ⊧ f XU g then w is nonempty. A formula f ∈ LTL_{T} (XU) defines the word language L(f) = {w ∈ T^{∞} | w ⊧ f}. We use the following proposition which is a consequence of several results on the equivalence between aperiodic word languages, star-free word languages, first order word languages and word languages expressible in LTL_{T} (XU) [18, 12, 14, 20, 8, 15, 16, 2].

Proposition 10. Every aperiodic word language K ∈ T^{∞} is expressible in LTL_{T} (XU).

We fix T = h(bΓ) and we define the mapping σ : (bΓ)^{∞} → T^{∞} by σ(t) = h(bt_{1})h(bt_{2}) ⋯ if t = bt_{1}bt_{2} ⋯ with t_{i} ∈ Γ for i ≥ 1. Note that the mapping σ is well-defined since each trace t ∈ (bΓ)^{∞} has a unique factorization t = bt_{1}bt_{2} ⋯ with t_{i} ∈ Γ for i ≥ 1.

Lemma 11. Let L ⊆ ℝ be recognized by h. Then,

1. L ∩ (bΓ)^{ω} = σ^{−1}(K) for some K expressible in LTL_{T} (XU).

2. L ∩ (bΓ)^{+} = σ^{−1}(K) for some K expressible in LTL_{T} (XU).

Next we show show how to lift an LTL_{T} (XU) formula for K ⊆ T^{∞} to a LocTL^{i} formula for σ^{−1}(K) ∈ (bΓ)^{∞}.

Lemma 12. Suppose that any aperiodic trace language over B is expressible in LocTL_{B}. Then, for all 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. The formula f̃ is defined by structural induction. We let { \atop f ∨ g} = f̃∨ g̃, ˜¬f = ¬f̃, { \atop f XU g} = EX((¬b ∨ f̃) U (b ∧ g̃)). The difficult case is when f = s ∈ T. For all r ∈ S, the trace language h^{−1}(r) ∩ 𝕄_{B} is aperiodic and therefore expressible in LocTL_{B} by the hypothesis of the lemma: we find α_{r} ∈ LocTL_{B} such that for all t′′ ∈ 𝕄_{B}, h(t′′) = r if and only if t′′ ⊧ α_{r}. Let \overline{α_{r}} ∈ LocTL_{Σ}^{i} be the formula obtained using Lemma 6. We let s̃ = ⋁_{h(b)·r=s} \overline{α_{r}}. ⊓ ⊔

Lemma 13. Suppose that any aperiodic trace language over B is expressible in LocTL_{B}. Let A ⊆ Σ be non-empty and let f ∈ LTL_{T} (XU). There exists f̃ ∈ LocTL_{Σ}^{i} such that for all t = t_{1}t_{2}t_{3} with t_{1} ∈ ℝ, t_{2} ∈ (bΓ)^{∗}, t_{3} ∈ bΓ^{A}Ω_{A}, we have σ(t_{2}) ⊧ f iff t, min(t_{2}t_{3}) ⊧ f̃.

Lemma 14. Suppose that for any proper subset A of Σ, any aperiodic trace language over A is expressible in LocTL_{A}. Let L ⊆ ℝ be an aperiodic trace language over Σ. Then, for all b ∈ Σ, there exists φ ∈ LocTL_{Σ}^{i} such that for all t = t_{0}t′ with t_{0}, t′ ∈ ℝ and min(t′) = {b}, t′ ∈ L iff t, min(t′) ⊧ φ.

Proof. We prove this lemma by induction on the size of the alphabet Σ. If Σ = ∅ then there is nothing to prove. Now, suppose that Σ ≠ ∅ and let b ∈ Σ. We assume that L is recognized by the aperiodic morphism h : 𝕄 → S. Now, L ∩ (min = {b}) can be written as

(L ∩ ((bΓ)^{∞} \ {1})) ⊎ ⋃_{∅≠A⊆B}(L ∩ (bΓ)^{∗}bΓ^{A}Ω_{A}).

By Lemma 11 we get L ∩ ((bΓ)^{∞} \ {1}) = σ^{−1}(L(f)) for some f ∈ LTL_{T} (XU). From the hypothesis, aperiodic languages over B are expressible in LocTL_{B}. Hence, we can apply Lemma 12 and we get f̃ such that for all t = t_{0}t′ with t_{0} ∈ ℝ and t′ ∈ (bΓ)^{∞} \ {1}, we have σ(t′) ⊧ f iff t, min(t′) ⊧ f̃. We conclude this case taking φ = β ∧ f̃ where β is defined in Lemma 8.

Now, we consider L ∩ (bΓ)^{∗}bΓ^{A}Ω_{A} where ∅ ≠ A ⊆ B. By Lemma 9,

L ∩ (bΓ)^{∗}bΓ^{A}Ω_{A} = ⋃ ; finite(L_{1} ∩ (bΓ)^{∗})b(L_{2} ∩ Γ^{A})(L_{3} ∩ Ω_{A})

where each L_{i} is an aperiodic language recognized by h. Thus, it suffices to show that for aperiodic languages L_{1}, L_{2} and L_{3} recognized by h, there is a formula φ such that for all t = t_{0}t′ with t_{0}, t′ ∈ ℝ and min(t′) = {b}, we have t, min(t′) ⊧ φ if and only if t′ ∈ (L_{1} ∩ (bΓ)^{∗})b(L_{2} ∩ Γ^{A})(L_{3} ∩ Ω_{A}).

By Lemma 11 we get L_{1} ∩ (bΓ)^{∗} = σ^{−1}(L(f_{1})) for some f_{1} ∈ LTL_{T} (XU). From the hypothesis, aperiodic languages over B are expressible in LocTL_{B}. Hence, we can apply Lemma 13 and we get f̃_{1} such that for all t = t_{0}t_{1}t′′ with t_{0} ∈ ℝ and t_{1} ∈ (bΓ)^{∗}, and t′′ ∈ bΓ^{A}Ω_{A}, we have t_{1} ∈ L_{1} iff t, min(t_{1}t′′) ⊧ f̃_{1}.

Using again the hypothesis of the lemma, we get some formula α_{2} ∈ LocTL_{B} such that L_{2} ∩ ℝ_{B} = L(α_{2}). By Lemma 6 we find \overline{α_{2}} ∈ LocTL_{Σ}^{i} such that for all t = t_{0}t_{1}bt_{2}t_{3} with t_{0} ∈ ℝ and t_{1} ∈ (bΓ)^{∗}, t_{2} ∈ Γ^{A} and t_{3} ∈ Ω_{A}, we have t_{2} ∈ L_{2} iff t, min(bt_{2}t_{3}) ⊧ \overline{α_{2}}.

Finally, L_{3} is an aperiodic trace language over a smaller alphabet (since A ≠ ∅, I(A) is a proper subset of Σ) and hence by induction hypothesis there is a formula φ_{3} such that for all t = t_{0}t_{1}bt_{2}t_{3} with t_{0} ∈ ℝ and t_{1} ∈ (bΓ)^{∗}, t_{2} ∈ Γ^{A} and t_{3} ∈ Ω_{A} with t_{3} ≠ 1, we have t_{3} ∈ L_{3} iff t, min(t_{3}) ⊧ φ_{3}.

Putting these three pieces together we let

ψ = f̃_{1} ∧ F(b ∧ F_{b}^{∞} a ∧ \overline{α_{2}} ∧ (φ_{4} ∨ F_{b} EX(b ∧ φ_{3})))

with φ_{4} = ⊥ if 1 ∉ L_{3} and φ_{4} = ¬ EX F b otherwise. Then, for all t = t_{0}t_{1}bt_{2}t_{3} with t_{0} ∈ ℝ and t_{1} ∈ (bΓ)^{∗}, t_{2} ∈ Γ^{A} and t_{3} ∈ Ω_{A}, we get from the above discussion that t_{1}bt_{2}t_{3} ∈ L_{1}bL_{2}L_{3} if and only if t, min(t_{1}bt_{2}t_{3}) ⊧ ψ. We complete the proof with φ = γ ∧ ψ where γ is the formula defined in Lemma 8. ⊓ ⊔

Theorem 15. Any aperiodic real trace language over ℝ(Σ, D) is expressible in LocTL_{Σ}.

Proof. The proof proceeds by induction on the size of Σ. When Σ = {a} is a singleton, L is either a finite set or the union of a finite set and a set of the form a^{n}a^{∗} for some n ≥ 0. In both cases, it is easy to check that L is expressible in LocTL_{Σ}.

For the inductive step, assume that the theorem holds for any aperiodic language over any proper subset of Σ. Let L be recognized by an aperiodic morphism h : 𝕄 → S. Let b ∈ Σ and B = Σ \ {b} as usual. We can show as in Lemma 9 that L can be written as follows:

L = ⋃_{finite}(L_{1} ∩ ℝ_{B})(L_{2} ∩ (min ⊆ {b}))

where L_{1} and L_{2} are languages recognized by the same aperiodic morphism h.

Since the decomposition of any trace t ∈ ℝ as t_{1}t_{2} with t_{1} ∈ ℝ_{B} and t_{2} ∈ (min ⊆ {b}) is unique, the above decomposition can be rewritten as

L = ⋃_{finite}(L_{1} ∩ ℝ_{B})(min ⊆ {b}) ∩ (ℝ_{B}(L_{2} ∩ (min ⊆ {b})))

Now, by the induction hypothesis, there is formula α_{1} in LocTL_{B} such that for t_{1} ∈ ℝ_{B}, t_{1} ⊧ α_{1} if and only if t_{1} ∈ L_{1}. Thus, by Lemma 7, there is a formula α̃_{1} in LocTL_{Σ} such that t ⊧ α̃_{1} if and only if t_{1} ⊧ α_{1} whenever t = t_{1}t_{2} with t_{1} ∈ ℝ_{B} and min(t_{2}) ⊆ {b}. Thus, (L_{1} ∩ ℝ_{B})(min ⊆ {b}) = L(α̃_{1}).

Since we have assumed expressive completeness for every proper subset of Σ, by Lemma 14 there is a formula φ_{2} such that for any t = t_{1}t_{2} with min(t_{2}) = b, t_{2} ∈ L_{2} if and only if t, min(t_{2}) ⊧ φ_{2}. Consider the formula α = α′ ∨ EM((b ∧ φ_{2}) ∨ (¬b ∧ F_{b} EX(b ∧ φ_{2}))) where α′ = ⊥ if 1 ∉ L_{2} and α′ = ¬ EM F b otherwise. Then, t ⊧ α if and only if either t ∈ ℝ_{B} and 1 ∈ L_{2}, or there is a minimal b event x in the trace t and t, x ⊧ φ_{2}. That is t = t_{1}t_{2} with t_{1} ∈ ℝ_{B}, min(t_{2}) = {b} and t_{2} ∈ L_{2}. Thus ℝ_{B}(L_{2} ∩ (min ⊆ {b})) = L(α) is also expressible in LocTL_{Σ}. ⊓ ⊔

References

1. B. Adsul and M. Sohoni. Complete and tractable local linear time temporal logics over traces. In Proc. of ICALP’02, LNCS 2380, 926–937. Springer Verlag, 2002.

2. J. Cohen, D. Perrin, and J.-E. Pin. On the expressive power of temporal logic. Journal of Computer and System Sciences, 46:271–295, 1993.

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

4. V. Diekert and P. Gastin. LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences, 64:396–418, 2002.

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

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

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

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

9. P. Gastin and D. Kuske. Satisfiability and model checking for MSO-definable temporal logics are in PSPACE. To appear in Proc. of CONCUR’03.

10. P. Gastin and M. Mukund. An elementary expressively complete temporal logic for Mazurkiewicz traces. In Proc. of ICALP’02, LNCS 2380, 938–949. Springer Verlag, 2002.

11. P. Gastin, M. Mukund, and K. Narayan Kumar. Local LTL with past constants is expressively complete for Mazurkiewicz traces. Tech. Rep. 2003-008, LIAFA, Université Paris 7 (France), 2003.

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

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

14. R. McNaughton and S. Papert. Counter-Free Automata. MIT Press, 1971.

15. D. Perrin. Recent results on automata and infinite words. In Proc. of MFCS’84, LNCS 176, 134–148. Springer Verlag, 1984.

16. D. Perrin and J.-E. Pin. First order logic and star-free sets. Journal of Computer and System Sciences, 32:393–406, 1986.

17. A. Pnueli. The temporal logic of programs. In FOCS’77, 46–57, 1977.

18. M.-P. Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8:190–194, 1965.

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

20. W. Thomas. Star-free regular sets of ω-sequences. Information and Control, 42:148–156, 1979.

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

22. I. Walukiewicz. Local logics for traces. Journal of Automata, Languages and Combinatorics, 7(2):259–290, 2002.

23. Th. Wilke. Classifying discrete temporal properties. In Proc. of STACS’99, LNCS 1563, 32–46. Springer Verlag, 1999.

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