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.
This research is supported by EPSRC grant EP/M014290/1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
About 9.5 KSLOC, available at http://bitbucket.org/caminati/oeises.
- 2.
Such a notation has the form, in the simplest but typical case,
, and intuitively represents the list obtained by applying the generic function 
to the entries of a given list 
which satisfy a condition 
.
, and intuitively represents the list obtained by applying the generic function 
to the entries of a given list 
which satisfy a condition 
.References
Aho, A.V., Garey, M.R., Ullman, J.D.: The transitive reduction of a directed graph. SIAM J. Comput. 1(2), 131–137 (1972)
Assous, M.R., et al.: Finite labelling problem in event structures. Theor. Comput. Sci. 123(1), 9–19 (1994)
Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures, and processes. Inf. Comput. 171(1), 1–49 (2001)
Bowles, J.K.F.: Decomposing interactions. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 189–203. Springer, Heidelberg (2006). doi:10.1007/11784180_16
Bowles, J.K.F., Caminati, M.B.: Mind the gap: addressing behavioural inconsistencies with formal methods. In: 2016 23rd Asia-Pacific Software Engineering Conference (APSEC). IEEE Computer Society (2016)
Bruni, R., Melgratti, H., Montanari, U.: Event structure semantics for nominal calculi. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 295–309. Springer, Heidelberg (2006). doi:10.1007/11817949_20
Butelle, F., Hivert, F., Mayero, M., Toumazet, F.: Formal proof of SCHUR conjugate function. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) CICM 2010. LNCS, vol. 6167, pp. 158–171. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14128-7_15
Caminati, M.B., et al.: Sound auction specification and implementation. In: Proceedings of the Sixteenth ACM Conference on Economics and Computation, pp. 547–564. ACM (2015)
Costa-Gomes, M., et al.: Choice, Deferral and Consistency. Discussion Paper Series, Department of Economics 201416. Department of Economics, University of St. Andrews (2014)
Distler, A., Shah, M., Sorge, V.: Enumeration of AG-Groupoids. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS, vol. 6824, pp. 1–14. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22673-1_1
Genestier, R., Giorgetti, A., Petiot, G.: Sequential generation of structured arrays and its deductive verification. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 109–128. Springer, Cham (2015). doi:10.1007/978-3-319-21215-9_7
Kammüller, F.: Mechanical analysis of finite idempotent relations. Fundamenta Informaticae 107(1), 43–65 (2011)
Kleitman, D.J., Rothschild, B.L.: Asymptotic enumeration of partial orders on a finite set. Trans. Am. Math. Soc. 205, 205–220 (1975)
Lochbihler, A.: Formalising finfuns – generating code for functions as data from Isabelle/HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 310–326. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_22
Pfeiffer, G.: Counting transitive relations. J. Integer Sequences 7(2), 3 (2004)
Sloane, N.: The on-line Encyclopedia of integer sequences. Ann. Math. Informaticae 41, 219–234 (2013)
Vera-López, A., Arregi, J.: Conjugacy classes in unitriangular matrices. Linear Algebra Appl. 370, 85–124 (2003)
Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science: Semantic Modelling, vol. 4, pp. 1–148. Oxford University Press, Oxford (1995)
Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987). doi:10.1007/3-540-17906-2_31
Winskel, G.: Events, causality and symmetry. Comput. J. 54(1), 42–57 (2011). https://doi.org/10.1093/comjnl/bxp052
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Bowles, J., Caminati, M.B. (2017). A Verified Algorithm Enumerating Event Structures. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds) Intelligent Computer Mathematics. CICM 2017. Lecture Notes in Computer Science(), vol 10383. Springer, Cham. https://doi.org/10.1007/978-3-319-62075-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-62075-6_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-62074-9
Online ISBN: 978-3-319-62075-6
eBook Packages: Computer ScienceComputer Science (R0)