Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
DeepAlgebra - An Outline of a Program Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

A Verified Algorithm Enumerating Event Structures

verfasst von : Juliana Bowles, Marco B. Caminati

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Mathematical Models as Research Data via Flexiformal Theory Graphs
Nächstes Kapitel Reasoning with Concept Diagrams About Antipatterns in Ontologies
Fußnoten
1
 
2
Such a notation has the form, in the simplest but typical case, https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-62075-6_17/454024_1_En_17_IEq184_HTML.gif , and intuitively represents the list obtained by applying the generic function https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-62075-6_17/454024_1_En_17_IEq185_HTML.gif to the entries of a given list https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-62075-6_17/454024_1_En_17_IEq186_HTML.gif which satisfy a condition https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-62075-6_17/454024_1_En_17_IEq187_HTML.gif .
 
Literatur
1.
2.
3.
Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures, and processes. Inf. Comput. 171(1), 1–49 (2001)MathSciNetCrossRefMATH
4.
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)
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 CrossRef
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 CrossRef
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)
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 CrossRef
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 CrossRef
12.
Kammüller, F.: Mechanical analysis of finite idempotent relations. Fundamenta Informaticae 107(1), 43–65 (2011)MathSciNetMATH
13.
Kleitman, D.J., Rothschild, B.L.: Asymptotic enumeration of partial orders on a finite set. Trans. Am. Math. Soc. 205, 205–220 (1975)MathSciNetCrossRefMATH
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 CrossRef
15.
16.
Sloane, N.: The on-line Encyclopedia of integer sequences. Ann. Math. Informaticae 41, 219–234 (2013)MathSciNetMATH
17.
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.
20.
Metadaten
Titel
A Verified Algorithm Enumerating Event Structures
verfasst von
Juliana Bowles
Marco B. Caminati
Copyright-Jahr
2017
Buch
Intelligent Computer Mathematics

Print ISBN: 978-3-319-62074-9

Electronic ISBN: 978-3-319-62075-6

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-62075-6_17