BRICS RS-97-8 Henriksen & Thiagarajan: Dynamic Linear Time Temporal Logic BRICS

Basic Research in Computer Science

Dynamic Linear Time Temporal Logic

Jesper G. Henriksen P. S. Thiagarajan BRICS Report Series RS-97-8 ISSN 0909-0878 April 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, 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/97/8/

Dynamic Linear Time Temporal Logic

Jesper Gulmann Henriksen BRICS^{∗}, Department of Computer Science,

University of Aarhus, Denmark

          email: gulmann@brics.dk

P. S. Thiagarajan^{†}

SPIC Mathematical Institute, Madras, India

          email: pst@smi.ernet.in

April 1997

Abstract

A simple extension of the propositional temporal logic of linear time is proposed. The extension consists of strengthening the until operator by indexing it with the regular programs of propositional dynamic logic (PDL). It is shown that DLTL, the resulting logic, is expressively equivalent to S1S, the monadic second-order theory of ω-sequences. In fact a sublogic of DLTL which corresponds to propositional dynamic logic with a linear time semantics is already as expressive as S1S. We pin down in an obvious manner the sublogic of DLTL which correponds to the first order fragment of S1S. We show that DLTL has an exponential time decision procedure. We also obtain an axiomatization of DLTL. Finally, we point to some natural extensions of the approach presented here for bringing together propositional dynamic and temporal logics in a linear time setting.

∗ Basic Research in Computer Science, Centre of the Danish National Research Foundation.

† Part of this work was done while visiting BRICS.

Part of this work has been supported by IFCPAR Project 1502-1.

1 Introduction

We present here a simple extension of the propositional temporal logic of linear time (LTL). The basic idea is to strengthen the until modality by indexing it with the regular programs of propositional dynamic logic (PDL). The resulting logic, called dynamic linear time temporal logic (DLTL), is easy to handle. It has the full expressive power of the monadic second order theory of ω-sequences (S1S). Indeed a sublogic of DLTL is already equal in expressive power to S1S. A pleasant feature of this sublogic is that it is just PDL operating in a linear time framework.

In addition to our expressiveness results we show that DLTL has an exponential time decision procedure. We also extend the well known axiomatization of PDL [9] to obtain an axiomatization of DLTL.

Our work may be viewed from two different perspectives. The first one is from the standpoint of process logics [6, 14, 16] which attempt a rapprochement between dynamic and temporal logics. However the study of process logics is committed to viewing dynamic logic as a restricted kind of a branching time temporal logic. One then attempts to bring in some additional mechanisms for talking about the computational paths of a Kripke frame in a more sophisticated fashion. Our point of departure from this line of work consists of merging, in a very simple way, dynamic logic and temporal logic in a linear time setting.

The second perspective from which our work may be viewed has to do with attempts to augment the limited expressive power of LTL. One route consists of permitting quantification over atomic propositions. The resulting logic called QPTL [18] has the expressive power of S1S and has a decision procedure of non-elementary complexity. The second route consists of augmenting LTL with the so called automaton connectives. Indeed this additional feature is so powerful that the next and until modalities become derived ones. The resulting logic called ETL [23] is equal in expressive power to S1S while admitting an exponential time decision procedure. To be precise, the version of ETL we have in mind is the one referred to as ETL_{f} in [21] but for convenience we will call it just ETL here.

Our logic is, in spirit, inspired by ETL and in fact it may appear to be at first sight just a reformulation of ETL with some cosmetic changes. This however has to do with the instinctive identification one makes between finite state automata and regular expressions. In fact DLTL is quite different in terms of the mechanisms it offers for structuring formulas and we feel that it is more transparent and easier to work with. The results and the proofs we present here are designed to support this claim. Our approach also leads to smooth generalizations in non-sequential settings where similar extensions in terms of ETL will be hard to cope with at least in terms of transparency.

In the next section we start with an action-based version of LTL in order to fix terminology and to introduce a key feature of DLTL. In Section 3 we present DLTL and its semantics. This is then followed by a more detailed assessment of the similarities and the differences between ETL and DLTL.

In Section 4 we prove the decidability of DLTL by reducing it to the emptiness problem for Büchi automata. In Section 5 we show that DLTL^{−}, a sublogic of DLTL, has the same expressive power as S1S. This then easily leads to the conclusion that DLTL, DLTL^{−} and S1S are all equal in expressive power. We then establish similar results for the firstorder fragment of S1S with the help of the “star-free” fragments of DLTL and DLTL^{−}.

In Section 6, we extend the axiomatization of PDL and the completeness proof in [9] to obtain finitary axiomatizations of DLTL and DLTL^{−}. In the final section we point to two natural generalizations in the setting of distributed systems. These generalizations appear to be eminently accessible and offer additional support to our belief that the synthesis of dynamic and temporal logics in a linear time framework as pursued here is a fruitful one.

2 Linear Time Temporal Logic

One key feature of the syntax and semantics of our temporal logic is the treatment of actions as first class objects.

The usual treatment of LTL [10, 15] is based on states viewed as subsets of a finite set of atomic propositions. We wish to bring in actions explicitly for a number of reasons. Firstly, in a state-based approach there is a mismatch between the models of a formula and the language accepted by the associated ω-automaton. A model will consist of a sequence of states whereas the automaton will accept or reject a sequence of actions. Thus the alphabet of the automaton will correspond to the possible states of the model. However this is not a major hurdle and it leads, at worst, to minor technical overheads. The more important point is that it is difficult to define synchronized products of sequential components in a purely state-based setting. Since this is a very common and useful method of specifying distributed behaviours, we feel that it is handy to work with logics in which both states and actions can be treated on an equal footing.

As a vehicle for introducing some terminology and for later comparisons we shall first introduce an action-based version of LTL denoted LTL(Σ). We begin with some notations.

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

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

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

Through the rest of this section α, β will range over LTL(Σ). The modality ⟨a⟩ is an action-indexed version of the next state modality of LTL as we shall soon see.

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

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

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

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

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

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

For further reference we note that the next-state modality of LTL is definable via Oα ⟺^{Δ} ⋁_{a∈Σ}⟨a⟩α. It is well known [4, 8] that LT L(Σ) is expressively equivalent to the first-order theory of sequences. Hence this temporal logic has definite limitations of expressive power. In particular, as pointed out by Wolper in a state-based setting [22], the property “p holds at every even position” is not definable in this logic. The dynamic version of LTL(Σ) that we introduce in the next section is designed to overcome this kind of expressive limitation.

3 Dynamic Linear Time Temporal Logic

Our extension of LTL(Σ) basically consists of indexing the until operator with the programs of PDL (e.g. [3, 5]). We start by defining the set of programs (regular expressions) generated by Σ. This set is denoted by Prg(Σ) and its syntax is given by:

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

Here and elsewhere, π, π′ with or without subscripts will range over Prg(Σ). With each program we associate a set of finite words via the map || · || : Prg(Σ) ⟶ 2^{Σ^{∗}}. This map is defined in the standard fashion.

• ||a|| = {a}.

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

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

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

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

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

Again we fix a countable set of atomic propositions P = {p_{1}, p_{2}, …} and let p, q range over P. Then the set of formulas of DLTL(Σ) is given by the following syntax.

DLTL(Σ) ::= p | ∼α | α ∨ β | α U^{π}β.

Here and throughout the rest of the paper we take α, β to range over DLTL(Σ). The notion of a model is as in the case of LTL(Σ). So let M = (σ, V) be a model, τ ∈ prf(σ) and α ∈ DLTL(Σ). Then M, τ ⊧ α is defined inductively.

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

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

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

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

Thus DLTL(Σ) is obtained form LTL(Σ) by strengthening the until operator. To satisfy α U^{π}β, one must satisfy α Uβ along some finite stretch of behaviour which is in the (linear time) behaviour of the program π.

As usual, α ∈ DLTL(Σ) is satisfiable iff there exist a model M = (σ, V) and τ ∈ prf(σ) such that M, τ ⊧ α. The satisfiability problem is, given α, to decide whether α is satisfiable.

Apart from the conventional derived propositional connectives such as ∧, ⊃ and ≡ the derived modality ⟨π⟩ and its dual [π] will play an important role in the sequel. They are defined as follows:

• ⊤ ⟺^{Δ} p_{1}∨ ∼p_{1}. Recall that P = {p_{1}, p_{2}, …}.

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

• [π]α ⟺^{Δ} ∼⟨π⟩∼α.

Suppose M = (σ, V) is a model and τ ∈ prf(σ). It is easy to see that σ, τ ⊧ ⟨π⟩α iff there exists τ′ ∈ ||π|| such that ττ′ ∈ prf(σ) and σ, ττ′ ⊧ α. It is also easy to see that σ, τ ⊧ [π]α iff for every τ′ ∈ ||π||, if ττ′ ∈ prf(σ) then σ, ττ′ ⊧ α. In this sense, the program modalities of PDL acquire a linear time semantics in the present setting.

Note that a ∈ Σ is a member of Prg(Σ) and hence ⟨a⟩α is a derived modality. It is also easy to see that the until operator of LTL(Σ) can be obtained via: α Uβ ⟺^{Δ} α U^{Σ^{∗}}β. Thus LTL(Σ) is a fragment of DLTL(Σ). To see that DLTL(Σ) is strictly more expressive than LTL(Σ), let Σ = {a_{1}, a_{2}, …, a_{n}} and π_{ev} = ((a_{1}+a_{2}+…+a_{n}); (a_{1}+a_{2}+…+a_{n}))^{∗}.

It is now easy to see that α_{ev} = [π_{ev}]p is a specification of the property ”p holds at every even position”.

We shall close out the section by briefly discussing the key differences between DLTL(Σ) and ETL, the extension of LTL proposed by Wolper [22]. As mentioned earlier, the version of ETL we shall consider here is the one called ETL_{f} in [21]. We shall present a simplified form of ETL so as to stay close to DLTL. First we fix an enumeration of Σ = {a_{1}, a_{2}, …, a_{n}}. The syntax of the logic that we shall name as ETL(Σ) is then given by:

ETL(Σ) ::= p | ∼ϕ | ϕ ∨ ϕ′ | A(ϕ_{0}, ϕ_{1}, …, ϕ_{n}).

Here ϕ, ϕ′, ϕ_{0}, ϕ_{1}, …, ϕ_{n} are assumed to be formulas of ETL(Σ). Further, A is a finite state automaton of the form A = (Q, ⟶, Q_{in}, F) with ⟶ ⊆ Q × Σ × Q as the transition relation, Q_{in} ⊆ Q as the initial states and F ⊆ Q as the accepting states. In what follows we let L(A) be the language of finite words accepted by A. Moreover we shall assume for the sake of convenience that ε ∉ L(A) for each formula of the form A(ϕ_{0}, ϕ_{1}, …, ϕ_{n}).

A model for ETL(Σ) is, as before, a pair M = (σ, V) with V : prf(σ) ⟶ 2^{P}. Let τ ∈ prf(σ). Then M, τ ⊧ ϕ is defined via:

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

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

• M, τ ⊧ ϕ ∨ ϕ′ iff M, τ ⊧ ϕ or M, τ ⊧ ϕ′.

• M, τ ⊧ A(ϕ_{0}, ϕ_{1}, …, ϕ_{n}) iff there exists a_{i_{1}}a_{i_{2}} … a_{i_{m}} ∈ L(A) such that the following conditions are satisfied:

— i_{1}, i_{2}, …, i_{m} ∈ {1, 2, …, n}. (recall that Σ = {a_{1}, a_{2}, …, a_{n}}).

— τa_{i_{1}}a_{i_{2}} ⋯ a_{i_{m}} ∈ prf(σ).

— M, τ ⊧ ϕ_{0} and M, τa_{i_{1}} ⋯ a_{i_{j}} ⊧ ϕ_{i_{j}} for 1 ≤ j ≤ m.

Though the technical details are somewhat different, ETL(Σ) captures the spirit of the logic presented in [21]. The key drawback of ETL(Σ), as we see it, lies in its lack of structuring principles for forming compound formulas. Stated differently, the only mechanism that ETL(Σ) has — apart from the boolean connectives — to form compound formulas is by nesting the automaton formulas. Thus a typical compound formula would look like:

A^{1}(ϕ_{0}^{1}, A^{2}(ϕ_{0}^{2}, ϕ_{1}^{2}, A^{3}(ϕ_{0}^{3}, …, ϕ_{n}^{3}), ϕ_{3}^{2}, …, ϕ_{n}^{2}), ϕ_{2}^{1}, …, ϕ_{n}^{1}).

In contrast, DLTL(Σ) adds to the familiar mechanisms of LTL an orthogonal and well-understood component; namely, the language of regular expressions. Equally important, this orthogonal component is formulated purely in terms of Σ and not in terms of arbitrary formulas as is the case of ETL. In fact, ETL, as formulated in [21] has an uncontrolled amount of “external” elements in the sense that the states and the alphabets of the automata which are used to write down the automaton formulas have little to do with the logic under consideration.

4 A Decision Procedure for DLTL

The goal here is to show that the satisfiability problem for DLTL(Σ) can be solved in deterministic exponential time. This will be achieved by effectively constructing for each α ∈ DLTL(Σ), a Büchi automaton B_{α} such that the language of ω-words accepted by B_{α} is non-empty iff α is satisfiable.

We shall use the terminology adopted in [20] for dealing with Büchi automata. In particular, a Büchi automaton over Σ is a tuple B = (Q, ⟶, Q_{in}, F) where:

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

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

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

• F ⊆ Q is a set of accepting states.

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

• ρ(ε) ∈ Q_{in}.

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

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

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

Through the rest of the section we fix a formula α_{0}. To construct B_{α_{0}} we first define the (Fischer-Ladner) closure of α_{0} as follows. cl(α_{0}) is the least set of formulas that satisfies:

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

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

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

• If α U^{π}β ∈ cl(α_{0}) then α, β ∈ cl(α_{0}).

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

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

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

A ⊆ CL is called an atom iff it is a subset of CL satisfying:

• β ∈ A iff ∼β ∉ A.

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

• If β ∈ A and ε ∈ ||π|| then α U^{π}β ∈ A.

AT (α_{0}) is the set of atoms and again we shall often write AT instead of AT (α_{0}). Next we define Req(α_{0}), the set of until requirements of α_{0}, to be the subset of CL given by:

Req(α_{0}) = {α U^{π}β | α U^{π}β ∈ CL}.

We shall write Req instead Req(α_{0}) and take ξ, ξ′ to range over Req. For each ξ = α U^{π}β ∈ Req we fix a finite state automaton A_{ξ} such that L(A_{ξ}) = ||π|| where L(A_{ξ}) is the language of finite words accepted by A_{ξ}. We shall assume each such A_{ξ} is of the form A_{ξ} = (Q_{ξ}, ⟶_{ξ}, I_{ξ}, F_{ξ}) where Q_{ξ} is the set of states, ⟶_{ξ} ⊆ Q_{ξ} × Σ × Q_{ξ} is the transition relation, I_{ξ} ⊆ Q_{ξ} is the set of initial states and F_{ξ} ⊆ Q_{ξ} is the set of final states. Without loss of generality, we shall assume that ξ ≠ ξ′ implies Q_{ξ} ∩ Q_{ξ′} = ∅ for every ξ, ξ′ ∈ Req. We set Q = ⋃_{ξ∈Req} Q_{ξ} and Q̂ = Q × {0, 1}.

The Büchi automaton B_{α_{0}} associated with α_{0} (from now on denoted as B) can now be defined as

B = (S, ⟹, S_{in}, F),

where the various components of B are specified as follows:

(1) S ⊆ AT × 2^{Q} × 2Q̂ × {0, 1} × {↓, ✓} such that (A, X, X̂, x, f) ∈ S iff the following conditions are satisfied for each ξ = α U^{π}β:

(i) If β ∈ A then F_{ξ} ⊆ X. (Recall that A_{ξ} = (Q_{ξ}, ⟶_{ξ}, I_{ξ}, F_{ξ})).

(ii) If α ∈ A and q ∈ X for some q ∈ I_{ξ} then α U^{π}β ∈ A.

(iii) If α U^{π}β ∈ A then either β ∈ A and ε ∈ ||π|| or (q, 1 − x) ∈ X̂ for some q ∈ I_{ξ}. (Note that we are considering the candidate (A, X, X̂, x, f) for membership in S).

(iv) If (q, z) ∈ X̂ with q ∉ F_{ξ} or β ∉ A then α ∈ A.

(2) The transition relation ⟹ ⊆ S × Σ × S is defined as follows:

(A, X, X̂, x, f) ⟹^{a} (B, Y, Ŷ, y, g)

iff the following conditions are satisfied for each ξ = α U^{π}β:

(i) Suppose q′ ∈ Q_{ξ} ∩ Y and q ⟶^{a}_{ξ} q′ and α ∈ A. Then q ∈ X.

(ii) Suppose (q, z) ∈ X̂ with q ∈ Q_{ξ}. Suppose further that q ∉ F_{ξ} or β ∉ A. Then (q′, z) ∈ Ŷ for some q′ with q ⟶^{a}_{ξ} q′.

(iii) If f = ✓ then (y, g) = (1 − x, ↓). If f = ↓ then,

(y, g) = \{ \begin{matrix}(x, ↓), & if there exists (q, x) ∈ X̂ such that \\ & q ∉ F_{ξ} or β ∉ A. \\ (x, ✓), & otherwise. \end{matrix}

(3) S_{in} = {(A, X, X̂, x, f) | α_{0} ∈ A and (x, f) = (0, ✓)}.

(4) F = {(A, X, X̂, x, f) | f = ✓}

We wish to prove that α_{0} is satisfiable iff L(B) ≠ ∅. Afterwards we will argue that the size of B can be chosen to be at most exponential in the size of α_{0}.

Lemma 4.1 Suppose L(B) ≠ ∅. Then α_{0} is satisfiable.

Proof: Let σ ∈ L(B) and ρ : prf(σ) ⟶ S be an accepting run. For each τ ∈ prf(σ), let ρ(τ) = (A_{τ}, X_{τ}, X̂_{τ}, x_{τ}, f_{τ}). Define the model M = (σ, V) via:

V (τ) = A_{τ} ∩ P for all τ ∈ prf(σ).

We shall prove the following intermediate result.

Claim: For all τ ∈ prf(σ) and δ ∈ CL,

M, τ ⊧ δ iff δ ∈ A_{τ}.

First note that if the claim is true then Lemma 4.1 follows at once. This is so because ρ is a run of B and hence ρ(ε) ∈ S_{in}. But from (3) (in the definition of B), it follows that α_{0} ∈ A_{ε}. Thus M, ε ⊧ α_{0} and α_{0} is satisfiable.

In proving the claim we will repeatedly refer to various clauses in the definition of the Büchi automaton B.

We proceed by structural induction on δ. For the base case and the boolean connectives the claim is obvious. Hence assume that δ = α U^{π}β.

Suppose that M, τ ⊧ α U^{π}β. Since M, τ ⊧ α U^{π}β there exists τ′ ∈ ||π|| such that ττ′ ∈ prf(σ) and M, ττ′ ⊧ β. Moreover, M, ττ′′ ⊧ α for every τ′′ ∈ Σ^{∗} such that ε ⪯ τ′′ ≺ τ′.

Suppose τ′ = ε. Then ε ∈ ||π|| and M, τ ⊧ β. By the induction hypothesis β ∈ A_{τ}. From the definition of an atom it follows that α U^{π}β ∈ A_{τ}.

So assume that τ′ ≠ ε. Let ξ = α U^{π}β and R be an accepting run of A_{ξ} over τ′ = a_{1}a_{2} … a_{n} with R(ε) = q_{0} ∈ I_{ξ} and R(a_{1}a_{2} … a_{i}) = q_{i} for 1 ≤ i ≤ n and q_{n} ∈ F_{ξ}. Since M, ττ′ ⊧ β we have from the induction hypothesis that β ∈ A_{ττ′}. Hence by (1.i), F_{ξ} ⊆ X_{ττ′}. Now by the definition of R we are assured that q_{n−1} ⟶^{a_{n}}_{ξ} q_{n}. On the other hand, the fact that M, τ ⊧ α U^{π}β and the choice of τ′ guarantee that M, τa_{1} … a_{n−1} ⊧ α (with the convention that ε = a_{1} … a_{n−1} in case n = 1). By the induction hypothesis α ∈ A_{τa_{1}...a_{n−1}}, so by (2.i) and the fact that q_{n} ∈ X_{τa_{1}...a_{n}}, we have that q_{n−1} ∈ X_{τa_{1}...a_{n−1}}. In case n ≥ 2 we repeat the above argument at q_{n−1} to conclude that q_{n−2} ∈ X_{τa_{1}...a_{n−2}}. Continuing this way we can finally arrive at q_{0} ∈ X_{τ} and α ∈ A_{τ}. But q_{0} ∈ I_{ξ} and hence by (1.ii) we are assured that α U^{π}β ∈ A_{τ}.

For the converse direction assume that α U^{π}β ∈ A_{τ}. The are four cases to consider depending on the values of x_{τ} and f_{τ}. We will only prove the first case. The remaining cases can be resolved by very similar arguments.

So assume that x_{τ} = 0 and f_{τ} = ↓. Suppose first that β ∈ A_{τ} and ε ∈ ||π||. Then by the induction hypothesis M, τ ⊧ β and hence we at once have M, τ ⊧ α U^{π}β. So assume that β ∉ A_{τ} or ε ∉ ||π||. Then by (1.iii), (q_{0}, 1) ∈ X̂_{τ} for some q_{0} ∈ I_{ξ}. Suppose q_{0} ∈ F_{ξ}. Then ε ∈ ||π|| and thus β ∉ A_{τ}. This implies, by (1.iv), that α ∈ A_{τ}, and by the induction hypothesis we have that M, τ ⊧ α.

Now with ρ being an accepting run of B over σ there must exist τ_{1} and τ_{2} in Σ^{∗} such that the following conditions are satisfied:

• τ_{1} ≠ ε and τ_{2} ≠ ε and ττ_{1}τ_{2} ∈ prf(σ).

• f_{ττ_{1}} = ✓ and f_{ττ_{1}τ_{2}} = ✓. (Recall the notational convention that ρ(u) = (A_{u}, X_{u}, X̂_{u}, x_{u}, f_{u}) for each u ∈ prf(σ)).

• For each τ′′_{1} and τ′′_{2} in Σ^{∗}, if ε ⪯ τ′′_{1} ≺ τ_{1} then f(ττ′′_{1}) ≠ ✓ and if ε ≺ τ′′_{2} ≺ τ_{2} then f(ττ_{1}τ′′_{2}) ≠ ✓.

Let τ_{1} = a_{1}a_{2} … a_{n} and τ_{2} = b_{1}b_{2} … b_{m}. Now ρ(τ) ⟹^{a_{1}} ρ(τa_{1}),

α U^{π}β ∈ A_{τ} and (q_{0}, 1) ∈ X̂_{τ}. Moreover, we have that q_{0} ∉ F_{ξ} (if ε ∉ ||π||) or β ∉ A_{τ}. Thus by (2.ii), there exists q_{1} ∈ Q_{ξ} such that

q_{0} ⟶^{a_{1}}_{ξ} q_{1} and (q_{1}, 1) ∈ X̂_{τa_{1}}.

Now suppose q_{1} ∈ F_{ξ} and β ∈ A_{τa_{1}}. Then a_{1} ∈ ||π|| and by the induction hypothesis M, τa_{1} ⊧ β. Since M, τ ⊧ α has already been deduced we have M, τ ⊧ α U^{π}β. So assume that q_{1} ∉ F_{ξ} or β ∉ A_{τa_{1}}. Then by repeating the arguments we had above for q_{0} at q_{1} we can arrive at α ∈ A_{τa_{1}}, and hence by the induction hypothesis M, τa_{1} ⊧ α. Moreover, we can conclude that there exists q_{2} ∈ Q_{ξ} such that q_{1} ⟶^{a_{2}}_{ξ} q_{2} and (q_{2}, 1) ∈ X̂_{τa_{1}a_{2}}. Marching down τ_{1} using this sequence of arguments we will either terminate with the conclusion M, τ ⊧ α U^{π}β or we will exhaust all of τ_{1} while being able to conclude that there must exist states

q_{0}, q_{1}, …, q_{n} ∈ Q_{ξ} such that q_{0} ⟶^{a_{1}}_{ξ} q_{1} ⟶^{a_{2}}_{ξ} q_{2} … q_{n−1} ⟶^{a_{n}}_{ξ} q_{n}. Further-

more, we will be able to conclude that M, ττ′′_{1} ⊧ α for every τ′′_{1} such that ε ⪯ τ′′_{1} ≺ τ_{1}. Finally, we will also be assured that (q_{n}, 1) ∈ X̂_{ττ_{1}}.

Now suppose q_{n} ∈ F_{ξ} and β ∈ A_{ττ_{1}}. Then τ_{1} ∈ ||π|| and M, ττ_{1} ⊧ β by the induction hypothesis. Consequently M, τ ⊧ α U^{π}β. So assume that q_{n} ∉ F_{ξ} or β ∉ A_{ττ_{1}}. Then α ∈ A_{ττ_{1}} (by (1.iv)) and hence M, ττ_{1} ⊧ α by the induction hypothesis. Now by the choice of τ_{1}, we know that (x_{ττ_{1}}, f_{ττ_{1}}) = (0, ✓) and hence (x_{ττ_{1}b_{1}}, f_{ττ_{1}b_{1}}) = (1, ↓) by (2.iii). On the other hand, ρ(ττ_{1}) ⟹^{b_{1}} ρ(ττ_{1}b_{1}) implies that there exists q′_{1} ∈ Q_{ξ} such

that q_{n} ⟶^{b_{1}}_{ξ} q′_{1} and (q′_{1}, 1) ∈ X̂_{ττ_{1}b_{1}}. Again q′_{1} ∈ F_{ξ} and β ∈ A_{ττ_{1}b_{1}} will

lead to the desired conclusion M, τ ⊧ α U^{π}β.

So suppose q′_{1} ∉ F_{ξ} or β ∉ A_{ττ_{1}b_{1}}. Then as before, α ∈ A_{ττ_{1}b_{1}} and hence M, ττ_{1}b_{1} ⊧ α by induction hypothesis. By the choice of τ_{2} we are assured that m ≥ 2 because f_{ττ_{1}b_{1}} = ↓. So consider ρ(ττ_{1}b_{1}) ⟹^{b_{2}} ρ(ττ_{1}b_{1}b_{2}). Then again it follows easily that there must exist q′_{2} ∈ Q_{ξ} such

that q′_{1} ⟶^{b_{2}}_{ξ} q′_{2} and (q′_{2}, 1) ∈ X̂_{ττ_{1}b_{1}b_{2}}. If q′_{2} ∈ F_{ξ} and β ∈ A_{ττ_{1}b_{1}b_{2}} then we

will at once obtain M, τ ⊧ α U^{π}β. If not, the facts that (q′_{1}, 1) ∈ X̂_{ττ_{1}b_{1}} and that q′_{1} ∉ F_{ξ} or β ∉ A_{ττ_{1}b_{1}} holds, guarantee us that f_{ττ_{1}b_{1}b_{2}} = ↓ by (2.iii). Hence m ≥ 3. Carrying on this way we will eventually exhaust all of τ_{2} and while doing so, reach the desired conclusion M, τ ⊧ α U^{π}β. □

Lemma 4.2 Suppose α_{0} is satisfiable. Then L(B) ≠ ∅.

Proof: Since our logic has no past modalities it is easy to see that if α_{0} is satisfiable then there exists a model M = (σ, V) such that M, ε ⊧ α_{0}. We shall show that σ ∈ L(B) by constructing a map ρ : prf(σ) ⟶ S so that ρ is an accepting run of B over σ. For each τ ∈ prf(σ) we set ρ(τ) = (A_{τ}, X_{τ}, X̂_{τ}, x_{τ}, f_{τ}) and define ρ in a componentwise manner.

For each τ ∈ prf(σ) define A_{τ} via:

A_{τ} = {α | M, τ ⊧ α}.

For each τ ∈ prf(σ) define X_{τ} as follows. Suppose ξ = α U^{π}β and q ∈ Q_{ξ}. Then q ∈ X_{τ} iff there exists a pair (τ′, R′) such that:

• ττ′ ∈ prf(σ) and M, ττ′ ⊧ β.

• For every τ′′, if ε ⪯ τ′′ ≺ τ′ then M, ττ′′ ⊧ α.

• R′ : prf(τ′) ⟶ Q_{ξ} such that R′(ε) = q and R′(τ′) ∈ F_{ξ} and

R′(τ′′) ⟶^{a}_{ξ} R′(τ′′a) for every τ′′a ∈ prf(τ′).

To define the remaining three components we will first define the fourth and fifth components by mutual induction. To this end we shall make use of some terminology.

We shall call the pair (τ, ξ) an obligation in M if τ ∈ prf(σ) and ξ = α U^{π}β ∈ Req such that M, τ ⊧ α U^{π}β but M, τ |̸= β or ε ∉ ||π||. Let (τ, ξ) be an obligation in M. We shall say that the pair (τ′, R′) is a witness for (τ, ξ) iff the following conditions are satisfied:

• ττ′ ∈ prf(σ) and M, ττ′ ⊧ β and for every τ′′, ε ⪯ τ′′ ≺ τ′ implies M, ττ′′ ⊧ α.

• τ′ ∈ ||π|| and R′ : prf(τ′) ⟶ Q_{ξ} such that R′(ε) ∈ I_{ξ}, R′(τ′) ∈ F_{ξ}

and R′(τ′′) ⟶^{a}_{ξ} R′(τ′′a) for every τ′′a ∈ prf(τ′).

Note that if (τ′, R′) is a witness for the obligation (τ, ξ) then τ′ ≠ ε. We shall fix a chronicle set CH for M. It is a set of quadruples which satisfies the following conditions:

• If (τ, ξ, τ′, R′) ∈ CH then (τ, ξ) is an obligation in M and (τ′, R′) is witness for (τ, ξ).

• If (τ, ξ) is an obligation in M then (τ, ξ, τ′, R′) ∈ CH for some witness (τ′, R′) for (τ, ξ).

• If (τ, ξ, τ′, R′), (τ, ξ, τ′′, R′′) ∈ CH then (τ′, R′) = (τ′′, R′′).

It is easy to check that CH exists. (In fact it can be chosen in a canonical manner by fixing a lexicographic order on Q_{ξ} for each ξ ∈ Req).

With these definitions in place, we are now prepared to define the fourth and the fifth components of ρ by induction on τ. For the base case, we set (x_{ε}, f_{ε}) = (0, ✓). Now consider the induction step where τ = τ_{0}a and assume that (x_{τ′}, f_{τ′}) is defined for every τ′ ∈ prf(τ_{0}). If f_{τ_{0}} = ✓ then (x_{τ}, f_{τ}) = (1 − x_{τ_{0}}, ↓). Suppose f_{τ_{0}} = ↓. Then (x_{τ}, f_{τ}) = (x_{τ_{0}}, ↓) if there exists (τ_{1}, ξ_{1}, τ′_{1}, R′_{1}) ∈ CH such that τ_{1} ⪯ τ_{0} ≺ τ_{1}τ′_{1} and x_{τ_{1}} = 1 − x_{τ_{0}}. Otherwise, f_{τ} = ✓ and x_{τ} = x_{τ_{0}}.

Finally, the third component of ρ can now be defined. For each τ ∈ prf(σ), we define X̂_{τ} as follows. Suppose ξ ∈ Req and q ∈ Q_{ξ} and z ∈ {0, 1}. Then (q, z) ∈ X̂_{τ} iff there exists (τ_{1}, ξ, τ′_{1}, R′_{1}) ∈ CH such that for some τ′′_{1} ∈ prf(τ′_{1}), τ_{1} ⪯ τ = τ_{1}τ′′_{1}. Moreover, R′_{1}(τ′′_{1}) = q and x_{τ_{1}} = 1 − z.

We now wish to argue that ρ : prf(σ) ⟶ S is an accepting run of B over σ. First we shall show that ρ is well defined. Let τ ∈ prf(σ) be given. We must show that ρ(τ) ∈ S. It is easy to see that A_{τ} is an atom, X_{τ} ⊆ Q, X̂_{τ} ⊆ Q̂, x_{τ} ∈ {0, 1} and f_{τ} ∈ {↓, ✓}. We will show that ρ(τ) satisfies all the clauses of the definition of B.

So fix some α U^{π}β = ξ. Assume initially that β ∈ A_{τ} and q ∈ F_{ξ}. Then M, τ ⊧ β by definition of A_{τ}. Now consider the pair (τ′, R′) where τ′ = ε and R′(ε) = q. From the definition of X_{τ} it now follows that q ∈ X_{τ}. Thus F_{ξ} ⊆ X_{τ} as required by (1.i).

Next assume that α ∈ A_{τ} and q ∈ X_{τ} for some q ∈ I_{ξ}. From the definition of X_{τ} it follows that there exists a pair (τ′, R′) such that ττ′ ∈ prf(σ) and M, ττ′ ⊧ β and M, ττ′′ ⊧ α for every τ′′ such that ε ⪯ τ′′ ≺ τ′. Furthermore, R′ : prf(τ′) ⟶ Q_{ξ} such that R′(ε) = q and R′(τ′) ∈ F_{ξ} and R′(τ′′) ⟶^{a}_{ξ} R′(τ′′a) for every τ′′a ∈ prf(τ′). But from the assumption that q ∈ I_{ξ} we have that τ′ ∈ ||π||, because R′ is an accepting run of A_{ξ} over τ′. Consequently M, τ ⊧ α U^{π}β and this leads to the conclusion that α U^{π}β ∈ A_{τ} as required by (1.ii).

Next assume that α U^{π}β ∈ A_{τ} and β ∉ A_{τ} or ε ∉ ||π||. Then (τ, ξ) is an obligation in M since by the definition of A_{τ}, M, τ ⊧ α U^{π}β but M, τ |̸= β or ε ∉ ||π||. Hence there exists (τ, ξ, τ′, R′) ∈ CH. Let R′(ε) = q. From the fact that (τ′, R′) is a witness for (τ, ξ) we have that q ∈ I_{ξ}. Moreover, by the definition of X̂_{τ} and from τ ⪯ τ = τ (i.e. τ_{1} = τ and τ′′_{1} = ε), it follows that (q, 1 − x_{τ}) ∈ X̂_{τ} as required by (1.iii).

Finally suppose that (q, z) ∈ X̂_{τ} with q ∈ Q_{ξ} such that q ∉ F_{ξ} or β ∉ A. Now (q, z) ∈ X̂_{τ} implies, by the definition of X̂_{τ}, that there exists (τ_{1}, ξ, τ′_{1}, R′_{1}) ∈ CH such that for some τ′′_{1} ∈ prf(τ′_{1}), τ_{1} ⪯ τ = τ_{1}τ′′_{1} and R′_{1}(τ′′_{1}) = q and x_{τ_{1}} = 1 − z. But (τ′_{1}, R′_{1}) is a witness for the obligation (τ_{1}, ξ) and hence R′_{1}(τ′_{1}) ∈ F_{ξ} and M, τ_{1}τ′_{1} ⊧ β. Since β ∉ A_{τ} or q ∉ F_{ξ} it must be the case that τ′′_{1} ≺ τ′_{1} and hence M, τ_{1}τ′′_{1} ⊧ α. But then τ = τ_{1}τ′′_{1} now leads to α ∈ A_{τ} as required by (1.iv).

We have now shown that ρ is well defined. Next we wish to show that ρ is a run of B over σ. Since M, ε ⊧ α_{0} we have α_{0} ∈ A_{ε}. By definition, (x_{ε}, f_{ε}) = (0, ✓). Hence ρ(ε) ∈ S_{in}.

Now suppose τa ∈ prf(σ). We must show that ρ(τ) ⟹^{a} ρ(τa). For this purpose we fix α U^{π}β = ξ ∈ Req. Suppose q, q′ ∈ Q_{ξ} with q′ ∈ X_{τa} such that q ⟶^{a}_{ξ} q′. Further suppose α ∈ A_{τ}. Now q′ ∈ X_{τa} implies that there exists a pair (τ′, R′) such that R′(ε) = q′ and R′(τ′) ∈ F_{ξ} and R′(τ′′) ⟶^{b}_{ξ} R′(τ′′b) for every τ′′b ∈ prf(τ′). Furthermore, M, τaτ′ ⊧ β and M, τaτ′′ ⊧ α for every τ′′ such that ε ⪯ τ′′ ≺ τ′. Now consider the pair (aτ′, R′_{a}) where R′_{a} : prf(aτ′) ⟶ Q_{ξ} is given as R′_{a}(ε) = q and for every τ′′ ∈ prf(τ′), R′_{a}(aτ′′) = R′(τ′′). From M, τ ⊧ α (as α ∈ A_{τ} by assumption) it now follows at once that q ∈ X_{τ} as required by (2.i).

Suppose now that q ∈ Q_{ξ} and (q, z) ∈ X̂_{τ} but q ∉ F_{ξ} or β ∉ A_{τ}. Since (q, z) ∈ X̂_{τ} there must exist (τ_{1}, ξ, τ′_{1}, R′_{1}) ∈ CH and τ′′_{1} ∈ prf(τ′_{1}) such that τ_{1} ⪯ τ = τ_{1}τ′′_{1} and x_{τ_{1}} = 1−z and R′_{1}(τ′′_{1}) = q. But (τ′_{1}, R′_{1}) is a witness for (τ_{1}, ξ) and hence R′_{1}(τ′_{1}) ∈ F_{ξ} and M, τ_{1}τ′_{1} ⊧ β. Consequently τ′′_{1} ≺ τ′_{1} and thus τ′′_{1}a ∈ prf(τ′_{1}) for the unique a. This implies that

R′_{1}(τ′′_{1}) ⟶^{a}_{ξ} R′_{1}(τ′′_{1}a). Let R′_{1}(τ′′_{1}a) = q′. Then q ⟶^{a}_{ξ} q′. But then

it follows directly from the definition of X_{τa}, that (q′, 1 − z) ∈ X̂_{τa} as required by (2.ii).

Next suppose that f_{τ} = ✓. Then clearly (x_{τa}, f_{τa}) = (1−x_{τ}, ↓) by the definition of ρ. So assume that f_{τ} = ↓. Supposing there exists α U^{π}β = ξ in Req and there exists q ∈ Q_{ξ} such that (q, z) ∈ X̂_{τ} where z = x_{τ}. Further suppose q ∉ F_{ξ} or β ∉ A_{τ}. Now (q, z) ∈ X̂_{τ} implies that there exists (τ_{1}, ξ, τ′_{1}, R1′) ∈ CH such that τ_{1} ⪯ τ = τ_{1}τ′′_{1} for some τ′′_{1} ∈ prf(τ′_{1}) with the further property that x_{τ_{1}} = 1 − z. From the definitions and the fact that q ∉ F_{ξ} or β ∉ A_{τ} it follows that τ_{1} ⪯ τ ≺ τ_{1}τ′_{1}. Hence by the definition of ρ it follows that (x_{τa}, f_{τa}) = (x_{τ}, ↓) as required by (2.iii). On the other hand, if such a (q, z) ∈ X̂_{τ} does not exist, then it follows directly from the definition that (x_{τa}, f_{τa}) = (x_{τ}, ✓) as required by (2.iii).

We have now verified that ρ is a run of B over σ. To show that ρ is accepting it suffices to prove that for any τ ∈ prf(σ) there exists τ′ such that ττ′ ∈ prf(σ) and f_{ττ′} = ✓.

Case 1: \underline{(x_{τ}, f_{τ}) = (0, ✓)}. By picking τ′ = ε the desired conclusion follows trivially.

Case 2: \underline{(x_{τ}, f_{τ}) = (0, ↓)}. Define the set Γ_{τ} ⊆ CH as follows. Suppose (τ, ξ, τ′, R′) ∈ CH. Then it must be the case that (τ_{1}, ξ_{1}, τ′_{1}, R′_{1}) ∈ Γ_{τ} iff τ_{1} ⪯ τ ≺ τ_{1}τ′_{1} and x_{τ_{1}} = 1. If Γ_{τ} = ∅ then it is easy to see that with τ′ = a where τa ∈ prf(σ) we must have f_{ττ′} = ✓ as required.

So suppose Γ_{τ} ≠ ∅. Define, for each ch = (τ_{1}, ξ_{1}, τ′_{1}, R′_{1}) ∈ Γ_{τ}, k_{ch} = |τ_{1}τ′_{1}| − |τ| and set k_{τ} = max({k_{ch}}_{ch∈Γ_{τ}}). Let τa ∈ prf(σ). Then it is easy to see that (x_{τa}, f_{τa}) = (0, ↓). But it is also easy to verify Γ_{τa} = ∅ or k_{τa} < k_{τ}. Proceeding in this way the required conclusion can be drawn eventually.

The two other cases can be resolved by similar arguments. □

It is now straightforward to establish the main result of this section. To start with we define the size of a formula α, denoted |α|, via:

• |p| = 1, |∼α| = 1 + |α| and |α ∨ β| = 1 + |α| + |β|.

• |α U^{π}β| = 1 + |α| + |π| + |β|,

where |π| is given by |a| = 1, |π + π′| = |π; π′| = 1 + |π| + |π′| and |π^{∗}| = 1 + |π|.

Theorem 4.3 For each α ∈ DLTL(Σ) the question whether or not α is satisfiable can be decided in time 2^{O(|α|)}.

Proof: Let α_{0} ∈ DLTL(Σ). Then α_{0} is satisfiable iff L(B_{α_{0}}) ≠ ∅ where α_{0} is the Büchi automaton constructed above. The emptiness problem for B_{α_{0}} can be settled in O(|S|) where S is the set of states of B [20].

Clearly CL(α_{0}) is linear in the size of α_{0} and hence |AT | = 2^{O(|α_{0}|)}. Let α U^{π}β ∈ Req. It is known that for π ∈ Prg(Σ), we can construct in polynomial time a non-deterministic finite state automaton A_{ξ} with L(A) = ||π|| such that |Q_{ξ}| is linear in the size of π (see [7] for a recent account on converting regular expression to small finite state automata).

Let Req = {α_{1} U^{π_{1}}β_{1}, …, α_{m} U^{π_{m}}β_{m}}. Then |π_{1}|+|π_{2}|+…+|π_{m}| ≤ |α_{0}|. Consequently both Q and Q̂ are linear in the size of α_{0}. It is now easy to see that |S| = 2^{O(|α_{0}|)}. □

As usual, the decision procedure can be applied to solve the associated model checking problem but we will not enter into details here.

5 Some Expressiveness Results

Our main goal here is to show that DLTL(Σ) has the same expressive power as the monadic second-order theory of infinite sequences over Σ. Towards the end of the section we will also establish that a natural sublogic of DLTL(Σ) captures the first order theory of infinite sequences over Σ.

In order to obtain clean formulations of the expressiveness results, we shall banish atomic propositions through the rest of the paper. Instead, we will just work with the constant ⊤ and its negation ∼⊤ ⟺^{Δ} ⊥. To be precise, the syntax of DLTL(Σ) will be from now on assumed to be:

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

where π ∈ Prg(Σ) with Prg(Σ) defined as before.

A model is now just a ω-sequence σ ∈ Σ^{ω}. For τ ∈ prf(σ) we define σ, τ ⊧ α via:

• σ, τ ⊧ ⊤.

• All the other clauses are filled in exactly as in Section 3 while replacing M by σ in the appropriate places.

Each formula α now defines a ω-language L_{α} ⊆ Σ^{ω} given by:

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

We say that L ⊆ Σ^{ω} is DLTL(Σ)-definable iff there exists some α ∈ DLTL(Σ) such that L = L_{α}.

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

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

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

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

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

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

We say that L ⊆ Σ^{ω} is S1S(Σ)-definable iff there exists a sentence ϕ ∈ S1S(Σ) such that L = L_{ϕ}.

Lemma 5.1 Let L ⊆ Σ^{ω}. If L is DLTL(Σ)-definable then L is S1S(Σ)- definable.

Proof: Consider the construction from the previous section which associates a Büchi automaton B_{α_{0}} with each formula α_{0} ∈ DLTL(Σ). Suppose we apply this construction to formulas arising from the restricted syntax assumed in the present section. Then it is easy to see that, in the absence of atomic propositions, L_{α_{0}} = L(B_{α_{0}}). But then the classic result of Büchi [1] asserts that L ⊆ Σ^{ω} is S1S(Σ)-definable iff there exists a Büchi automaton B operating over Σ such that L = L(B). □

Next we wish to show that if L ⊆ Σ^{ω} is S1S(Σ)-definable then L is DLTL(Σ)-definable. In fact, it turns out that it suffices to consider a natural fragment of DLTL(Σ) denoted DLTL^{−}(Σ) whose syntax is given by:

DLTL^{−}(Σ) ::= ⊤ | ∼α | α ∨ β | ⟨π⟩α,

where π ∈ Prg(Σ).

Here ⟨π⟩α is interpreted as ⊤ U^{π} α with the resulting semantics. As before L ⊆ Σ^{ω} is said to be DLTL^{−}(Σ)-definable iff there exists α ∈ DLTL^{−}(Σ) such that L = L_{α}, where L_{α} is defined as for DLTL(Σ). To get at the result we are after we need to work with Muller automata operating over Σ of the form A = (Q, ⟶, Q_{in}, F) where:

• Q, ⟶ and Q_{in} as in the case of a Büchi automaton.

• F ⊆ 2^{Q} is a family of accepting sets of states.

Let σ ∈ Σ^{ω}. Then the notion of a run ρ : prf(σ) ⟶ Q of A over σ is as in the case of a Büchi automaton. The definition of inf(ρ) is also as before. The run ρ is said to be accepting iff inf(ρ) ∈ F. Naturally L(A), the ω-language accepted by A, is given by : σ ∈ L(A) iff there exists an accepting run of A over σ.

The Muller automaton A = (Q, ⟶, Q_{in}, F) is said to be deterministic iff |Q_{in}| = 1 and ⟶ ⊆ Q × Σ × Q is a deterministic transition relation. In other words, whenever q ⟶^{a} q′ and q ⟶^{a} q′′, we have q′ = q′′. The well-known theorem of McNaughton [12] guarantees that L ⊆ Σ^{ω} is S1S(Σ)-definable iff there exists a deterministic Muller automaton operating over Σ such that L = L(A). This fact will be the basis for the proof of the next result.

Lemma 5.2 Let L ⊆ Σ^{ω}. If L is S1S(Σ)-definable then L is DLTL^{−}(Σ)- definable.

Proof: As remarked above L is S1S(Σ)-definable implies that there exists a deterministic Muller automaton A = (Q, ⟶, {q_{in}}, F) operating over Σ such that L = L(A). We will exhibit a formula α_{A} ∈ DLTL^{−}(Σ) such that L_{α_{A}} = L(A).

An easy argument shows that it involves no loss of generality to assume that A — apart from determinacy — has two additional properties:

(i) ∅ ∉ F.

(ii) ∀q ∈ Q ∀a ∈ Σ. ∃q′. q ⟶^{a} q′.

Determinacy and (ii) ensure that for every σ ∈ Σ^{ω} the Muller automaton A has a unique run over σ. This fact will be crucial in what follows.

Suppose F = ∅. In this case we have that L = ∅, so we set α_{A} = ⊥. So suppose that F ≠ ∅. For each F ∈ F we shall construct a formula

α_{F}. The required formula α_{A} defining L will then be the disjunction of all such α_{F}.

First we extend ⟶ ⊆ Q × Σ × Q to ⟶_{∗}, where ⟶_{∗} is the least subset of Q × Σ^{∗} × Q satisfying:

• q ⟶^{ε}_{∗} q for every q ∈ Q.

• If q ⟶^{τ}_{∗} q′ and q′ ⟶^{a} q′′ then q ⟶^{τa}_{∗} q′′.

Next define, for each q, q′ ∈ Q, the language of finite words L_{q,q′} ⊆ Σ^{∗} by:

L_{q,q′} = {τ | q ⟶^{τ}_{∗} q′}.

It is easy to see that each L_{q,q′} is a regular subset of Σ^{∗}. Hence we can fix a regular expression π_{q,q′} ∈ Prg(Σ) such that L_{q,q′} = ||π_{q,q′}||. Due to the determinacy of A it follows at once that if q, q′, q′′ ∈ Q such that L_{q,q′} ∩ L_{q,q′′} ≠ ∅ then q′ = q′′.

Now let F = {q_{0}, q_{1}, …, q_{n−1}} with n ≥ 1. Then the formula α_{F} is given by:

α_{F} = ⋁_{q∈F}⟨π_{q_{in},q}⟩ ( ⋀_{q′∉F}[π_{q,q′}]⊥ ∧ ⋀_{j=0}^{n−1}[π_{q,q_{j}}]⟨π_{q_{j},q_{j⊕1}}⟩⊤) ,

where ⊕ denotes addition modulo n. The required formula α_{A} is then defined as:

α_{A} = ⋁_{F ∈F} α_{F}

Clearly α_{A} ∈ DLTL^{−}(Σ). We wish to argue that L(A) = L_{α_{A}}. So first suppose that σ ∈ L(A). Let ρ : prf(σ) ⟶ Q be the (unique) run of A over σ. We must have inf(ρ) ∈ F since ρ is an accepting run. Assume that inf(ρ) = F = {q_{0}, q_{1}, …, q_{n−1}} with n ≥ 1. There must exist a τ ∈ prf(σ) such that ρ(τ) = q ∈ F and for all τ′ ∈ Σ^{∗}, ττ′ ∈ prf(σ) implies ρ(ττ′) ∈ F. This is so because inf(ρ) = F. If ρ(τ) = q then τ ∈ ||π_{q_{in},q}|| because ρ(ε) = q_{in} and (consequently) ρ being a run assures us that q_{in} ⟶^{τ}_{∗} q. Now suppose σ, τ ⊧ ⟨π_{q,q′}⟩⊤ for some q′ ∉ F. Then there exists τ′ ∈ ||π_{q,q′}|| such that ττ′ ∈ prf(σ). But this violates the assumed property of τ. Consequently, for every q′ ∉ F we must have σ, τ ⊧ [π_{q,q′}]⊥. Hence σ, τ ⊧ ⋀_{q′∉F} [π_{q,q′}]⊥.

Next suppose j ∈ {0, 1, …, n − 1} and τ′ ∈ ||π_{q,q_{j}}|| such that ττ′ ∈ prf(σ). Then by the assumed property of τ there must exist τ′′ ≠ ε such that ττ′τ′′ ∈ prf(σ) and ρ(ττ′τ′′) = q_{j⊕1}, because q_{j⊕1} ∈ F = inf(ρ). Clearly τ′′ ∈ ||π_{q_{j},q_{j⊕1}}|| because ρ(ττ′) = q_{j}. Thus σ, τ ⊧ [π_{q,q_{j}}]⟨π_{q_{j},q_{j⊕1}}⟩⊤ for every j ∈ {0, 1, …, n − 1}. We have now established that σ, ε ⊧ α_{F} where F ∈ F. This in turn implies that σ, ε ⊧ α_{A} and hence σ ∈ L_{α_{A}}.

Now assume that σ, ε ⊧ α_{A}. Then it must be the case that σ, ε ⊧ α_{F} for some F ∈ F with F = {q_{0}, q_{1}, …, q_{n−1}}, n ≥ 1. Consequently, there exist τ ∈ prf(σ) and q ∈ F such that τ ∈ ||π_{q_{in},q}|| and

σ, τ ⊧ ⋀_{q′∉F}[π_{q,q′}]⊥ ∧ ⋀_{j=0}^{n−1}[π_{q,q_{j}}]⟨π_{q_{j},q_{j⊕1}}⟩⊤.

Let ρ be the unique run of A over σ. From the determinacy of A it follows that ρ(τ) = q.

Claim: Suppose τ′ ∈ Σ^{∗} is such that ττ′ ∈ prf(σ). Then ρ(ττ′) ∈ F.

To see that the claim holds, let ττ′ ∈ prf(σ) and ρ(ττ′) = q′. If q′ ∉ F then τ′ ∈ ||π_{q,q′}|| would lead to the contradiction that σ, τ ⊧ ⟨π_{q,q′}⟩⊤ for some q′ ∉ F. Thus the claim holds, which at once implies that inf(ρ) ⊆ F.

If we now show that F ⊆ inf(ρ) we are done. So let j ∈ {0, 1, …, n − 1}. To show that q_{j} ∈ inf(ρ) assume that τ′ ∈ Σ^{∗} such that ττ′ ∈ prf(σ). Let ρ(ττ′) = q_{i}, say. We must show that there exists τ′′ such that ττ′τ′′ ∈ prf(σ) and ρ(ττ′τ′′) = q_{j}.

If i = j then we can set τ′′ = ε and be done. So suppose i ≠ j. Then clearly τ′ ∈ ||π_{q,q_{i}}||. But σ, τ ⊧ [π_{q,q_{i}}]⟨π_{q_{i},q_{i⊕1}}⟩⊤ and hence there must exist τ_{i} ∈ ||π_{q_{i},q_{i⊕1}}|| such that ττ′τ_{i} ∈ prf(σ) so that ρ(ττ′τ_{i}) = q_{i⊕1}. If i⊕1 = j then we can set τ′′ = τ_{i}. Otherwise τ′τ_{i} ∈ ||π_{q,q_{i⊕1}}|| and hence we can find τ_{i⊕1} such that ττ′τ_{i}τ_{i⊕1} ∈ prf(σ) such that ρ(ττ′τ_{i}τ_{i⊕1}) = q_{i⊕2}. If i ⊕ 2 = j we set τ′′ = τ_{i}τ_{i⊕1}, otherwise we proceed as before. Eventually we will be done. □

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

(i) L is S1S(Σ)-definable.

(ii) L is DLTL(Σ)-definable.

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

Proof: Follows immediately from Lemmas 5.1, 5.2 and the fact that DLTL^{−}(Σ) is a sublogic of DLTL(Σ). □

At present we do not know of a direct conversion of DLTL(Σ)-formulas into DLTL^{−}(Σ)-formulas. Although these two logics have the same expressive power in the sense of Theorem 5.3, it appears that DLTL(Σ) will admit more natural specifications. In addition, it is a conservative extension of LTL(Σ) even from a syntactic standpoint and hence conventional LTL specifications can be brought in with no overhead translation costs.

We shall conclude this section by pointing out that star-free programs can be used to capture the first-order definable subsets of Σ^{ω}. Admittedly this is not a big surprise, but it illustrates once more that our method of augmenting the expressive power of LTL is a natural one.

FO(Σ) will denote the first-order theory of ω-sequences generated by Σ. It is the fragment of S1S(Σ) obtained by eliminating set variables from the syntax. We shall say that L ⊆ Σ^{ω} is FO(Σ)-definable iff there exists a sentence ϕ in FO(Σ) such that L = L_{ϕ}.

The set of star-free regular programs over Σ is denoted Prg_{𝕊𝔽}(Σ) and its syntax is given by:

Prg_{𝕊𝔽}(Σ) ::= 0 | a | π + π′ | \overline{π} | π; π′.

The set of finite words denoted by each star-free program is obtained via the map || · || : Prg_{𝕊𝔽}(Σ) ⟶ 2^{Σ^{∗}} which is defined as follows: || \overline{π} || = Σ^{∗} − ||π|| and ||0|| = ∅. The remaining cases are handled as before.

Next let φ ∈ FO(Σ), τ ∈ Σ^{∗} and I : Var ⟶ {0, 1, …, |τ| − 1} where |τ| is the length of τ. In case τ = ε we set I — viewed as a set of ordered pairs — to the empty set. The notion τ ⊧_{I} φ is defined in the obvious way.

With each sentence φ ∈ FO(Σ) we can now associate the language of finite words L_{φ}^{fin} given by:

L_{φ}^{fin} = {τ | τ ∈ Σ^{∗} and τ ⊧ φ}.

We let SF^{fin}(Σ) be the subset of 2^{Σ^{∗}} where L ⊆ Σ^{∗} is admitted as a member of SF^{fin}(Σ) iff there exists a sentence φ ∈ FO(Σ) such that L = L_{φ}^{fin}. A well-known fact [13] is that SF^{fin}(Σ) and Prg_{𝕊𝔽}(Σ) denote each other in the following sense.

Proposition 5.4 Let L ⊆ Σ^{∗}. Then L ∈ SF^{fin}(Σ) iff there exists π ∈ Prg_{𝕊𝔽}(Σ) such that L = ||π||.

Next we recall a well-known characterization of FO(Σ)-definable subsets of Σ^{ω}. Let SF^{ω}(Σ) be the least subset of 2^{Σ^{ω}} which satisfies:

• ∅ ∈ SF^{ω}(Σ).

• If L̂ ∈ SF^{ω}(Σ) then Σ^{ω} − L̂ ∈ SF^{ω}(Σ).

• If L̂_{1}, L̂_{2} ∈ SF^{ω}(Σ) then L̂_{1} ∪ L̂_{2} ∈ SF^{ω}(Σ).

• If L ∈ SF^{fin}(Σ) and L̂ ∈ SF^{ω}(Σ) then {τσ | τ ∈ L and σ ∈ L̂} ∈ SF^{ω}(Σ).

We then have the following characterization (see [20]).

Proposition 5.5 Let L ⊆ Σ^{ω}. Then L ∈ SF^{ω}(Σ) iff L is FO(Σ)- definable.

The star-free version of DLTL(Σ) will be denoted — for want of a better notation — by DLTL_{𝕊𝔽}(Σ) and its syntax is given by:

DLTL_{𝕊𝔽}(Σ) ::= ⊤ | ∼α | α ∨ β | α U^{π}β (π ∈ Prg_{𝕊𝔽}(Σ)).

Thus the only difference is that the programs that are used to build up the until-formulas are required to be star-free programs. All the semantic notions concerning this logic are transported from DLTL(Σ) in the natural manner. The fragment of DLTL_{𝕊𝔽}(Σ) which corresponds to DLTL^{−}(Σ) has the syntax:

DLTL_{𝕊𝔽}^{−}(Σ) ::= ⊤ | ∼α | α ∨ β | ⟨π⟩α (π ∈ Prg_{𝕊𝔽}(Σ)).

Once again, all the semantic notions concerning DLTL_{𝕊𝔽}^{−}(Σ) are transported from DLTL^{−}(Σ) in the natural way.

We now wish to show that FO(Σ), DLTL_{𝕊𝔽}(Σ) and DLTL_{𝕊𝔽}^{−}(Σ) all have the same expressive power.

Lemma 5.6 Let L̂ ⊆ Σ^{ω}. If L̂ is FO(Σ)-definable then L̂ is DLTL_{𝕊𝔽}^{−}(Σ)- definable.

Proof: Using Proposition 5.5 and following the definition of SF^{ω}(Σ), we now inductively define the map g : SF^{ω}(Σ) ⟶ DLTL_{𝕊𝔽}^{−}(Σ) as follows.

• If L̂ = ∅ then g(L̂) = ⊥.

• Suppose L̂ = Σ^{ω} − L̂_{1} for some L̂_{1} ∈ SF^{ω}(Σ) with g(L̂_{1}) defined. Then g(L̂) = ∼g(L̂_{1}).

• Suppose L̂ = L̂_{1} ∪L̂_{2} with L̂_{1}, L̂_{2} ∈ SF^{ω}(Σ) so that both g(L̂_{1}) and g(L̂_{2}) are defined. Then g(L̂) = g(L̂_{1}) ∨ g(L̂_{2}).

• Suppose L_{1} ∈ SF^{fin}(Σ) and L̂_{1} ∈ SF^{ω}(Σ) such that L = {τσ | τ ∈ L_{1} and σ ∈ L̂_{1}} and g(L̂_{1}) is defined. Let π ∈ Prg_{𝕊𝔽}(Σ) such that L = ||π||. The existence of π is guaranteed by Proposition 5.4. Then g(L̂) = ⟨π⟩g(L̂_{1}).

It is now routine to verify that for each L̂ ∈ SF^{ω}(Σ)

L̂ = {σ | σ, ε ⊧ g(L̂)}.

Hence L̂ is DLTL_{𝕊𝔽}^{−}(Σ)-definable. □

The last step is to show that DLTL_{𝕊𝔽}(Σ)-definability implies FO(Σ)- definability. The proof will be syntactic and it will be convenient to go through some preliminaries.

First let φ ∈ FO(Σ) and x, y be variables that do not appear in φ (free or bound). Then the formulas Rel(φ, 0, x) and Rel(φ, x, y) — describing the relativizations of φ — are defined inductively as follows:

• Rel(R_{a}(z), 0, x) = z ≤ x ∧ R_{a}(z).

Rel(R_{a}(z), x, y) = x ≤ z ∧ z ≤ y ∧ R_{a}(z).

• Rel(z_{1} ≤ z_{2}, 0, x) = z_{2} ≤ x ∧ z_{1} ≤ z_{2}.

Rel(z_{1} ≤ z_{2}, x, y) = x ≤ z_{1} ∧ z_{2} ≤ y ∧ z_{1} ≤ z_{2}.

• Rel(∼φ, 0, x) = ∼Rel(φ, 0, x).

Rel(∼φ, x, y) = ∼Rel(φ, x, y).

• Rel(φ_{1} ∨ φ_{2}, 0, x) = Rel(φ_{1}, 0, x) ∨ Rel(φ_{2}, 0, x).

Rel(φ_{1} ∨ φ_{2}, x, y) = Rel(φ_{1}, x, y) ∨ Rel(φ_{2}, x, y).

• Rel((∃z)φ, 0, x) = (∃z)(z ≤ x ∧ Rel(φ, 0, x)).

Rel((∃z)φ, x, y) = (∃z)(x ≤ z ∧ z ≤ y ∧ Rel(φ, x, y)).

It is easy to see that both Rel(φ, 0, x) and Rel(φ, x, y) are members of FO(Σ) for any φ ∈ FO(Σ).

Next we fix for each π ∈ Prg_{𝕊𝔽}(Σ) a sentence φ_{π} ∈ FO(Σ) such that ||π|| = L_{φ}^{fin}. The existence of φ_{π} is guaranteed by Proposition 5.4 and the definition of SF^{fin}(Σ).

Finally we inductively define, for each α ∈ DLTL_{𝕊𝔽}(Σ), the formulas SAT(α, 0) and SAT(α, x) as follows:

• SAT(⊤, 0) = SAT(⊤, x) = (∀z)(z ≤ z).

• SAT(∼α, 0) = ∼SAT(α, 0).

SAT(∼α, x) = ∼SAT(α, x).

• SAT(α ∨ β, 0) = SAT(α, 0) ∨ SAT(β, 0).

SAT(α ∨ β, x) = SAT(α, x) ∨ SAT(β, x).

• Let α = β_{1} U^{π}β_{2}. Suppose first that ε ∈ ||π||. Then

SAT(α, 0) = SAT(β_{2}, 0) ∨ (SAT(β_{1}, 0) ∧ (∃x)(φ_{1} ∧ φ_{2} ∧ φ_{3})),

where

φ_{1} = SAT(β_{2}, x),
φ_{2} = (∀y)(y < x ⊃ SAT(β_{1}, y)),
φ_{3} = Rel(φ_{π}, 0, x).

Moreover,

SAT(α, x) = SAT(β_{2}, x)∨(SAT(β_{1}, x)∧(∃y)(x < y ∧φ′_{1} ∧φ′_{2} ∧φ′_{3})),

where

φ′_{1} = SAT(β_{2}, y),
φ′_{2} = (∀z)(x ≤ z ∧ z < y ⊃ SAT(β_{1}, z)),
φ′_{3} = Rel(φ_{π}, x, y).

Now, if it is the case that ε ∉ ||π|| we disregard SAT(β_{2}, 0) and SAT(β_{2}, x), respectively, above. In other words,

SAT(α, 0) = SAT(β_{1}, 0) ∧ (∃x)(φ_{1} ∧ φ_{2} ∧ φ_{3}),

and

SAT(α, x) = SAT(β_{1}, x) ∧ (∃y)(x < y ∧ φ′_{1} ∧ φ′_{2} ∧ φ′_{3}),

We can now prove the following result.

Lemma 5.7 Let L ⊆ Σ^{ω}. If L is DLTL_{𝕊𝔽}(Σ)-definable then L is FO(Σ)- definable.

Proof: Let L ⊆ Σ^{ω} be given such that L = L_{α} with α ∈ DLTL_{𝕊𝔽}(Σ), i.e. L = {σ | σ, ε ⊧ α}. It is now routine to check that SAT(α, 0) is a sentence of FO(Σ) and moreover that

L = {σ | σ ⊧ SAT(α, 0)}.

Hence, L is FO(Σ)-definable. □

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

(i) L is FO(Σ)-definable.

(ii) L is DLTL_{𝕊𝔽}(Σ)-definable.

(iii) L is DLTL_{𝕊𝔽}^{−}(Σ)-definable.

Proof: Follows easily from Lemmas 5.6 and 5.7. □

6 Axiomatizations

Our axiomatization of the set of valid formulas of DLTL is an extension of Segerberg’s axiomatization of PDL [17]. Moreover, our completeness argument is based on the elegant proof of completeness of Segerberg’s axioms due to Kozen and Parikh [9]. It will be convenient to first axiomatize DLTL^{−}.

We begin by augmenting the set of regular programs with the atomic program 1. We set ||1|| = {ε}. By abuse of notation this augmented set of programs will also be denoted as Prg(Σ). Next we define the transition relation ⟶_{Prg(Σ)} (from now on written as just ⟶) to be the least subset of Prg(Σ) × Σ × Prg(Σ) yielded by the following rules:

• \overline{a ⟶^{a} 1}

• \frac{π ⟶^{a} π_{1}}{π + π′ ⟶^{a} π_{1}}  \frac{π ⟶^{a} π_{1}}{π′ + π ⟶^{a} π_{1}}

• \frac{π ⟶^{a} π_{1}}{π; π′ ⟶^{a} π_{1}; π′} if π_{1} ≠ 1

• \frac{π ⟶^{a} 1}{π; π′ ⟶^{a} π′}

• \frac{π′ ⟶^{a} π′′}{π; π′ ⟶^{a} π′′} if ε ∈ ||π||

• \frac{π ⟶^{a} π′}{π^{∗} ⟶^{a} π′; π^{∗}} .

This transition relation is extended to the relation ⟶_{∗} ⊆ Prg(Σ) × Σ^{∗} × Prg(Σ) via:

• π ⟶^{ε}_{∗} π

• If π ⟶^{τ}_{∗} π′ and π′ ⟶^{a} π′′ then π ⟶^{τa}_{∗} π′′.

Finally the sets of programs δ_{a}(π) and δ_{∗}(π) for each π and each a are defined as follows:

• δ_{a}(π) = {π′ | π ⟶^{a} π′}.

• δ_{∗}(π) = {π′ | ∃τ. π ⟶^{τ}_{∗} π′}.

Proposition 6.1 For each π and each a, both δ_{a}(π) and δ_{∗}(π) are finite sets.

Proof: The proof follows easily by structural induction on π. □

We are now ready to present an axiomatization of DLTL^{−} (Recall that Oα ⟺^{Δ} ⋁_{a∈Σ}⟨a⟩α). The logical system DLT L^{−} is given as follows.

Axiom schemes:

(A0) All the tautologies of propositional calculus.
(A1) [π] (α ⊃ β) ⊃ ([π]α ⊃ [π]β).
(A2) ⟨π + π′⟩α ≡ ⟨π⟩α ∨ ⟨π′⟩α.
(A3) ⟨π; π′⟩α ≡ ⟨π⟩⟨π′⟩α.
(A4) ⟨π^{∗}⟩α ≡ α ∨ ⟨π⟩⟨π^{∗}⟩α.
(A5) [π^{∗}](α ⊃ [π]α) ⊃ (α ⊃ [π^{∗}]α).
(A6) α ≡ ⟨1⟩α.
(A7) O⊤.
(A8) ⟨a⟩⊤ ⊃ ⋀_{b≠a}[b]⊥.
(A9) ⟨a⟩α ⊃ [a]α.
(A10) ⟨π⟩α ≡ α ∨ (⋁_{a∈Σ}⟨a⟩ ⋁_{π′∈δ_{a}(π)}⟨π′⟩α) , (ε ∈ ||π||).
(A11) ⟨π⟩α ≡ ⋁_{a∈Σ}⟨a⟩ ⋁_{π′∈δ_{a}(π)}⟨π′⟩α, (ε ∉ ||π||).

Inference rules:

\begin{matrix}(MP) & \frac{α α ⊃ β}{β}. \\ (TG) & \frac{α}{[π]α}. \end{matrix}

(A0) through (A5) and the inference rules together constitute an axiomatization of PDL. The behaviour of 1 is captured by (A6). The remaining axiom schemes describe the linear time semantics provided for regular programs in the setting of DLTL^{−}. Due to Proposition 6.1 both (A10) and (A11) are well-defined. It is easy to see that the axioms are valid and that the inference rules preserve validity.

We shall say, as usual, that a formula α is (DLT L^{−} −) consistent in case ∼α is not a thesis derivable from the system DLT L^{−}. We shall prove that every consistent formula is satisfiable. To this end, fix a consistent formula α_{0}. Define ĉl(α_{0}) to be the least set of formulas containing cl(α_{0}) (recall the definition of cl(α_{0}) in Section 4) and satisfying:

• If ⟨π⟩α ∈ ĉl(α_{0}) and π′ ∈ δ_{a}(π) then⟨π′⟩α, ⟨a⟩⟨π′⟩α ∈ ĉl(α_{0}).

• If ⟨1⟩α ∈ ĉl(α_{0}) then α ∈ ĉl(α_{0}).

• ⟨a⟩⊤ ∈ ĉl(α_{0}) for every a ∈ Σ.

Next define ĈL(α_{0}) as ĈL(α_{0}) = ĉl(α_{0}) ∪ {∼ β | β ∈ ĉl(α_{0})}. As usual, we will identify ∼∼β with β in what follows.

Proposition 6.2 ĈL(α_{0}) is a finite set.

Proof: Follows at once from Proposition 6.1. □

In this section, an atom is a maximal consistent subset of ĈL(α_{0}). If A is an atom then Â will be the conjunction of all the formulas in A. Let AT_{0} be the set of all atoms. We now define the transition system T S_{0} = (AT_{0}, ⟹) where ⟹ ⊆ AT_{0} × Σ × AT_{0} is given by A ⟹^{a} B iff Â∧ ⟨a⟩B̂ is consistent. As before, the transition relation ⟹ is extended to ⟹_{∗} ⊆ AT_{0} × Σ^{∗} × AT_{0} in the obvious way.

Lemma 6.3

(i) Suppose A, B ∈ AT_{0} and π ∈ Prg(Σ) such that Â ∧ ⟨π⟩B̂ is consistent. Then there exists τ ∈ ||π|| such that A ⟹^{τ}_{∗} B.

(ii) Suppose ⟨π⟩α ∈ A ∈ AT_{0}. Then there exists B ∈ AT_{0} and τ ∈ ||π|| such that α ∈ B and A ⟹^{τ}_{∗} B.

Proof: Part (i) can be established by just repeating the proof of [9, Lemma 1]. Now part (ii) follows easily from part (i) with the help of a few tautologies of propositional calculus. □

We are now ready to extract a model of α_{0} from T S_{0}. We shall do so by inductively defining a map ρ̂: ω ⟶ AT_{0} and an ascending chain of sequences τ_{0} ≺ τ_{1} ≺ … where each τ_{i} is in Σ^{∗}. In what follows we will denote ρ̂(i) by A_{i} for each i ∈ ω. We shall also assume that we have fixed an enumeration of the countable set ĈL(α_{0}) × Σ^{∗}.

• ρ̂(0) = A_{0} where A_{0} ∈ AT_{0} such that α_{0} ∈ A_{0}. Further, τ_{0} = ε.

• Assume ρ̂(i) and τ_{i} are defined. We say that the pair (⟨π⟩α, τ) is a requirement at stage i provided the following conditions are satisfied:

– τ ⪯ τ_{i} and ⟨π⟩α ∈ A_{j} where |τ| = j.

– For every τ′ ∈ Σ^{∗}, if ττ′ ⪯ τ_{i} then τ′ ∉ ||π|| or α ∉ A_{k} where

|ττ′| = k.

Let RQ_{i} be the set of requirements at stage i. Assume that RQ_{i} = ∅. Let a ∈ Σ such that ⟨a⟩⊤ ∈ A_{i}. The fact that such an a exists and is unique is guaranteed by (A7) and (A8). Since ⋁_{A∈AT_{0}} Â is a thesis, it follows from simple propositional reasoning that Â ∧ ⟨a⟩B̂ is consistent for some B ∈ AT_{0}. Consequently A ⟹^{a} B. Now let ρ̂(i + 1) = B and τ_{i+1} = τ_{i}a. The construction now proceeds from stage i + 1.

Assume now that RQ_{i} ≠ ∅. Let (⟨π⟩α, τ) be the least member of RQ_{i} in the enumeration we have fixed for ĈL(α_{0}) × Σ^{∗}. Let j = |τ| and ττ′ = τ_{i}. Then using (A10) and (A11) it is easy to show that there exists

π′ such that π ⟶^{τ′}_{∗} π′ and ⟨π′⟩α ∈ A_{i}. Moreover α ∉ A_{i} or ε ∉ ||π′||.

By part (ii) of Lemma 6.3, there exists B ∈ AT_{0} and τ′′ ∈ ||π′|| such that A_{i} ⟹^{τ′′}_{∗} B and α ∈ B. Let τ′′ = b_{1}b_{2} … b_{m}. Then we can find

B_{0}, B_{1}, ⋯, B_{m} ∈ AT_{0} such that A_{i} = B_{0} and B_{m} = B and B_{k} ⟹^{b_{k}} B_{k+1}

for 0 ≤ k < m. We now extend ρ̂ by:

ρ̂(i + k) = B_{k} for 1 ≤ k ≤ m.

Further we define τ_{i+k} = τ_{i}b_{1}b_{2} … b_{k} for 1 ≤ k ≤ m. The construction now proceeds from stage i + m.

Now consider the model M_{0} = (σ, V_{0}) where σ ∈ Σ^{ω} is the sequence satisfying that τ_{i} ⪯ σ for every i ∈ ω. Further, V_{0}(τ) = A_{|τ|} ∩ P for each τ ∈ prf(σ). It is a routine exercise to establish that for all τ ∈ prf(σ) and α ∈ ĈL(α_{0}), M_{0}, τ ⊧ α iff α ∈ A_{|τ|}. Hence M_{0}, ε ⊧ α_{0} as required.

The system DLT L is obtained by replacing (A10) and (A11) with the following axiom schemes:

\begin{matrix}(A12) & α U^{π}β ⊃ ⟨π⟩β. \\ (A13) & α U^{π}β ≡ β ∨ (α ∧ ⋁_{a∈Σ}⟨a⟩ ⋁_{π′∈δ_{a}(π)} α U^{π′}β) , (ε ∈ ||π||). \\ (A14) & α U^{π}β ≡ α ∧ ⋁_{a∈Σ}⟨a⟩ ⋁_{π′∈δ_{a}(π)} α U^{π′}β, (ε ∉ ||π||). \end{matrix}

It is an easy exercise to extend the completeness argument for DLT L^{−} to DLT L. Thus we have:

Theorem 6.4

(i) DLT L^{−} is a sound and complete axiomatization of the set of valid formulas of DLTL^{−}(Σ).

(ii) DLT L is a sound and complete axiomatization of the set of valid formulas of DLTL(Σ).

7 Conclusion

We have presented here an enriched version of LTL called DLTL. The extension is obtained by indexing the until operator of LTL with regular programs. We have shown that in terms of the complexity of the decision procedure and expressiveness, DLTL compares very favourably with ETL. It is worth pointing out here that the decision procedure for DLTL is carried out directly in terms of Büchi automata whereas for ETL it is carried out in terms of the so called set-subword automata, which are then translated to Büchi automata [21]. Two additional results that are available for DLTL are: A characterization of the first order fragment of S1S in terms of the sublogics DLTL_{𝕊𝔽}^{−} and DLTL_{𝕊𝔽}; and a relatively clean axiomatization of DLTL^{−} and DLTL. All these results demonstrate that our means of bringing together propositional dynamic and temporal logics in a linear time setting is natural.

It turns out that our idea extends smoothly to richer domains. In particular, we can obtain similar results concerning the so called ω-regular product languages [19] in terms of the product version of DLTL. Roughly speaking, a ω-regular product language is a ω-regular language L ⊆ Σ^{ω} generated by a distributed alphabet {Σ_{i}}_{i=1}^{K} with Σ = ⋃_{i=1}^{K} Σ_{i}. The language L is a product language in the sense it is a finite union languages of the form L_{1} ⊗ L_{2} ⊗ ⋯ ⊗ L_{K} with each L_{i} a regular subset of finite and infinite strings over Σ_{i} and ⊗ standing for the synchronized product operation. In other words σ ∈ Σ^{ω} is in L_{1} ⊗L_{2} ⊗⋯⊗L_{K} iff σ ↾ Σ_{i} (i.e. the sequence obtained by erasing all symbols from σ that are not in Σ_{i}) is in L_{i} for each i. The interesting distributed alphabets are of course those in which the component alphabets are not pairwise disjoint. The ω-regular product languages can be used to capture the linear time behaviour of a widely used model of distributed programs. These programs consist of a fixed set of finite state sequential programs that coordinate their behaviours by performing common actions together. Our logical characterization of ω-regular product languages is obtained by taking boolean combinations of formulas in ⋃_{i=1}^{K} DLTL(Σ_{i}).

Yet another extension is obtained by considering ω-regular trace languages over a trace alphabet (Σ, I) with I ⊆ Σ × Σ being an irreflexive and symmetric independence relation. Here by traces we mean the class of Σ-labelled posets known as Mazurkiewicz traces. These objects play a fundamental role in the theory of distributed systems [2, 11]. It turns out that ω-regular trace languages can be captured by a natural extension of DLTL(Σ) denoted DLTL(Σ, I). The main idea is that one must use regular “parallel” programs instead of regular programs to index the until operator. What is interesting about this characterization is that so far there has been no comparable result concerning ω-regular trace languages in terms of a modal logic with a fixed point operator or in terms of a linear time temporal logic. These results and related generalizations will be reported in a forthcoming paper.

References

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

[2] V. Diekert and G. Rozenberg, eds., The Book of Traces (World Scientific Singapore, 1995).

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

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

[5] D. Harel, Dynamic logic, in D. Gabbay and F. Guenthner, eds., “Handbook of Philosophical Logic - Vol. II” (Reidel Dordrecht, 1984) 497–604.

[6] D. Harel, D. Kozen, and R. Parikh, Process logic: expressiveness, decidability, completeness, Journal of Computer and System Sciences 25 (1982) 144–170.

[7] J. Hromkovič, S. Seibert, and T. Wilke, Translating regular expressions into small ε-free nondeterministic automata, Proceedings of the 12th Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 1200 (Springer-Verlag, 1997) 55–66.

[8] H. R. Kamp, Tense Logic and the Theory of Linear Order, Ph.D. thesis, University of California (1968)

[9] D. Kozen and R. Parikh, An elementary proof of the completeness of PDL, Theoretical Computer Science 14 (1981) 113–118.

[10] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems (Specification) (Springer-Verlag, 1992).

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

[12] R. McNaughton, Testing and generating infinite sequences by a finite automaton, Information and Control 9 (1966) 521–530.

[13] R. McNaughton and S. Papert, Counter-Free Automata (MIT Press, 1971).

[14] H. Nishimura, Descriptively complete process logic, Acta Informatica 14(4) (1980) 359–369.

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

[16] V. R. Pratt, Process logic, Proceedings of the 6th Symposium on Principles of Programming Languages (ACM, 1979) 93–100.

[17] K. Segerberg, A completeness theorem in the modal logic of programs, Notices AMS 24(6) (1977) A–522.

[18] A. P. Sistla, Theoretical issues in the design and verification of distributed systems, Ph.D. Thesis, Harvard University (1983).

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

[20] W. Thomas, Automata over infinite objects, in: J. van Leeuwen, ed., Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics (Elsevier/MIT Press, 1990) 133–191.

[21] M. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation 115(1) (1994) 1–35.

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

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

Recent BRICS Report Series Publications

RS-97-8 Jesper G. Henriksen and P. S. Thiagarajan. Dynamic Linear Time Temporal Logic. April 1997. 33 pp.

RS-97-7 John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus (Extended Version). March 1997. 55 pp. Extended version of article to appear in the Journal of Functional Programming.

RS-97-6 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. March 1997. 53 pp. Extended version of an article to appear in the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’97), Amsterdam, The Netherlands, June 1997.

RS-97-5 Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. March 1997. 18 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-4 Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for Labelled Markov Processes. March 1997. 48 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-3 Carsten Butz and Ieke Moerdijk. A Definability Theorem for First Order Logic. March 1997. 10 pp.

RS-97-2 David A. Schmidt. Abstract Interpretation in the Operational Semantics Hierarchy. March 1997. 33 pp.

RS-97-1 Olivier Danvy and Mayer Goldberg. Partial Evaluation of the Euclidian Algorithm (Extended Version). January 1997. 16 pp. To appear in the journal Lisp and Symbolic Computation.

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

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