BRICS RS-96-32 P. S. Thiagarajan: Regular Trace Event Structures

BRICS

Basic Research in Computer Science

Regular Trace Event Structures

P. S. Thiagarajan

BRICS Report Series RS-96-32 ISSN 0909-0878 September 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, 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 publications in the BRICS Report Series. 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 WWW and anonymous FTP:

http://www.brics.dk/
ftp ftp.brics.dk (cd pub/BRICS)

Regular Trace Event Structures

P.S. Thiagarajan^{∗} BRICS^{†} Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark

September, 1996

Abstract

We propose trace event structures as a starting point for constructing effective branching time temporal logics in a non-interleaved setting. As a first step towards achieving this goal, we define the notion of a regular trace event structure. We then provide some simple characterizations of this notion of regularity both in terms of recognizable trace languages and in terms of finite 1-safe Petri nets.

0 Introduction

This paper may be viewed as a first step towards the construction of effective branching time temporal logics in a non-interleaved setting. We believe the study of such logics will yield the formal basis for extending – to a branching time framework – the partial order based verification techniques that have been established in the linear time world [GW, Pel, Val].

∗On leave from School of Mathematics, SPIC Science Foundation, Madras, India † Basic Research In Computer Science, Centre of the Danish National Research Foundation.

For achieving the stated goal one must identify the structures over which the logics are to be interpreted. We propose here objects called trace event structures as suitable candidates. We also initiate their systematic study by pinning down the notion of regularity for these structures.

Trace event structures constitute a common generalization of trees and (Mazurkiewicz) traces. In a linear time setting, moving from sequences to traces has turned out to be a very fruitful way of going from total orders to partial orders. Trees, which may be viewed as objects obtained by gluing together sequences, constitute the basic structures in the branching time world. Hence it seems worthwhile to glue together traces and consider the resulting structures, called trace event structures as a basic class of structures for settings in which the underlying temporal frames have the flavour of both branching time and non-interleaved behaviours.

A good deal of the solutions to the decidability and model checking problems for branching time logics hinges on the notion of a regular labelled tree. For instance, SnS, the monadic second order theory of n-branching trees, is decidable because the decision problem for this logic can be reduced (as shown in the famous paper by Rabin [Rab]) to the emptiness problem for tree automata running over labelled infinite trees. The emptiness problem for these tree automata is decidable because the language of labelled infinite trees accepted by a tree automaton is non-empty only if it accepts a regular labelled tree.

Thus, to test the effectiveness and adequacy of automata and logics to be interpreted over trace event structures, one must understand what are regular trace event structures. Here we provide an obvious definition and some simple characterizations of this notion of regularity.

We start with a presentation of trace structures. We do so because they are known in the literature [NW, PK] and the means for going back and forth between trace structures and trace event structures is also well-understood. Indeed, in [PK] a number of branching time temporal logics over trace structures are considered. However these logics turn out to be undecidable. In our view, the key to obtaining useful and yet decidable branching time logics over trace structures is to suitably limit the quality of the objects over which quantification is to be allowed. We feel that the study of trace event structures will help in identifying the required restrictions.

In section 2 we define regular trace structures and provide an “eventbased” characterization of regularity. Trace event structures are introduced in section 3. The notion of regularity and its characterization is transported from trace structures to trace event structures in section 4. Labelled trace event structures are introduced in section 5 and regular labelled trace event structures are characterized in this section.

The result concerning labelled trace event structures turns out to be – in an event-based language – a conservative extension of the standard result concerning regular labelled trees (see for instance [Tho]). In section 6 we show that regular trace event structures and their labelled versions can be identified with unfoldings of finite 1-safe Petri nets. In the concluding section we discuss future work.

1 Trace Structures

A (Mazurkiewicz) trace alphabet is a pair (DR, I) where DR is a finite non-empty alphabet set and I ⊆ DR × DR is an irreflexive and symmetric relation called the independence relation. We will often refer to DR as the set of directions.

Example 1.1 As a running example we shall use the trace alphabet (DR_{0}, I_{0}) where DR_{0} = {l, m, r} and I_{0} = {(l, r), (r, l)}. □

As usual, DR^{∗} is the set of finite words generated by DR and ϵ is the null word. The independence relation I induces the natural equivalence relation ∼_{I}. It is the least equivalence relation contained in DR^{∗} × DR^{∗} which satisfies:

• If σ, σ′ ∈ DR^{∗} and (a, b) ∈ I then σabσ′ ∼_{I} σbaσ′.

The ∼_{I}-equivalence classes are called (finite Mazurkiewicz) traces. [σ]_{∼_{I}} will denote the ∼_{I}-equivalence class containing σ. We let T R(DR, I) be the set of traces over (DR, I). In other words, T R(DR, I) = DR^{∗}/∼_{I}. Where (DR, I) is clear from the context, we will write [σ] instead of [σ]_{∼_{I}} and we will write T R instead of T R(DR, I).

Example 1.1 (cont.) Let T R_{0} be the set of traces over (DR_{0}, I_{0}). Then {lrm, rlm} is a member of T R_{0}. Note also that [lmr] = {lmr}. □

Traces can be ordered in an obvious way. This ordering relation ⊑_{(DR,I)} ⊆ T R × T R is given by

• [σ] ⊑_{(DR,I)} [σ′] iff there exists σ′′ ∈ DR^{∗} such that σσ′′ ∈ [σ′].

It is easy to observe that ⊑_{(DR,I)} is a partial order. From now on, we shall almost always write ⊑ instead of ⊑_{(DR,I)} whenever (DR, I) is clear from the context. Abusing notation, we shall also use ⊑ to denote the restriction of ⊑ to a given subset of T R.

Example 1.1 (cont.) In T R_{0}, we have [r] ⊑ [llrm]. We also have [lmr] ⋢ [rml] and [rml] ⋢ [lmr]. □

We can now define one of the primary objects of interest in this paper.

Definition 1.2 Let (DR, I) be a trace alphabet. A trace structure over (DR, I) is a subset B ⊆ T R(DR, I) of traces which satisfies the following conditions.

(TS1) If [σ] ∈ B and [σ′] ⊑ [σ] then [σ′] ∈ B.

(TS2) If [σa], [σb] ∈ B with σ ∈ DR^{∗} and (a, b) ∈ I then [σab] ∈ B.

□

Trace structures have a well-understood relationship with prime event structures ([RT, NW]). This relationship, which finds a clean and general presentation in [NW], will play a central role in the present work. Trace structures have been called trace systems in a logical setting [PK].

We shall adopt the standpoint that trace structures represent distributed behaviours in a branching time framework just as traces represent distributed behaviours in a linear time framework (see for instance [Thi]). Let B ⊆ T R(DR, I) be a trace structure. Then B is supposed to stand for the poset (B, ⊑). The crucial new feature – in contrast to the classical setting – is that some elements of B might have a common future due to the causal independence of directions as permitted by I. Indeed, the classical setting is restored whenever I = ∅.

Example 1.1 (cont.) {[ϵ], [l], [r], [lm], [lr], [lrm]} is a trace structure over (DR_{0}, I_{0}). The Hasse diagram of the behaviour captured by this structure is shown in fig. 1.1. □

[figure: [ϵ]; [l]; [r]; [lm]; [lr]; [lrm]]

Figure 1.1

As this example suggests, we have a very generous notion of a branching time behaviour at this stage. In the classical setting (i.e. when I = ∅), one would demand that the tree represented by a trace structure should have “proper” frontiers; for each node either all its successors must be present or none must be present. This demand is usually made for obtaining clean automata theoretic constructions. At present we do not have a good notion of automata running over trace (event) structures. Hence we shall ignore the issue of proper frontiers and work with the generous class of behaviours admitted by def. 1.2.

It will be convenient to establish the link between trace languages and I-consistent word languages. A trace language is just a subset of T R. The word language L ⊆ DR^{∗} is said to be I-consistent in case [σ] ⊆ L for every σ ∈ L. In other words, either all members of a trace are in L or none of them are in L. It is easy to see that subsets of T R and I-consistent subsets of DR^{∗} represent each other. Through the remaining sections, we shall often refer to this connection via the map ts : 2^{T R} → 2^{DR^{∗}} given by

ts(L̂) = ⋃ {[σ] | [σ] ∈ L̂}.

Clearly, for every L̂ ⊆ T R, ts(L̂) is an I-consistent subset of DR^{∗}. We shall often apply ts to a trace structure. After all, a trace structure can be viewed as a trace language which satisfies the two closure properties (TS1) and (TS2).

2 Regular Trace Structures

Through the rest of the paper we fix a trace alphabet (DR, I) and often refer to it implicitly. We let a.b.d range over DR and let σ, σ′, and σ′′ with or without subscripts range over DR^{∗}. D is the dependence relation given by D = (DR × DR) − I. The notations and terminology developed so far w.r.t. (DR, I) will be assumed throughout. For convenience, we will often write σ instead of [σ] in talking about traces. From the context it should be clear whether we are referring to the word σ or the trace [σ].

Definition 2.1

(i) Let B ⊆ T R be a trace structure and σ ∈ B. Then B_{σ} = {σ′ | σσ′ ∈ B}.

(ii) The equivalence relation R_{B} ⊆ B × B is given by:

σ R_{B} σ′ iff B_{σ} = B_{σ′}.

(iii) The trace structure B is regular iff R_{B} is of finite index. □

Our main goal is to characterize the regularity of objects called labelled trace event structures to be introduced in section 5. They will be labelled versions of the event structure representations of trace structures. With this as motivation, the rest of this section will be devoted to establishing an event-based characterization of regular trace structures. We note that the regularity of a trace structure just guarantees that it has an ultimately periodic shape. However, for the labelled objects dealt with later, our definition will amount to a conservative extension of the notion of a regular labelled tree.

It should be clear that the trace structure (B, ⊑) is regular iff B is a recognizable subset of T R. It will be convenient to first bring this out in a more formal fashion.

We say that L̂ ⊆ T R is recognizable iff ts(L̂) is a recognizable (equivalently, regular) subset of DR^{∗}. For L ⊆ DR^{∗} we denote by ≡_{L} the right congruence contained in DR^{∗} × DR^{∗} which is induced by L via

σ ≡_{L} σ′ iff ∀σ′′.[σσ′′ ∈ L iff σ′σ′′ ∈ L].

From the well-known fact that L is a recognizable subset of DR^{∗} iff ≡_{L} is of finite index, the next observation is immediate.

Proposition 2.2 The following statements are equivalent:

(i) (B, ⊑) is a regular trace structure.

(ii) B ⊆ T R is recognizable. □

For the event-based characterization we are after, it is necessary to define so-called prime elements of TR. Suppose σ ≠ ϵ. Then last(σ) is the letter that appears last in σ.

We say that σ is prime iff σ ≠ ϵ and there exists d such that last(σ′) = d for every σ′ ∈ [σ].

Example 2.3 In T R_{0}, [llrm] is prime but [lmlr] is not. □

For each σ, we define pr(σ) = {σ′ | σ′ is prime and σ′ ⊑ σ}. Of course, pr(σ) = ∅ only if σ = ϵ. Finally, for L̂ ⊆ T R we set pr(L̂) = ⋃_{σ∈L̂} pr(σ).

It turns out prime traces constitute the building blocks of the poset of traces (T R, ⊑). To bring this out, let the compatibility relation ↑⊆ T R×T R be defined as: σ ↑ σ′ iff there exists σ′′ such that σ ⊑ σ′′ and σ′ ⊑ σ′′. Further, if X ⊆ T R then ⊔X will denote the l.u.b. of X (under ⊑) in T R if it exists. The next set of results have been assembled from [NW].

Proposition 2.4

(i) Suppose X ⊆ T R such that σ ↑ σ′ for every σ, σ′ ∈ X. Then ⊔X exists.

(ii) σ = ⊔pr(σ) for every σ.

(iii) Let B be a trace structure and X ⊆ B such that ⊔X exists in T R. Then ⊔X ∈ B.

(iv) Let B be a trace structure and σ ∈ T R. Then σ ∈ B iff pr(σ) ⊆ B.

The rest of the section will be devoted to establishing the following characterization of regular trace structures.

Theorem 2.5 Let B be a trace structure. Then the following statements are equivalent.

(i) B is regular.

(ii) pr(B) is recognizable. □

We shall show that B is recognizable iff pr(B) is recognizable. Theorem 2.5 will then follow at once from proposition 2.2.

Lemma 2.6 Suppose the trace structure B is recognizable. Then pr(B) is also recognizable.

Proof: Let L = ts(B). Then L is recognizable and hence there exists a deterministic finite state automaton A operating over DR such that L(A), the language recognized by A, is L. Now consider the deterministic automaton A^{top} = (Q, →, q_{in}, F) also operating over DR defined by

• Q = 2^{DR}

• → ⊆ Q × DR × Q is given by: X →^{d} Y iff Y = (X − D(d)) ∪ {d} where

D(d) = {d′ | d′ D d}.

• q_{in} = ∅.

• F = {{d} | d ∈ DR}.

It is easy to see that L(A) ∩ L(A^{top}) = L_{pr} where L_{pr} = ts(pr(B)). □

For showing the converse of lemma 2.6 we shall make use of Zielonka’s theorem [Zie] and the gossip automaton [MS]. For presenting Zielonka’s theorem we need to introduce asynchronous automata operating over distributed alphabets. A distributed alphabet is a family {Σ_{p}}_{p∈P} where P is a finite set of processes (sequential agents) and each Σ_{p} is a finite set of actions; the set of actions the agent p participates in. We associate a distribution function locΣ̃ : Σ → 2^{P} with Σ̃ where Σ = ⋃_{p∈P} Σ_{p} is the global alphabet and locΣ̃(x) = {p | x ∈ Σ_{p}} for each x in Σ. This in turn induces canonically the trace alphabet (Σ, IΣ̃) where IΣ̃ ⊆ Σ × Σ is obtained via: x IΣ̃ y iff locΣ̃(x) ∩ locΣ̃(y) = ∅.

On the other hand, a trace alphabet can be implemented as a distributed alphabet in many different ways. Here we shall exclusively work with maximal D-cliques. For our specific trace alphabet (DR, I) we call p ⊆ DR a maximal D-clique in case p is a maximal subset of DR with the property p × p ⊆ D. We let P = {p_{1}, p_{2}, …, p_{K}} be the set of maximal D-cliques of (DR, I). We let p, q range over P and P, Q range over non-empty subsets of P. For Q = {p_{i_{1}}, p_{i_{2}}, …, p_{i_{l}}} with i_{1} < i_{2} … < i_{l} we will often instead write Q = {i_{1}, i_{2}, …, i_{l}}. This will be especially convenient when dealing with the gossip automaton.

P, viewed as the names of a set of processes gives rise to the distributed alphabet D̃R = {DR_{p}}_{p∈P} where DR_{p} = p for each p. This distributed alphabet implements (DR, I) in the sense that the canonical trace alphabet induced by D̃R is exactly (DR, I).

Example 2.3 (cont.) The maximal D-cliques of (DR_{0}, I_{0}) are {l, m} and {m, r}. Hence the distributed alphabet obtained via maximal D-cliques is D̃R_{0} = {{l, m}, {m, r}}. □

In what follows, we shall often have to deal with P-indexed families of the form {X_{p}}_{p∈P} and DR-indexed families of the form {Y_{d}}_{d∈DR}. In both cases, we shall often write {X_{p}} and {Y_{d}} respectively.

An asynchronous automaton over D̃R = {DR_{p}} is a structure A = ({S_{p}}, {→_{d} }, S_{in}, F) where the various parts of A are defined as follows. In doing so, we shall also develop some terminology and notations.

• Each S_{p} is a finite non-empty set of states called p-states. They are the local states of the agent p.

S = ⋃_{p∈P} S_{p} is the set of local states. A Q-state is a map s : Q → S such that s(q) ∈ S_{q} for each q in Q. We let S_{Q} denote the set of Qstates and call S_{P}, the set of global states. A d-state is just a Q-state where Q = loc_{DR}(d). Recall that loc_{DR}(d) = {p | d ∈ p}.

We let S_{d} denote the set of d-states. If P ⊆ Q and s is a Q-state then (s)_{P} is the restriction of s to P.

• →_{d} ⊆ S_{d} × S_{d} for each d.

• S_{in} ⊆ S_{P} is the set of global initial states.

• F ⊆ S_{P} is the set of global finite states.

From now on we shall only consider asynchronous automata operating over the fixed distributed alphabet D̃R = {DR_{p}}. Hence we will almost always suppress mention of D̃R and write loc instead of loc_{DR}.

Let A = ({S_{p}}, {→_{d}}, S_{in}, F) be an asynchronous automaton. Then {→ _{d}} induces the global transition relation → _{A} ⊆ S_{P} × DR × S_{P} given by:

Let s, s′ ∈ S_{P} and d ∈ DR. Then s →^{d}_{A} s′ iff the following conditions are satisfied:

(i) ((s)_{d}, (s′)_{d}) ∈→_{d}.

(ii) ∀p ∉ loc(d). s(p) = s′(p).

Let prf (σ) be the set of prefixes of σ. Then a run of A over σ is a map ρ : prf(σ) → S_{P} such that ρ(ϵ) ∈ S_{in} and for every σ′d ∈ prf (σ), ρ(σ′) →^{d}_{A} ρ(σ′d). The run ρ is accepting iff ρ(σ) ∈ F. The language recognized by A is denoted as L(A) and is defined to be the least subset DR^{∗} satisfying:

σ ∈ L(A) iff there exists an accepting run of A over σ.

We say that A is deterministic in case →_{A} is a deterministic transition relation. In other words, s →^{d}_{A} s′ and s →^{d}_{A} s′′ imply s′ = s′′. Moreover, |S_{in}| = 1. We shall say that A is complete in case A has a run over every σ in DR^{∗}. Zielonka’s theorem can be phrased as follows.

Theorem 2.7 Let L̂ ⊆ T R and ts(L̂) = L. Then L̂ is recognizable iff there exists a deterministic complete asynchronous automaton A such that L(A) = L.

□

For presenting the gossip automaton we need the notion of a local view of a trace. The p-view of σ is denoted as ↓^{p} (σ) and is defined as: ↓^{p} (σ) = ⊔{σ′ | σ′ ∈ pr(σ) and last(σ′) ∈ p}. Noting that ⊔∅ = {ϵ}, it follows easily that ↓^{p} (σ) is well-defined for every σ.

The next set of observations follows easily from the definitions and [NW].

Proposition 2.8

(i) For every σ, σ = ⊔_{p∈P} ↓^{p}(σ).

(ii) Suppose B is a trace structure and σ ∈ T R. Then σ ∈ B iff ↓^{p}(σ) ∈ B for every p. □

We can now define a function which will pick out the agent in Q which has the latest information – among the agents in Q – at a trace about some agent (which might or might not be in Q).

Accordingly, latest_{Q} : T R × P → Q is defined as:

latest_{Q}(σ, p) = q̂ provided q̂ is the agent in Q with least index which has the property that ↓^{j} (↓^{q} (σ)) ⊆ ↓^{j} (↓q̂ (σ)) for every q ∈ Q. Recall that P = {p_{1}, p_{2}, …, p_{K}}. In dealing with the gossip automaton, we will often write i instead of p_{i} (with i ∈ {1, 2, …, K}). The gossip automaton computes the latest_{Q} using only a bounded amount of information. For our purposes, the key result proved in [MS] can be phrased as follows:

Theorem 2.9 There exists an effectively constructible deterministic complete asynchronous automaton

A_{Γ} = ({Γ_{p}}, {⇒_{d}}, Γ_{in}, Γ_{P})

such that for each Q = {i_{1}, i_{2}, …, i_{n}} ⊆ P there exists an effectively computable function gossip_{Q} = Γ_{i_{1}} × Γ_{i_{2}} … × Γ_{i_{n}} × P → Q such that, for every σ and every p,

latest_{Q}(σ, p) = gossip_{Q} (ν(i_{1}), ν(i_{2}), …, ν(i_{n}), p)

where ρ_{Γ}(σ) = ν and ρ_{Γ} is the unique run of ρ_{Γ} over σ. □

Thus, by examining the Q-states of A_{Γ} at ρ_{Γ}(σ), we can, with a bit of work, determine which agent among Q has the latest information about p at σ.

Using the gossip automaton we can associate with each asynchronous automaton, a second asynchronous automaton A^{pr} with the following property.

Fix σ and suppose that A reaches the global state s^{(p)} after running over ↓^{p} (σ) (i.e. after running over some member of ts(↓^{p} (σ)). Further suppose that A^{pr} reaches the global state ŝ after running over σ and A_{Γ} (the gossip automaton) reaches the global state ν after running over σ. Then for each p, it will be the case that ŝ(p) = (s^{(p)}, ν(p)).

Using this association between A and A^{pr} we can easily obtain the result we are after. Let A = ({S_{p}}, {→_{d}}, S_{in}, F). Recall that A_{Γ} = ({Γ_{p}}, {⇒_{d}}, Γ_{in}, Γ_{P}). We now define the asynchronous automaton A^{pr} = ({Ŝ_{p}}, {R_{d}}, Ŝ_{in}, F̂) as follows:

• For each q, Ŝ_{q} = S_{P} × Γ_{q}.

• Let ŝ, t̂ ∈ Ŝ_{d} with ŝ(p) = (s^{(p)}, ν_{p}) and t̂(p) = (t^{(p)}, δ_{p}) for each p in loc(d). Then (ŝ, t̂) ∈ R_{d} iff the following conditions are satisfied:

(i) ((s^{(p)})_{d}, (t^{(p)})_{d}) ∈→_{d}. Recall that (s)_{d} is s restricted to loc(d) in case s is a Q-state with loc(d) ⊆ Q.

(ii) (ν_{d}, δ_{d}) ∈ ⇒_{d} where ν_{d} and δ_{d} are the two d-states of A_{Γ} satisfying ν_{d}(p) = ν_{p} and δ_{d}(p) = δ_{p} for every p ∈ loc(d).

(iii) Suppose loc(d) = Q = {i_{1}, i_{2}, …, i_{n}}, q ∈ Q and p ∉ Q. Then t^{(q)}(p) = s^{(q̂)}(p) where q̂ = gossip_{Q}(ν_{i_{1}}, ν_{i_{2}}, …, ν_{i_{n}}, p). Recall that ŝ(x) = (s^{(x)}, ν_{x}) foe every x ∈ loc(d).

(iv) For every p, q ∈ loc(d), t^{(p)} = t^{(q)}.

• Let S_{in} = {s_{in}} and Γ_{in} = {ν_{in}}. Then Ŝ_{in} = {ŝ_{in}} where for each p, ŝ_{in}(p) = (s_{in}, ν_{in}(p)).

• Let ŝ ∈ Ŝ_{P} with ŝ(p) = (s^{(p)}, ν_{p}) for each p. Then ŝ ∈ F̂ iff s^{(p)} ∈ F for every p.

Lemma 2.10 Let B be a trace structure. Suppose pr(B) is recognizable. Then B is also recognizable.

Proof: Let ts(pr(B)) = L. Then by theorem 2.7, there exists a deterministic complete asynchronous automaton A such that L(A) = L. Now consider the automaton A^{pr} associated with A and constructed as specified above. Then we claim that L(A^{pr}) = L′ where L′ = ts(B).

To see this, for each σ let ρ_{σ} (ρ̂_{σ}) be the unique run of A (A^{pr}) over σ. Then induction on the length of σ accompanied by an examination of the definitions will yield the following:

Fact: Let ρ̂_{σ}(ρ) = ŝ with ŝ(p) = (s^{(p)}, ν_{p}) for each p. Let σ_{q} ∈ ts(↓^{q} (σ)) and ρ_{σ_{q}}(σ_{q}) = s. Then s^{(q)} = s.

Hence from the definition of A^{pr} it follows that σ ∈ L(A^{pr}) iff ↓^{p} (σ) ⊆ L(A) = L for every p. But then according to proposition 2.8, σ ∈ B iff ↓^{p}(σ) ∈ B for every p. Consequently, σ ∈ L′ iff ↓^{p}(σ) ⊆ L for every p. Thus σ ∈ L′ iff σ ∈ L(A^{pr}) as required. □

Theorem 2.5 now follows at once from lemmas 2.6, 2.10 and prop. 2.2. Lemma 2.10 admits a direct proof as shown in [DM]. However, for the net theoretic characterization of regularity that we obtain later, it is necessary to have our construction underlying the proof of lemma 2.10.

3 Trace Event Structures

We now wish to view trace structures as prime event structures. In this representation the causality, conflict and concurrency relation that glue together a trace structure will become explicit. The main motivation for considering this representation is that we expect the automata theoretic treatment of trace structures to be carried out in terms of their prime event structure representations.

We start with a notation concerning posets. Let (X, ≤) be a poset and Y ⊆ X. Then ↓ Y = {x | ∃y ∈ Y, x ≤ y} and ↑ Y = {x | ∃y ∈ Y, y ≤ x}. Whenever Y is a singleton with Y = {y} we will write ↓ y (↑ y) instead of ↓ {Y } (↑ {Y }).

A prime event structure is a triple ES = (E, ≤, #) where (E, ≤) is a poset and # ⊆ E × E is an irreflexive and symmetric relation such that the following conditions are met:

• ↓ e is a finite set for every e ∈ E.

• For every e_{1}, e_{2}, e_{3} ∈ E, if e_{1}#e_{2} and e_{2} ≤ e_{3} then e_{1}#e_{3}.

E is the set of events and ≤ is the causality relation. # is the conflict relation.

As usual, the states of a prime event structure will be called configurations. We say that c ⊆ E is a configuration iff c =↓ c and (c × c) ∩ # = ∅. It is easy to see that ∅ is always a configuration and more interestingly, ↓ e is a configuration for every event e. We let C_{ES}^{∞} be the set of (finite and infinite) configurations and C_{ES} denote the set of finite configurations of ES.

It will be useful to introduce two derived relations associated with a prime event structure. Let ES = (E, ≤, #) be a prime event structure. Then ⋖⊆ E × E is defined as: e ⋖ e′ iff e < e′ (i.e. e ≤ e′ and e ≠ e′) and for every e′′, if e ≤ e′′ ≤ e′ then e = e′′ or e′′ = e′. In other words, ⋖=< − <^{2}.

Next we define the minimal conflict relation #_{μ} ⊆ E × E via:

e #_{μ} e′ iff (↓e× ↓e′) ∩ # = {(e, e′)}.

A DR-labelled prime event structure is a quadruple ES = (E, ≤, #, λ) where (E, ≤, #) is a prime event structure and λ : E → DR is a labelling function. We can now present the proposed event structure representation of trace structures.

Definition 3.1 A trace event structure over (DR, I) is a DR-labelled prime event structure ES = (E, ≤, #, λ) which satisfies the following requirements (with e, e′ ranging over E):

(TES1) e #_{μ} e′ implies λ(e) ≠ λ(e′)

(TES2) If e ⋖ e′ or e #_{μ} e′ then (λ(e), λ(e′)) ∈ D

(TES3) If (λ(e), λ(e′)) ∈ D then e ≤ e′ or e′ ≤ e or e # e′.

□

Thus a trace event structure is a DR-labelled prime event structure in which the DR-orientation of the events (as specified by the labelling function) respects the independence relation I. This is captured by the conditions (TES2) and (TES3). The first condition (TES1) merely reflects the fact that if [σ] = [σ′] then [σd] = [σ′d]. These remarks might be easier to appreciate once we explain how trace structures and trace event structures represent each other. But first we shall consider some examples.

In diagramatic descriptions of labelled prime event structures the poset of events ordered by the causality relation will be shown by its Hasse diagram. The elements of the minimal conflict relation will be shown as squiggly edges. The conflict relation is then the relation uniquely induced by the causality and the minimal conflict relations. The events will be drawn as boxes.

Example 3.1 Recall (DR_{0}, I_{0}) with DR_{0} = {l, m, r} and I_{0} = {(l, r), (r, l)}. In fig. 3.1 (a) and 3.1 (b) and 3.1 (c) we show three examples of DR_{0}-labelled prime event structures. None of them constitutes a trace event structure over (DR_{0}, I_{0}).

(a)  (b)  (c)^{[figure: e_{1} l; l e_{2}; l e_{1}; r e_{2}; e_{1} l; r e_{2}; e_{3} r; m e_{4}]}

Figure 3.1

In fig. 3.1 (a) we have e_{1} #_{μ} e_{2} with λ(e_{1}) = λ(e_{2}). In fig. 3.1 (b) we have e_{1} ⋖ e_{2} with (λ(e_{1}) = λ(e_{2})) ∉ D. In fig. 3.1 (c) we have two violations. Firstly e_{1} #_{μ} e_{2}. But (λ(e_{1}) = λ(e_{2})) ∉ D. Secondly we have (λ(e_{3}), λ(e_{4})) ∈ D but e_{3} ≰ e_{4}, e_{4} ≰ e_{3} and (e_{3}, e_{4}) ∉ #.

Example 3.2 In fig. 3.2 we show an infinite trace event structure over (DR_{0}, I_{0}).

[figure: m; l; m; r; l; m; r; l; m; r]

Figure 3.2

Example 3.3 Let (DR_{1}, I_{1}) be the trace alphabet with DR_{1} = {l, r} and I_{1} = ∅. Then every trace over this trace alphabet is a singleton. In figure 3.3 we show a trace event structure over (DR_{1}, I_{1}). It may be viewed as an event structure representation of the full binary tree DR_{1}^{∗}.

[figure: l; r; l; r; l; l]

Figure 3.3

Let ES_{i} = (E_{i}, ≤_{i}, #_{i}, λ_{i}), i = 1, 2 be a pair of DR-labelled prime event structures. We say that ES_{1} and ES_{2} are isomorphic – and denote this by ES_{1} ≡ ES_{2} – iff there exists a bijection f : E_{1} → E_{2} such that e_{1} ≤_{1} e′_{1} iff f(e_{1}) ≤_{2} f(e′_{1}) and e_{1} #_{1} e′_{1} iff f(e_{1}) #_{2} f(e′_{1}) for every e_{1}, e′_{1} ∈ E_{1}. Furthermore we require λ_{2}(f(e_{1})) = λ_{1}(e_{1}) for every e_{1} ∈ E_{1}.

Let T RS(DR, I) be the class of trace structures over (DR, I) (written from now on as just T RS). Let T ES(DR, I) be the class of trace event structures over (DR, I) (written from now on as T ES). Using the maps tes : T RS → T ES and est : T ES → T RS we will bring out the fact that T RS and T ES are different but equivalent descriptions of the same class of objects.

Let B ∈ T RS. Then tes(B) = (E, ≤, #, λ) where:

• E = pr(B).

• ≤ is ⊑ restricted to pr(B) × pr(B).

• # = {(σ, σ′) | σ, σ′ ∈ pr(B) and σ ↑̸ σ′}.

(Recall that σ ↑ σ′ iff there exists σ′′ ∈ T R such that σ ⊑ σ′′ and σ′ ⊑ σ′′.)

• λ(σ) = last(σ) for every σ ∈ pr(B).

To define the map est we must consider linearizations of the configurations of a trace event structure and read off traces from these linearizations using the labelling function. Let ES = (E, ≤, #, λ) be a trace event structure and let c ∈ C_{ES}. Then ρ ∈ E^{∗} is called a linearization of c iff it is a linearization of the poset (c, ≤_{c}) where ≤_{c} is ≤ restricted to c × c. More precisely, ρ is required to satisfy:

• No event e ∈ E − c appears in ρ.

• Every event e ∈ c appears exactly once in ρ.

• If e, e′ ∈ c with e < e′ then e appears before e′ in ρ.

We let lin(c) be the set of linearizations of the configuration c. By abuse of notation, we use λ to also denote the unique homomorphic extension of λ : E →DR to λ : E^{∗} →DR^{∗}. In other words λ(ϵ) = ϵ and λ(ρe) = λ(ρ)λ(e) for ρ ∈ E^{∗}. Finally, we define λ(c) = {λ(ρ) | ρ ∈ lin(c)}.

Let ES = (E, ≤, #, λ) ∈ T ES. Then est(ES) = {[σ] | σ ∈ λ(c) for some c ∈ C_{ES}. From the results of [NW] it is straightforward to establish the following:

(i) tes is well defined. In other words, tes(B) ∈ T ES for every B ∈ T RS.

(ii) est is well defined. In other words, est(ES) ∈ T RS for every ES ∈ T ES.

(iii) est(tes(B)) = B for every B ∈ T RS.

(iv) tes(est(ES)) ≡ ES for every ES ∈ T ES. □

It is in the sense of (iii) and (iv) trace event structures and trace structures represent each other. A strong version of this statement in a categorical setting can be found in [NW]. To conclude this section, we show in fig. 3.4, the trace event structure corresponding to the trace behaviour of fig. 1.1.

\xymatrix{l \ar[dr] \ar[d] & r \ar@{^{(}->}[d] \\ m & m}

Figure 3.4

4 Regular Trace Event Structures

Our goal here is to transport the notion of regularity from trace structures to trace event structures. As before, the material in this section also will be developed w.r.t. the fixed trace alphabet (DR, I).

Let ES = (E, ≤, #, λ) be a trace event structure and c ∈ CS. We define #(c) = {e′ | ∃e ∈ c. e # e′}. We then denote the substructure rooted at c as ES\c and define it to be the quadruple ES\c = (E′, ≤′, #′, λ′) where

• E′ = E − (c ∪ #(c)).

• ≤′ is ≤ restricted to E′ × E′.

• #′ is # restricted to E′ × E′.

• λ′ is λ restricted to E′.

Proposition 4.1 Let ES = (E, ≤, #, λ) be a trace event structure and c ∈ C_{ES}. Then ES\c is also a trace event structure.

Proof: Let ES\c = (E′, ≤′, #′, λ′). From the definitions it is clear that ES\c is a DR-labelled prime event structure. We must verify that λ′ respects I in the required sense.

Suppose x, y ∈ E′ with x ⋖′ y. We must show that (λ′(x), λ′(y)) ∈ D. It suffices to show that x ⋖ y (in ES) because then (λ(x), λ(y)) ∈ D due to the fact that ES is a trace event structure and λ′(x) = λ(x) and λ′(y) = λ(y).

So assume for contradiction that there exists z ∈ E such that x < z < y in ES. If z ∈ E′ then we have x <′ z <′ y as well which would contradict x ⋖′ y. But z ∉ E′ implies z ∈ c or z ∈ #(c). If z ∈ c then c =↓ c leads to x ∈ c which contradicts x ∈ E′. If z ∈ #(c) then for some z′ ∈ c it is the case that z′ # z. But then z < y and hence z′ # y so that y ∈ #(c) which contradicts y ∈ E′. Hence it must be the case that x ⋖ y.

Next suppose that x, y ∈ E′ with x #′_{μ} y. Again it suffices to show that x #_{μ} y (in ES) because then we can easily conclude (λ′(x), λ′(y)) ∈ D. So assume for contradiction that (x, y) ∉ #_{μ}. Note that x #′_{μ} y implies x #′ y and hence x # y.

If (x, y) ∉ #_{μ}, then there exists a pair (x′, y′) in (↓x× ↓y) ∩ # such that (x′, y′) ≠ (x, y). Assume without loss of generality that x′ ≠ x. Then x′ < x and y′ ≤ y. Hence x′#y. Suppose x′ ∈ E′. Then x′ <′ x and x′ #′ y as well, leading to the contradiction that (x, y) ∉ #′_{μ}.

So assume that x′ ∉ E′. Hence x′ ∈ c or x′ ∈ #(c). If x′ ∈ c then x′#y leads to y ∈ #(c) which contradicts y ∈ E′. If x′ ∈ #(c) then x′#z for some z ∈ c. But then x′ < x leads to z # x which in turn implies that x ∈ #(c). But this contradicts x ∈ E′. Hence x #_{μ} y and consequently (λ′(x), λ′(y)) ∈ D as required.

Now suppose that x, y ∈ E′ such that (λ′(x), λ′(y)) ∈ D. Then (λ(x), λ(y)) ∈ D. Since ES is a trace event structure we must have x ≤ y or y ≤ x or x # y. Hence x ≤′ y or y ≤′ x or x #′ y as required. □

We can now define regularity of trace event structures.

Definition 4.2 Let ES be a trace event structure.

(i) R_{ES} ⊆ C_{ES} × C_{ES} is given by:

c R_{ES} c′ iff ES\c ≡ ES\c′.

(ii) ES is regular iff the equivalence relation R_{ES} is of finite index. □

It should be clear that the trace event structure ES is regular iff est(ES) is a regular trace structure. It will be worthwhile to establish this connection precisely.

Recall that if B is a trace structure with σ ∈ B then B_{σ} = {σ′ | σσ′ ∈ B}.

Lemma 4.3 Let ES be a trace event structure with c ∈ CS and σ ∈ λ(c). Then est(ES\c) = B_{σ}.

Proof: Follows easily from the definitions and the constructions in [NW].□

Proposition 4.4 The trace event structure ES is regular iff est(ES) is a regular trace structure.

Proof: Follows easily from lemma 4.3 and prop. 4.1. □

Let ES = (E, ≤, #, λ) be a trace event structure and e ∈ E. Then ↓ e can be identified with the trace λ(↓e). We now wish to show that ES is regular iff for every d, the collection of d-labelled events, viewed as a collection of traces, is recognizable. Let ES = (E, ≤, #, λ) be a trace event structure.

We let E_{d} = {e | e ∈ E and λ(e) = d}. We next define, for each d, the trace language L_{d}^{ES} via:

L_{d}^{ES} = {[σ] | σ ∈ λ(↓e) for some e ∈ E_{d}}.

The matching notion for trace structures will be denoted pr_{d}(B). More precisely, if B is a trace structure then pr_{d}(B) = {σ | σ ∈ pr(B) and last(σ) = d}. The next observation again follows from [NW] easily.

Proposition 4.5 Let ES = (E, ≤, #, λ) be a trace event structure and est(ES) = B. Let f : C_{ES} → B be given by f(c) = λ(c) for every c ∈ C_{ES}. Then:

(i) f is an isomorphism between the posets (C_{ES}, ⊆) and (B, ⊑).

(ii) f({↓e | e ∈ E}) = pr(B).

(iii) f({↓e | e ∈ E_{d}}) = pr_{d}(B).

(iv) L_{d}^{ES} = pr_{d}(B) for every d. □

We can now state the main result of this section.

Theorem 4.6 The trace event structure ES is regular iff L_{d}^{ES} is recognizable for every d.

Proof: \underline{⇒} Suppose ES = (E, ≤, #, λ) is regular and est(ES) = B. Then by prop. 4.4, (B, ⊑) is regular and hence by theorem 2.5, pr(B) is recognizable. Let A be a deterministic finite state automaton recognizing L = ts(pr(B)). Now recall the automaton A^{top} = (Q, →, q_{in}, F) constructed in the proof of lemma 2.6. Consider the automaton A_{d}^{top} obtained from A^{top} by setting A_{d}^{top} = (Q, →, q_{in}, F_{d}) where F_{d} = {{d}}. Let L_{d} be the language recognized by A_{d}^{top}. It is easy to verify that L_{d} = ts(pr_{d}(T R)). Hence ts(pr_{d}(B)) = L ∩ L_{d}. Consequently pr_{d}(B) is recognizable for each d. But now from prop. 4.5 (part (iv)) we also have that L_{d}^{ES} is recognizable for each d.

\underline{⇐} Suppose L_{d}^{ES} is recognizable for each d. Then by prop. 4.5 (part (iv)), pr_{d}(B) is recognizable for each d where B = est(ES). But this implies that pr(B) = ⋃_{d∈DR} pr_{d}(B) is recognizable and hence, by theorem 2.5, B is regular. Prop. 4.4 now tells us that ES is also regular. □

5 Labelled Trace Event Structures

Through the rest of the paper fix Σ, a finite non-empty set of labels.

Definition 5.1 A Σ-labelled trace event structure is a pair LES = (ES, φ) where ES = (E, ≤, #, λ) is a trace event structure (over (DR, I)) and φ : E →Σ is a labelling function. □

Note that LES has an “internal” labelling function λ. This function orients the events along the directions in DR while respecting the independence relation I in the manner specified in section 3. On the other hand, φ is an “external” and, in the present setting, unrestricted labelling function which labels the events by members of Σ.

One could ask why not start with Σ-labelled trace structures? The answer is that a variety of negative results are at present available concerning logics interpreted over trace structures and related models (see for instance [LPRT, PK]). These results suggest that trace structures accompanied by unrestricted labelling functions will not be a tractable collection of objects. Indeed an observation due to Walukiewicz [Wal] suggests that even trace structures accompanied by unrestricted labelling functions will not constitute a tractable collection of objects. (We will say a little more about this in the concluding section.) Nevertheless we feel that it will be fruitful to study of Σ-labelled trace event structures and identify the required restrictions in some suitable logical and/or automata theoretic framework. These notions can then be transported, if necessary, to trace structures at a later stage.

Since Σ is fixed we shall often say “labelled” to mean “Σ-labelled”. Let LES_{i} = (ES_{i}, φ_{i}), i = 1, 2 be a pair of labelled trace event structures with ES_{i} = (E_{i}, ≤_{i}, #_{i}, λ_{i}). Then LES_{1} and LES_{2} are said to be isomorphic (also denoted by abuse of notation as LES_{1} ≡ LES_{2}) iff there exists a trace event structure isomorphism f : E_{1} → E_{2} such that λ_{1}(e_{1}) = λ_{2}(f(e_{1})) for every e_{1} ∈ E_{1}. Thus the isomorphism is also required to respect the external labelling.

Definition 5.2 Let LES = (ES, φ) be a labelled trace event structure with ES = (E, ≤, #, λ).

(i) Suppose c ∈ C_{ES}. Then LES\c = (ES′, φ′) where ES′ = (E′, ≤′,#′, λ′) = ES\c and φ′ is φ restricted to E′.

(ii) The equivalence relation R_{LES} ⊆ C_{ES} × C_{ES} is given by:

c R_{LES} c′ iff LES\c ≡ LES\c′.

(iii) LES is regular iff R_{LES} is of finite index. □

The main result of this section is a conservative extension of the classical characterization of regular Σ-labelled trees [Tho]. To formulate this result let LES = (ES, φ) be a labelled trace event structure with ES = (E, ≤, #, λ). Let x ∈ Σ. Then L_{x}^{LES} ⊆ T R is defined as:

[σ] ∈ L_{x}^{LES} iff σ ∈ λ(↓e) for some e ∈ φ^{−1}(x).

Theorem 5.3 The labelled trace event structure LES = (ES, φ) is regular iff L_{x}^{LES} is a recognizable trace language for every x ∈ Σ.

Proof: Let ES = (E, ≤, #, λ). Consider the trace alphabet (D̂R, Î) where D̂R = DR × Σ and Î ⊆ D̂R × D̂R is given by

((a, x), (b, y)) ∈ Î iff (a, b) ∈ I.

Let ÊS = (E, ≤, #, λ̂) where λ̂ : E →D̂R is given by:

λ̂(e) = (d, x) iff λ(e) = d and φ(e) = x.

Clearly ÊS is a trace event structure over (D̂R, Î). Moreover the labelled trace event structure LES is regular iff the trace event structure ÊS is regular. By theorem 4.6, ÊS is regular iff L_{ES} ; d̂ is a recognizable trace language

for every d̂∈ D̂R. Now define, for each x ∈ Σ, the trace language L_{ES} ; x via:

L_{ES} ; x = ⋃ {L_{ES} ; d̂ | d̂∈ DR × {x}}.

Clearly L_{ES} ; x is recognizable for each x if L_{ES} ; d̂ is recognizable for each d̂∈ D̂R.

Conversely, suppose L_{ES} ; x is recognizable for each x ∈ Σ. Then it is easy to verify (using the automaton A^{top} constructed in the proof of lemma 2.6) that L_{ES} ; d̂ is recognizable for each d̂∈ D̂R.

But now the required result follows from the easy observation that L_{x}^{ES} = L_{ES} ; x for each x ∈ Σ. □

6 A Net Theoretic Characterization

The basic result shown in [NPW] says that every 1-safe Petri net unfolds into a prime event structure. Later results appearing in a uniform setting (see [NW] for exact references) show in fact that 1-safe Petri nets and prime event structures represent each other in a strong sense. Based on this connection we show here that regular trace event structures and (labelled) finite 1-safe Petri nets are strongly related to each other.

We shall define here a 1-safe Petri net to be a quadruple N = (B, E, F, M_{in}) where (B, E, F) is a net and M_{in} ⊆ B is the initial marking. (B, E, F) is a net in the sense B is a set of conditions, E is the set of events with B ∩E = ∅. Furthermore F ⊆ (B ×E)∪(E ×F) is the flow relation. We say that N is finite if both B and E are finite sets. From now by “Petri net” we shall mean “1-safe Petri net”. As usual, for x ∈ B ∪ E, we set ^{•}x = {y | (y, x) ∈ F } and x^{•} = {y | (y, x) ∈ F }. The dynamics of N are captured by the associated transition system T S_{N} = (RM_{N} , →_{N} , M_{in}) where RM_{N} ⊆ 2^{B} and →_{N} ⊆ RM_{N} × E × RM_{N} are the least sets satisfying:

• M_{in} ∈ RM_{N}.

• Suppose M ∈ RM_{N} and e ∈ E such that ^{•}e ⊆ M and (e^{•} −^{•}e)∩M = ∅.

Then M′ ∈ RM_{N} and M →^{e}_{N} M′ where M′ = (M −^{•}e) ∪ e^{•}.

RM_{N} is the set of reachable markings of N. F S_{N}, the set of firing sequences of the Petri net N = (B, E, F, M_{in}) is the least subset of E^{∗} defined as follows. In doing so, it will be convenient to also build up the relation [figure: ∗; N]

• ϵ ∈ F S_{N} and [figure: M_{in}; ∗; N; M_{in}]

• Suppose τ ∈ F S_{N}, [figure: M_{in}; ∗; τ; N; M] and [figure: M; e; N; M′] . Then τe ∈ F S_{N}

and [figure: M_{in}; ∗; τe; M′] .

In what follows, we will define notion of an es-unfolding (event structure unfolding) of only finite 1-safe Petri nets. This silliness is mainly due to the fact we have chosen to phrase the basic notions of trace theory in terms of finite trace alphabets in order to appeal to the automaton theoretic constructions for recognizable trace languages. The material to follow that is concerned with unfoldings can however be easily modified to apply to the whole class of Petri nets.

The finite Petri net N = (B, E, F, M_{in}) gives rise to the trace alphabet (E, I_{N}) where I_{N} = {(e_{1}, e_{2}) | (^{•}e_{1} ∪ e_{1}^{•}) ∩ (^{•}e_{2} ∪ e_{2}^{•}) = ∅}. For τ ∈ E^{∗} let [τ]_{N} denote the ∼_{I_{N}} -equivalence class containing τ.

Now for every τ ∈ F S_{N} it is easy to see that [τ]_{N} ⊆ F S_{N}. Clearly F S_{N} is prefix-closed. Furthermore, τe, τe′ ∈ F S_{N} and e I_{N} e′ implies τee′ ∈ F S_{N}. Thus B_{N} = {[τ]_{N} | τ ∈ F S_{N} } is a trace structure with ts(B_{N}) = F S_{N}. We let ES_{N} denote tes(B_{N}) and call ES_{N} the es-unfolding of N. Note that according to prop. 3.2, ES_{N} is a trace event structure over (E, I_{N}).

Let X be a finite non-empty set of labels. Then an X-labelled Petri net is a pair LN = (N , lb) where N = (B, E, F, M_{in}) is a Petri net and lb : E → X is a labelling function.

Let LN = (N , lb) be an X-labelled Petri net and ES_{N} = (Ê, ˆ≤, ˆ#, λ̂). Then we let ES_{LN} denote the X-labelled prime event structure ES_{LN} = (Ê, ˆ≤, ˆ#, lb o λ̂) and call it the es-unfolding of LN.

We can now state our net theoretic characterisation of regular trace event structures.

Theorem 6.1 The trace event structure ES over (DR, I) is regular iff there exists a finite DR-labelled Petri net LN = (N , lb) such that ES is isomorphic to ES_{LN}. □

One half of the theorem is quite easy to prove.

Lemma 6.2 Suppose LN = (N , lb) is a finite DR-labelled Petri net such that ES_{LN} is a DR-labelled trace event structure. Then ES_{LN} is regular.

Proof: Let ES_{N} = (Ê, ˆ≤, ˆ#, λ̂) so that ES_{LN} = (Ê, ˆ≤, ˆ#, lb o λ̂). Let ES = (Ê, ˆ≤, ˆ#) and N = (B, E, F, c_{in}). Recall that ES_{N} is a trace event structure over (E, I_{N}). Define now the map μ : C_{ES} → RM_{N} via μ(c) = M provided there exists τ ∈ λ̂(c) such that [figure: M_{in}; ∗; τ; N; M] .

It is easy to check that μ is well defined. Next define the equivalence relation R_{N} ⊆ C_{ES} × C_{ES} as:

c R_{N} c′ iff μ(c) = μ(c′).

The number of equivalence classes of this equivalence relation is at most 2^{|B|}.

Claim Suppose c R_{N} c′. Then c R_{ES_{N}} c′ and in fact c R_{ES_{LN}} c′.

If the claim holds then the index of R_{ES_{LN}} is at most 2^{|B|} and hence ES_{LN} is regular. To see that the claim holds let τ ∈ λ̂(c) and τ′ ∈ λ̂(c′). Then from μ(c) = μ(c′) it follows that ∀τ′′ ∈ E^{∗}, ττ′ ∈ F S_{N} iff ττ′′ ∈ F S_{N}. This observation at once leads to the claim. □

To prove the second half of theorem 3.1, we will prune away some local transitions of the automaton A^{pr} that was constructed to prove lemma 2.10. To be precise, let A = ({S_{p}}, {→_{d}}, S_{in}, F) be a deterministic and complete asynchronous automaton operating over {DR_{p}}. Recall that p ranges over P, the set of maximal D-cliques of (DR, I) with DR_{p} = p for each p.

Let A^{pr} = ({Ŝ_{p}}, {R_{d}}, Ŝ_{in}, F̂) be the deterministic complete asynchronous automaton constructed from A as in the proof of lemma 2.10. We now define the asynchronous automaton B^{pr} = ({S̃_{p}}, {⇝_{d}}, S̃_{in}, F̃) as follows:

• S̃_{p} = Ŝ_{p} for each p.

• For each d, ⇝_{d} is the least subset of R_{d} which satisfies: Suppose (ŝ, t̂) ∈ R_{d} with ŝ(p) = (s^{(p)}, ν_{p}) and t̂(p) = (t^{(p)}, δ_{p}) for each p ∈ loc(d). Then (ŝ, t̂) ∈⇝_{d} iff s^{(p)} ∈ F and t^{(p)} ∈ F for each p ∈ loc(d). Recall that s^{(p)} ∈ S_{P}, the set of global states of A and F is the set of global final states of A.

• S̃_{in} = Ŝ_{in}.

• F̃ is the least subset of S̃_{P} (the set of global states of B^{pr}) which satisfies: Suppose σ ∈ DR^{∗} such that ρ̃_{σ} is a run of B^{pr} with ρ̃_{σ}(σ) = s̃. Then s̃ ∈ F̃.

It is easy to observe that B^{pr} is also a deterministic asynchronous automaton. However it might not be complete. In fact, its characteristic feature is that it accepts a word iff it has a run over the word.

Lemma 6.3 Let B be a regular trace structure over (DR, I) with ts(B) = L. Then there exists an asynchronous automaton B operating over {DR_{p}} such that L(B) = L. Moreover, for every σ ∈ DR^{∗} − L, B has no run over σ.

Proof: Since B is regular, L is recognizable. Let A be a deterministic and complete asynchronous automaton with A = ({S_{p}}, {→_{d}}, S_{in}, F) such that L(A) = L. Let A^{pr} = ({Ŝ_{p}}, {R_{d}}, Ŝ_{in}, F̂) be the automaton constructed from A as in the proof of lemma 2.10. Finally, let B^{pr} be the deterministic asynchronous automaton constructed from A^{pr} as detailed above. We wish to argue that B^{pr} has the properties required by the lemma. We shall decompose the argument into three steps.

Claim 1 L(A^{pr}) = L(A).

Claim 2 L(B^{pr}) = L(A^{pr}).

Claim 3 Let σ ∈ DR^{∗}. Then σ ∈ L(B^{pr}) iff B^{pr} has a run over σ.

To see that claim 1 must hold, we note that, by the construction of A^{pr}, σ ∈ L(A^{pr}) iff ↓^{p}(σ) ⊆ L(A) for every p. But from the fact that B is a trace structure it follows from prop. 2.8, that σ ∈ L(A) iff ↓^{p}(σ) ⊆ L(A) for every p. Hence indeed L(A^{pr}) = L(A).

To settle claim 2, we consider σ ∈ DR^{∗} and proceed by induction on |σ| to show that ρ̃ : P rf(σ) → S̃_{P} is a run of B^{pr} over σ iff ρ̃_{σ} is the accepting run of A^{pr} over σ.

Suppose |σ| = 0 so that σ = ϵ. Since L is prefix-closed, ϵ ∈ L and hence the basis step follows immediately from the definitions.

So suppose σ = σ′d. First assume that ρ̃: P rf(σ) →S̃ is a run of B^{pr} over σ. Let ρ̃_{σ′} be the restriction of ρ̃ to P rf(σ′). By the induction hypothesis, ρ̃_{σ′} is the accepting run of A^{pr} over σ′. Let ρ̃(σ′) = ŝ and ρ̃(σ′d) = t̂. Then ((ŝ)d, (t̂)d) ∈⇝_{d}⊆ R_{d} and consequently ρ̃ is also the run of A^{pr} over σ.

Suppose ρ̃ is not an accepting run of A^{pr} over σ. Then t̂ ∉ F̂. Hence, by the definition of F̂, it must be the case that t^{(p)} ∉ F for some p. Let t̂(p) = (t^{(p)}, δ_{p}) for each p.

If p ∉ loc(d) then ŝ(p) = t̂(p) and hence ŝ ∉ F̂. But this contradicts the fact that ρ̃_{σ′} is the accepting run of A^{pr} over σ′. So suppose that p ∈ loc(d). We now have t^{(p)} ∉ F and p ∈ loc(d) which contradicts that ((ŝ)_{d}, (t̂)_{d}) ∈⇝_{d}. Hence it must be the case that t̂∈ F̂.

On the other hand, if ρ̃: prf(σ) →S̃ is the accepting run of A^{pr} over σ. Then from the fact that L is prefix-closed, it follows that σ′ ∈ L and hence ŝ ∈ F̂ where ρ̃(σ) = t̂ and ρ̃(σ′) = ŝ. Consequently ((ŝ)_{d}, (t̂)_{d}) ∈⇝_{d}. But then by the induction hypothesis, ρ̃ restricted to prf(σ′) is a run of B^{pr} over σ′. Consequently ρ̃ is a run of B^{pr} over σ = σ′d.

Claim 3 follows at once from the definition of F̃. Hence B^{pr} has the properties required by the lemma. □

With these preparations out of the way, we can now deal with the second half of the proof of theorem 6.1.

Lemma 6.4 Suppose ES is a regular trace structure over (DR, I). Then there exists a finite DR-labelled Petri net LN = (N , lb) such that ES is isomorphic to ES_{LN}.

Proof: Let est(ES) = B and ts(B) = L. B is a regular trace structure by prop. 4.4 and hence B ⊆ T R is recognizable by prop. 2.2. Consequently, by theorem 2.7, there exists a deterministic complete asynchronous automaton A = ({S_{p}}, {→ _{d}}, S_{in}, F) such that L(A) = L. Let A^{pr} = ({Ŝ_{p}}, {R_{d}}, Ŝ_{in}, F̂) and B^{pr} = ({S̃_{p}}, {⇝_{d}}, S̃_{in}, F̃) be the deterministic asynchronous automaton constructed from A as in the proof of the previous lemma. In what follows, we will assume without loss of generality that if p ≠ q then S̃_{p} ∩ S̃_{q} = ∅ and that if a ≠ b then ⇝_{a} ∩ ⇝_{b}= ∅.

We define the DR-labelled finite Petri net LN = (N , lb) with N = (B, E, F, M_{in}) as follows:

• B = S̃ = ⋃_{p} S̃_{p}.

• E = ⋃_{d} ⇝_{d}.

• F = {(s̃(p), (s̃, t̃)) | (s̃, t̃) ∈⇝_{d} and p ∈ loc(d) for some d} ∪{((s̃, t̃), t̃(p)) | (s̃, t̃) ∈⇝_{d} and p ∈ loc(d) for some d}.

• M_{in} = {s̃_{in}(p) | p ∈ P} where S̃ = {s̃_{in}}.

• For each e ∈ E, lb(e) = d provided e ∈⇝_{d}.

By abuse of notation let the unique extension of lb to E^{∗} (with co-domain DR^{∗}) also be denoted lb.

Claim 1 Let τ ∈ E^{∗}. Then τ ∈ F S_{N} iff lb(τ) ∈ L.

Claim 2 Let τ, τ′ ∈ F S_{N}. Then τ ⊑_{I_{N}} τ′ iff lb(τ) ⊑ lb(τ′).

It is tedious but straightforward to prove these two claims. The required result then follows easily. □

Thus theorem 6.1 is now established. A simple consequence is that one can now obtain a similar characterization of regular Σ-labelled trace event structures in terms of finite Σ-labelled Petri nets.

Corollary 6.5 Let ES be a Σ-labelled trace event structure over (DR, I). Then ES is regular iff there exists a finite Σ-labelled Petri net LN = (N , lb) such that ES is isomorphic to ES_{LN}.

Proof: Consider the trace alphabet (D̂R, Î) where D̂R = DR × Σ and Î = {((a, x), (b, y)) | a I b}. Then following the lines of the proof of theorem 6.1, we can easily extract the corollary from theorem 6.4. □

7 Conclusion

In this paper we have introduced the notion of a regular trace event structure. We view trace event structures as a common generalization – in an event-based framework – of trees and Mazurkiewicz traces. As pointed out earlier, the notion of a trace event structure and hence that of a trace structure admitted here is rather generous. Even trace event structures whose underlying prime event structures have an empty conflict relation will be allowed. Surely this is not what one intends when talking about branching time behaviours. In the case of (finite) trees the required branching structure is guaranteed by typing the nodes with arities or by demanding that each node should have all its successors or none of its successors present in the tree. Something similar will have to be done for trace event structure. The possibilities that are available are many. It is not clear at present what is the best way to proceed.

We do not know at present what is the proper monadic second order logic for trace event structures. As mentioned earlier, blind generalization over configurations (i.e. over traces in the setting of trace structures) will at once result in an undecidable logic. Surprisingly enough, it turns out, as pointed out by Walukiewicz [Wal] that a logic over trace event structures which permits quantification over events will also be undecidable. To see this, consider the trace alphabet (DR_{0}, I_{0}) with DR_{0} = {l, m, r} and I_{0} = {(l, r), (r, l)}. Then the events corresponding to the set of prime traces {l^{n_{1}}, r^{n_{2}}m | n_{1} ≥ 0, n_{2} ≥ 0} can be used to code up the two-dimensional grid. Thus we must find a suitable restriction on trace event structures in order to arrive at branching time legics that are decidable and hopefully interesting.

Recently, Huhn and Niebert [HN] have proposed what may be called confusion-free trace event structures as a suitable class of objects. They also formulate a related class of automata and show that the emptiness problem for these automata is decidable. We feel that confusion-freeness is a much too drastic restriction and one should look for a larger class of trace event structures. It is however not clear at present what this larger class ought to be.

Our notion of regular trace event structures gives rise to an interesting conjecture which appears to be difficult to prove. First note that for a prime event structure ES = (E, ≤, #) we can define the equivalence relation R_{ES} ⊆ C_{ES} × C_{ES} via:

c R_{ES} c′ iff ES\c ≡ ES\c′.

(The notion of isomorphism that ≡ captures is the natural one.)

Next we say that e ∈ E is enabled at c ∈ C_{ES} iff e ∉ c and c ∪ {e} ∈ C_{ES}. Let en(c) be the set of events enabled at the configuration c.

Finally, we say that ES is regular iff R_{ES} is of finite index and there exists an integer k such that |en(c)| ≤ k for every c ∈ C_{ES}.

Conjecture The prime event structure ES is regular iff it is isomorphic to the es-unfolding of a finite 1-safe Petri net.

References

[DM] V. Diekert and A. Muscholl: Deterministic Asynchronous Automata for Infinite Traces, Acta Informatica, 31, (1994) 379-397.

[GW] P. Godefroid and P. Wolper: A Partial Approach to Model Checking, Information and Computation, 110 (1994) 305-326.

[HN] M. Huhn and P. Niebert: Towards Automata for branching time and partial order, Proc. of CONCUR’96, LNCS 1119 (1996), 611-627.

[LPRT] K. Lodaya, R. Parikh, R. Ramanujam and P.S. Thiagarajan: A Logical Study of Distributed Transition Systems, Information and Computation, 119 (1995) 91-118.

[MS] M. Mukund and M.S. Sohoni: Keeping track of the latest gossip: Bounded time-stamps suffice, Proc. FST & TSC’93, LNCS 761 (1993) 388-399.

[NPW] M. Nielsen, G. Plotkin and G. Winskel: Petri nets, Event structures and Domains I, Theor. Comput. Sci., 13 (1980) 86-108.

[NW] M. Nielsen and G. Winskel: Trace Structures and other Models for Concurrency, In: V. Diekert and G. Rozenberg (eds.), The Book of Traces, World Scientific, Singapore (1995) 271-305.

[Pel] D. Peled: All from one, one for all: On model checking using representatives. Proceedings of CAV’93, LNCS 697 (1993) 409-424.

[PK] W. Penczek and R. Kuiper: Traces and Logic, In: V. Diekert and G. Rozenberg (eds.), The Book of Traces, World Scientific, Singapore (1995) 307-379.

[Rab] M.O. Rabin: Decidability of second order theories and automata on infinite trees, Trans. Amer. Math. Soc., 141: 1-35, 1969.

[RT] B. Rozoy and P.S. Thiagarajan: Event Structures and Trace Monoids, Theoretical Computer Science, 91 (1991) 285-313.

[Thi] P.S. Thiagarajan: A Trace Based Extension of Linear Time Temporal Logic, Proc. 9th IEEE LICS (1994) 438-447.

[Tho] W. Thomas: Automata on infinite objects, In: J. van Leeuwen (ed.) Handbook of Theoretical Computer Science, Volume B, North-Holland, Amsterdam (1990) 130-191.

[Val] A. Valmari: Stubborn Sets for Reduced State Space Generation, LNCS 483 (1990) 491-515

[Wal] I. Walukiewicz. Private communication.

[Zie] W. Zielonka: Notes on finite asynchronous automata, R.A.I.R.O. – Inf. Théor. et Appl., 21 (1987) 99-135.

Recent Publications in the BRICS Report Series

RS-96-32 P. S. Thiagarajan. Regular Trace Event Structures. September 1996. 34 pp.

RS-96-31 Ian Stark. Names, Equations, Relations: Practical Ways to Reason about ‘new’. September 1996. ii+22 pp.

RS-96-30 Arne Andersson, Peter Bro Miltersen, and Mikkel Thorup. Fusion Trees can be Implemented with AC^{0} Instructions only. September 1996. 8 pp.

RS-96-29 Lars Arge. The I/O-Complexity of Ordered Binary-Decision Diagram Manipulation. August 1996. 35 pp. An extended abstract version appears in Staples, Eades, Kato, and Moffat, editors, Algorithms and Computation: 6th International Symposium, ISAAC ’95 Proceedings, LNCS 1004, 1995, pages 82�91.

RS-96-28 Lars Arge. The Buffer Tree: A New Technique for Optimal I/O Algorithms. August 1996. 34 pp. This report is a revised and extended version of the BRICS Report RS-94-16. An extended abstract appears in Akl, Dehne, Sack, and Santoro, editors, Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS 955, 1995, pages 334�345.

RS-96-27 Devdatt Dubhashi, Volker Priebe, and Desh Ranjan. Negative Dependence Through the FKG Inequality. July 1996. 15 pp.

RS-96-26 Nils Klarlund and Theis Rauhe. BDD Algortihms and Cache Misses. July 1996. 15 pp.

RS-96-25 Devdatt Dubhashi and Desh Ranjan. Balls and Bins: A Study in Negative Dependence. July 1996. 27 pp.

RS-96-24 Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL. July 1996. 20 pp. Presented at DIMACS Workshop SPIN96 � 2nd International SPIN Veri�cation Workshop on Algorithms, Applications, Tool Use, Theory (Rutgers University, New Jersey, USA, August 5,