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.
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 conjunctive 1 binary causality, represented by a partial order and being under the principle of nite causes, and symmetric irreexive conict, obeying the principle of conict 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 irreexive conict, not obeying the principle of conict 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-conicting causal predecessors sets for an event is a causal predecessors set for the event) resulting in unique enablings within a conguration); event structures for resolvable conict [14] (with dynamic conicts, i.e. conicts 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 eventoriented 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.
conguration structure [13], can be distinguished: a conguration-based and a residual-based method. In the rst case, 2 states are understood as sets of events, called congurations, and state transitions are built by starting with the empty conguration and enlarging congurations 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, 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 [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 conguration-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 conict. Counterexamples illustrated that an isomorphism cannot be achieved with the various removal operators dened in [5,23]. The paper [6] demonstrated that the operators can be tightened in such a way that isomorphisms, rather than just bisimulations, between the two types of transition systems belonging to a single event structure can be obtained. A key idea is to employ non-executable (impossible) events 4 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 literature on conguration-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 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 Event Structure Models
In this section, we consider event structures for resolvable conict, which were put forward in [14] to give semantics to general Petri nets. A structure for resolvable conict 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 conict until the occurrence of c resolves this conict. Notice that the event structure classes under consideration in this paper are unable to model the phenomena of resolvable conict. In resolvable conict structures, the enabling relation can also model conicts: events from a set Y are in irresolvable conict 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 innite causes or has impossible causes/prececessors. Denition 1. An event structure for resolvable conict (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 ⊆ X : ∃Z ⊆ E : Z X; f Con(X) ⇐⇒ X is nite and Con(X). The conict relation ⊆ E × E is given by: d e ⇐⇒ d = e ∧ ¬Con({d, e}). The direct causality relation ≺⊆ E × E is dened 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 ⊆ X there exists X ⊆ X such that X X. The set of the left-closed sets of E is denoted as LC(E). Clearly, any left-closed set is conict-free. Let Conf (E) = {{e 1 , . . . , e n } ⊆ E | n ≥ 0, ∀i ≤ n : ∀X ⊆ {e 1 , . . . , e i } : ∃Y ⊆ {e 1 , . . . , e i−1 } : Y X} be the set of congurations of E. Clearly, any conguration X is a left-closed set but not conversely.
Consider some properties of resolvable conict event structures.
Denition 2. An RC-structure
Lemma 1. An RC-structure E = (E, , L, l) can be transformed into:
As an example, consider the pure, manifestly conjuctive, non-singular, non-2-coherent RC-structure E rc = (E rc , rc , L, l rc ) with nite causes and binary conict from [15], where E rc = {a, b, c}; rc consists of ∅ X for all X = {a, b} and {c} {a, b}; L = E rc ; and l rc 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 conict 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
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 ∈ LC(E), a removal operator is dened as follows: E \ X = (E , , L, l ), where
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 E rc L to denote the class of rooted, singular, locally conjuctive RC-structures with binary conict.
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, , L, l) can be directly obtained by putting =
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 conict 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 overlapping between the enabling and the conict relation, or because of impossible causes/predecessors. 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 E ep L denote the class of EP -structures over L.
Let E = (E, , ≺, L, l) be an EP -structure. For e ∈ E, dene ↓ e as a maximal subset of E such that ∀e ∈↓ e : e ≺ e. For X ⊆ E, let (X) = {e ∈ E | ∃e ∈ X : e e }. We call a set X ⊆ E a conguration of E if X is nite, conict-free (i.e. ∀e, e ∈ X : ¬(e e )), left-closed (i.e. ∀e, e ∈ E : e ≺ e ∧ e ∈ X ⇒ e ∈ X), and does not contain enabling cycles (i.e., ∃e 1 , . . . , e n ∈ X : e 1 ≺ . . . ≺ e n ≺ e 1 (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 . Consider the denition of the removal operator for EP -structures.
Denition 5. For E ∈ E ep L and X ∈ Conf (E), a removal operator is dened as follows: E \ X = (E , ≺ , , L, l ), with 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 EPstructure EP = (E, , ≺, L, l), dene RC(EP ) = (E = E, ,L, l = l ), where (ii) For RC a singular, conjuctive RC-structure with binary conict, EP(RC) is an EP -structure such that Conf (RC) = Conf (EP(RC)).
Stable event structures, introduced in the work of Winskel [27] in order to overcome the unique enabling problem of prime event structures, have an enabling relation indicating which (usually nite) sets X of events are possible prerequisites of a single event e, written X e. We consider the version of stable event structures of [28] where the conict relation is specied for sets with two events. Denition 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 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 ∀e, e ∈ X : ¬(e e ). 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 satises 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 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.
Let E s L denote the class of S-structures over L. A set X ⊆ E is a conguration of an S-structure E i X is nite, conict-free (i.e., X ∈ Con), and secured (i.e., there are e 1 , . . . , e n such that X = {e 1 , . . . , e n } and {e 1 , . . . , e i } e i+1 , for all i < n). The set of congurations of E is denoted Conf (E). For an S-structure E, X ∈ Conf (E), and e, e ∈ X, let e ≺ X e i e belongs to the smallest subset Y of X with Y e. ; and the identity labeling function l s . The set of congurations 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 conicting with the event a may be a cause for d or may not. Denition 7. For E = (E, , , L, l) ∈ E s L and X ∈ Conf (E), a removal operator is dened as follows: E \ X = (E , , , L, l ), with
We see that all the events in X are deleted; the conict relation contains the pairs of remaining conicting events; the denition of is based on that of min , 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) = (E = E, ,L, l ), where
For an RC-structure RC = (E , ,L, l ), let S(RC) = (E = E , = , ,L, l ), where X e ⇐⇒ e ∈ E , X ⊆ E , f Con (X), and ∃Y ⊆ X : Y {e}.
Lemma 3. [15] (i) For S an S-structure, RC(S) is a rooted, singular, locally conjuctive RCstructure with nite causes and binary conict s.t. Conf (S) = Conf (RC(F )). (ii) For RC a rooted, singular, locally conjuctive RC-structure with nite causes and binary conict, S(RC) is an S-structure s.t. Conf (RC) = Conf (S(RC)).
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
We rst introduce auxiliary notations. Given congurations X, X ∈ Conf (E), we write: Lemma 4. Given an event structure E ∈ E L and , * ∈ {int, step, pom}, (i) for a conguration X ∈ Conf (E), the transitive and reexive closure of
Given ∈ {int, step, pom}, an event structure E over L, and congurations X, X ∈ Conf (E) such that X → X , we write:
Let E be an event structure over L and
3 Transition Systems TC (E) and TR(E)
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 ∈ 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 × S a bisimulation between transition systems T and T over L i (i, i ) ∈ R, and for all (s, s ) ∈ R and l ∈ L: if (s, l, s 1 ) ∈→, then (s , l, s 1 ) ∈→ and (s 1 , s 1 ) ∈ R, for some s 1 ∈ S ; and if (s , l, s 1 ) ∈→, then (s, l, s 1 ) ∈→ and (s 1 , s 1 ) ∈ R, for some s 1 ∈ S.
Introduce additional auxiliary notations. For a xed set L of labels of event structures, dene L int := L, L pom := P om L (the set of isomorphic classes of partial orders labeled over L), and L Der := L * , being another sets of labels of the transition systems.
We are ready to dene labeled transition systems with congurations as states.
Denition 8. For an event structure E over L and ∈ {int, step, pom}, TC (E) is the transition system (Conf (E), , ∅) over L , where X p X i X → X and p = l (X \ X); TC whp (E) is the transition system (Conf int (E), whp , ∅) over L pom , where X p whp X i X → whp X and p = l whp (X ); TC hp (E) is the transition system ({Der(X) | X ∈ Conf int (E)}, hp , ) over L Der , where [e 1 . . . e n ] q hp [e 1 . . . e n e n+1 ] (n ≥ 0) i {e 1 , . . . , e n }, {e 1 , . . . , e n , e n+1 } ∈ Conf int (E), and q = l hp ([e 1 . . . e n e n+1 ]).
Consider the denition of labeled transition systems with residuals as states. Denition 9. For an event structure E over L and ∈ {int, step, pom},
TR (E) is the transition system (Reach (E), , E) over L , where F p F i ∃X ∈ Conf (F) : F X F and p = l (X); TR whp (E) is the transition system (Reach int (E), whp , E) over L pom , where
, X whp X , and p = l whp (X ); TR hp (E) is the transition system (Reach int (E), hp , E) over L pom , where 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
It is easy to see that even for the EP -structure We rst introduce bisimulation concepts on the event structure models.
Event structures E and E from E L are interleaving, step, pomset, respectively, bisimilar i TC (E ) and TC (E ) are bisimilar for ∈ {int, step, pom}, respectively. For event structures E and E over L,
Conf int (E ), and f : E X → E Y is an isomorphism, is called history preserving bisimulation i (∅, ∅, ∅) ∈ R and for any (X, f, Y ) ∈ R it holds:
• if X ⊆ X for some X ∈ Conf int (E), then Y ⊆ Y for some Y ∈ Conf int (E ) such that f | X = f for some isomorphism f : X → Y , and (X , f , Y ) ∈ R; • if Y ⊆ Y for some Y ∈ Conf int (E ), then X ⊆ X for some X ∈ Conf int (E) such that f | X = f for some isomorphism f : X → Y , and (X , f , Y ) ∈ R.
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 [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 conict structures [14] and to the multiset transition relation.