Home > Research > Publications & Outputs > A verified algorithm enumerating event structures

Text available via DOI:

View graph of relations

A verified algorithm enumerating event structures

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published

Standard

A verified algorithm enumerating event structures. / Bowles, Juliana; Caminati, Marco B.
Intelligent Computer Mathematics. Vol. 10383 Springer, 2017.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Harvard

Bowles, J & Caminati, MB 2017, A verified algorithm enumerating event structures. in Intelligent Computer Mathematics. vol. 10383, Springer. https://doi.org/10.1007/978-3-319-62075-6_17

APA

Bowles, J., & Caminati, M. B. (2017). A verified algorithm enumerating event structures. In Intelligent Computer Mathematics (Vol. 10383). Springer. https://doi.org/10.1007/978-3-319-62075-6_17

Vancouver

Bowles J, Caminati MB. A verified algorithm enumerating event structures. In Intelligent Computer Mathematics. Vol. 10383. Springer. 2017 doi: 10.1007/978-3-319-62075-6_17

Author

Bowles, Juliana ; Caminati, Marco B. / A verified algorithm enumerating event structures. Intelligent Computer Mathematics. Vol. 10383 Springer, 2017.

Bibtex

@inproceedings{f2c1453f8627477eaef0d4a1dc15ea60,
title = "A verified algorithm enumerating event structures",
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.",
author = "Juliana Bowles and Caminati, {Marco B.}",
year = "2017",
month = jun,
day = "28",
doi = "10.1007/978-3-319-62075-6_17",
language = "English",
isbn = "9783319620749",
volume = "10383",
booktitle = "Intelligent Computer Mathematics",
publisher = "Springer",

}

RIS

TY - GEN

T1 - A verified algorithm enumerating event structures

AU - Bowles, Juliana

AU - Caminati, Marco B.

PY - 2017/6/28

Y1 - 2017/6/28

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-62075-6_17

DO - 10.1007/978-3-319-62075-6_17

M3 - Conference contribution/Paper

SN - 9783319620749

SN - 9783319620756

VL - 10383

BT - Intelligent Computer Mathematics

PB - Springer

ER -