Information Technology Reference
In-Depth Information
Proposition 2 (
e-non-refusability
).
After event s
.
x has occurred in T
(
P
)
,
no event e
.
x can be refused until e
.
x has occurred:
(
t
u
,
R
):
∀
s
.
x
F
(
T
(
P
))
·
e
.
x
in
u
⇒
e
.
x
/
∈
R
.
Traces are normally used to follow the evolution of a process using the 'after'
operator. Here we instead use failures, so that instances of events are identified
uniquely; as a result the resolution of nondeterministic choices can be observed
directly, without introducing a
τ
operator. For example, evolution of the process
(
a
→
STOP
b
→
STOP
)to
a
→
STOP
is recorded as evolution from
{
(
,
{}
)
,
(
,
{
a
}
)
,
(
,
{
b
}
)
}
to
{
(
,
{}
)
,
(
,
{
b
}
)
}
.
Now instances of two events
x
and
y
are said to be possibly
conflicting
in
P
if they are exclusive at some point (determining the instance) of
P
's evolu-
tion. For example, the events
a
and
b
are conflicting in the initial state of
a
STOP
. The following weak definition of conflict freedom cap-
tures this intuition.
→
STOP
b
→
Definition 1 (
Conflict freedom
).
Events x and y of P are
conflict-free
at
the point determined by
(
t
,
R
):
F
(
P
)
in P if
(
t
,
R
):
R
.
∀
x
F
(
P
)
·
y
/
∈
R
⇒
y
/
∈
Thus the translation
T
ensures:
Proposition 3 (
s-e-conflict freedom
).
The s and e events are conflict-free
throughout T
(
P
)
:
(
t
,
R
)
,
(
t
,
R
):
R
.
∀
e
.
x
F
(
T
(
P
))
·
(
R
∩{|
s
|}
)
⊆
If two non-conflicting events are available at some point then they may be per-
formed concurrently. This is captured by the following proposition.
Definition 2 (
Possible concurrency
).
Let
Σ
x
=
Σ
\{
e
.
x
,
eh
.
x
}
,
∈{
s
,
sh
}
s
,e
(
s
)=
eande
(
sh
)=
eh. The set of all possibly concurrent events
of P is defined:
t
u
:
traces
(
T
(
P
))
,
u
:(
Σ
x
)
∗
·
conc
(
P
)=
{
(
x
,
y
)
|∃
s
.
x
e
(
s
)
.
x
s
.
y
in
u
∨
e
(
s
)
.
y
in
u
}
.
Then event y
:
Σ
P
is said to be
possibly concurrent
with event x
:
Σ
P
in P iff
(
x
,
y
)
∈
conc
(
P
)
.
Search WWH ::
Custom Search