A Verified Algorithm Enumerating Event Structures

TL;DR

This paper introduces a verified algorithm for generating all event structures over a finite set, along with implementations and enumeration results, including a new sequence added to OEIS.

Contribution

It presents the first verified algorithm to enumerate all event structures, preorders, and partial orders over finite sets, with formal proofs and a new OEIS sequence.

Findings

Successfully verified the enumeration algorithm using Isabelle/HOL.

Generated a new integer sequence for event structures added to OEIS.

Provided a functional implementation of the enumeration process.

Abstract

An event structure is a mathematical abstraction modeling concepts as causality, conflict and concurrency between events. While many other mathematical structures, including groups, topological spaces, rings, abound with algorithms and formulas to generate, enumerate and count particular sets of their members, no algorithm or formulas are known to generate or count all the possible event structures over a finite set of events. We present an algorithm to generate such a family, along with a functional implementation verified using Isabelle/HOL. As byproducts, we obtain a verified enumeration of all possible preorders and partial orders. While the integer sequences counting preorders and partial orders are already listed on OEIS (On-line Encyclopedia of Integer Sequences), the one counting event structures is not. We therefore used our algorithm to submit a formally verified addition, which has been successfully reviewed and is now part of the OEIS.