A verified algorithm enumerating event structures

Juliana Kuster Filipe Bowles, Marco Bright Caminati

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 af inite 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.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings
EditorsHerman Geuvers, Matthew England, Osman Hasan, Florian Rabe, Olaf Teschke
Place of PublicationCham
PublisherSpringer
Pages239-254
ISBN (Print)9783319620749, 9783319620756
DOIs
Publication statusPublished - 2017
Event10th Conference on Intelligent Computer Mathematics (CICM 2017) - Edinburgh, United Kingdom
Duration: 17 Jul 201721 Jul 2017
Conference number: 10
http://www.cicm-conference.org/2017

Publication series

NameLecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)
PublisherSpringer
Volume10383
ISSN (Print)0302-9743

Conference

Conference10th Conference on Intelligent Computer Mathematics (CICM 2017)
Abbreviated titleCICM
Country/TerritoryUnited Kingdom
CityEdinburgh
Period17/07/1721/07/17
Internet address

Fingerprint

Dive into the research topics of 'A verified algorithm enumerating event structures'. Together they form a unique fingerprint.

Cite this