A verified algorithm enumerating event structures

DOI10.1007/978-3-319-62075-6_17MaRDI QIDQ2364684zbMATH OpenOpenAlexFDO

Authors Marco Caminati, Juliana Küster-Filipe

Publication date 21 July 2017

Full work available at URL https://arxiv.org/abs/1705.07228, http://hdl.handle.net/10023/11248

zbMATH Keywords

discreteenumerationcountingformal methodslogicevent structuresautomated reasoningIsabelle/HOLverified algorithmOEIS

Mathematics Subject Classification ID

Exact enumeration problems, generating functions (05A15) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35) Software, source code, etc. for problems pertaining to ordered structures (06-04)

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.

Recommendations

• scientific article; zbMATH DE number 4018370
• Event structures and domains
• scientific article; zbMATH DE number 1361142
• scientific article; zbMATH DE number 4119660
• Simultaneity in event structures

Cites work

• scientific article; zbMATH DE number 2186890 (Why is no real title available?)
• scientific article; zbMATH DE number 4018370 (Why is no real title available?)
• Asymptotic Enumeration of Partial Orders on a Finite Set
• Conjugacy classes in unitriangular matrices.
• Contextual Petri nets, asymmetric event structures, and processes
• Decomposing Interactions
• Enumeration of AG-groupoids.
• Event Structure Semantics for Nominal Calculi
• Finite labelling problem in event structures
• Formal proof of SCHUR conjugate function
• Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
• Mechanical Analysis of Finite Idempotent Relations
• The On-Line Encyclopedia of Integer Sequences
• The Transitive Reduction of a Directed Graph

Cited in

(5)

• scientific article; zbMATH DE number 4208063 (Why is no real title available?)
• Tests and proofs for custom data generators
• Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
• Reconstructing invisible deviating events: a conformance checking approach for recurring events
• Isabelle formalisation of original representation theorems

Describes a project that uses

Uses Software

• FinFuns
• OEIS
• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication: A verified algorithm enumerating event structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2364684)