×

A verified algorithm enumerating event structures. (English) Zbl 1367.68245

Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 239-254 (2017).
Summary: 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.
For the entire collection see [Zbl 1364.68010].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
05A15 Exact enumeration problems, generating functions
06-04 Software, source code, etc. for problems pertaining to ordered structures
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

References:

[1] Aho, A.V., Garey, M.R., Ullman, J.D.: The transitive reduction of a directed graph. SIAM J. Comput. 1(2), 131–137 (1972) · Zbl 0247.05128 · doi:10.1137/0201008
[2] Assous, M.R., et al.: Finite labelling problem in event structures. Theor. Comput. Sci. 123(1), 9–19 (1994) · Zbl 0801.68057 · doi:10.1016/0304-3975(94)90065-5
[3] Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures, and processes. Inf. Comput. 171(1), 1–49 (2001) · Zbl 1005.68103 · doi:10.1006/inco.2001.3060
[4] 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 · Zbl 1236.68039 · doi:10.1007/11784180_16
[5] 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) · doi:10.1109/APSEC.2016.051
[6] 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 · Zbl 1151.68512 · doi:10.1007/11817949_20
[7] 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 · Zbl 1286.68392 · doi:10.1007/978-3-642-14128-7_15
[8] 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) · doi:10.1145/2764468.2764511
[9] Costa-Gomes, M., et al.: Choice, Deferral and Consistency. Discussion Paper Series, Department of Economics 201416. Department of Economics, University of St. Andrews (2014)
[10] 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 · Zbl 1250.20055 · doi:10.1007/978-3-642-22673-1_1
[11] 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 · doi:10.1007/978-3-319-21215-9_7
[12] Kammüller, F.: Mechanical analysis of finite idempotent relations. Fundamenta Informaticae 107(1), 43–65 (2011) · Zbl 1230.68175
[13] Kleitman, D.J., Rothschild, B.L.: Asymptotic enumeration of partial orders on a finite set. Trans. Am. Math. Soc. 205, 205–220 (1975) · Zbl 0302.05007 · doi:10.1090/S0002-9947-1975-0369090-9
[14] 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 · Zbl 1252.68260 · doi:10.1007/978-3-642-03359-9_22
[15] Pfeiffer, G.: Counting transitive relations. J. Integer Sequences 7(2), 3 (2004) · Zbl 1071.06003
[16] Sloane, N.: The on-line Encyclopedia of integer sequences. Ann. Math. Informaticae 41, 219–234 (2013) · Zbl 1274.11001
[17] Vera-López, A., Arregi, J.: Conjugacy classes in unitriangular matrices. Linear Algebra Appl. 370, 85–124 (2003) · Zbl 1045.20045 · doi:10.1016/S0024-3795(03)00371-9
[18] 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)
[19] 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 · Zbl 0626.68022 · doi:10.1007/3-540-17906-2_31
[20] Winskel, G.: Events, causality and symmetry. Comput. J. 54(1), 42–57 (2011). https://doi.org/10.1093/comjnl/bxp052 · doi:10.1093/comjnl/bxp052
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.