LINK DOWNLOAD MIỄN PHÍ TÀI LIỆU "Tài liệu Regular Trace Event Structures doc": http://123doc.vn/document/1050105-tai-lieu-regular-trace-event-structures-doc.htm
ics 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 “event-
based” 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)whereDR 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 re-
lation ∼
I
. It is the least equivalence relation contained in DR
∗
×DR
∗
which
satisfies:
• If σ, σ
∈ DR
∗
and (a, b) ∈ I then σabσ
∼
I
σbaσ
.
3
The ∼
I
-equivalence classes are called (finite Mazurkiewicz) traces. [σ]
∼
I
will denote the ∼
I
-equivalence class containing σ.WeletTR(DR, I)bethe
set of traces over (DR, I). In other words, TR(DR, I)=DR
∗
/∼
I
.Where
(DR, I) is clear from the context, we will write [σ] instead of [σ]
∼
I
and we
will write TR instead of TR(DR, I).
Example 1.1 (cont.) Let TR
0
be the set of traces over (DR
0
,I
0
). Then
{lrm, rlm} is a member of TR
0
. Note also that [lmr]={lmr}. ✷
Traces can be ordered in an obvious way. This ordering relation
(DR,I)
⊆ TR×TR 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 TR.
Example 1.1 (cont.) In TR
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 ⊆ TR(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.
✷
4
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 ⊆
TR(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. ✷
[]
①
①
①
①
①
①
①
①
①
①
❉
❉
❉
❉
❉
❉
❉
❉
❉
[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
5
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 TR.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 TR 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
TR
→2
DR
∗
given by
ts(
ˆ
L)=
{[σ]|[σ]∈
ˆ
L}.
Clearly, for every
ˆ
L ⊆ TR, ts(
ˆ
L)isanI-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 ⊆ TRbe a trace structure and σ ∈ B. Then B
σ
= {σ
| σσ
∈ B}.
(ii) The equivalence relation R
B
⊆ B ×B is given by:
σR
B
σ
iff B
σ
= B
σ
.
6
(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 moti-
vation, 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,)isregulariffBis a
recognizable subset of TR. It will be convenient to first bring this out in a
more formal fashion.
We say that
ˆ
L ⊆ TR is recognizable iff ts(
ˆ
L) is a recognizable (equiv-
alently, regular) subset of DR
∗
.ForL⊆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 ⊆ TR is recognizable. ✷
For the event-based characterization we are after, it is necessary to define
so-called prime elements of TR. Suppose σ = .Thenlast(σ) 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 TR
0
, [llrm] is prime but [lmlr] is not. ✷
7
For each σ , we define pr(σ)={σ
|σ
is prime and σ
σ}.Ofcourse,
pr(σ)=∅only if σ = . Finally, for
ˆ
L ⊆ TR we set pr(
ˆ
L)=
σ∈
ˆ
L
pr(σ).
It turns out prime traces constitute the building blocks of the poset of
traces (TR,). To bring this out, let the compatibility relation ↑⊆ TR×TR
be defined as: σ ↑ σ
iff there exists σ
such that σ σ
and σ
σ
. Further,
if X ⊆ TR then X will denote the l.u.b. of X (under )inTR if it exists.
The next set of results have been assembled from [NW].
Proposition 2.4
(i) Suppose X ⊆ TRsuch 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 TR.
Then X ∈ B.
(iv) Let B be a trace structure and σ ∈ TR. Then σ ∈ B iff pr(σ) ⊆ B.
The rest of the section will be devoted to establishing the following char-
acterization 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.
8
Proof: Let L = ts(B). Then L is recognizable and hence there exists a de-
terministic finite state automaton A operating over DR such that L(A), the
language recognized by A,isL. 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
Dd}.
•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 theo-
rem [Zie] and the gossip automaton [MS]. For presenting Zielonka’s theorem
we need to introduce asynchronous automata operating over distributed al-
phabets. 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 func-
tion 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
˜
Σ
)whereI
˜
Σ
⊆Σ×Σ is obtained via: xI
˜
Σ
yiff
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 max-
imal D-cliques. For our specific trace alphabet (DR, I)wecallp⊆DR a
maximal D-clique in case p is a maximal subset of DR with the property
p × p ⊆ D.WeletP={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.ForQ={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.
9
P, viewed as the names of a set of processes gives rise to the distributed
alphabet
DR = {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
DR 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
DR
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
.Inboth
cases, we shall often write {X
p
} and {Y
d
} respectively.
An asynchronous automaton over
DR = {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.WeletS
Q
denote the set of Q-
states 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
DR = {DR
p
}. Hence we will almost
always suppress mention of
DR and write loc instead of loc
DR
.
10
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.Thens
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 ⊆ TR 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(σ)andlast(σ
) ∈ p}.Notingthat∅ = {}, it follows easily that
↓
p
(σ) is well-defined for every σ.
The next set of observations follows easily from the definitions and [NW].
11
Proposition 2.8
(i) For every σ, σ =
p∈P
↓
p
(σ).
(ii) Suppose B is a trace structure and σ ∈ TR. 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
: TR×P→Qis defined as:
latest
Q
(σ, p)=ˆqprovided ˆ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 com-
plete asynchronous automaton
A
Γ
=({Γ
p
},{⇒
d
}, Γ
in
, Γ
P
)
such that for each Q = {i
1
,i
2
, ,i
n
}⊆Pthere exists an effectively com-
putable function gossip
Q
=Γ
i
1
×Γ
i
2
×Γ
i
n
×P→Qsuch 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 au-
tomaton, a second asynchronous automaton A
pr
with the following property.
12
Không có nhận xét nào:
Đăng nhận xét