Design of Stable Event Structures

[eupp]

Stable Event Structures.

Let's discuss an encoding of stable event structures.

First, a classical textbook definition [1].
A stable E.S. is a tuple < E, Cons, |- > where:

• E is a set of events;
• Cons is a set of all finite consistent (i.e. conflict-free) subset of events;
• C |- e is enabling relation, asserting that e depends on conflict free subset of events C.

Additionally, the following axioms must hold.

• Monotonicity of Cons
  X <= Y and Y \in Cons implies X \in Cons for all X and Y.

• Monotonicity of Enabling
  X |- e and X <= Y \in Cons implies Y |- e for all X, Y, and e.

• Stability
  X |- e, Y |- e, and X \cup Y \cup {e} \in Cons implies X \cap Y |- e.

Next, the configuration C (a subset of events) of a stable event structure is defined as follows:

• C is conflict-free
  X <= C and finite(X) implies X \in Cons (i.e. all finite subsets of C are conflict free)

• C is secured:
  for all e \in C there exists [e1, ..., en = e], s.t. {e1, ..., ei} |- e{i+1} for all 0 <= i < n.

Now, the stability axiom ensures that in the configuration each event is enabled in a "unique way".
It allows us to define (within a particular configuration C) the usual binary causality relation <=.

e1 <= e2 <---> forall C' <= C s.t. C' is configuration itself, e2 \in C' implies e1 \in C'

Now, there are several problems with the theory formulated this way
which preclude us from formulating it in Coq naively as is.

1. The definition of securedness property leads to ambiguous representation.
   To see the problem, imagine an event structure s.t. {} |- e1, {} |- e2, and {e1, e2} |- e3.
   Then {e1, e2, e3} is a valid configuration (which is actually a prefix of e3).
   It has two securing chains for e3: [e1, e2, e3] and [e2, e1, e3].
   Now, although it's stated that in stable E.S. each event is enabled in a "unique way",
   the sequence-based representation of securing does not reflect this fact.
   In other words, we need to compare securing chains modulo permutation of "independent" events
   (e1 and e2 in our example).

2. The definition of causality relation for the configuration (as stated above),
   is not decidable, i.e. it is not a bool-valued but a Prop-valued relation,
   because of the forall quantifier over the set of (potentially infinite) configurations.
   The Prop-valued relation would not fit the design of our library and
   we will not be able to use mathcomp lemmas.

Therefore I propose the following alternative encodings.

1. To address the first problem, I propose to encode securing directly as a partial order, instead of a total order (derived from the securing chain).
   Then we will be able to get the "uniqueness" for free.
   Yet, there is still the question how to represent partial order.
   Here I propose to use the same trick we've already did with "execution" event structures.
   We can encode the partial order via its covering function f : E -> seq E, i.e. a function that maps the event to the (finite) set of its immediate predecessors.
   Then, to guarantee that the covering function will generate the partial order (i.e. there is no loops like in the case of f := { e1 -> [e2], e2 -> [e1] }) we can require that f satisfies the descend property w.r.t. some well-founded order on E, that is x \in f y implies x <= y.
   Finally, we also require that f is finitely supported function (i.e. f x != [] only for finite number of events).
   This corresponds to the requirement that securing chain is a finite sequence.
   Using the property that for finitely supported function pointwise equality implies propositional equality (lemma), we would be able to prove that stability axiom implies the uniqueness of f for each event within a configuration.

2. To address the second problem, I propose to alter the definition of binary causality for configuration.
   e1 <= e2 is true iff e1 <=(f) e2 where <=(f) is a partial order generated from covering function f for an event e2 in configuration C (that is f is a finitely supported function from the previous item).
   Since the f is unique, the alternative definition "should work". We will also have to prove that the alternative definition is indeed equivalent to the original one (via reflection lemma).

That's my idea. Any comments or suggestions are welcome.
It's also worth to recheck my proposals, as I'm not 100% sure my alternative encodings are correct.