Skip to content

Research at St Andrews

A verified algorithm enumerating event structures

Research output: ResearchConference contribution


Open Access permissions



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
ISBN (Print)9783319620749, 9783319620756
StatePublished - 2017
Event10th Conference on Intelligent Computer Mathematics (CICM 2017) - Edinburgh, United Kingdom
Duration: 17 Jul 201721 Jul 2017
Conference number: 10

Publication series

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


Conference10th Conference on Intelligent Computer Mathematics (CICM 2017)
Abbreviated titleCICM
CountryUnited Kingdom
Internet address

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. An integrated framework for verifying multiple care pathways

    Bowles, J. K. F., Caminati, M. B. & Cha, S. 13 Sep 2017 Eleventh International Symposium on Theoretical Aspects of Software Engineering. IEEE Computer Society, 8 p.

    Research output: ResearchConference contribution

  2. A flexible approach for finding optimal paths with minimal conflicts

    Bowles, J. K. F. & Caminati, M. B. 2017 Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings. Duan, Z. & Ong, L. (eds.). Springer, p. 209-225 16 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 10610)

    Research output: ResearchConference contribution

  3. Correct composition of dephased behavioural models

    Bowles, J. K. F. & Caminati, M. B. 2017 Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings. Proença, J. & Lumpe, M. (eds.). Springer, p. 233-250 18 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 10487)

    Research output: ResearchConference contribution

  4. Mind the gap: addressing behavioural inconsistencies with formal methods

    Bowles, J. K. F. & Caminati, M. B. 6 Dec 2016 2016 23rd Asia-Pacific Software Engineering Conference (APSEC). Potanin, A., Murphy, G. C., Reeves, S. & Dietrich, J. (eds.). IEEE Computer Society, p. 313-320 8 p. 7890603

    Research output: ResearchConference contribution

  5. Aplicação de técnicas quantitativas de modelagem na busca da eficiência de processos hospitalares

    Webber, T., Caminati, M. B., Mueller, M., Redeker, G., Bowles, J. K. F., Czekster, R. & Quickert, S. 23 Sep 2016 (Accepted/In press)

    Research output: Research - peer-reviewPoster

ID: 250067602