Document Open Access Logo

Minimisation of Event Structures

Authors Paolo Baldan , Alessandra Raffaetà

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2019.30.pdf
  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Software and its engineering → Formal methods
Keywords
  • Event structures
  • minimisation
  • history-preserving bisimilarity
  • behaviour-preserving quotient

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Event structures are fundamental models in concurrency theory, providing a representation of events in computation and of their relations, notably concurrency, conflict and causality. In this paper we present a theory of minimisation for event structures. Working in a class of event structures that generalises many stable event structure models in the literature, (e.g., prime, asymmetric, flow and bundle event structures) we study a notion of behaviour-preserving quotient, taking hereditary history preserving bisimilarity as a reference behavioural equivalence. We show that for any event structure a uniquely determined minimal quotient always exists. We observe that each event structure can be seen as the quotient of a prime event structure, and that quotients of general event structures arise from quotients of (suitably defined) corresponding prime event structures. This gives a special relevance to quotients in the class of prime event structures, which are then studied in detail, providing a characterisation and showing that also prime event structures always admit a unique minimal quotient.

Cite As Get BibTex

Paolo Baldan and Alessandra Raffaetà. Minimisation of Event Structures. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 30:1-30:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSTTCS.2019.30

Author Details

Paolo Baldan
  • University of Padova, Italy
Alessandra Raffaetà
  • Ca' Foscari University of Venice, Italy

Funding

  • Baldan, Paolo: Supported by the PRIN Project Analysis of Program Analyses (ASPRA).

References

  1. A. Armas-Cervantes, P. Baldan, M. Dumas, and L. García-Bañuelos. Diagnosing behavioral differences between business process models: An approach based on event structures. Information Systems, 56:304-325, 2016. Google Scholar
  2. A. Armas-Cervantes, P. Baldan, and L. García-Bañuelos. Reduction of event structures under history preserving bisimulation. Journal of Logical and Algebraic Methods in Programming, 85(6):1110-1130, 2016. Google Scholar
  3. P. Baldan. Modelling concurrent computations: from contextual Petri nets to graph grammars. PhD thesis, University of Pisa, 2000. Google Scholar
  4. P. Baldan, A. Corradini, H. Ehrig, M. Löwe, U. Montanari, and F. Rossi. Concurrent Semantics of Algebraic Graph Transformation Systems. In G. Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformation, volume III: Concurrency, pages 107-187. World Scientific, 1999. Google Scholar
  5. P. Baldan, A. Corradini, and U. Montanari. Contextual Petri nets, asymmetric event structures and processes. Information and Computation, 171(1):1-49, 2001. Google Scholar
  6. P. Baldan and A. Raffaetà. Minimising Event Structures, 2019. URL: http://arxiv.org/abs/1907.07042.
  7. M.A. Bednarczyk. Hereditary History Preserving Bisimulations or What is the Power of the Future Perfect in Program Logics. Technical report, Polish Academy of Sciences, 1991. Google Scholar
  8. G. Boudol. Flow Event Structures and Flow Nets. In Semantics of System of Concurrent Processes, volume 469 of LNCS, pages 62-95. Springer Verlag, 1990. Google Scholar
  9. G. Boudol and I. Castellani. Permutation of transitions: an event structure semantics for CCS and SCCS. In Linear Time, Branching Time and Partial Order Semantics in Logics and Models for Concurrency, volume 354 of LNCS, pages 411-427. Springer Verlag, 1988. Google Scholar
  10. R. Bruni, H.C. Melgratti, and U. Montanari. Event Structure Semantics for Nominal Calculi. In C. Baier and H. Hermanns, editors, CONCUR 2006, volume 4137 of LNCS, pages 295-309. Springer, 2006. Google Scholar
  11. S. Castellan. Weak memory models using event structures. In Proceedings of JFLA'16, 2016. Google Scholar
  12. I. Castellani. Bisimulations for Concurrency. PhD thesis, University of Edimburgh, 1988. Google Scholar
  13. S. Chakraborty and V. Vafeiadis. Grounding thin-air reads with event structures. PACMPL, 3(POPL):70:1-70:28, 2019. Google Scholar
  14. I. Cristescu, J. Krivine, and D. Varacca. Rigid families for CCS and the pi-calculus. In Proceedings of ICTAC'15, volume 9399 of LNCS, pages 223-240. Springer, 2015. Google Scholar
  15. M. Dumas and L. García-Bañuelos. Process Mining Reloaded: Event Structures as a Unified Representation of Process Models and Event Logs. In R.R. Devillers and A. Valmari, editors, Petri Nets 2015, volume 9115 of LNCS, pages 33-48. Springer, 2015. Google Scholar
  16. J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 2006. Google Scholar
  17. A. Jeffrey and J. Riely. On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory. In M. Grohe, E. Koskinen, and N. Shankar, editors, LICS 2016, pages 759-767. ACM, 2016. Google Scholar
  18. A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from Open Maps. Information and Computation, 127(2):164-185, 1996. Google Scholar
  19. M. Jurdzinski, M. Nielsen, and J. Srba. Undecidability of domino games and hhp-bisimilarity. Information and Computation, 184(2):343-368, 2003. Google Scholar
  20. R. Langerak. Bundle Event Structures: A Non-Interleaving Semantics for Lotos. In 5th Intl. Conf. on Formal Description Techniques (FORTE'92), pages 331-346. North-Holland, 1992. Google Scholar
  21. R. Langerak. Transformation and Semantics for LOTOS. PhD thesis, Department of Computer Science, University of Twente, 1992. Google Scholar
  22. A.R. Meyer and L.J. Stockmeyer. The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Space. In SWAT (FOCS), pages 125-129. IEEE Computer Society, 1972. Google Scholar
  23. U. Montanari and M. Pistore. Minimal Transition Systems for History-Preserving Bisimulation. In 14th Annual Symposium on Theoretical Aspects of Computer Science, volume 1200 of LNCS, pages 413-425. Springer Verlag, 1997. Google Scholar
  24. M. Nielsen, G. Plotkin, and G. Winskel. Petri Nets, Event Structures and Domains, Part 1. Theoretical Computer Science, 13:85-108, 1981. Google Scholar
  25. J. Pichon-Pharabod and P. Sewell. A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In R. Bodík and R. Majumdar, editors, POPL 2016, pages 622-633. ACM, 2016. Google Scholar
  26. A. Rensink. Posets for Configurations! In W. R. Cleaveland, editor, Proceedings of CONCUR'92, volume 630 of LNCS, pages 269-285. Springer, 1992. Google Scholar
  27. G. Schied. On relating Rewriting Systems and Graph Grammars to Event Structures. In H.-J. Schneider and H. Ehrig, editors, Dagstuhl Seminar 9301 on Graph Transformations in Computer Science, volume 776 of LNCS, pages 326-340. Springer, 1994. Google Scholar
  28. R.J. van Glabbeek. History preserving process graphs. Draft available at http://theory.stanford.edu/~rvg/abstracts.html#hppg, 1996.
  29. R.J. van Glabbeek and U. Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37(4/5):229-327, 2001. Google Scholar
  30. R.J. van Glabbeek and G.D. Plotkin. Configuration structures, event structures and Petri nets. Theoretical Computer Science, 410(41):4111-4159, 2009. Google Scholar
  31. D. Varacca and N. Yoshida. Typed event structures and the linear pi-calculus. Theoretical Computer Science, 411(19):1949-1973, 2010. Google Scholar
  32. G. Winskel. Event Structure Semantics for CCS and Related Languages. Technical Report DAIMI PB-159, University of Aarhus, 1983. Google Scholar
  33. G. Winskel. Event Structures. In Petri Nets: Applications and Relationships to Other Models of Concurrency, volume 255 of LNCS, pages 325-392. Springer, 1987. Google Scholar
  34. G. Winskel. Events, Causality and Symmetry. Computer Journal, 54(1):42-57, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact