Minimisation of Event Structures

Alessandra Raffaet\`a; Paolo Baldan

arxiv: 1907.07042 · v1 · pith:TMNEI2DFnew · submitted 2019-07-16 · 💻 cs.LO

Minimisation of Event Structures

Paolo Baldan , Alessandra Raffaet\`a This is my paper

Pith reviewed 2026-05-24 20:31 UTC · model grok-4.3

classification 💻 cs.LO

keywords event structuresminimisationfoldingshereditary history-preserving bisimilarityquotientsprime event structuresasymmetric event structuresconcurrency theory

0 comments

The pith

Every event structure has a uniquely determined minimal quotient via folding.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Event structures model computations as events linked by causality, concurrency and conflict relations. The paper defines foldings as quotients that preserve behavior according to hereditary history-preserving bisimilarity. It proves that in a broad class covering prime, asymmetric, flow and bundle models, every event structure possesses a unique minimal folding quotient. The same uniqueness holds inside the subclass of prime event structures. All foldings between general structures arise from foldings between corresponding prime structures.

Core claim

For any event structure a folding producing a uniquely determined minimal quotient always exists. Each event structure can be seen as the folding of a prime event structure, and all foldings between general event structures arise from foldings of suitably defined corresponding prime event structures. Prime event structures always admit a unique minimal quotient.

What carries the argument

Folding: a behavior-preserving quotient with respect to hereditary history-preserving bisimilarity.

If this is right

Minimal quotients supply canonical representatives for behaviorally equivalent event structures.
Minimisation of general event structures reduces to minimisation of their corresponding prime event structures.
Explicit folding conditions identified for prime and asymmetric event structures enable direct computation of minimal forms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The unique minimal quotients could serve as compressed models for verifying properties of concurrent systems.
The reduction from general to prime structures suggests a uniform way to compare minimisation across different event-structure variants.
If hereditary history-preserving bisimilarity is replaced by another equivalence, the existence of unique minimal quotients may fail.

Load-bearing premise

The structures belong to the generalized stable class and hereditary history-preserving bisimilarity is the right equivalence for the behaviors of interest.

What would settle it

An event structure in the class that admits two distinct minimal foldings or none at all under hereditary history-preserving bisimilarity.

read the original abstract

Event structures are fundamental models in concurrency theory, providing a representation of events in computation and of their relations, notably concurrency, conflict and causality. In this paper we present a theory of minimisation for event structures. Working in a class of event structures that generalises many stable event structure models in the literature (e.g., prime, asymmetric, flow and bundle event structures), we study a notion of behaviour-preserving quotient, referred to as a folding, taking (hereditary) history preserving bisimilarity as a reference behavioural equivalence. We show that for any event structure a folding producing a uniquely determined minimal quotient always exists. We observe that each event structure can be seen as the folding of a prime event structure, and that all foldings between general event structures arise from foldings of (suitably defined) corresponding prime event structures. This gives a special relevance to foldings in the class of prime event structures, which are studied in detail. We identify folding conditions for prime and asymmetric event structures, and show that also prime event structures always admit a unique minimal quotient (while this is not the case for various other event structure models).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a folding-based minimisation for a broad class of event structures that yields unique minimal quotients under hereditary history-preserving bisimilarity, with a clean reduction to the prime case.

read the letter

The main point is that any event structure in their generalised class has a folding to a unique minimal quotient that preserves hereditary history-preserving bisimilarity, and the same holds for prime event structures even though it fails for some other models. They also show that general structures can be recovered as foldings of prime ones, so the prime case carries most of the weight. This is new: earlier work on event structures lacked a canonical minimal form with uniqueness guarantees under this equivalence. The development looks self-contained and ties together prime, asymmetric, flow and bundle models without obvious circularity. The abstract states the existence and uniqueness results directly, which is useful if the proofs check out. A minor limitation is that the choice of hereditary history-preserving bisimilarity may not match every verification task; if a coarser or finer equivalence is preferred, the quotients might not be the right ones. Still, within the stated framework the claims are consistent and the reduction to primes is a sensible move. This is aimed at concurrency theorists and tool builders who care about compact representations of concurrent behaviour. Readers working on bisimulation minimisation or event-structure semantics will find the uniqueness results worth checking. It is solid enough on its own terms to deserve referee time rather than a desk reject.

Referee Report

0 major / 3 minor

Summary. The paper develops a minimisation theory for event structures via foldings (behaviour-preserving quotients w.r.t. hereditary history-preserving bisimilarity) in a class generalising prime, asymmetric, flow and bundle event structures. It proves existence of a folding to a uniquely determined minimal quotient for any such structure, shows every event structure arises as the folding of a prime one (with all general foldings reducing to the prime case), identifies folding conditions for prime and asymmetric structures, and proves that prime event structures also admit unique minimal quotients (unlike some other models).

Significance. If the existence and uniqueness results hold, the work supplies a canonical, behaviour-preserving reduction procedure for event structures that is directly relevant to concurrency theory. The reduction of the general case to prime event structures is a useful structural insight, and the explicit folding conditions for prime/asymmetric structures provide concrete applicability. The paper's self-contained development of new notions (folding, minimal quotient) with existence proofs is a clear strength.

minor comments (3)

[§1] §1 (Introduction): the claim that the class 'generalises many stable event structure models' would benefit from an explicit list or diagram showing which models are included and how the hereditary history-preserving bisimilarity specialises in each case.
[Abstract] The abstract states that 'all foldings between general event structures arise from foldings of corresponding prime event structures'; a forward reference to the precise statement of this reduction (likely in §4 or §5) would improve readability.
[§2] Notation for the folding relation and the minimal quotient construction is introduced gradually; a consolidated table of definitions in §2 would aid readers.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary and recommendation of minor revision. The assessment correctly captures the main contributions regarding the existence of unique minimal quotients under folding with respect to hereditary history-preserving bisimilarity, the reduction of the general case to prime event structures, and the specific results for prime event structures.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper develops a theory of foldings as behaviour-preserving quotients for a generalized class of event structures, proving existence of a uniquely determined minimal quotient w.r.t. hereditary history-preserving bisimilarity and uniqueness for prime event structures. These are existence and uniqueness theorems established by direct construction and proof within the paper's definitions, without any reduction to fitted parameters, self-referential equations, or load-bearing self-citations that presuppose the result. The development introduces new notions (folding, minimal quotient) and derives their properties from the model axioms and the chosen equivalence, remaining independent of external fitted data or circular self-justification.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard definitions from concurrency theory and introduces the concept of folding as a behaviour-preserving quotient. No free parameters or invented entities are apparent from the abstract.

axioms (2)

domain assumption Event structures generalise stable models like prime, asymmetric, flow and bundle event structures
The working class is defined to generalise many models in the literature.
domain assumption Hereditary history preserving bisimilarity is the reference behavioural equivalence
Chosen explicitly as the reference for behaviour-preserving quotients.

pith-pipeline@v0.9.0 · 5720 in / 1423 out tokens · 26438 ms · 2026-05-24T20:31:55.557811+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

48 extracted references · 48 canonical work pages

[1]

for allC∈ Conf (E), we haveC[x]⊑C, henceC[x]∈ Conf (E)

work page
[2]

for allC1,C 2∈ Conf (E), C1⊑C2 iﬀ for allx∈C1, C1[x] =C2[x]

work page
[3]

for allH1,H 2∈ Hist(x), ifH1 ⌢H2 then H1 =H2; Proof. 1. Immediate by the deﬁnition ofC[x]

work page
[4]

For allx∈C1 we have that C2[x] ={y∈C2|y≤C2 x} ={y∈C1|y≤C1 x} [since C1⊑C2] =C1[x] P

Let C1,C 2∈ Conf (E) such thatC1⊑C2. For allx∈C1 we have that C2[x] ={y∈C2|y≤C2 x} ={y∈C1|y≤C1 x} [since C1⊑C2] =C1[x] P. Baldan and A.Raﬀaetà 19 Conversely, assume that for allx∈C1 we have thatC1[x] =C2[x]. Then, sincex∈Ci[x], for i∈{ 1, 2}, clearlyC1⊆ C2. Moreover, for ally∈ C1 and x∈ C2, ifx≤C2 y then x∈C2[y]. Therefore, since by hypothesisC1[y] =C2[y]...

work page
[5]

This means that there existsC∈ Conf (E) such thatH1,H 2⊆C

Let H1,H 2∈ Hist(x) and assume thatH1 ⌢ H2. This means that there existsC∈ Conf (E) such thatH1,H 2⊆C. Therefore, by point (2), we haveH1 =H1[x] =C[x] = H2[x] =H2. ◀ ▶ Lemma A.2(conﬁgurations are reachable). Let E be an event structure and letC∈ Conf (E) be a conﬁguration. Then∅− →∗ C. More in detail, ifx1,x 2,...,x n is any linearisation ofC compatible w...

work page
[6]

Sincef(C1)∈ Conf (E′) and f′ is a folding, there exists x′ such thatf(C1) x′ −→C′ 2 with f′(x′) =x′′ and f′(C′

work page
[7]

In turn, sincef is a folding, from f(C1) x′ −→C′ 2, we derive the existence of a transitionC1 x − →C2 with f(x) = x′ and f(C2) =C′

work page
[8]

◀ ▶Lemma 17(from morphisms to foldings)

Thereforef′(f(x)) =x′′ and f′(f(C2)) =C′′ 2, as desired. ◀ ▶Lemma 17(from morphisms to foldings). Let E and E′ be event structures and letf : E→ E′ be a morphism. If for allC1∈ Conf (E) and transitionf(C1) x′ −→C′ 2 there existsC1 x − →C2 such thatf(C2) =C′ 2 then f is a folding. Proof. We have to show thatRf ={(C,f|C,f (C))|C∈ Conf (E)} satisﬁes conditio...

work page
[9]

If we view conﬁgurations C1,C′ 2 as pomsets, then we can build the following commuting square C1 E C′ 2 E′ f|C1 fc′′ By the fact that f is open, we get the morphism c′′, and it is immediate to see that C1 x − →c′′(C′

work page
[10]

◀ ▶ Lemma 19(folding as equivalences)

is the desired transition that completes the proof. ◀ ▶ Lemma 19(folding as equivalences). Let E, E′ be event structures and letf : E→ E′ be a morphism. Iff is a folding thenE/≡f is isomorphic toE′. Proof. Consider the functiong :E/≡f→ E′ deﬁned byg([x]≡f ) =f(x). It is well deﬁned, since all elements in[x]≡f have the samef-image, and clearly injective. M...

work page
[11]

Therefore f(C′′ 1 ) = g(h(C′′ 1 ) = g(C1) x′ −→C′

Sinceh is a folding, there is a conﬁgurationC′′ 1∈ Conf (E′′) such that C1 =h(C′′ 1 ). Therefore f(C′′ 1 ) = g(h(C′′ 1 ) = g(C1) x′ −→C′

work page
[12]

Since f is a folding there is a transitionC′′ 1 x′′ − − →C′′ 2 with f(C′′ 2 ) = C′

work page
[13]

Therefore h(C′′ 2 ) = C1 h(x′′) − −−− →h(C′′ 2 ) with g(h(C′′ 2 )) =f(C2) =C′ 2, as desired. ◀ P. Baldan and A.Raﬀaetà 21 ▶ Proposition 21 (joining foldings). Let E, E′, E′′ be event structures and letf′ : E→ E′, f′′ : E→ E′′ be foldings. Deﬁne E′′′ as the quotient E/≡ where≡ is the transitive closure of≡f′∪≡ f′′. Then g′ : E′→ E′′′ deﬁned byg′(x′) = [x]≡...

work page
[14]

(2) Deﬁne D′ 1 = f′(D1)∈ Conf (E′)

and D1 x − →D2. (2) Deﬁne D′ 1 = f′(D1)∈ Conf (E′). Now, sincef′ is a folding andC′ 1∈ Conf (E1), there is alsoC1∈ Conf (E) such thatf′(C1) =C′

work page
[15]

From (2), since f′′ is a folding, we deducef′′(C1) =f′′(D1) x′′ − − →D′′ 2, withf′′(D2) =D′′

=f′(g′(D1)) =g′(C′ 1), hence, by pushout properties, it must bef′′(C1) = f′′(D1). From (2), since f′′ is a folding, we deducef′′(C1) =f′′(D1) x′′ − − →D′′ 2, withf′′(D2) =D′′

work page
[16]

Now, we use the fact thatf′ is a folding, and derive thatC′ 1 =f′(C1) f′(x1) −−−−→f′(C2)

And, using again the fact thatf′′ is a folding, this impliesC1 y − →C2, withf′′(C2) =D′′ 2 =f′′(D2). Now, we use the fact thatf′ is a folding, and derive thatC′ 1 =f′(C1) f′(x1) −−−−→f′(C2). If we callC′ 2 =f′(C2), we have thatg′(C′

work page
[17]

In the same way, one concludes that alsog′′ is a folding

=g′(D′ 2), as desired, sincef′′(C2) =f′′(D2). In the same way, one concludes that alsog′′ is a folding. Given any otherE1 with morphismsg′ 1 : E′→ E1 and g′′ 1 : E′′→ E1 such thatg′ 1◦f′ = g′ 2◦f′′, we show that there exists a unique morphismh : E′′′→ E1 that makes the diagram commute. 22 Minimisation of Event Structures a1 a2 b1 b2 a1 a2 b1 b2 a12 b12 P4...

work page
[18]

It is easy to see thatConf (ER) is well-deﬁned

The set of conﬁgurations ofER is Conf (ER) ={CR|C∈ Conf (E)}. It is easy to see thatConf (ER) is well-deﬁned. Preﬁx-closedness ofConf (ER) follows from the fact thatR is downward-closed by deﬁnition of hhp-bisimulation. It can be seen that ER is actually a prime event structure, with causality deﬁned by(H′ 1,f 1,H′′ 1 )≤ (H′ 2,f 2,H′′ 2 ) if H′ 1⊑ H′ 2 an...

work page
[19]

Sincef is a folding, by Lemma 17, there exists a transitionC′ 1 x′ −→C′ 2 such thatf(C′

=φE(g(C′ 1)) φE(H) −−−−→φE(D2). Sincef is a folding, by Lemma 17, there exists a transitionC′ 1 x′ −→C′ 2 such thatf(C′

work page
[20]

Observe that this implies f(x′) =φE(H) and more generallyf(⌊x′⌋) =φE(⌊H⌋), but sinceφE(⌊H⌋) =H f(⌊x′⌋) =H

=φE(C2). Observe that this implies f(x′) =φE(H) and more generallyf(⌊x′⌋) =φE(⌊H⌋), but sinceφE(⌊H⌋) =H f(⌊x′⌋) =H. We only need to show thatg(C′

work page
[21]

This is an immediate consequence of the fact that g(C′

=D2. This is an immediate consequence of the fact that g(C′

work page
[22]

◀ 26 Minimisation of Event Structures ▶ Proposition 30(folding through pess)

=g(C′ 1)∪{g(x′)} =D1∪{H} =D2, as desired. ◀ 26 Minimisation of Event Structures ▶ Proposition 30(folding through pess). Let E, E′ be event structures. For all morphisms f : E→ E′ consider P(f) : P(E)→ P(E′) deﬁned by P(f)(H) =f(H). Thenf is a folding iﬀ P(f) is a folding. Proof. This can be derived from the characterisation of foldings as Pom-open maps (L...

work page
[23]

if f(x) ↷f(y) then x ↷y

work page
[24]

Moreover, if E, E′ have global precedence, then

if f(x) =f(y) then x ↷y, hence by dualityx#y. Moreover, if E, E′ have global precedence, then

work page
[25]

Let x,y∈E

if x ↷y and¬(y ↷x) then f(x) ↷f(y); Proof. Let x,y∈E

work page
[26]

Let C∈ Conf (E) be a conﬁguration such thatx,y ∈ C

Assume f(x) ↷ f(y). Let C∈ Conf (E) be a conﬁguration such thatx,y ∈ C. Then f(x),f (y)∈f(C) and C∈ Conf (E′). Sincef(x) ↷f(y) we have thatf(x)<f (C) f(y) and thus, sincef is a morphism,x <C y. Since this holds for any conﬁguration, we conclude x ↷y

work page
[27]

Sincef is injective on conﬁgurations, there cannot beC∈ Conf (E) such thatx,y∈C

Assume f(x) =f(y). Sincef is injective on conﬁgurations, there cannot beC∈ Conf (E) such thatx,y∈C. Therefore, triviallyx ↷y (and y ↷x, whencex#y)

work page
[28]

Since E has global precedence, x≤C y

If E, E′ have global precedence,f is a folding andx ↷ y and¬(y ↷ x) then¬(x#y) and thus there is some conﬁgurationC ∈ Conf (E) such thatx,y ∈ C. Since E has global precedence, x≤C y. Now f(x),f (y)∈ f(C) which is in Conf (E′). Therefore f(x)≤f (C) f(y). Again, since E′ has global precedence,f(x) ↷f(y), as desired. ◀ D Proofs for Section 4 (Foldings for Pr...

work page
[29]

f(⌊x⌋) =⌊f(x)⌋; namely (a) for allx′∈ P′, ifx′≤ f(y) there existsx∈ P such that x≤y and f(x) =x′ (b) ifx≤y then f(x)≤f(y)

work page
[30]

(a) iff(x) =f(y) and x̸=y then x#y and (b) iff(x)#f(y) then x#y. Proof. First observe thatpess have global precedence andx ↷y iﬀ x≤y or x#y. Now, assume thatf is a morphism. Then property (1) holds by deﬁnition. Property (2) follows from the fact that⌊x⌋∈ Conf (P). Hencef(⌊x⌋)∈ Conf (P′) andf(⌊x⌋)≃⌊x⌋, which implies f(⌊x⌋) =⌊f(x)⌋. Concerning condition (3...

work page
[31]

if x#∀f−1(y′) then f(x)#y′

work page
[32]

if ⌢(X∪{x}), ⌢(Y∪{y}), ⌢(X∪Y ) and f(x) =f(y) then there existsz∈ P such that f(z) =f(x) and ⌢(X∪Y∪{z}). Proof. Let f : P→ P′ be a folding. Let us ﬁrst observe thatf is surjective. Takex′∈ P′. Since⌊x′⌋ ∈Conf (P′), we have that∅ ⌊x′⌋ −−→ ⌊x′⌋. Since f is a folding, there must be C∈ Conf (P) such thatf(C) =⌊x′⌋, and thus there isx∈C such thatf(x) =x′, as d...

work page
[33]

Assume thatf(x) ⌢y′

We prove the contronominal, namely that iff(x) ⌢ y′ then there isy∈ P such that f(y) =y′ and x ⌢y. Assume thatf(x) ⌢y′. We distinguish two possibilities: If y′≤f(x) then, by Lemma 31(2a), there existsy≤x such thatf(y) =y′. Hence x ⌢y, as desired. Assume that, instead,¬(y′≤ f(x)). Therefore, if we let C′ =⌊f(x)⌋∪⌊ y′⌋ and X′ =C′\⌊f(x)⌋ ⌊f(x)⌋ X′ −−→C′ (3) ...

work page
[34]

DeﬁneC =⌊X∪Y⌋∈ Conf (P)

Assume that⌢(X∪{x}), ⌢(Y∪{y}), ⌢(X∪Y )andf(x) =f(y). DeﬁneC =⌊X∪Y⌋∈ Conf (P). We distinguish two cases. If x∈C then we can simply takez =x, since clearly⌢(X∪Y∪{x}). Assume now thatx /∈C. Clearlyf(x) /∈f(C). Moreover, ⌢(f(C)∪{f(x)}). In fact, by Lemma 31(3), if for somew∈C it weref(w)#f(x) =f(y) we would havew#x and w#y, contradicting either⌢(X∪{x}) or ⌢(Y...

work page
[35]

By Lemma 31(2b) we havef(⌊x⌋) =⌊x′⌋ ={x′}, and thus⌊x⌋ ={x}

IfC1 =∅, take anyx∈ P such that f(x) =x′, which exists by surjectivity. By Lemma 31(2b) we havef(⌊x⌋) =⌊x′⌋ ={x′}, and thus⌊x⌋ ={x}. This means thatC1 =∅ x − →{x}, and we conclude. P. Baldan and A.Raﬀaetà 29 Otherwise, ifC1̸=∅, since for ally∈C1 it holds thatf(y) ⌢x′, by condition (1), there exists some elementxy∈ P such thatxy ⌢ y and f(xy) = x. Note tha...

work page
[36]

Let P, P′ be pes and letf : P→ P′ be a function

f(conc(x)) = conc(f(x)) ▶ Lemma D.2(foldings vs abstraction homomorphisms). Let P, P′ be pes and letf : P→ P′ be a function. Thenf is an abstraction morphism iﬀf is a pes morphism additionally satisying condition (1) of Lemma 32. Proof. Letf beanabstractionhomomorphism. Weﬁrstproveconditions(1)-(3)ofLemma31. The ﬁrst condition is already in Deﬁnition D.1....

work page
[37]

Moreover, for allx,y∈ P, X,Y ⊆ P

x#y. Moreover, for allx,y∈ P, X,Y ⊆ P

work page
[38]

if x#∀[y]≡ then [x]≡#∀[y]≡

work page
[39]

if ⌢(X∪{x}), ⌢(Y∪{y}), ⌢(X∪Y ) there existsz∈ [x]≡ such that ⌢(X∪Y∪{z}). P. Baldan and A.Raﬀaetà 31 Proof. Let P be a pess and let≡ be a folding equivalence. This means that there exists a foldingf : P→ P′ such that≡ and≡f coincide. By Lemma 19 we know thatP/≡f is isomorphic to P′. Therefore using Lemma 31 and Proposition 32 we immediately get the validit...

work page
[40]

(a) iff(x)↗f(y) then x↗y and (b) ifx↗y and¬(y↗x) then f(x)↗f(y)

work page
[41]

if f(x) =f(y) then x↗y. Proof. Let f : A→ A′ be a morphism. Just observe thatpess have global precedence and x ↷y iﬀ x↗y. Condition (1) is obviously true. Property (2) follows by observing that, for allx∈ A, since⌊x⌋∈ Conf (A) and f is a morphism, thenf(⌊x⌋)∈ Conf (A). Since conﬁgurations are causally closed we deduce that⌊f(x)⌋⊆ f(⌊x⌋). The validity of p...

work page
[42]

if f−1(y′)↗∀ x then y′↗∃ f(⌊x⌋)

work page
[43]

if¬(x↗∃ X),¬(y↗∃ Y ), ⌢(X∪Y ) and f(x) =f(y) then there existsz∈ A such that f(z) =f(x) and¬(z↗∃ X∪Y )

work page
[44]

given H∈ Hist(x), if¬(H↗∃ X), andH1 ĹH such thatf(H1)∪{f(x)}∈ Hist(f(x)) there existsx1 such thatH1∪{x1}∈ Hist(x1) and¬(x1↗∃ X). Proof. Let f : A→ A′ be a folding. Surjectivity off can be proved exactly as in Proposi- tion 32. We show that properties (1)-(3) hold

work page
[45]

LetH =⌊x⌋∈ Conf (A) and assume that¬(y′↗∃ f(H))

We prove the contronominal, namely that if¬(y′↗∃ f(⌊x⌋)) then there isy∈ A such that f(y) =y′ and¬(y↗x). LetH =⌊x⌋∈ Conf (A) and assume that¬(y′↗∃ f(H)). Since f is a morphismH′ =f(H)∈ Hist(f(x)). Observe that we can safely assume that y′̸∈H′. In fact, otherwise, since¬(y′↗∃ H′), the only possibility would bey′ =f(x) P. Baldan and A.Raﬀaetà 33 and thus we...

work page
[46]

Deﬁne C =⌊X∪Y⌋∈ Conf (A)

Assume thatx /∈X, y /∈Y ¬(x↗∃ X),¬(y↗∃ Y ), ⌢(X∪Y ) and f(x) =f(y). Deﬁne C =⌊X∪Y⌋∈ Conf (A). We show thatx̸∈ C. In fact, x /∈⌊ X⌋ since x /∈ X and ¬(x↗∃ X), and, for analogous reasons,y /∈⌊Y⌋. Now, ifx =y we are done. Otherwise, we can prove thatx̸∈⌊Y⌋ and conclude. In fact, assume by contradiction thatx∈⌊Y⌋, i.e., x≤w for somew∈Y. Sincef(x) =f(y) and x̸...

work page
[47]

Consider C =H1∪⌊X⌋

TakeH∈ Hist(x) with¬(H↗∃ X) andH1 ĹH such thatf(H1)∪{f(x)}∈ Hist(f(x)), hence f(H1) f (x) −−−→f(H1)∪{f(x)}. Consider C =H1∪⌊X⌋. Since H1∪{x}⊆ H and ¬(H↗∃ X), we have¬(H1∪{x}↗∃⌊X⌋)and thus, by Lemma 36(3a),¬(f(H1∪{x})↗∃ f(⌊X⌋). Therefore f(H1∪⌊X⌋) = f(H1)∪f(⌊X⌋) f (x) −−−→C′ 1, and sincef is a folding H1∪⌊X⌋ x1 −→C1, withf(x1) =f(x)and clearly (given that ...

work page
[48]

Otherwise, ifC1̸=∅, for ally∈ C1 it holds⌊y⌋⊆ C1 and thus¬(x′↗∃ f(⌊y⌋)

When C1 = ∅ we argue as in Proposition 32. Otherwise, ifC1̸=∅, for ally∈ C1 it holds⌊y⌋⊆ C1 and thus¬(x′↗∃ f(⌊y⌋). Thus, by condition (1), there exists some elementxy∈ A such thatf(xy) =x′ and ¬(xy↗y). Note that necessarilyxy̸=y, Since C1 is ﬁnite and consistent, an inductive argument based on condition (2), allows to derive the existence ofx such thatf(x...

work page

[1] [1]

for allC∈ Conf (E), we haveC[x]⊑C, henceC[x]∈ Conf (E)

work page

[2] [2]

for allC1,C 2∈ Conf (E), C1⊑C2 iﬀ for allx∈C1, C1[x] =C2[x]

work page

[3] [3]

for allH1,H 2∈ Hist(x), ifH1 ⌢H2 then H1 =H2; Proof. 1. Immediate by the deﬁnition ofC[x]

work page

[4] [4]

For allx∈C1 we have that C2[x] ={y∈C2|y≤C2 x} ={y∈C1|y≤C1 x} [since C1⊑C2] =C1[x] P

Let C1,C 2∈ Conf (E) such thatC1⊑C2. For allx∈C1 we have that C2[x] ={y∈C2|y≤C2 x} ={y∈C1|y≤C1 x} [since C1⊑C2] =C1[x] P. Baldan and A.Raﬀaetà 19 Conversely, assume that for allx∈C1 we have thatC1[x] =C2[x]. Then, sincex∈Ci[x], for i∈{ 1, 2}, clearlyC1⊆ C2. Moreover, for ally∈ C1 and x∈ C2, ifx≤C2 y then x∈C2[y]. Therefore, since by hypothesisC1[y] =C2[y]...

work page

[5] [5]

This means that there existsC∈ Conf (E) such thatH1,H 2⊆C

Let H1,H 2∈ Hist(x) and assume thatH1 ⌢ H2. This means that there existsC∈ Conf (E) such thatH1,H 2⊆C. Therefore, by point (2), we haveH1 =H1[x] =C[x] = H2[x] =H2. ◀ ▶ Lemma A.2(conﬁgurations are reachable). Let E be an event structure and letC∈ Conf (E) be a conﬁguration. Then∅− →∗ C. More in detail, ifx1,x 2,...,x n is any linearisation ofC compatible w...

work page

[6] [6]

Sincef(C1)∈ Conf (E′) and f′ is a folding, there exists x′ such thatf(C1) x′ −→C′ 2 with f′(x′) =x′′ and f′(C′

work page

[7] [7]

In turn, sincef is a folding, from f(C1) x′ −→C′ 2, we derive the existence of a transitionC1 x − →C2 with f(x) = x′ and f(C2) =C′

work page

[8] [8]

◀ ▶Lemma 17(from morphisms to foldings)

Thereforef′(f(x)) =x′′ and f′(f(C2)) =C′′ 2, as desired. ◀ ▶Lemma 17(from morphisms to foldings). Let E and E′ be event structures and letf : E→ E′ be a morphism. If for allC1∈ Conf (E) and transitionf(C1) x′ −→C′ 2 there existsC1 x − →C2 such thatf(C2) =C′ 2 then f is a folding. Proof. We have to show thatRf ={(C,f|C,f (C))|C∈ Conf (E)} satisﬁes conditio...

work page

[9] [9]

If we view conﬁgurations C1,C′ 2 as pomsets, then we can build the following commuting square C1 E C′ 2 E′ f|C1 fc′′ By the fact that f is open, we get the morphism c′′, and it is immediate to see that C1 x − →c′′(C′

work page

[10] [10]

◀ ▶ Lemma 19(folding as equivalences)

is the desired transition that completes the proof. ◀ ▶ Lemma 19(folding as equivalences). Let E, E′ be event structures and letf : E→ E′ be a morphism. Iff is a folding thenE/≡f is isomorphic toE′. Proof. Consider the functiong :E/≡f→ E′ deﬁned byg([x]≡f ) =f(x). It is well deﬁned, since all elements in[x]≡f have the samef-image, and clearly injective. M...

work page

[11] [11]

Therefore f(C′′ 1 ) = g(h(C′′ 1 ) = g(C1) x′ −→C′

Sinceh is a folding, there is a conﬁgurationC′′ 1∈ Conf (E′′) such that C1 =h(C′′ 1 ). Therefore f(C′′ 1 ) = g(h(C′′ 1 ) = g(C1) x′ −→C′

work page

[12] [12]

Since f is a folding there is a transitionC′′ 1 x′′ − − →C′′ 2 with f(C′′ 2 ) = C′

work page

[13] [13]

Therefore h(C′′ 2 ) = C1 h(x′′) − −−− →h(C′′ 2 ) with g(h(C′′ 2 )) =f(C2) =C′ 2, as desired. ◀ P. Baldan and A.Raﬀaetà 21 ▶ Proposition 21 (joining foldings). Let E, E′, E′′ be event structures and letf′ : E→ E′, f′′ : E→ E′′ be foldings. Deﬁne E′′′ as the quotient E/≡ where≡ is the transitive closure of≡f′∪≡ f′′. Then g′ : E′→ E′′′ deﬁned byg′(x′) = [x]≡...

work page

[14] [14]

(2) Deﬁne D′ 1 = f′(D1)∈ Conf (E′)

and D1 x − →D2. (2) Deﬁne D′ 1 = f′(D1)∈ Conf (E′). Now, sincef′ is a folding andC′ 1∈ Conf (E1), there is alsoC1∈ Conf (E) such thatf′(C1) =C′

work page

[15] [15]

From (2), since f′′ is a folding, we deducef′′(C1) =f′′(D1) x′′ − − →D′′ 2, withf′′(D2) =D′′

=f′(g′(D1)) =g′(C′ 1), hence, by pushout properties, it must bef′′(C1) = f′′(D1). From (2), since f′′ is a folding, we deducef′′(C1) =f′′(D1) x′′ − − →D′′ 2, withf′′(D2) =D′′

work page

[16] [16]

Now, we use the fact thatf′ is a folding, and derive thatC′ 1 =f′(C1) f′(x1) −−−−→f′(C2)

And, using again the fact thatf′′ is a folding, this impliesC1 y − →C2, withf′′(C2) =D′′ 2 =f′′(D2). Now, we use the fact thatf′ is a folding, and derive thatC′ 1 =f′(C1) f′(x1) −−−−→f′(C2). If we callC′ 2 =f′(C2), we have thatg′(C′

work page

[17] [17]

In the same way, one concludes that alsog′′ is a folding

=g′(D′ 2), as desired, sincef′′(C2) =f′′(D2). In the same way, one concludes that alsog′′ is a folding. Given any otherE1 with morphismsg′ 1 : E′→ E1 and g′′ 1 : E′′→ E1 such thatg′ 1◦f′ = g′ 2◦f′′, we show that there exists a unique morphismh : E′′′→ E1 that makes the diagram commute. 22 Minimisation of Event Structures a1 a2 b1 b2 a1 a2 b1 b2 a12 b12 P4...

work page

[18] [18]

It is easy to see thatConf (ER) is well-deﬁned

The set of conﬁgurations ofER is Conf (ER) ={CR|C∈ Conf (E)}. It is easy to see thatConf (ER) is well-deﬁned. Preﬁx-closedness ofConf (ER) follows from the fact thatR is downward-closed by deﬁnition of hhp-bisimulation. It can be seen that ER is actually a prime event structure, with causality deﬁned by(H′ 1,f 1,H′′ 1 )≤ (H′ 2,f 2,H′′ 2 ) if H′ 1⊑ H′ 2 an...

work page

[19] [19]

Sincef is a folding, by Lemma 17, there exists a transitionC′ 1 x′ −→C′ 2 such thatf(C′

=φE(g(C′ 1)) φE(H) −−−−→φE(D2). Sincef is a folding, by Lemma 17, there exists a transitionC′ 1 x′ −→C′ 2 such thatf(C′

work page

[20] [20]

Observe that this implies f(x′) =φE(H) and more generallyf(⌊x′⌋) =φE(⌊H⌋), but sinceφE(⌊H⌋) =H f(⌊x′⌋) =H

=φE(C2). Observe that this implies f(x′) =φE(H) and more generallyf(⌊x′⌋) =φE(⌊H⌋), but sinceφE(⌊H⌋) =H f(⌊x′⌋) =H. We only need to show thatg(C′

work page

[21] [21]

This is an immediate consequence of the fact that g(C′

=D2. This is an immediate consequence of the fact that g(C′

work page

[22] [22]

◀ 26 Minimisation of Event Structures ▶ Proposition 30(folding through pess)

=g(C′ 1)∪{g(x′)} =D1∪{H} =D2, as desired. ◀ 26 Minimisation of Event Structures ▶ Proposition 30(folding through pess). Let E, E′ be event structures. For all morphisms f : E→ E′ consider P(f) : P(E)→ P(E′) deﬁned by P(f)(H) =f(H). Thenf is a folding iﬀ P(f) is a folding. Proof. This can be derived from the characterisation of foldings as Pom-open maps (L...

work page

[23] [23]

if f(x) ↷f(y) then x ↷y

work page

[24] [24]

Moreover, if E, E′ have global precedence, then

if f(x) =f(y) then x ↷y, hence by dualityx#y. Moreover, if E, E′ have global precedence, then

work page

[25] [25]

Let x,y∈E

if x ↷y and¬(y ↷x) then f(x) ↷f(y); Proof. Let x,y∈E

work page

[26] [26]

Let C∈ Conf (E) be a conﬁguration such thatx,y ∈ C

Assume f(x) ↷ f(y). Let C∈ Conf (E) be a conﬁguration such thatx,y ∈ C. Then f(x),f (y)∈f(C) and C∈ Conf (E′). Sincef(x) ↷f(y) we have thatf(x)<f (C) f(y) and thus, sincef is a morphism,x <C y. Since this holds for any conﬁguration, we conclude x ↷y

work page

[27] [27]

Sincef is injective on conﬁgurations, there cannot beC∈ Conf (E) such thatx,y∈C

Assume f(x) =f(y). Sincef is injective on conﬁgurations, there cannot beC∈ Conf (E) such thatx,y∈C. Therefore, triviallyx ↷y (and y ↷x, whencex#y)

work page

[28] [28]

Since E has global precedence, x≤C y

If E, E′ have global precedence,f is a folding andx ↷ y and¬(y ↷ x) then¬(x#y) and thus there is some conﬁgurationC ∈ Conf (E) such thatx,y ∈ C. Since E has global precedence, x≤C y. Now f(x),f (y)∈ f(C) which is in Conf (E′). Therefore f(x)≤f (C) f(y). Again, since E′ has global precedence,f(x) ↷f(y), as desired. ◀ D Proofs for Section 4 (Foldings for Pr...

work page

[29] [29]

f(⌊x⌋) =⌊f(x)⌋; namely (a) for allx′∈ P′, ifx′≤ f(y) there existsx∈ P such that x≤y and f(x) =x′ (b) ifx≤y then f(x)≤f(y)

work page

[30] [30]

(a) iff(x) =f(y) and x̸=y then x#y and (b) iff(x)#f(y) then x#y. Proof. First observe thatpess have global precedence andx ↷y iﬀ x≤y or x#y. Now, assume thatf is a morphism. Then property (1) holds by deﬁnition. Property (2) follows from the fact that⌊x⌋∈ Conf (P). Hencef(⌊x⌋)∈ Conf (P′) andf(⌊x⌋)≃⌊x⌋, which implies f(⌊x⌋) =⌊f(x)⌋. Concerning condition (3...

work page

[31] [31]

if x#∀f−1(y′) then f(x)#y′

work page

[32] [32]

if ⌢(X∪{x}), ⌢(Y∪{y}), ⌢(X∪Y ) and f(x) =f(y) then there existsz∈ P such that f(z) =f(x) and ⌢(X∪Y∪{z}). Proof. Let f : P→ P′ be a folding. Let us ﬁrst observe thatf is surjective. Takex′∈ P′. Since⌊x′⌋ ∈Conf (P′), we have that∅ ⌊x′⌋ −−→ ⌊x′⌋. Since f is a folding, there must be C∈ Conf (P) such thatf(C) =⌊x′⌋, and thus there isx∈C such thatf(x) =x′, as d...

work page

[33] [33]

Assume thatf(x) ⌢y′

We prove the contronominal, namely that iff(x) ⌢ y′ then there isy∈ P such that f(y) =y′ and x ⌢y. Assume thatf(x) ⌢y′. We distinguish two possibilities: If y′≤f(x) then, by Lemma 31(2a), there existsy≤x such thatf(y) =y′. Hence x ⌢y, as desired. Assume that, instead,¬(y′≤ f(x)). Therefore, if we let C′ =⌊f(x)⌋∪⌊ y′⌋ and X′ =C′\⌊f(x)⌋ ⌊f(x)⌋ X′ −−→C′ (3) ...

work page

[34] [34]

DeﬁneC =⌊X∪Y⌋∈ Conf (P)

Assume that⌢(X∪{x}), ⌢(Y∪{y}), ⌢(X∪Y )andf(x) =f(y). DeﬁneC =⌊X∪Y⌋∈ Conf (P). We distinguish two cases. If x∈C then we can simply takez =x, since clearly⌢(X∪Y∪{x}). Assume now thatx /∈C. Clearlyf(x) /∈f(C). Moreover, ⌢(f(C)∪{f(x)}). In fact, by Lemma 31(3), if for somew∈C it weref(w)#f(x) =f(y) we would havew#x and w#y, contradicting either⌢(X∪{x}) or ⌢(Y...

work page

[35] [35]

By Lemma 31(2b) we havef(⌊x⌋) =⌊x′⌋ ={x′}, and thus⌊x⌋ ={x}

IfC1 =∅, take anyx∈ P such that f(x) =x′, which exists by surjectivity. By Lemma 31(2b) we havef(⌊x⌋) =⌊x′⌋ ={x′}, and thus⌊x⌋ ={x}. This means thatC1 =∅ x − →{x}, and we conclude. P. Baldan and A.Raﬀaetà 29 Otherwise, ifC1̸=∅, since for ally∈C1 it holds thatf(y) ⌢x′, by condition (1), there exists some elementxy∈ P such thatxy ⌢ y and f(xy) = x. Note tha...

work page

[36] [36]

Let P, P′ be pes and letf : P→ P′ be a function

f(conc(x)) = conc(f(x)) ▶ Lemma D.2(foldings vs abstraction homomorphisms). Let P, P′ be pes and letf : P→ P′ be a function. Thenf is an abstraction morphism iﬀf is a pes morphism additionally satisying condition (1) of Lemma 32. Proof. Letf beanabstractionhomomorphism. Weﬁrstproveconditions(1)-(3)ofLemma31. The ﬁrst condition is already in Deﬁnition D.1....

work page

[37] [37]

Moreover, for allx,y∈ P, X,Y ⊆ P

x#y. Moreover, for allx,y∈ P, X,Y ⊆ P

work page

[38] [38]

if x#∀[y]≡ then [x]≡#∀[y]≡

work page

[39] [39]

if ⌢(X∪{x}), ⌢(Y∪{y}), ⌢(X∪Y ) there existsz∈ [x]≡ such that ⌢(X∪Y∪{z}). P. Baldan and A.Raﬀaetà 31 Proof. Let P be a pess and let≡ be a folding equivalence. This means that there exists a foldingf : P→ P′ such that≡ and≡f coincide. By Lemma 19 we know thatP/≡f is isomorphic to P′. Therefore using Lemma 31 and Proposition 32 we immediately get the validit...

work page

[40] [40]

(a) iff(x)↗f(y) then x↗y and (b) ifx↗y and¬(y↗x) then f(x)↗f(y)

work page

[41] [41]

if f(x) =f(y) then x↗y. Proof. Let f : A→ A′ be a morphism. Just observe thatpess have global precedence and x ↷y iﬀ x↗y. Condition (1) is obviously true. Property (2) follows by observing that, for allx∈ A, since⌊x⌋∈ Conf (A) and f is a morphism, thenf(⌊x⌋)∈ Conf (A). Since conﬁgurations are causally closed we deduce that⌊f(x)⌋⊆ f(⌊x⌋). The validity of p...

work page

[42] [42]

if f−1(y′)↗∀ x then y′↗∃ f(⌊x⌋)

work page

[43] [43]

if¬(x↗∃ X),¬(y↗∃ Y ), ⌢(X∪Y ) and f(x) =f(y) then there existsz∈ A such that f(z) =f(x) and¬(z↗∃ X∪Y )

work page

[44] [44]

given H∈ Hist(x), if¬(H↗∃ X), andH1 ĹH such thatf(H1)∪{f(x)}∈ Hist(f(x)) there existsx1 such thatH1∪{x1}∈ Hist(x1) and¬(x1↗∃ X). Proof. Let f : A→ A′ be a folding. Surjectivity off can be proved exactly as in Proposi- tion 32. We show that properties (1)-(3) hold

work page

[45] [45]

LetH =⌊x⌋∈ Conf (A) and assume that¬(y′↗∃ f(H))

We prove the contronominal, namely that if¬(y′↗∃ f(⌊x⌋)) then there isy∈ A such that f(y) =y′ and¬(y↗x). LetH =⌊x⌋∈ Conf (A) and assume that¬(y′↗∃ f(H)). Since f is a morphismH′ =f(H)∈ Hist(f(x)). Observe that we can safely assume that y′̸∈H′. In fact, otherwise, since¬(y′↗∃ H′), the only possibility would bey′ =f(x) P. Baldan and A.Raﬀaetà 33 and thus we...

work page

[46] [46]

Deﬁne C =⌊X∪Y⌋∈ Conf (A)

Assume thatx /∈X, y /∈Y ¬(x↗∃ X),¬(y↗∃ Y ), ⌢(X∪Y ) and f(x) =f(y). Deﬁne C =⌊X∪Y⌋∈ Conf (A). We show thatx̸∈ C. In fact, x /∈⌊ X⌋ since x /∈ X and ¬(x↗∃ X), and, for analogous reasons,y /∈⌊Y⌋. Now, ifx =y we are done. Otherwise, we can prove thatx̸∈⌊Y⌋ and conclude. In fact, assume by contradiction thatx∈⌊Y⌋, i.e., x≤w for somew∈Y. Sincef(x) =f(y) and x̸...

work page

[47] [47]

Consider C =H1∪⌊X⌋

TakeH∈ Hist(x) with¬(H↗∃ X) andH1 ĹH such thatf(H1)∪{f(x)}∈ Hist(f(x)), hence f(H1) f (x) −−−→f(H1)∪{f(x)}. Consider C =H1∪⌊X⌋. Since H1∪{x}⊆ H and ¬(H↗∃ X), we have¬(H1∪{x}↗∃⌊X⌋)and thus, by Lemma 36(3a),¬(f(H1∪{x})↗∃ f(⌊X⌋). Therefore f(H1∪⌊X⌋) = f(H1)∪f(⌊X⌋) f (x) −−−→C′ 1, and sincef is a folding H1∪⌊X⌋ x1 −→C1, withf(x1) =f(x)and clearly (given that ...

work page

[48] [48]

Otherwise, ifC1̸=∅, for ally∈ C1 it holds⌊y⌋⊆ C1 and thus¬(x′↗∃ f(⌊y⌋)

When C1 = ∅ we argue as in Proposition 32. Otherwise, ifC1̸=∅, for ally∈ C1 it holds⌊y⌋⊆ C1 and thus¬(x′↗∃ f(⌊y⌋). Thus, by condition (1), there exists some elementxy∈ A such thatf(xy) =x′ and ¬(xy↗y). Note that necessarilyxy̸=y, Since C1 is ﬁnite and consistent, an inductive argument based on condition (2), allows to derive the existence ofx such thatf(x...

work page