A verified algorithm enumerating event structures

DOI10.1007/978-3-319-62075-6_17zbMATH Open1367.68245arXiv1705.07228OpenAlexW2620363064MaRDI QIDQ2364684FDOQ2364684

Authors: Marco Caminati, Juliana Küster-Filipe 

Publication date: 21 July 2017

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.

Full work available at URL: https://arxiv.org/abs/1705.07228

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

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)

Cites Work

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

Cited In (5)

• Title not available (Why is that?)
• 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

Uses Software

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

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)