=Paper=
{{Paper
|id=Vol-2240/paper13
|storemode=property
|title=Preserving Behavior in Transition Systems from Event Structure Models
|pdfUrl=https://ceur-ws.org/Vol-2240/paper13.pdf
|volume=Vol-2240
|authors=Irina Virbitskaite,Nataliya Gribovskaya
|dblpUrl=https://dblp.org/rec/conf/csp/VirbitskaiteG18
}}
==Preserving Behavior in Transition Systems from Event Structure Models==
https://ceur-ws.org/Vol-2240/paper13.pdf
Preserving Behavior in Transition Systems
from Event Structure Models?
Nataliya Gribovskaya1 and Irina Virbitskaite1,2
1
A.P. Ershov Institute of Informatics Systems, SB RAS,
6, Acad. Lavrentiev av., 630090 Novosibirsk, Russia
2
Novosibirsk State University, 2, Pirogov av., 630090 Novosibirsk, Russia
{gribovskaya,virb}@iis.nsk.su
Abstract. Two structurally dierent methods of associating transition
system semantics to event structure models are distinguished in the lit-
erature. One of them is based on con gurations (event sets), the other
on residuals (model fragments). In this paper, we consider three kinds
of event structures (resolvable con ict structures, extended prime struc-
tures, stable structures), translate the other models into resolvable con-
ict structures and back, provide the isomorphism results on the two
types of transition systems, and demonstrate the preservation of some
bisimulations on them.
1 Introduction
Since the introduction of event structures in [26], many variants of event-oriented
models have been proposed based on dierent behavioural relations between
events and thus providing a dierent expressive power. Among the models are
prime event structures [26] (with conjunctive1 binary causality, represented by
a partial order and being under the principle of nite causes, and symmetric
irre exive con ict, obeying the principle of con ict heredity; all these guarantee
unique event enablings within the model); extended prime event structures [1]
(with conjuctive binary causality, being possibly with cycles and not being under
the principle of nite causes, and symmetric irre exive con ict, not obeying
the principle of con ict heredity; moreover, the relations can be overlapped);
stable event structures [28] (with non-binary conjuctive causality, allowing for
alternative enablings, and the stability constraint (i.e .the intersection of two
non-con icting causal predecessors sets for an event is a causal predecessors
set for the event) resulting in unique enablings within a con guration); event
structures for resolvable con ict [14] (with dynamic con icts, i.e. con icts can
be resolved or created by the occurrences of other events), etc. Comparative
analysis of some classes of event structures can be found in the works [1, 2, 11,
12, 14, 15, 16, 18].
Two methods of associating a labeled transition system [20] with an event-
oriented model of a distributed system, such as an event structure [26] or a
?
Supported by German Research Foundation through grant Be 1267/14-1.
1
An event is enabled once all of its causal predecessors have occurred.
con guration structure [13], can be distinguished: a con guration-based and a
residual-based method. In the rst case,2 states are understood as sets of events,
called con gurations, and state transitions are built by starting with the empty
con guration and enlarging con gurations by already executed events. In the
second approach,3 states are understood as event structures, and transitions are
built by starting with the given event structure as an initial state and removing
already executed parts thereof in the course of an execution.
In the literature, con guration-based transition systems seem to be predom-
inantly used as the semantics of event structures, whereas residual-based tran-
sition systems are actively used in providing operational semantics of process
calculi and in demonstrating the consistency of operational and denotational se-
mantics. The two kinds of transition systems have occasionally been used along-
side each other (see [18] as an example), but their general relationship has not
been studied for a wide range of existing models. In a seminal paper, viz. [23],
bisimulations between con guration-based and residual-based transition systems
have been proved to exist for prime event structures [28]. The result of [23] has
been extended in [5] to more complex event structure models with asymmetric
con ict. Counterexamples illustrated that an isomorphism cannot be achieved
with the various removal operators de ned in [5, 23]. The paper [6] demon-
strated that the operators can be tightened in such a way that isomorphisms,
rather than just bisimulations, between the two types of transition systems be-
longing to a single event structure can be obtained. A key idea is to employ
non-executable (impossible) events4 if the model allows them (and to introduce
a special non-executable event otherwise), in order to turn model fragments into
parts of states. This idea has been applied by the authors on a wide variety of
event structure models, and for a full spectrum of semantics (interleaving, step,
pomset, multiset). Thanks to the results, a variety of facts known from the lit-
erature on con guration-based transition systems (e.g., [4, 10, 13, 28]) can be
extended to residual-based ones.
The aim of this paper is to connect several models of event structures by
providing behaviour preserving translations between them, and to demonstrate
the retention of some of the bisimulation concepts in the two types of transition
systems associated with the models under consideration.
In Section 2 of this paper, we consider three kinds of event structure mod-
els (resolvable con ict, extended prime, stable event structures), de ne removal
operators for them, and translate the other models into resolvable con ict event
structures and back. Section 3 contains the de nitions of the two types of tran-
sition systems, describes the isomorphism results, and demonstrate the preser-
vation of some bisimulations on the transition systems. Section 4 concludes.
2
E.g., see [1, 2, 11, 12, 14, 15, 17, 18, 24, 27].
3
E.g., see [3, 7, 8, 9, 18, 19, 21, 22, 25].
4
In an event structure, an event is called non-executable or impossible if it does not
occur in any con guration of the structure, i.e. the event is never executed.
2 Event Structure Models
2.1 Event Structures for Resolvable Con ict
In this section, we consider event structures for resolvable con ict, which were
put forward in [14] to give semantics to general Petri nets. A structure for re-
solvable con ict consists of a set of events and an enabling relation ` between
sets of events. The enabling X ` Y with sets X and Y imposes restrictions on
the occurrences of events in Y by requiring that for all events in Y to occur,
their causes the events in X have to occur before. This allows for modeling
the case when a and b cannot occur together until c occurs, i.e., initially a and
b are in con ict until the occurrence of c resolves this con ict. Notice that the
event structure classes under consideration in this paper are unable to model the
phenomena of resolvable con ict. In resolvable con ict structures, the enabling
relation can also model con icts: events from a set Y are in irresolvable con ict
i there is no enabling of the form X ` Y for any set X of events. Further, an
event can be impossible (i.e. non-executable in any system's run) if it has no
enabling or has in nite causes or has impossible causes/prececessors.
De nition 1. An event structure for resolvable con ict (RC -structure) over L
is a tuple E = (E , `, L, l), where E is a set of events; ` ⊆ P(E) × P(E) is the
enabling relation; L is a set of labels; l : E → L is a labeling function.
Let E be an RC -structure over L. For X ⊆ E and e ∈ E , Con(X) ⇐⇒ ∀X b⊆
X : ∃Z ⊆ E : Z ` X b ; f Con(X) ⇐⇒ X is nite and Con(X). The con ict
relation ] ⊆ E × E is given by: d ] e ⇐⇒ d 6= e ∧ ¬Con({d, e}). The direct
causality relation ≺⊆ E × E is de ned as follows: d ≺ e ⇐⇒ ∀X ⊆ E : (X `
e ⇒ d ∈ X). A set X ⊆ E is left-closed i X is nite, and for all X e ⊆ X there
exists X ⊆ X such that X ` X . The set of the left-closed sets of E is denoted as
b b e
LC(E). Clearly, any left-closed set is con ict-free. Let Conf (E) = {{e1 , . . . , en } ⊆
E | n ≥ 0, ∀i ≤ n : ∀X ⊆ {e1 , . . . , ei } : ∃Y ⊆ {e1 , . . . , ei−1 } : Y ` X} be the set
of con gurations of E . Clearly, any con guration X is a left-closed set but not
conversely.
Consider some properties of resolvable con ict event structures.
De nition 2. An RC -structure E = (E, `, L, l) is called
rooted i (∅, ∅) ∈ `;
pure i X ` Y ⇒ X ∩ Y = ∅;
singular i X ` Y ⇒ X = ∅ ∨ | Y |= 1;
manifestly conjunctive i there is atTmost one X with X ` Y , for all Y ⊆ E ;
conjuctive i Xi ` Y (i ∈ I 6= ∅) ⇒ i∈I Xi ` YS;
locally conjuctive i Xi ` Y (i ∈ I 6= ∅) ∧ Con( i∈I Xi ∪ Y ) ⇒ i∈I Xi ` Y ;
T
with nite causes i X ` Y ⇒ Xisf inite;
with binary con ict i | X |> 2 ⇒ ∅ ` X ;
in the standard form i ` = {(A, B) | A ∩ B = ∅, A ∪ B ∈ LC(E)};
2-coherent i X ∪ Y ∈ LC(E), for all X, Y ∈ LC(E) s.t. X ∪ Y ⊆ Z ∈
LC(E).5
5
This property is useful when proving Theorem 1.
Lemma 1. An RC -structure E = (E, `, L, l) can be transformed into:
a pure RC -structure P U (E) = (E, `,
b L, l)6 s.t. Conf (E) = Conf (P U (E)), if
E is a singular RC -structure;
an RC -structure SF (E) = (E, `,
e L, l)7 in the standard form s.t. LC(E) =
LC(SF (E)). Moreover, Conf (E) = Conf (SF (E)), if E is a pure RC -structure.
Example 1. As an example, consider the pure, manifestly conjuctive, non-singular,
non-2-coherent RC -structure E rc = (E rc , `rc , L, lrc ) with nite causes and bi-
nary con ict from [15], where E rc = {a, b, c}; `rc consists of ∅ ` X for all
X 6= {a, b} and {c} ` {a, b}; L = E rc ; and lrc is the identity labeling function.
It is easy to see that LC(E rc ) = Conf (E rc ) = {∅, {a}, {b}, {c}, {a, c}, {b, c},
{a, b, c}}. This RC -structure models the initial con ict between the events a
and b that can be resolved by the occurrence of the event c. The structure E rc
can be presented in the standard form Eerc with ` erc consisting of A `e B such
rc
that B ⊆ C ∈ LC(E) and A = C \ B , i.e. ` e = {(∅, ∅), (∅, {a}), ({a}, ∅),
(∅, {b}), ({b}, ∅), (∅, {c}), ({c}, ∅), (∅, {a, c}), ({a, c}, ∅), ({a}, {c}), ({c}, {a}),
. . ., (∅, {a, b, c}), ({a, b, c}, ∅)}.
The standard form of RC -structures and the ability to specify impossible
events in the model allows for developing a relatively simple structural de nition
of a removal operator which is necessary for residual semantics.
De nition 3. For an RC -structure E = (E , `, L, l) in the standard form and
X ∈ LC(E), a removal operator is de ned as follows: E \ X = (E 0 , `0 , L, l0 ),
where
E0 = E \ X
`0 = {(A0 , B 0 ) | ∃(A, B) ∈ ` s.t. A0 = A∩E 0 , B 0 = B∩E 0 , (A0 ∪B 0 ∪X) ∈ LC(E)}
l 0 = l |E 0
According to the de nition above, all the events in X are removed; however, we
retain the events, not forming left-closed sets with the events in X and hence
con icting with some events in X , making the retained events impossible by
deleting their enabling relations.
From now on, we use Erc L to denote the class of rooted, singular, locally
conjuctive RC -structures with binary con ict.
2.2 Extended Prime Event Structures
For reasons of exibility, the authors of [1] propose to generalise ordinary prime
event structures [28]8 by dropping the transitivity and acyclicity of causality,
6
An RC -structure P U (E) = (E, `,
b L, l) can be directly obtained by putting ` b = `
\{(A, B) ∈ `| ∅ 6= B ⊆ A}.
7
An RC -structure SF (E) = (E, `,e L, l) can be directly obtained by putting ` e =
{(A, B) | B ⊆ C ∈ LC(E), A = C \ B}.
8
A labeled prime event structure over a set L of actions is a tuple E = (E, ], ≤, L, l),
where E is a set of events; ≤ ⊆ E × E is a partial order (the causality relation),
as well as the principles of nite causes and con ict inheritance.9 As opposed
to prime event structures, the extended version allows for impossible events. In
this model, events can be impossible because of enabling cycles, or an overlap-
ping between the enabling and the con ict relation, or because of impossible
causes/predecessors.
De nition 4. An extended prime event structure (EP -structure) over L is a
triple E = (E, ], ≺, L, l), where E is a set of events; ] ⊆ E × E is an irre exive
symmetric relation (the con ict relation); ≺⊆ E × E is the enabling relation; L
is a set of labels; l : E → L is a labeling function. Let EepL denote the class of
EP -structures over L.
Let E = (E , ], ≺, L, l) be an EP -structure. For e ∈ E , de ne ↓ e as a maximal
subset of E such that ∀e0 ∈↓ e : e0 ≺ e. For X ⊆ E , let ](X) = {e0 ∈ E | ∃e ∈
X : e ] e0 }. We call a set X ⊆ E a con guration of E if X is nite, con ict-free
(i.e. ∀e, e0 ∈ X : ¬(e ] e0 )), left-closed (i.e. ∀e, e0 ∈ E : e ≺ e0 ∧ e0 ∈ X ⇒ e ∈ X ),
and does not contain enabling cycles (i.e., 6 ∃e1 , . . . , en ∈ X : e1 ≺ . . . ≺ en ≺ e1
(n ≥ 1)). The set of con gurations of E is denoted by Conf (E).
In the graphical representation of an EP -structure, pairs of events related
by the enabling relation are connected by arrows; pairs of the events included in
the con ict relation are marked by the symbol ].
E ep : b ] a c
Fig. 1. An extended prime event structure E ep
Example 2. Figure 1 depicts the EP -structure E ep over L = {a, b, c}, with
E ep = L; ]ep = {(a, b), (b, a)}; ≺ep = {(a, c)}; and the identity labeling func-
tion lep . Observe that the principle of con ict inheritance is violated. The set of
con gurations of E ep is {∅, {a}, {b}, {a, c}}.
Consider the de nition of the removal operator for EP -structures.
De nition 5. For E ∈ Eep
L and X ∈ Conf (E), a removal operator is de ned as
follows: E \ X = (E 0 , ≺0 , ]0 , L, l0 ), with
E0 = E\X
]0 = ] ∩ (E 0 × E 0 )
≺0 = (≺ ∩ (E 0 × E 0 )) ∪ {(e, e) | e ∈ ](X)}
l0 = l |E 0
satisfying the principle of nite causes: ∀e ∈ E : bec = {e0 ∈ E | e0 ≤ e} is nite;
] ⊆ E × E is an irre exive and symmetric relation (the con ict relation), satisfying
the principle of hereditary con ict: ∀e, e0 , e00 ∈ E : e ≤ e0 and e ] e00 then e0 ] e00 ; and
l : E → L is a labeling function.
9
It was noted in [1] that, as far as nite con gurations are concerned, this does not
lead to an increase in expressive power.
We see that the events in X are removed, yielding a reduction of the enabling and
con ict relations. At the same time, any event con icting with some event in X
is retained, equipping it with an enabling cycle, thereby making the con icting
event impossible.
Translate EP -structures into RC -structures and conversely. For an EP -
structure EP = (E , ], ≺, L, l), de ne RC(EP ) = (E 0 = E, `0 ,L, l = l0 ), where
either Y = {e}, X =↓ e,
X `0 Y ⇐⇒ or Y = {e, e0 }, e 6= e0 , ¬(e ] e0 ), X = ∅,
or | Y |6= 1, 2, X = ∅.
For an RC -structure RC = (E 0 , `0 , L, l0 ), let EP(RC) = (E 00 = E 0 , ]00 = ]0 ,
≺ =≺0 , L, l00 = l0 ).
00
Lemma 2. (i) For EP an EP -structure, RC(EP ) is a rooted, singular, man-
ifestly conjuctive RC -structure with binary con ict such that Conf (EP ) =
Conf (RC(EP )).
(ii) For RC a rooted, singular, conjuctive RC -structure with binary con ict,
EP(RC) is an EP -structure such that Conf (RC) = Conf (EP(RC)).
2.3 Stable Event Structures
Stable event structures, introduced in the work of Winskel [27] in order to over-
come the unique enabling problem of prime event structures, have an enabling
relation indicating which (usually nite) sets X of events are possible prerequi-
sites of a single event e, written X ` e. We consider the version of stable event
structures of [28] where the con ict relation is speci ed for sets with two events.
De nition 6. A stable event structure over L (S -structure) is a tuple E = (E,
], `, L, l), where
E is a set of events;
] ⊆ E × E is an irre exive, symmetric relation (the con ict relation). We
shall write Con for the set of nite con ict-free subsets of E , i.e. those nite
subsets X ⊆ E for which ∀e, e0 ∈ X : ¬(e ] e0 ). X ∈ Con means that the
events in X could happen in the same run, i.e. they are consistent;
` ⊆ Con×E is the enabling relation which satis es X ` e and X ⊆ Y ∈ Con
⇒ Y ` e; and, moreover, X ` e, Y ` e, and X ∪ Y ∪ {e} ∈ Con ⇒ X ∩ Y ` e
(the stability principle). ` indicates possible causes: an event e can occur
whenever for some X with X ` e all events in X have occurred before. The
minimal enabling relation `min is de ned as follows: X `min e i X ` e and
for all Y ⊆ X if Y ` e then Y = X ;
L is a set of actions;
l : E → L is a labeling function.
Let EsL denote the class of S -structures over L.
A set X ⊆ E is a con guration of an S -structure E i X is nite, con ict-free
(i.e., X ∈ Con), and secured (i.e., there are e1 , . . . , en such that X = {e1 , . . . , en }
and {e1 , . . . , ei } ` ei+1 , for all i < n). The set of con gurations of E is denoted
Conf (E). For an S -structure E , X ∈ Conf (E), and e, e0 ∈ X , let e0 ≺X e i e0
belongs to the smallest subset Y of X with Y ` e.
Example 3. Consider the S -structure E s over L = {a, b, c, d}, with E s = L;
]s = {(a, b), (b, a)}; `smin = {(∅, a), (∅, b), (∅, c), ({a}, d), ({b, c}, d)}; and the
identity labeling function ls . The set of con gurations of E s is {∅, {a}, {b},
{c}, {a, c}, {b, c}, {a, d}, {a, c, d}, {b, c, d}}. Notice that E s is not a ow event
structure because the event c not con icting with the event a may be a cause
for d or may not.
De nition 7. For E = (E , ], `, L, l) ∈ EsL and X ∈ Conf (E), a removal
operator is de ned as follows: E \ X = (E 0 , ]0 , `0 , L, l0 ), with
E0 = E \ X
]0 = ] ∩ (E 0 × E 0 )
`0 = {(W 0 , e) | W 0 ∈ Con0 , ∃(W 00 , e) ∈ `0min s.t. W 00 ⊆ W 0 } where
`0min = {(W 00 , e) | ∃(W, e) ∈ `min s.t. W 00 = W ∩ E 0 , e ∈ E 0 ,
W 00 ∪ X ∈ Con, {e} ∪ X ∈ Con}
0
l = l |E 0
We see that all the events in X are deleted; the con ict relation ]0 contains the
pairs of remaining con icting events; the de nition of `0 is based on that of `0min ,
which consists of the pairs from ` without the pairs whose events con ict with
some event in X , thereby making them impossible.
For an S -structure S = (E, ], `, L, l), let RC(G) = (E 0 = E, `0 ,L, l0 ), where
either Y = {e}, e ∈ E, X ` e,
X `0 Y ⇐⇒ or | Y |= 2, Y ∈ Con, X = ∅,
or | Y |6= 1, 2, X = ∅.
For an RC -structure RC = (E 0 , `0 ,L, l0 ), let S(RC) = (E 00 = E 0 , ]00 =
] , `00 ,L, l00 ), where X `00 e ⇐⇒ e ∈ E 0 , X ⊆ E 0 , f Con0 (X), and ∃Y ⊆
0
X : Y `0 {e}.
Lemma 3. [15]
(i) For S an S -structure, RC(S) is a rooted, singular, locally conjuctive RC -
structure with nite causes and binary con ict s.t. Conf (S) = Conf (RC(F )).
(ii) For RC a rooted, singular, locally conjuctive RC -structure with nite causes
and binary con ict, S(RC) is an S -structure s.t. Conf (RC) = Conf (S(RC)).
2.4 Dierent Semantics
In this subsection, we de ne dierent semantics for the event structure models
under consideration. From now on, we treat E as an event structure over L
speci ed in De nitions 1, 4, and 6, if not de ned otherwise. Moreover, let EL =
Eep
L ∪ EL ∪ EL .
s rc
We rst introduce auxiliary notations. Given con gurations X, X 0 ∈ Conf (E),
we write:
X →int X 0 i X ⊆ X 0 and X 0 \ X = {e};
X →step X 0 i X ⊆ X 0 and X 00 ∈ Conf (E), for all X ⊆ X 00 ⊆ X 0 ;
X →pom X 0 i X ⊆ X 0 and ≤X 0 \X is a partial order;
X →whp X 0 i X ⊆ X 0 and ≤X 0 is a partial order.
For ? ∈ {int, step, pom}, a con guration X ∈ Conf (E) is a con guration in
?-semantics of E i ∅ →∗? X , where →∗? is the re exive and transitive closure of
→? . Let Conf ? (E) denote the set of con gurations in ?-semantics of E .
Lemma 4. Given an event structure E ∈ EL and ?, ∗ ∈ {int, step, pom},
(i) for a con guration X ∈ Conf (E), the transitive and re exive closure of ≺X ,
≤X , is a partial order. Let EdX = (X, ≤X , L, l |X );
(ii) Conf (E) = Conf ? (E) = Conf ∗ (E).
Given ? ∈ {int, step, pom}, an event structure E over L, and con gurations
X, X 0 ∈ Conf ? (E) such that X →? X 0 , we write:
lint (X 0 \ X) = a i X 0 \ X = {e} and l(e) = a, if ? = int;
lstep (X 0 \ X) = M i M (a) = |{e ∈ X 0 \ X | l(e) = a}|, for all a ∈ L, if
? = step;
lpom (X 0 \ X)=Y i Y = [(X 0 \ X, ≤X 0 ∩(X 0 \ X × X 0 \ X), L, l |X 0 \X )], if
? = pom;
lwhp (X)=Y i Y = [(X, ≤X , L, l |X )].
Let E be an event structure over L and X = {e1 , . . . , en } ∈ Conf int (E)
(n ≥ 0). We call e1 . . . en a derivation of X i X0 = ∅ →int X1 . . . Xn−1 →int
Xn = X , and Xi \ Xi−1 = {ei }, for all 1 ≤ i ≤ n. A derivation e1 . . . en
of X ∈ Conf int (E) and a derivation f1 . . . fn of X 0 ∈ Conf int (E 0 ) are equal
(denoted e1 . . . en ∼ f1 . . . fn ) i there is an isomorphism ι : EdX → E 0 dX 0
with ι(e1 . . . en ) := ι(e1 ) . . . ι(en ) = f1 . . . fn . Let Der(X) denote the set of all
equivalence classes [e1 . . . en ] of derivations of X . For [e1 . . . en ] ∈ Der(X), de ne
lhp ([e1 . . . en ]) := a1 . . . an , where li (ei ) = ai (1 ≤ i ≤ n).
3 Transition Systems TC (E) and TR(E)
3.1 De nitions and Comparisons
In this subsection, we rst give some basic de nitions concerning labeled transi-
tion systems, and then de ne the mappings TC (E) and TR(E), which associate
two distinct kinds of transition systems one whose states are con gurations
and one whose states are residual event structures with an event structure E
over L.
A transition system T = (S, →, i) over a set L of labels consists of a set of
states S , a transition relation →⊆ S × L × S , and an initial state i ∈ S . Two
transition systems over L are isomorphic if their states can be mapped one-to-
one to each other, preserving transitions and initial states. We call a relation
R ⊆ S × S 0 a bisimulation between transition systems T and T 0 over L i
(i, i0 ) ∈ R, and for all (s, s0 ) ∈ R and l ∈ L: if (s, l, s1 ) ∈→, then (s0 , l, s01 ) ∈→
and (s1 , s01 ) ∈ R, for some s01 ∈ S 0 ; and if (s0 , l, s01 ) ∈→, then (s, l, s1 ) ∈→ and
(s1 , s01 ) ∈ R, for some s1 ∈ S .
Introduce additional auxiliary notations. For a xed set L of labels of event
structures, de ne Lint := L, Lpom := P omL (the set of isomorphic classes of
partial orders labeled over L), and LDer := L∗ , being another sets of labels of
the transition systems.
We are ready to de ne labeled transition systems with con gurations as
states.
De nition 8. For an event structure E over L and ? ∈ {int, step, pom},
TC ? (E) is the transition system (Conf ? (E), +? , ∅) over L? , where X +? X 0
p
i X →? X and p = l? (X \ X);
0 0
TC whp (E) is the transition system (Conf int (E), +whp , ∅) over Lpom , where
X +whp X 0 i X →whp X 0 and p = lwhp (X 0 );
p
TC hp (E) is the transition system ({Der(X) | X ∈ Conf int (E)}, +hp , )
over LDer , where [e1 . . . en ] +hp [e1 . . . en en+1 ] (n ≥ 0) i {e1 , . . . , en },
q
{e1 , . . . , en , en+1 } ∈ Conf int (E), and q = lhp ([e1 . . . en en+1 ]).
Consider the de nition of labeled transition systems with residuals as states.
De nition 9. For an event structure E over L and ? ∈ {int, step, pom},
Reach? (E) = {F | ∃E0 , . . . , Ek (k ≥ 0) s.t. E0 = E , Ek = F , and Ei *X
? Ei+1
(i < k)}, where Ei *X ? Ei+1 i ∃X ∈ Conf ? (Ei ) : Ei+1 = Ei \ X and ∅ →? X
in Ei ;
TR ? (E) is the transition system (Reach? (E), *? , E) over L? , where F *?
p
F 0 i ∃X ∈ Conf ? (F) : F *X ? F and p = l? (X);
0
TR whp (E) is the transition system (Reachint (E), *whp , E) over Lpom , where
F *whp F 0 i ∃X, X 0 ∈ Conf int (E) : F = E \ X, F 0 = E \ X 0 , X +whp X 0 ,
p
and p = lwhp (X 0 );
TR hp (E) is the transition system (Reachint (E), *hp , E) over Lpom , where
F *hp F 0 i ∃X, X 0 ∈ Conf int (E) : F = E \ X , F 0 = E \ X 0 , [e1 . . . en ] +hp
q q
[e1 . . . en en+1 ], where [e1 . . . en ] ∈ Der(X), [e1 . . . en en+1 ] ∈ Der(X 0 ), and
q = l([e1 . . . en en+1 ]).
For instance, Figures 24 indicate the transition systems TR ? (E) with the
states the residuals of the structures considered in Examples 13, respectively.
Here, ? = step, if E = E rc ; ? = whp, if E = E ep ; and ? = pom, if E = E s .
Theorem 1. Given ? ∈ {int, step, pom, whp}, TC ? (E) and TR ? (SF (P U (E)))
(TR ? (E)) are isomorphic; however, TC hp (E) and TR hp (SF (P U (E))) (TR hp (E))
are not bisimilar; where E ∈ Erc
L (E ∈ EL ∪ EL ).
ep s
It is easy to see that even for the EP -structure E1ep over L = {a, b, c}, with
E1 = L;, ]ep
ep ep ep
1 = ∅, →1 = {(a, c), (b, c)}, and the identity labeling function l1 ,
ep ep
TC hp (E1 ) and TR hp (E1 ) are not bisimilar.
From Lemmas 1, 2, 3, and Theorem 1 we get
E = {b, c} c E = {b}
LC(E \ {a}) = LC(E \ {a, c}) =
= {∅, {c}, {b, c}} = {∅, {b}}
c
a a|| a b
E = {a, b, c}
LC(E) = {∅, {a}, c E = {a, b} a||b E = ∅
LC(E \ {c}) =
{b}, {c}, {a, c}, LC(E \ {a, b, c}) = {∅}
= {∅, {a}, {b}, {a, b}}
{b, c}, {a, b, c}}
b b|| b a
c
E = {a, c} E = {a}
LC(E \ {b}) = LC(E \ {b, c}) =
= {∅, {c}, {a, c}} c = {∅, {a}}
Fig. 2. The residual transition system TR step (E rc )
a c b
c
a; a; c
b
b ] a c
b c
a
Fig. 3. The residual transition system TR whp (E ep )
E = {a, b, d}
E = {b}
d E = {b, d} a `min = {(∅, a), (∅, b), b E = {a, d}
d E = {a}
`min = ∅ `min = {(∅, d)} `min = {(∅, d)} `min = ∅
({a}, d), ({b}, d)}
] = ∅ ] = ∅ ] = ∅ ] = ∅
] = {(a, b), (b, a)}
c|| a||
c
c d c c c c
b||
E = {a, b, c, d} E = {a, c, d}
E = {b, c} E = {b, c, d}
`min = {(∅, a), (∅, b), (∅, c), `min = {(∅, c),
`min = {(∅, c)} `min = {(∅, c), (∅, d)}
({a}, d), ({b, c}, d)} ({c}, d)}
] = ∅ d ] = ∅ a ] = {(a, b), (b, a)}
b ] = ∅
a; d
(a; d)||c (b||c); d
Fig. 4. The residual transition system TR pom (E s )
Corollary 1. Given ? ∈ {int, step, pom, whp},
(i) TR ? (E) and TR ? (SF (P U (RC(E)))) are isomorphic, if E ∈ Eep
L ∪ EL ;
s
(ii) TR ? (SF (P U (E))), TR ? (EP(E)), and TR ? (S(E)) are isomorphic, if E ∈ Erc
L.
3.2 Preserving Bisimulations by the Operators TC (·) and TR(·)
We rst introduce bisimulation concepts on the event structure models.
Event structures E and E 0 from EL are interleaving, step, pomset, respec-
tively, bisimilar i TC (E? ) and TC (E?0 ) are bisimilar for ? ∈ {int, step, pom},
respectively. For event structures E and E 0 over L,
a relation R ⊆ Conf int (E) × Conf int (E 0 ) is called weak history preserving
bisimulation i (∅, ∅) ∈ R and for any (X, Y ) ∈ R it holds:
• there is an isomorphism between EdX and E 0 dY ;
• if X ⊆ X 0 for some X 0 ∈ Conf int (E), then Y ⊆ Y 0 for some Y 0 ∈
Conf int (E 0 ) such that (X 0 , Y 0 ) ∈ R;
• if Y ⊆ Y 0 for some Y 0 ∈ Conf int (E 0 ), then X ⊆ X 0 for some X 0 ∈
Conf int (E) such that (X 0 , Y 0 ) ∈ R.
a relation R consisting of triples (X, f, Y ), where X ∈ Conf int (E), Y ∈
Conf int (E 0 ), and f : EdX → E 0 dY is an isomorphism, is called history pre-
serving bisimulation i (∅, ∅, ∅) ∈ R and for any (X, f, Y ) ∈ R it holds:
• if X ⊆ X 0 for some X 0 ∈ Conf int (E), then Y ⊆ Y 0 for some Y 0 ∈
Conf int (E 0 ) such that f 0 |X = f for some isomorphism f 0 : X 0 → Y 0 , and
(X 0 , f 0 , Y 0 ) ∈ R;
• if Y ⊆ Y 0 for some Y 0 ∈ Conf int (E 0 ), then X ⊆ X 0 for some X 0 ∈
Conf int (E) such that f 0 |X = f for some isomorphism f 0 : X 0 → Y 0 , and
(X 0 , f 0 , Y 0 ) ∈ R.
Theorem 2. Given E, E 0 ∈ EL , E and E 0 are weak history preserving bisimi-
lar i T Cwhp (E) and T Cwhp (E 0 ) are bisimilar; E and E 0 are history preserving
bisimilar i T Chp (E) and T Chp (E 0 ) are bisimilar.
Corollary 2. E and E 0 are interleaving, step, pomset, weak history preserving,
respectively, bisimilar i TR ? (ST (P U (E))) and TR ? (ST (P U (E 0 ))) (TR ? (E) and
TR ? (E 0 )) are bisimilar for ? ∈ {int, step, pom, whp}, respectively, where E, E 0 ∈
L (E, E ∈ EL ∪ EL ).
0 ep
Erc s
4 Concluding Remarks
In this paper, we have de ned two structurally dierent ways of giving various
(interleaving, step, pomset, weak history preserving, history preserving) transi-
tion system semantics in the context of three event-oriented models extended
prime event structures, stable event structures, and resolvable con ict structures.
For each model, we have obtained an isomorphism between the corresponding
transition systems for all the semantics except for history preserving one. Also,
we have developed some translations of the event structures from the classes un-
der consideration into resolvable con ict structures and back, so as to compare
residual-based transition systems, constructed from the original structures, with
the ones constructed from the structures obtained after translation. Further,
we have demonstrated that interleaving, step, pomset, weak history preserving
bisimulations are captured by the corresponding bisimulations on the transtion
systems.
Work on extending our approach (e.g., to precursor [9], probabilistic [29],
local [17], dynamic [1] event structures, and to labeled event structures with
invisible actions) is presently under way and has yielded promising intermediate
results. Another future line of research is to extend our results on comparing two
kinds of transition systems to the non-pure case of resolvable con ict structures
[14] and to the multiset transition relation.
References
1. Arbach, Y., Karcher, D., Peters, K., Nestmann, U.: Dynamic causality in
event structures. Lecture Notes in Computer Science 9039 (2015) 8397.
2. Armas-Cervantes, A., Baldan, B., Garcia-Banuelos, L.: Reduction of event
structures under history preserving bisimulation. J. Log. Algebr. Meth. Program.
85(6) (2016) 1110-1130.
3. Baier, C., Majster-Cederbaum, M.: The connection between event structure
semantics and operational semantics for TCSP. Acta Informatica 31 (1994).
4. Baldan, P., Corradini, A., Gadducci, F.: Domains and event structures for
fusions. LICS 2017: 1-12
5. Best, E., Gribovskaya, N., Virbitskaite, I.: Con guration- and residual-
based transition systems for event structures with asymmetric con ict. Proc. Sof-
Sem 2017, Lecture Notes in Computer Science 10877 (2018) 117-139.
6. Best, E., Gribovskaya, N., Virbitskaite, I.: From Event-Oriented Models
to Transition Systems. Proc. Petri Nets 2018, Lecture Notes in Computer Science
10139 (2017) 132146.
7. Boudol, G.: Flow event structures and ow nets. Lecture Notes in Computer
Science 469 (1990) 6295.
8. Crafa, S., Varacca, D., Yoshid, N.: Event structure semantics of parallel
extrusion in the pi-calculus. Lecture Notes in Computer Science 7213 (2012) 225
239.
9. Fecher, H., Majster-Cederbaum, M.: Event structures for arbitrary disrup-
tion. Fundamenta Informaticae 68(1-2) (2005) 103130.
10. van Glabbeek, R.J.: History preserving process graphs. Report, Stanford Uni-
versity, available at http://boole.stanford.edu/ rvg/pub/abstracts/history.
11. van Glabbeek, R.J.: On the expressiveness of higher dimensional automata.
Theoretical Computer Science 356(3) (2006) 265290.
12. van Glabbeek R.J., Goltz U.: Re nement of actions and equivalence notions
for concurrent systems. Acta Informatica 37 (2001) 229327.
13. van Glabbeek R.J., Plotkin G.D.: Con guration structures. Proc. LICS 1995:
199-209
14. van Glabbeek R.J., Plotkin G.D.: Event structures for resolvable con ict.
Lecture Notes in Computer Science 3153 (2004) 550561.
15. van Glabbeek R.J., Plotkin G.D.: Con guration structures, event structures
and Petri nets. Theoretical Computer Science 410(41) (2009) 4111-4159.
16. van Glabbeek, R.J., Vaandrager F.W.: Bundle event structures and CCSP.
Lecture Notes in Computer Science 2761 (2003) 5771.
17. Hoogers, P.W., Kleijn, H.C.M., Thiagarajan, P.S.: An event structure se-
mantics for general Petri nets. Theoretical Computer Science 153 (1996) 129170.
18. Katoen, J.-P.: Quantitative and qualitative extensions of event structures. PhD
Thesis, Twente University, 1996.
19. Katoen, J.-P., Langerak, R., Latella, D.: Modeling systems by probabilistic
process algebra: an event structures approach. IFIP Transactions C-2 (1993) 253
268.
20. Keller, R.M.: Formal veri cation of parallel programs. Communications of the
ACM, vol 19 nr 7 (1976) 371384.
21. Langerak, R.: Bundle event structures: a non-interleaving semantics for LOTOS.
Formal Description Techniques V. IFIP Transactions C-10 (1993) 331346.
22. Loogen, R., Goltz, U.: Modelling nondeterministic concurrent processes with
event structures. Fundamenta Informatica 14(1) (1991) 3974.
23. Majster-Cederbaum, M., Roggenbach, M.: Transition systems from event
structures revisited. Information Processing Letters 67(3) (1998) 119-124.
24. Nielsen M., Plotkin G., Winskel G.: Petri nets, event structures and domains.
Theoretical Computer Science, 13(1) (1981) 8508.
25. Nielsen M., Thiagarajan P.S.: Regular event structures and nite Petri nets:
the con ict-free case. Lecture Notes in Computer Science 2360 (2002) 335351.
26. Winskel G.: Events in computation. PhD Thesis, University of Edinburgh, 1980.
27. Winskel G.: Event structures. Lecture Notes in Computer Science 255 (1986)
325392.
28. Winskel G.: Introduction to event structures. Lecture Notes in Computer Science
354 (1989) 364397.
29. Winskel, G.: Distributed probabilistic and quantum strategies. Electronic Notes
in Theoretical Computer Science 298 (2013) 403425.