BRICS RS-97-9 Henriksen & Thiagarajan: A Product Version of Dynamic Linear Time Temporal Logic BRICS

Basic Research in Computer Science

A Product Version of Dynamic Linear Time Temporal Logic

Jesper G. Henriksen P. S. Thiagarajan BRICS Report Series RS-97-9 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/9/

A Product Version of 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

We present here a linear time temporal logic which simultaneously extends LTL, the propositional temporal logic of linear time, along two dimensions. Firstly, the until operator is strengthened by indexing it with the regular programs of propositional dynamic logic (PDL). Secondly, the core formulas of the logic are decorated with names of sequential agents drawn from fixed finite set. The resulting logic has a natural semantics in terms of the runs of a distributed program consisting of a finite set of sequential programs that communicate by performing common actions together. We show that our logic, denoted DLTL^{⊗}, admits an exponential time decision procedure. We also show that DLTL^{⊗} is expressively equivalent to the so called regular product languages.

∗ Appears in the proceedings of the eighth International Conference on Concurrency Theory (CONCUR’97), Warsaw, Poland.

† 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.

Roughly speaking, this class of languages is obtained by starting with synchronized products of (ω-)regular languages and closing under boolean operations. We also sketch how the behaviours captured by our temporal logic fit into the framework of labelled partial orders known as Mazurkiewicz traces.

1 Introduction

We present a linear time temporal logic which extends LTL, the propositional temporal logic of linear time [8, 13] along two dimensions. Firstly, we strengthen the until modality by indexing it with the regular programs of PDL, propositional dynamic logic [1, 4]. Secondly, we consider networks of sequential agents that communicate by performing common actions together. We then reflect this in the logic by decorating the “core” formulas with the names of the agents. The resulting logic, denoted DLTL^{⊗}, is a smooth generalization of the logic called product LTL [16] and the logic called dynamic linear time temporal logic [5].

DLTL^{⊗} admits a pleasant theory and our technical goal here is to sketch the main results of this theory. We believe that these results provide additional evidence — in a non-sequential setting — suggesting that our technique of combining dynamic and temporal logic as initiated in [5] is a fruitful one.

In the next section we introduce dynamic linear time temporal logic. We then state two main results concerning this logic. In Section 3 we define regular product languages. These are basically boolean combinations of synchronized products of (ω-)regular languages. We then present a characterization of this class of languages in terms of networks of Büchi automata that coordinate their activities by synchronizing on common letters.

In Section 4 we formulate the temporal logic DLTL^{⊗}, the main object of study in this paper. In Section 5 we establish an exponential time decision procedure for this logic by exploiting the Büchi automata networks presented in Section 3. In the subsequent section we show that DLTL^{⊗} captures exactly the class of regular product languages. It is worth noting that this is the first temporal logical characterization of this important class of distributed behaviours. In the final section we sketch how the behaviours described by our temporal logic (i.e. regular product languages) lie naturally within the domain of regular Mazurkiewicz trace languages.

2 Dynamic Linear Time Temporal Logic

One key feature of the syntax and semantics of our temporal logic is that actions will be treated as first class objects. The usual presentation of LTL [8, 13] is based on states; they are represented as subsets of a finite set of atomic propositions. We wish to bring in actions explicitly because it is awkward, if not difficult, to define synchronized products of sequential components in a purely state-based setting. This method of forming distributed systems is a common and useful one. Moreover, it is the main focus of attention in this paper. Hence it will be 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 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 prf(σ) is the set of finite prefixes of σ.

The set of formulas of LTL(Σ) is then given by the syntax:

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

For convenience we have avoided introducing atomic propositions and instead just deal with the constant ⊤ and its negation ∼ ⊤ ⟺^{Δ} ⊥. 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. A model is a ω-sequence σ ∈ Σ^{ω}. For τ ∈ prf(σ) we define σ, τ ⊧ α via:

• σ, τ ⊧ ⊤.

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

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

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

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

It is well known that LTL(Σ) is equal in expressive power to the first order theory of sequences [2, 7]. Consequently this temporal logic is quite limited in in terms of what it can not say. As an example, let Σ = {a, b}. Then the property “at every even position the action b is executed” is not definable in LTL(Σ). This observation, made in a state-based setting by Wolper, is the starting point for the extension of LTL called ETL [20, 21]. The route that we have taken to augment the expressive power of LTL(Σ) is similar in spirit but quite different in terms of the structuring mechanisms made available for constructing compound formulas. A more detailed assessment of the similarities and the differences between the two approaches is given in [5].

The extension that we have proposed is called DLTL(Σ). It basically consists of indexing the until operator with the programs of PDL (e.g. [1]). We start by defining the set of regular programs (expressions) generated by Σ. This set is denoted by Prg(Σ) and its syntax is given by:

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

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 ∈ ω.

The set of formulas of DLTL(Σ) is given by the following syntax.

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

A model is a ω-sequence σ ∈ Σ^{ω}. For τ ∈ prf(σ) we define σ, τ ⊧ α just as we did for LTL(Σ) in the case of the first three clauses. As for the last one,

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

Thus DLTL(Σ) adds to LTL(Σ) by strengthening the until operator. To satisfy α U^{π}β, one must satisfy α Uβ along some finite stretch of behaviour which is required to be in the (linear time) behaviour of the program π. We now wish to state two of the main results of [5]. To do so, we first say that a formula α ∈ DLTL(Σ) is satisfiable if there exist σ ∈ Σ^{ω} and τ ∈ prf(σ) such that σ, τ ⊧ α. Secondly, we associate with a formula α the ω-language L_{α} via:

L_{α} =^{def} {σ ∈ Σ^{ω} | σ, ε ⊧ α}.

A language L ⊆ Σ^{ω} is said to be DLTL(Σ)-definable if there exists some α ∈ DLTL(Σ) such that L = L_{α}. Finally, we assume the notions of Büchi and Muller automata and ω-regular languages as formulated in [17].

Theorem 2.1

(i) Given an α_{0} ∈ DLTL(Σ) one can effectively construct a Büchi automaton B_{α_{0}} of size 2^{O(|α_{0}|)} such that L(B_{α_{0}}) ≠ ∅ iff α_{0} is satisfiable. Thus the satisfiability problem for DLTL(Σ) is decidable in exponential time.

(ii) L ⊆ Σ^{ω} is ω-regular iff L is DLTL(Σ)-definable.

It is also easy to formulate and solve a natural model checking problem for DLTL(Σ) where finite state programs are modelled as Büchi automata. But we shall not enter into details here.

To close out the section we shall point to two useful derived operators of DLTL(Σ):

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

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

Suppose σ ∈ Σ^{ω} 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 τ′ ∈ ||π||, ττ′ ∈ prf(σ) implies σ, ττ′ ⊧ α. In this sense, the program modalities of PDL acquire a linear time semantics in the present setting. As shown in [5] the second part of Theorem 2.1 goes through even for the the sublogic of DLTL(Σ) obtained by banishing the until operator and instead using ⟨π⟩α and the boolean connectives. For an example of what can be said in this sublogic, assume Σ = {a, b} and define π_{ev} to be the program ((a + b); (a + b))^{∗}.

Then the formula [π_{ev}]⟨b⟩⊤ says ”at every even position the action b is executed”.

Next we note that a ∈ Σ is a member of Prg(Σ) and the until operator of LTL(Σ) can be obtained via: α Uβ ⟺^{Δ} α U^{Σ^{∗}}β. Due to second part of Theorem 2.1 we now have that both syntactically and semantically, LTL(Σ) is a proper fragment of DLTL(Σ).

To conclude the section, we note that the material presented here can be easily extended to include finite sequences over Σ as well. We shall assume from now on that this extension has indeed been carried out.

3 Regular Product Languages

A restricted but very useful model of finite state concurrent programs consists of a fixed number of finite state sequential programs that coordinate their activities by performing common actions together. A regular product language is an abstract specification of the linear time behaviour of such concurrent programs. The idea is to start with synchronized products of regular languages and close under boolean operations. Formally, we start with a distributed alphabet Σ̃ = {Σ_{i}}_{i=1}^{K}, a family of alphabets with each Σ_{i} a non-empty finite set of actions. One key point is that the component alphabets are not necessarily disjoint. Intuitively, Loc = {1, …, K} is the set of names of communicating sequential processes synchronizing on common actions, where Σ_{i} is the set of actions which require the participation of the agent i. Through the rest of the paper we fix a distributed alphabet Σ̃ = {Σ_{i}}_{i=1}^{K} and set Σ = ⋃_{i=1}^{K} Σ_{i}. We carry over the terminology developed in the previous section for dealing with finite and infinite sequences over Σ. In addition, for σ ∈ Σ^{∞} and i ∈ Loc we denote by σ ↾ i the projection of σ down to Σ_{i}. In other words, it is the sequence obtained by erasing from σ all occurrences of symbols that are not in Σ_{i}. We let i, j, k range over Loc = {1, …, K} and define Loc(a) = {i | a ∈ Σ_{i}}. We note that Loc(a) is the set of processes that participate in each occurrence of the action a.

Next we define the K-ary operator ⊗ : 2^{Σ_{1}^{∞}} × … × 2^{Σ_{K}^{∞}} → 2^{Σ^{∞}} by

⊗(L_{1}, …, L_{K}) = {σ ∈ Σ^{∞} | σ ↾ i ∈ L_{i} for each i ∈ Loc}.

Usually we will write ⊗(L_{1}, …, L_{K}) as L_{1} ⊗ L_{2} ⊗ … ⊗ L_{K}. Finally, we will say that the language L ⊆ Σ^{∞} is regular iff L∩Σ^{∗} is a regular subset of Σ^{∗} and L∩Σ^{ω} is an ω-regular subset of Σ^{ω}. Regular product languages can be built up as follows.

Definition 3.1 L ⊆ Σ^{∞} is a direct regular product language over Σ̃ iff L = L_{1} ⊗ … ⊗ L_{K} with L_{i} a regular subset of Σ_{i}^{∞} for each i ∈ Loc.

We let R_{0}^{⊗}(Σ̃) be the class of direct regular product languages over Σ̃.

Definition 3.2 The class of regular product languages over Σ̃ is denoted R^{⊗}(Σ̃) and is the least class of languages containing R_{0}^{⊗}(Σ̃) and satisfying:

• If L_{1}, L_{2} ∈ R^{⊗}(Σ̃) then L_{1} ∪ L_{2} ∈ R^{⊗}(Σ̃).

In what follows we will often suppress the mention of the distributed alphabet Σ̃. It is easy to prove that R^{⊗} is closed under boolean operations. The proof of this result as well as other results mentioned in this section can be found in [15]. Just as ω-regular languages are captured by Büchi automata, we can capture regular product languages with the help of networks of Büchi automata. For convenience such automata will be termed product automata.

Definition 3.3 A product automaton over Σ̃ is a structure

A = ({A_{i}}_{i∈Loc}, Q_{in}),

where each A_{i} = (Q_{i}, ⟶_{i}, F_{i}, F_{i}^{ω}) satisfies:

• Q_{i} is a non-empty finite set of i-local states.

• ⟶_{i} ⊆ Q_{i} ×Σ_{i} ×Q_{i} is the transition relation of the ith component.

• F_{i} ⊆ Q_{i} is a set of finitary accepting states of the ith component.

• F_{i}^{ω} ⊆ Q_{i} is a set of infinitary accepting states of the ith component.

Moreover, Q_{in} ⊆ Q_{1} × … × Q_{K} is a set of global initial states.

Thus, a product automaton is a network of local automata with a global set of initial states. It is necessary to have global initial states in order to obtain the required expressive power. Each local automaton is equipped to cope with both finite and infinite behaviours using the finitary and infinitary accepting states. The infinitary accepting states are to be interpreted as defining a Büchi acceptance condition. This will become clear once we define the language accepted by a product automaton. We choose to deal with both finite and infinite component behaviours because the global behaviour can always induce finite local behaviours. In other words, even if ω-behaviour is the main focus of interest, a global infinite run will consist of one or more components running forever but with some other components, in general, quitting after making a finite number of moves. The notational complications involved in artificially making all components to run forever do not seem to be worth the trouble.

Let A be a product automaton over Σ̃. Then Q_{G}^{A} = Q_{1} × … × Q_{K} is the set of global states of A. The i-local transition relations induce a global transition relation ⟶_{A} ⊆ Q_{G}^{A} × Σ × Q_{G}^{A} as follows:

q ⟶_{A}^{a} q′ iff q[i] ⟶_{i}^{a} q′[i] for each i ∈ Loc(a) and
q[i] = q′[i] for each i ∉ Loc(a),

where q[i] denotes the ith component of q = (q_{1}, …, q_{K}). A run of A over σ ∈ Σ^{∞} is a mapping ρ : prf(σ) → Q_{G}^{A} satisfying that ρ(ε) ∈ Q_{in} and ρ(τ) ⟶_{A}^{a} ρ(τa) for all τa ∈ prf(σ). The run is accepting iff the following conditions are satisfied for each i:

• If σ ↾ i is finite then ρ(τ)[i] ∈ F_{i} for some τ ∈ prf(σ) with τ ↾ i = σ ↾ i.

• If σ ↾ i is infinite then ρ(τ)[i] ∈ F_{i}^{ω} for infinitely many τ ∈ prf(σ).

We next define

L(A) = {σ ∈ Σ^{∞} | there exists an accepting run of A over σ}.

The next result established relates regular product languages to product automata.

Theorem 3.4 L ∈ R^{⊗}(Σ̃) iff L = L(A) for some product automaton A over Σ̃.

We will later give solutions to the satisfiability problem for a product version of DLTL with the help of product automata. The following results will be useful in this context. In stating these results we take the size of the product automaton A to be |Q_{G}^{A}|.

Lemma 3.5 • Let A be a product automaton. The question L(A) ≠^{?} ∅ can be

effectively decided in time O(n^{2}), where n is the size of A.

• Let A_{1} and A_{2} be product automata of sizes n_{1} and n_{2}, respectively. Then a product automaton A of size O(n_{1}n_{2}) with L(A) = L(A_{1})∩ L(A_{2}) can be effectively constructed.

4 A Product Version of DLTL

We now wish to design a product version of DLTL denoted DLTL^{⊗}(Σ̃). It will turn out to have the expressive power of regular product languages over Σ̃. The set of formulas and their locations are given by:

• ⊤ is a formula and loc(⊤) = ∅.

• Suppose α and β are formulas. Then so are ∼ α and α ∨ β. Furthermore, loc(∼α) = loc(α) and loc(α ∨ β) = loc(α) ∪ loc(β).

• Suppose α and β are formulas such that loc(α), loc(β) ⊆ {i} and suppose π ∈ Prg(Σ_{i}). Then α U_{i}^{π}β is a formula. Moreover, loc(α U_{i}^{π}β) = {i}.

We note that each formula in DLTL^{⊗}(Σ̃) is a boolean combination of formulas taken from the set ⋃_{i∈Loc} DLTL_{i}^{⊗}(Σ̃) where, for each i,

DLTL_{i}^{⊗}(Σ̃) = {α | α ∈ DLTL^{⊗}(Σ̃) and loc(α) ⊆ {i} }.

Once again, we have chosen to avoid dealing with atomic propositions for the sake of convenience. They can be introduced in a local fashion as done in [15]. The decidability result to be presented will go through with minor notational overheads.

As before, we will often suppress the mention of Σ̃. We will also often write τ_{i}, τ′_{i} and τ′′_{i} instead of τ ↾ i , τ′ ↾ i and τ′′ ↾ i, respectively with τ, τ′, τ′′ ∈ Σ^{∗}.

A model is a sequence σ ∈ Σ^{∞} and the semantics of this logic is given as before, with τ ∈ prf(σ).

• σ, τ ⊧ ⊤.

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

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

• σ, τ ⊧ α U_{i}^{π}β iff there exists τ′ such that τ′_{i} ∈ ||π|| (recall that τ′_{i} = τ′ ↾ i) and ττ′ ∈ prf(σ) and σ, ττ′ ⊧ β. Further, for every τ′′ ∈ prf(τ′), if ε ⪯ τ′′_{i} ≺ τ′_{i} then σ, ττ′′ ⊧ α.

We will say that a formula α ∈ DLTL^{⊗}(Σ̃) is satisfiable if there exist σ ∈ Σ^{∞} and τ ∈ prf(σ) such that σ, τ ⊧ α. The language defined by α is given by

L_{α} =^{def} {σ ∈ Σ^{∞} | σ, ε ⊧ α}.

We say that L ⊆ Σ^{∞} is DLTL^{⊗}(Σ̃)-definable if there exists some α ∈ DLTL^{⊗}(Σ̃) with L_{α} = L.

5 A Decision Procedure for DLTL^{⊗}

We will show the satisfiability problem for DLTL(Σ) is solvable in deterministic exponential time. This will be achieved by effectively constructing a product automaton A_{α} for each α ∈ DLTL^{⊗}(Σ̃) such that the language accepted by A_{α} is non-empty iff α is satisfiable. Our construction is a common generalization of the one for product LTL in [16] and the one for DLTL(Σ) in [5]. The solution to the satisfiability problem will at once lead to a solution to the model checking problem for programs modelled as synchronizing sequential agents.

Through the rest of the section we fix a formula α_{0} ∈ DLTL^{⊗}. In order to construct A_{α_{0}} we first define the (Fischer-Ladner) closure of α_{0}. As a first step let cl(α_{0}) be the least set of formulas satisfying:

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

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

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

• α U_{i}^{π}β ∈ cl(α_{0}) implies α, β ∈ cl(α_{0}).

We will now take the closure of α_{0} to be CL(α_{0}) = cl(α_{0}) ∪ {∼ α | α ∈ cl(α_{0})}. From now on we shall identify ∼∼ α with α. Set CL_{i}(α_{0}) = CL(α_{0})∩DLTL_{i}^{⊗}(Σ̃) for each i. We will often write CL instead of CL(α_{0}) and CL_{i} instead of CL_{i}(α_{0}). All formulas considered from now on will be assumed to belong to CL_{i} unless otherwise stated.

An i-type atom is a subset A ⊆ CL_{i} which satisfies:

• ⊤ ∈ A.

• α ∈ A iff ∼α ∉ A.

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

• β ∈ A and ε ∈ ||π|| implies α U_{i}^{π}β ∈ A.

The set of i-type atoms is denoted AT_{i}. We next define the predicate Member(α, (A_{1}, …, A_{K})) for each α ∈ CL(α_{0}) and (A_{1}, …, A_{K}) ∈ AT_{1} × … × AT_{K}. For convenience this predicate will be denoted as α ∈ (A_{1}, …, A_{K}) and is given inductively by:

• Let α ∈ CL_{i}. Then α ∈ (A_{1}, …, A_{K}) iff α ∈ A_{i}.

• Let α = ∼β. Then α ∈ (A_{1}, …, A_{K}) iff β ∉ (A_{1}, …, A_{K}).

• Let α = β ∨ γ. Then α ∈ (A_{1}, …, A_{K}) iff β ∈ (A_{1}, …, A_{K}) or γ ∈ (A_{1}, …, A_{K}).

The set of i-type until requirements is the subset of CL_{i} given by

Req_{i} = {α U_{i}^{π}β | α U_{i}^{π}β ∈ CL_{i}}.

We shall let ξ, ξ′ range over Req_{i}. For each ξ = α U_{i}^{π}β ∈ Req_{i} 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_{i}. We set Q_{i} = ⋃_{ξ∈Req_{i}} Q_{ξ} and Q̂_{i} = Q_{i} × {0, 1}.

The product automaton A_{α_{0}} associated with α_{0} is now defined to be A_{α_{0}} = ({A_{i}}_{i∈Loc}, Q_{in}) where for each i, A_{i} = (S_{i}, ⟹_{i}, F_{i}, F_{i}^{ω}) is specified as

1. S_{i} ⊆ AT_{i} × 2^{Q_{i}} × 2Q̂_{i} × {stop, go} × {0, 1} × { ↓, ✓} such that

(A, X, X̂, s, x, f) ∈ S_{i}

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

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

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

(iii) If α U_{i}^{π}β ∈ A then either β ∈ A and ε ∈ ||π|| or (q, 1 − x) ∈ X̂ for some q ∈ I_{ξ}. (Note that we are considering the candidate (A, X, X̂, s, x, f) for membership in S_{i}). (iv) If (q, z) ∈ X̂ with q ∉ F_{ξ} or β ∉ A then α ∈ A.

2. The transition relation ⟹_{i} ⊆ S_{i} × Σ_{i} × S_{i} is defined as follows:

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

iff the following conditions are satisfied for each ξ = α U_{i}^{π}β ∈ Req_{i}:

(i) s = go.

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

(iv) 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. F_{i} = {(A, X, X̂, s, x, f) | s = stop and X̂ = ∅}.

4. F_{i}^{ω} = {(A, X, X̂, s, x, f) | f = ✓}. Finally, Q_{in} ⊆ Q_{1} × … × Q_{K} is specified as

((A_{1}, X_{1}, X̂_{1}, s_{1}, x_{1}, f_{1}), …, (A_{K}, X_{K}, X̂_{K}, s_{K}, x_{K}, f_{K})) ∈ Q_{in} iff α_{0} ∈ (A_{1}, …, A_{K}) and (x_{i}, f_{i}) = (0, ✓) for every i ∈ Loc.

The main result of this section can now be formulated. Theorem 5.1 L(A_{α_{0}}) = L_{α_{0}} where A_{α_{0}} is as defined above. Hence α_{0} is satisfiable iff L(A_{α_{0}}) ≠ ∅. Moreover, the size of A_{α_{0}} is 2^{O(|α_{0}|)} and consequently the satisfiability problem for DLTL^{⊗}(Σ̃) is decidable in exponential time. Proof: Let σ ∈ L(A_{α_{0}}) by the accepting run ρ : prf(σ) → Q_{G}^{A}. For each τ ∈ prf(σ) let ρ(τ)[i] = (A_{τ_{i}}, X_{τ_{i}}, X̂_{τ_{i}}, s_{τ_{i}}, x_{τ_{i}}, f_{τ_{i}}). Then a detailed examination of the above construction reveals that for all τ ∈ prf(σ) and δ ∈ CL_{i},

σ, τ ⊧ δ iff δ ∈ A_{τ_{i}}.

By definition of Q_{in} we are assured that α_{0} ∈ (ρ(ε)[1], …, ρ(ε)[K]). Hence a simple induction on the structure of α_{0} will show that σ, ε ⊧ α_{0}.

Conversely, if α_{0} is satisfiable we may assume that σ, ε ⊧ α_{0} for some σ. We will construct an accepting run ρ : prf(σ) → Q_{G}^{A}. For each τ ∈ prf(σ) and each i, we set ρ(τ)[i] = (A_{τ_{i}}, X_{τ_{i}}, X̂_{τ_{i}}, s_{τ_{i}}, x_{τ_{i}}, f_{τ_{i}}) and define the various components of this tuple as follows. First we define A_{τ_{i}} by A_{τ_{i}} = {α ∈ CL_{i} | σ, τ ⊧ α}. Next s_{τ_{i}} is defined as s_{τ_{i}} = stop iff σ ↾ i = τ_{i} (recall the convention τ ↾ i = τ_{i}). In defining the other components it will be convenient to adopt the following terminology.

Let ξ = α U_{i}^{π}β and q ∈ Q_{ξ} and τ_{i} ∈ Σ_{i}^{∗}. Then an accepting run of A_{ξ} over τ_{i} starting from q is a map R : prf(τ_{i}) ⟶ Q_{ξ} such that R(ε) = q,

R(τ_{i}) ∈ F_{ξ} and R(τ′′_{i}) ⟶^{a}_{ξ} R(τ′′_{i}a) for every τ′′_{i}a ∈ prf(τ_{i}). In case q ∈ I_{ξ}

we shall just say that R is an accepting run of A_{ξ} over τ_{i}.

Let ξ = α U_{i}^{π}β and q ∈ Q_{ξ}. Then q ∈ X_{τ_{i}} iff there exist τ′ and R′ such that ττ′ ∈ prf(σ), σ, ττ′ ⊧ β, and for every τ′′ ∈ prf(τ′), if ε ⪯ τ′′_{i} ≺ τ′_{i} then σ, ττ′′ ⊧ α. Furthermore, R′ should be an accepting run of A_{ξ} over τ′_{i} starting from q.

To specify the remaining three components we shall make use of a chronicle of obligations.

We’ll say that (τ, ξ) is an obligation if τ ∈ prf(σ) and ξ = α U_{i}^{π}β ∈ Req_{i} such that σ, τ ⊧ α U_{i}^{π}β but σ, τ |̸= β or ε ∉ ||π||. Let (τ, ξ) be an obligation. We shall say that the pair (τ′, R′) is a witness for (τ, ξ) iff ττ′ ∈ prf(σ) and σ, ττ′ ⊧ β and for every τ′′ ∈ prf(τ′), if ε ⪯ τ′′_{i} ≺ τ′_{i} then σ, ττ′′ ⊧ α. Furthermore, τ′_{i} ∈ ||π|| and R′ is an accepting run of A_{ξ} over τ′_{i}. A chronicle set CH is a set of quadruples satisfying that if (τ, ξ, τ′, R′) ∈ CH then (τ, ξ) is an obligation and (τ′, R′) is witness for (τ, ξ). Moreover, for every obligation (τ, ξ) there is a unique element of the form (τ, ξ, τ′, R′) in CH. We fix such a set CH which clearly exists.

Now x_{τ_{i}} and f_{τ_{i}} are defined by mutual induction as follows. For the base case, (x_{ε}, f_{ε}) = (0, ✓). For the induction step, let τ = τ′a. Suppose a ∉ Σ_{i}. Then (x_{τ_{i}}, f_{τ_{i}}) = (x_{τ′_{i}}, f_{τ′_{i}}). So assume that a ∈ Σ_{i}. If f_{τ′_{i}} = ✓ then (x_{τ_{i}}, f_{τ_{i}}) = (1 − x_{τ′_{i}}, ↓). Suppose f_{τ′_{i}} = ↓. Then (x_{τ_{i}}, f_{τ_{i}}) = (x_{τ′_{i}}, ↓) if there exists (τ′′, ξ_{1}, τ′′′, R′_{1}) ∈ CH such that τ′′ ⪯ τ′ ≺ τ′′τ′′′ and x_{τ′′_{i}} = 1 − x_{τ′_{i}}. Otherwise, f_{τ_{i}} = ✓ and x_{τ_{i}} = x_{τ′_{i}}.

The only remaining component to be dealt with is X̂_{τ_{i}}. This is now defined via: (q, z) ∈ X̂_{τ_{i}} iff there exists (τ′, ξ, τ′′, R′_{1}) ∈ CH such that for some τ′′′ ∈ prf(τ′′), τ′_{i} ⪯ τ_{i} = τ′_{i}τ′′′_{i} and furthermore R′_{1}(τ′′′_{i}) = q and x_{τ′_{i}} = 1 − z. Using these definitions it is not difficult to show that ρ is an accepting run.

Finally, by Lemma 3.5 it suffices to show that our construction yields a product automaton of exponential size. Clearly, CL(α_{0}) is linear in α_{0}, and surely then |AT_{1}| + … + |AT_{K}| = 2^{O(|α_{0}|)}. Moreover, it is wellknown that each π ∈ Prg(Σ_{i}) in polynomial time can be converted to a finite (non-deterministic) automaton with a linear state space (see [6] for a recent account of such conversions). Then both Q_{1} + … + Q_{K} and Q̂_{1} + … + Q̂_{K} are of size O(|α_{0}|). Consequently, |Q_{G}^{A}| = 2^{O(|α_{0}|)} as required. □

The procedure outlined above also lends itself to a solution to the model checking problem, which is defined as for DLTL except that a finite-state program is now simply a product automaton P. Once again, we do not wish to enter into details.

6 An Expressiveness Result

We now wish to show that our logic is expressively complete with respect to the regular product languages. In fact we will identify a natural sublogic — to be denoted DLTL_{−}^{⊗} — which also enjoys this property.

The syntax of the formulas of DLTL_{−}^{⊗}(Σ̃) remains as for DLTL^{⊗}(Σ̃), but the until modality is to be restricted to the derived operator ⟨ ⟩_{i}. Formally, the set of formulas and locations of this sublogic is obtained via:

• ⊤ is a formula and loc(⊤) = ∅.

• Suppose α and β are formulas so are ∼ α and α ∨ β. Moreover loc(∼α) = loc(α) and loc(α ∨ β) = loc(α) ∪ loc(β).

• Suppose α is formula such that loc(α) ⊆ {i} and π ∈ Prg(Σ_{i}). Then ⟨π⟩_{i}α is formula. Moreover, loc(⟨π⟩_{i}α) = {i}.

Proposition 6.1 If L ∈ R^{⊗}(Σ̃) then L is DLTL_{−}^{⊗}(Σ̃)-definable.

Proof: It suffices to show that the claim holds for L ∈ R_{0}^{⊗}(Σ̃) because each member of R^{⊗}(Σ̃) is a finite union of languages in R_{0}^{⊗}(Σ̃).

Let L = L_{1}⊗…⊗L_{K} ∈ R_{0}^{⊗}(Σ̃). Then each L_{i}∩Σ_{i}^{∗} is regular. Clearly L_{i} ∩Σ_{i}^{∗} = ||π_{i}|| for some π_{i} ∈ Prg(Σ_{i}). Now define α_{∗}^{i} = ⟨π_{i}⟩_{i}[π′_{i}]_{i}⊥ where π′_{i} = (a_{1} + … + a_{n}) with Σ_{i} = {a_{1}, …, a_{n}}.

Next, L_{i}∩Σ_{i}^{ω} is ω-regular. Hence it is accepted, due to McNaughton’s theorem [10], by a deterministic Muller automaton. Choose such an automaton M = (Q, q_{in}, ⟶, F), which we, without loss of generality, assume to be complete. (See [5] for the formal details). For q, q′ ∈ Q we set L_{q,q′} = {τ | q ⟶^{τ} q′}, which is obviously a regular subset of Σ_{i}^{∗}. So we can fix π_{q,q′} ∈ Prg(Σ_{i}) such that L_{q,q′} = ||π_{q,q′}||. Moreover, by the determinacy of M it follows that L_{q,q′} ∩ L_{q,q′′} ≠ ∅ implies q′ = q′′. We now define

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

with the assumption {q_{0}, q_{1}, …, q_{n−1}} is an enumeration of the F ∈ F under consideration and “⊕” denotes addition modulo n. It is easy to show that σ ↾ i ∈ L_{i} ∩ Σ_{i}^{ω} iff σ, ε ⊧ α_{ω}^{i}.

The required formula α is given by α = ⋀_{i∈Loc} α^{i} where α^{i} = α_{∗}^{i} ∨ α_{ω}^{i} for each i. It is a routine exercise to establish L_{α} = L_{1} ⊗ … ⊗ L_{K}.

□

On the other hand, Theorem 3.4 together with Theorem 5.1 states that L_{α_{0}} is a product language over Σ̃ for any α_{0} ∈ DLTL^{⊗}(Σ̃). Since DLTL_{−}^{⊗} is a sublogic of DLTL^{⊗} we have the following expressiveness result.

Corollary 6.2 Let L ⊆ Σ^{∞}. Then the following statements are equivalent:

(i) L ∈ R^{⊗}(Σ̃).

(ii) L is DLTL_{−}^{⊗}(Σ̃)-definable.

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

7 Discussion

We shall conclude this section by placing regular product languages in the broader context of regular Mazurkiewicz trace languages. For an introduction to (Mazurkiewicz) traces related to the concerns of the present paper, we refer the reader to [11]. We shall assume the bare minimum of the background material on traces.

We begin by noting that the distributed alphabet Σ̃ = {Σ_{i}}_{i=1}^{K} induces the trace alphabet (Σ, IΣ̃) where the irreflexive and symmetric independence relation IΣ̃ ⊆ Σ × Σ is given by:

a IΣ̃ b iff Loc(a) ∩ Loc(b) = ∅.

Recall that Loc(x) = {i | x ∈ Σ_{i}} for x ∈ Σ. We shall write I instead of IΣ̃ from now on. This independence relation in turn induces the equivalence relation ≈_{I} ⊆ Σ^{∞} × Σ^{∞} (from now on written as ≈) given by:

σ ≈ σ′ iff σ ↾ i = σ′ ↾ i for every i ∈ Loc.

The ≈-equivalence classes of Σ^{∞} constitute the set of finite and infinite traces generated by the trace alphabet (Σ, I). Traces can be — upto isomorphisms — uniquely represented as certain Σ-labelled posets where the labelling functions respect I in a natural manner. A trace language is just a subset of Σ^{∞}/ ≈.

A language L ⊆ Σ^{∞} is trace consistent in case σ ∈ L and σ ≈ σ′ implies σ′ ∈ L, for every σ, σ′. The point is, a trace consistent language L canonically represents the trace language {[σ]_{≈} | σ ∈ L}. We extend this idea to logical formulas by saying that α ∈ DLTL^{⊗}(Σ̃) is trace consistent iff L_{α} is trace consistent. It is easy to show that every formula of DLTL^{⊗}(Σ̃) is trace consistent. An important feature of properties defined by trace consistent formulas is that they can often be verified efficiently using partial order based reduction techniques [3, 12, 18]. Consequently, DLTL^{⊗}(Σ̃) provides a flexible and powerful means for specifying trace consistent properties of distributed programs. As it turns out, every formula of DLTL^{⊗}(Σ̃) defines — via the canonical representation — a regular trace language contained in Σ^{∞}/ ≈. Hence by Corollary 6.2, every regular product language corresponds to a regular trace language.

The converse however is not true. To bring this out, consider the distributed alphabet Σ̃ = {{a, a′, c}, {b, b′, c}} and the language L = {cab, cba, ca′b′, cb′a′}^{ω}. Then it is easy to check that L is trace consistent and ω-regular and that it is not a regular product language. In a forthcoming paper we shall deal with the problem of extending DLTL^{⊗}(Σ̃) so as to capture all of the regular trace languages.

References

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

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

[3] Godefroid, P.: Partial-order Methods for the Verification of Concurrent Systems. Lecture Notes in Computer Science 1032, Springer-Verlag (1996)

[4] Harel, D.: Dynamic logic. In Gabbay, D., Guenthner, F., eds.: Handbook of Philosophical Logic, Vol. II, Reidel, Dordrecht (1984) 497– 604

[5] Henriksen, J. G., Thiagarajan, P. S.: Dynamic linear time temporal logic. BRICS technical report RS-97-8, Department of Computer Science, University of Aarhus, Denmark (1997)

[6] Hromkovič, J., Seibert, S., Wilke, T.: 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

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

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

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

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

[11] Mukund, M., Thiagarajan, P. S.: Linear time temporal logics over Mazurkiewicz traces. Proceedings of the 21st Intl. Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 1113, Springer-Verlag (1996) pp. 62–92

[12] Peled, D.: Partial order reduction: model checking using representatives. Proceedings of the 21st Intl. Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 1113, Springer-Verlag (1996) 93–112

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

[14] Thiagarajan, P. S.: A trace based extension of linear time temporal logic. Proceedings of the 9th Annual Symposium on Logic in Computer Science, IEEE (1994) 438–447

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

[16] Thiagarajan, P. S.: A trace consistent subset of PTL. Proceedings of the 6th International Conference on Concurrency Theory, Lecture Notes in Computer Science 962, Springer-Verlag (1995) 438–452

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

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

[19] Vardi, M. Y., Wolper, P.: An automata-theoretic approach to automatic program verification. Proceedings of the 1st Annual Symposium on Logic in Computer Science, IEEE (1986) 332–345

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

[21] Wolper, P., Vardi, M. Y., Sistla, A. P.: 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-9 Jesper G. Henriksen and P. S. Thiagarajan. A Product Version of Dynamic Linear Time Temporal Logic. April 1997. 18 pp. To appear in Concurrency Theory: 7th International Conference, CONCUR ’97 Proceedings, LNCS, 1997.

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.