A284276 Number of event structures with n labeled elements.

1, 4, 41, 916, 41099, 3528258, 561658287

Offset

1,2

Comments

Little is known about event structures enumeration. The entries were obtained by a dedicated algorithm recursively constructing all possible event structures. This algorithm has been formally verified to be correct by construction using the theorem prover Isabelle/HOL (see the Links section). The formal proof also formally certifies the correctness of other sequences already in the OEIS (quasi-orders, partial orders). Note that we count what are called "event structures" in the given References. Other sources, however, refer to the same objects as "prime event structures".

Links

Table of n, a(n) for n=1..7.

Juliana Bowles and Marco B. Caminati, A Verified Algorithm Enumerating Event Structures, arXiv:1705.07228 [cs.LO], 2017.

Marco B. Caminati, Isabelle/HOL code

Marco B. Caminati and Juliana K. F. Bowles, Representation Theorems Obtained by Mining across Web Sources for Hints, Lancaster Univ. (UK, 2022).

M. Nielsen, G. Plotkin, and G. Winskel, Petri nets, event structures and domains, part I, Theoretical Computer Science 13, no. 1 (1981): 85-108.

G. Winskel and M. Nielsen, Models for concurrency, DAIMI Report Series 21, no. 429 (1992) (revised version).

Example

An event structure is given by a poset and a conflict relation (denoted #) on it. The conflict relation is irreflexive and symmetric, and must propagate over the order: a<=b and a#c imply b#c.
For n=2, (i.e., two elements a and b), there are three possible posets: a<=b, b<=a, and neither of the two. For the first two cases, only the empty conflict is possible. For the third case, you can have either the empty conflict relation, or a#b. Hence the total number of event structures is 4.

Prog

(Isabelle/HOL)
definition "ReducedRelation2 ReflPartialOrder == (let min = (List.find (%x. x : (snd`((set ReflPartialOrder)-{(x, x)}))) (map fst ReflPartialOrder)) in (min, filter (%(x, y). x ~= the min & y ~= the min) ReflPartialOrder))"
definition "generateConflicts5 Or m c ==
[c Int ({m}×Y) Int (Y×{m}). Y <- map (Image {z:Or. fst z ~= m & snd z ~= m})
(map set (sublists (if (Or``{m})-{m}={} then (sorted_list_of_set (Domain Or)) else
sorted_list_of_set (Inter {c``{M}|M. M ? next1 Or {m}}))))]"
function conflictsFor2 where "conflictsFor2 Or=(let (M, or)=ReducedRelation2 Or in if M=None then [{}]
else let m=the M in concat [remdups (generateConflicts5 (set Or) m c). c <- conflictsFor2 or])"
value "map (%n. listsum (map (size o conflictsFor2 o adj2PairList) (allReflPartialOrders n))) [1..<7]
(*Correctness theorem*)
theorem assumes "N>0" shows "card (esOver {0..<N}) =
listsum (map (size o remdups o conflictsFor2 o adj2PairList) (allReflPartialOrders N))"

Crossrefs

Cf. A001035 (generating all the event structures entails generating all the posets), A000798 (to generate all the posets we preemptively generated all the quasi-orders).

Sequence in context: A244437 A265003 A193363 * A327026 A244751 A022515

Adjacent sequences: A284273 A284274 A284275 * A284277 A284278 A284279

Keyword

nonn,hard,more

Author

Marco B. Caminati, Mar 24 2017

Extensions

a(7) from Marco B. Caminati, Aug 01 2017

Status

approved