Two structurally dierent methods of associating transition system semantics to event structure models are distinguished in the literature. One of them is based on congurations (event sets), the other on residuals (model fragments). In this paper, we consider three kinds of event structures (resolvable conict structures, extended prime structures, stable structures), translate the other models into resolvable conict structures and back, provide the isomorphism results on the two types of transition systems, and demonstrate the preservation of some bisimulations on them.
conguration structure [
In the literature, conguration-based transition systems seem to be
predominantly used as the semantics of event structures, whereas residual-based
transition systems are actively used in providing operational semantics of process
calculi and in demonstrating the consistency of operational and denotational
semantics. The two kinds of transition systems have occasionally been used
alongside each other (see [
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
models (resolvable conict, extended prime, stable event structures), dene removal
operators for them, and translate the other models into resolvable conict event
structures and back. Section 3 contains the denitions of the two types of
transition systems, describes the isomorphism results, and demonstrate the
preservation of some bisimulations on the transition systems. Section 4 concludes.
2 E.g., see [
In this section, we consider event structures for resolvable conict, which were
put forward in [
Consider some properties of resolvable conict event structures.
Denition 2.
An RC-structure E = (E; `; L; l) is called rooted i (;; ;) 2 `; pure i X ` Y ) X \ Y = ;; singular i X ` Y ) X = ; _ j Y j= 1; manifestly conjunctive i there is at most one X with X ` Y , for all Y E; conjuctive i Xi ` Y (i 2 I 6= ;) ) Ti2I Xi ` Y ; locally conjuctive i Xi ` Y (i 2 I 6= ;) ^ Con(Si2I Xi [ Y ) ) Ti2I Xi ` Y ; with nite causes i X ` Y ) Xisf inite; with binary conict i j X j> 2 ) ; ` X; in the standard form i ` = f(A; B) j A \ B = ;, A [ B 2 LC(E )g; 2-coherent i X [ Y 2 LC(E ), for all X; Y 2 LC(E ) s.t. X [ Y Z 2 LC(E ).5
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 = (Erc; `rc; L; lrc) with nite causes and
binary conict from [
The standard form of RC-structures and the ability to specify impossible events in the model allows for developing a relatively simple structural denition of a removal operator which is necessary for residual semantics.
Denition 3. For an RC-structure E = (E, `, L, l) in the standard form and X 2 LC(E ), a removal operator is dened as follows: E n X = (E0, `0, L, l0), where E0 = E n X `0 = f(A0; B0) j 9(A; B) 2 ` s.t. A0 = A\E0; B0 = B\E0; (A0[B0[X) 2 LC(E )g l0 = l jE0 According to the denition 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 conicting with some events in X, making the retained events impossible by deleting their enabling relations.
From now on, we use ErLc to denote the class of rooted, singular, locally conjuctive RC-structures with binary conict. 2.2
Extended Prime Event Structures
For reasons of exibility, the authors of [
Denition 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 irreexive symmetric relation (the conict relation ); E E is the enabling relation; L is a set of labels; l : E ! L is a labeling function. Let EeLp denote the class of EP -structures over L.
Let E = (E, ], , L, l) be an EP -structure. For e 2 E, dene # e as a maximal subset of E such that 8e0 2# e : e0 e. For X E, let ](X) = fe0 2 E j 9e 2 X : e ] e0g. We call a set X E a conguration of E if X is nite, conict-free (i.e. 8e; e0 2 X : :(e ] e0)), left-closed (i.e. 8e; e0 2 E : e e0 ^ e0 2 X ) e 2 X), and does not contain enabling cycles (i.e., 6 9e1; : : : ; en 2 X : e1 : : : en e1 (n 1)). The set of congurations 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 conict relation are marked by the symbol ].
Eep : b ] a
c Example 2. Figure 1 depicts the EP -structure E ep over L = fa; b; cg, with Eep = L; ]ep = f(a; b), (b; a)g; ep= f(a; c)g; and the identity labeling function lep. Observe that the principle of conict inheritance is violated. The set of congurations of E ep is f;, fag, fbg, fa; cgg.
Denition 5. For E 2 EeLp and X 2 Conf (E ), a removal operator is dened as follows: E n X = (E0, 0, ]0, L, l0), with
E0 = E n X ]0 = ] \ (E0
0 = ( \ (E0 l0 = l jE0
E0)
E0)) [ f(e; e) j e 2 ](X)g
satisfying the principle of nite causes : 8e 2 E : bec = fe0 2 E j e0 eg is nite;
] E E is an irreexive and symmetric relation (the conict relation ), satisfying
the principle of hereditary conict : 8e; e0; e00 2 E : e e0 and e ] e00 then e0 ] e00; and
l : E ! L is a labeling function.
9 It was noted in [
We see that the events in X are removed, yielding a reduction of the enabling and conict relations. At the same time, any event conicting with some event in X is retained, equipping it with an enabling cycle, thereby making the conicting event impossible.
Translate EP -structures into RC-structures and conversely. For an EP structure EP = (E, ], , L, l), dene RC(EP ) = (E0 = E; `0,L; l = l0), where 8 either Y = feg; X =# e; < X `0 Y () or Y = fe; e0g; e 6= e0; :(e ] e0); X = ;;
: or j Y j6= 1; 2; X = ;:
For an RC-structure RC = (E0, `0, L, l0), let E P(RC) = (E00 = E0, ]00 = ]0, 00= 0, L, l00 = l0).
Lemma 2. (i) For EP an EP -structure, RC(EP ) is a rooted, singular, manifestly conjuctive RC-structure with binary conict such that Conf (EP ) = Conf (RC(EP )). (ii) For RC a rooted, singular, conjuctive RC-structure with binary conict,
E P(RC) is an EP -structure such that Conf (RC) = Conf (E P(RC)). 2.3
Stable Event Structures
Stable event structures, introduced in the work of Winskel [
E is a set of events; ] E E is an irreexive, symmetric relation (the conict relation ). We shall write Con for the set of nite conict-free subsets of E, i.e. those nite subsets X E for which 8e; e0 2 X : :(e ] e0). X 2 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 satises X ` e and X Y 2 Con ) Y ` e; and, moreover, X ` e, Y ` e, and X [ Y [ feg 2 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 dened 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.
A set X E is a conguration of an S-structure E i X is nite, conict-free (i.e., X 2 Con), and secured (i.e., there are e1; : : : ; en such that X = fe1; : : : ; eng and fe1; : : : ; eig ` ei+1, for all i < n). The set of congurations of E is denoted Conf (E ). For an S-structure E , X 2 Conf (E ), and e; e0 2 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 = fa; b; c; dg, with Es = L; ]s = f(a; b), (b; a)g; `smin= f(;; a), (;; b), (;; c), (fag; d), (fb; cg; d)g; and the identity labeling function ls. The set of congurations of E s is f;, fag, fbg, c , fa; cg, fb; cg, fa; dg, fa; c; dg, fb; c; dgg. Notice that E s is not a ow event f g structure because the event c not conicting with the event a may be a cause for d or may not.
Denition 7. For E = (E, ], `, L, l) 2 EsL and X 2 Conf (E ), a removal operator is dened as follows: E n X = (E0, ]0, `0, L, l0), with l0
= l jE0 E0 = E n X ]0 = ] \ (E0 E0) `0 = f(W 0; e) j W 0 2 Con0; 9(W 00; e) 2 `0min s.t. W 00 W 0g where `0min= f(W 00; e) j 9(W; e) 2 `min s.t. W 00 = W \ E0; e 2 E0;
W 00 [ X 2 Con; feg [ X 2 Cong We see that all the events in X are deleted; the conict relation ]0 contains the pairs of remaining conicting events; the denition of `0 is based on that of `0min, which consists of the pairs from ` without the pairs whose events conict with some event in X, thereby making them impossible.
For an S-structure S = (E; ]; `; L; l), let RC(G) = (E0 = E; `0,L; l0), where 8 either Y = feg; e 2 E; X ` e; < X `0 Y () or j Y j= 2; Y 2 Con; X = ;;
: or j Y j6= 1; 2; X = ;:
For an RC-structure RC = (E0; `0,L; l0), let S(RC) = (E00 = E0; ]00 = ]0; `00,L; l00), where X `00 e () e 2 E0, X E0, f Con0(X), and 9Y X : Y `0 feg.
Lemma 3. [
Dierent Semantics In this subsection, we dene dierent semantics for the event structure models under consideration. From now on, we treat E as an event structure over L specied in Denitions 1, 4, and 6, if not dened otherwise. Moreover, let EL = EeLp [ EL [ ErLc.
s
We rst introduce auxiliary notations. Given congurations X; X0 2 Conf (E ), we write:
X !int X0 i X X !step X0 i X X !pom X0 i X X !whp X0 i X
X0 and X0 n X = feg; X0 and X00 2 Conf (E ), for all X X0 and X0nX is a partial order; X0 and X0 is a partial order.
For ? 2 fint; step; pomg, a conguration X 2 Conf (E ) is a conguration in ?-semantics of E i ; !? X, where !? is the reexive and transitive closure of !?. Let Conf ?(E ) denote the set of congurations in ?-semantics of E .
2 fint; step; pomg, (i) for a conguration X 2 Conf (E ), the transitive and reexive closure of
X , is a partial order. Let E dX = (X; X ; L; l jX ); (ii) Conf (E ) = Conf ?(E ) = Conf (E ).
X ,
Given ? 2 fint; step; pomg, an event structure E over L, and congurations X; X0 2 Conf ?(E ) such that X !? X0, we write: lint(X0 n X) = a i X0 n X = feg and l(e) = a, if ? = int; lstep(X0 n X) = M i M (a) = jfe 2 X0 n X j l(e) = agj, for all a 2 L, if ? = step; lpom(X0 n X)=Y i Y = [(X0 n X; X0 \(X0 n X X0 n X); L; l jX0nX )], if ? = pom; lwhp(X)=Y i Y = [(X; X ; L; l jX )].
Let E be an event structure over L and X = fe1; : : : ; eng 2 Conf int(E ) (n 0). We call e1 : : : en a derivation of X i X0 = ; !int X1 : : : Xn 1 !int Xn = X, and Xi n Xi 1 = feig, for all 1 i n. A derivation e1 : : : en of X 2 Conf int(E ) and a derivation f1 : : : fn of X0 2 Conf int(E 0) are equal (denoted e1 : : : en f1 : : : fn) i there is an isomorphism : E dX ! E 0dX0 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] 2 Der(X), dene lhp([e1 : : : en]) := a1 : : : an, where li(ei) = ai (1 i n). 3 3.1
In this subsection, we rst give some basic denitions concerning labeled transition systems, and then dene the mappings TC (E ) and TR(E ), which associate two distinct kinds of transition systems one whose states are congurations 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 2 S. Two transition systems over L are isomorphic if their states can be mapped one-toone to each other, preserving transitions and initial states. We call a relation R S S0 a bisimulation between transition systems T and T 0 over L i (i; i0) 2 R, and for all (s; s0) 2 R and l 2 L: if (s; l; s1) 2!, then (s0; l; s01) 2! and (s1; s01) 2 R, for some s01 2 S0; and if (s0; l; s01) 2!, then (s; l; s1) 2! and (s1; s01) 2 R, for some s1 2 S.
Introduce additional auxiliary notations. For a xed set L of labels of event structures, dene 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 dene labeled transition systems with congurations as states.
For an event structure E over L and ? 2 fint; step; pomg, p TC ?(E ) is the transition system (Conf ?(E ), +?, ;) over L?, where X +? X0 i X !? X0 and p = l?(X0 n X); TC whp(E ) is the transition system (Conf int(E ), +whp, ;) over Lpom, where X +pwhp X0 i X !whp X0 and p = lwhp(X0); TC hp(E ) is the transition system (fDer(X) j X 2 Conf int(E )g, +hp, ) over LDer, where [e1 : : : en] +qhp [e1 : : : enen+1] (n 0) i fe1; : : : ; eng, fe1; : : : ; en; en+1g 2 Conf int(E ), and q = lhp([e1 : : : enen+1]).
Consider the denition of labeled transition systems with residuals as states.
For an event structure E over L and ? 2 fint; step; pomg, (Rie<ackh)?g(,E w)h=erfeFEij *9E?X0; :E:i+:;1Eik (k 0) s.t. E0 = E , Ek = F , and Ei *?X Ei+1 9X 2 Conf ?(Ei) : Ei+1 = Ei n X and ; !? X in Ei; p TR?(E ) is the transition system (Reach?(E ), *?, E ) over L?, where F *? F 0 i 9X 2 Conf ?(F ) : F *?X F 0 and p = l?(X); TRwhp(E ) is the transition system (Reachint(E ), *whp, E ) over Lpom, where p F *whp F 0 i 9X; X0 2 Conf int(E ) : F = E n X; F 0 = E n X0, X +whp X0, and p = lwhp(X0); TRhp(E ) is the transition system (Reachint(E ), *hp, E ) over Lpom, where F *qhp F 0 i 9X; X0 2 Conf int(E ) : F = E n X, F 0 = E n X0, [e1 : : : en] +qhp [e1 : : : enen+1], where [e1 : : : en] 2 Der(X), [e1 : : : enen+1] 2 Der(X0), and q = l([e1 : : : enen+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 ? 2 fint; step; pom; whpg, TC ?(E ) and TR?(SF (P U (E ))) (TR?(E )) are isomorphic; however,ET2CEheLpp(E[)EasLn)d. TRhp(SF (P U (E ))) (TRhp(E )) are not bisimilar; where E 2 ErLc (
It is easy to see that even for the EP -structure E1ep over L = fa; b; cg, with TECeph=p(EL1e;p,)]aepnd=T;R, h!p(1E1e=p)fa(rae; cn)o;t(bb; ics)igm, ialanrd. the identity labeling function l1ep, ep 1 1
E = fb; cg LC(E n fag) = = f;; fcg; fb; cgg
E = fbg LC(E n fa; cg) = = f;; fbgg
E = fa; b; cg LC(E) = f;; fag; fbg; fcg; fa; cg; fb; cg; fa; b; cgg a b
E = fa; cg LC(E n fbg) = = f;; fcg; fa; cgg
E = fag LC(E n fb; cg) =
= f;; fagg We rst introduce bisimulation concepts on the event structure models.
Event structures E and E 0 from EL are interleaving, step, pomset, respectively, bisimilar i TC (E?) and TC (E ?0) are bisimilar for ? 2 fint; step; pomg, 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 (;; ;) 2 R and for any (X; Y ) 2 R it holds: there is an isomorphism between E dX and E 0dY ; if X X0 for some X0 2 Conf int(E ), then Y Y 0 for some Y 0 2 Conf int(E 0) such that (X0; Y 0) 2 R; if Y Y 0 for some Y 0 2 Conf int(E 0), then X X0 for some X0 2 Conf int(E ) such that (X0; Y 0) 2 R. a relation R consisting of triples (X; f; Y ), where X 2 Conf int(E ), Y 2 Conf int(E 0), and f : E dX ! E d
0 Y is an isomorphism, is called history preserving bisimulation i (;; ;; ;) 2 R and for any (X; f; Y ) 2 R it holds: if X X0 for some X0 2 Conf int(E ), then Y Y 0 for some Y 0 2 Conf int(E 0) such that f 0 jX = f for some isomorphism f 0 : X0 ! Y 0, and (X0; f 0; Y 0) 2 R; if Y Y 0 for some Y 0 2 Conf int(E 0), then X X0 for some X0 2 Conf int(E ) such that f 0 jX = f for some isomorphism f 0 : X0 ! Y 0, and (X0; f 0; Y 0) 2 R.
Theorem 2. Given E ; E 0 2 EL, E and E 0 are weak history preserving bisimilar 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 ? 2 fint; step; pom; whpg, respectively, where E ; E 0 2 ErLc (E ; E 0 2 EeLp [ EsL). 4
Concluding Remarks In this paper, we have dened two structurally dierent ways of giving various (interleaving, step, pomset, weak history preserving, history preserving) transition system semantics in the context of three event-oriented models extended prime event structures, stable event structures, and resolvable conict 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 under consideration into resolvable conict 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 [
References