Document Open Access Logo

Structural Operational Semantics for Heterogeneously Typed Coalgebras

Authors Harald König , Uwe Wolter , Tim Kräuter

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2023.7.pdf
  • Filesize: 1.99 MB
  • 17 pages

Document Identifiers

Author Details

Harald König
  • Fachhochschule für die Wirtschaft Hannover, Germany
  • Western Norway University of Applied Sciences, Bergen, Norway
Uwe Wolter
  • University of Bergen, Norway
Tim Kräuter
  • Western Norway University of Applied Sciences, Bergen, Norway

Funding

  • König, Harald: The author thanks the University of Bergen for support of this project.

Acknowledgements

The authors thank the anonymous referees for their helpful suggestions that have helped to improve this article.

Cite AsGet BibTex

Harald König, Uwe Wolter, and Tim Kräuter. Structural Operational Semantics for Heterogeneously Typed Coalgebras. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CALCO.2023.7

Abstract

Concurrently interacting components of a modular software architecture are heterogeneously structured behavioural models. We consider them as coalgebras based on different endofunctors. We formalize the composition of these coalgebras as specially tailored segments of distributive laws of the bialgebraic approach of Turi and Plotkin. The resulting categorical rules for structural operational semantics involve many-sorted algebraic specifications, which leads to a description of the components together with the composed system as a single holistic behavioural system. We evaluate our approach by showing that observational equivalence is a congruence with respect to the algebraic composition operation.

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
Keywords
  • Coalgebra
  • Bialgebra
  • Structural operational semantics
  • Compositionality

Metrics

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

References

  1. Luca Aceto, Wan J. Fokkink, and Chris Verhoef. Structural operational semantics. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 197-292. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50021-7.
  2. Falk Bartels. On generalised coinduction and probabilistic specification formats: distributive laws in coalgebraic modelling. Academisch Proefschrift, Vrije Universiteit Amsterdam, 2004. Google Scholar
  3. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. In Jeanne Ferrante and Peter Mager, editors, Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, pages 229-239. ACM Press, 1988. URL: https://doi.org/10.1145/73560.73580.
  4. Marco Brambilla, Jordi Cabot, and Manuel Wimmer. Model-driven software engineering in practice. Synthesis lectures on software engineering, 3(1):1-207, 2017. Google Scholar
  5. Julien Deantoni. Modeling the behavioral semantics of heterogeneous languages and their coordination. In 2016 Architecture-Centric Virtual Integration (ACVI), pages 12-18. IEEE, 2016. Google Scholar
  6. Gregor Engels, Jochen Malte Küster, Reiko Heckel, and Luuk Groenewegen. A methodology for specifying and analyzing consistency of object-oriented behavioral models. In A Min Tjoa and Volker Gruhn, editors, Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, Vienna, Austria, September 10-14, 2001, pages 186-195. ACM, 2001. URL: https://doi.org/10.1145/503209.503235.
  7. Cláudio Gomes, Casper Thule, David Broman, Peter Gorm Larsen, and Hans Vangheluwe. Co-simulation: a survey. ACM Computing Surveys (CSUR), 51(3):1-33, 2018. Google Scholar
  8. Jan Friso Groote and Frits Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and computation, 100(2):202-260, 1992. Google Scholar
  9. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. The microcosm principle and concurrency in coalgebra. In International Conference on Foundations of Software Science and Computational Structures, pages 246-260. Springer, 2008. Google Scholar
  10. Charles Antony Richard Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666-677, 1978. Google Scholar
  11. Bart Jacobs. Object-oriented hybrid systems of coalgebras plus monoid actions. Theoretical Computer Science, 239(1):41-95, 2000. Google Scholar
  12. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  13. Marco Kick, John Power, and Alex Simpson. Coalgebraic semantics for timed processes. Information and Computation, 204(4):588-609, 2006. Google Scholar
  14. Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci., 412(38):5043-5069, 2011. URL: https://doi.org/10.1016/j.tcs.2011.03.023.
  15. Harald König and Uwe Wolter. Consistency of heterogeneously typed behavioural models: A coalgebraic approach. In Yamine Aït Ameur and Florin Craciun, editors, Theoretical Aspects of Software Engineering - 16th International Symposium, TASE 2022, Cluj-Napoca, Romania, July 8-10, 2022, Proceedings, volume 13299 of Lecture Notes in Computer Science, pages 308-325. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10363-6_21.
  16. Alexander Kurz and Dirk Pattinson. Coalgebras and modal logic for parameterised endofunctors. Centrum voor Wiskunde en Informatica, 2000. Google Scholar
  17. Jochen Malte Küster. Towards Inconsistency Handling of Object-Oriented Behavioral Models. Electron. Notes Theor. Comput. Sci., 109:57-69, 2004. URL: https://doi.org/10.1016/j.entcs.2004.02.056.
  18. Marina Lenisa, John Power, and Hiroshi Watanabe. Category theory for operational semantics. Theor. Comput. Sci., 327(1-2):135-154, 2004. URL: https://doi.org/10.1016/j.tcs.2004.07.024.
  19. Dorian Leroy, Erwan Bousse, Manuel Wimmer, Tanja Mayerhofer, Benoit Combemale, and Wieland Schwinger. Behavioral interfaces for executable DSLs. Software and Systems Modeling, 19(4):1015-1043, 2020. Google Scholar
  20. Giovanni Liboni and Julien Deantoni. Cosim20: An integrated development environment for accurate and efficient distributed co-simulations. In Proceedings of the 2020 International Conference on Big Data in Management, pages 76-83, 2020. Google Scholar
  21. Robin Milner. Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, 1999. Google Scholar
  22. Mogens Nielsen and Glynn Winskel. Models for concurrency. In Handbook of Logic in Computer Science, Volume 4. Oxford Science Publications, 1995. Google Scholar
  23. Dirk Pattinson. Translating logics for coalgebras. In International Workshop on Algebraic Development Techniques, pages 393-408. Springer, 2002. Google Scholar
  24. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  25. Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-17336-3.
  26. Ana Sokolova. Probabilistic systems coalgebraically: A survey. Theoretical Computer Science, 412(38):5095-5110, 2011. Google Scholar
  27. Daniele Turi and Gordon Plotkin. Towards a mathematical operational semantics. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 280-291. IEEE, 1997. Google Scholar
  28. U. Wolter. (Co)Institutions for Coalgebras. Reports in Informatics 415, Dep. of Informatics, University of Bergen, 2016. Google Scholar
  29. Shuzhen Yao and Sol M Shatz. Consistency checking of UML dynamic models based on Petri net techniques. In 2006 15th International Conference on Computing, pages 289-297. IEEE, 2006. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact