Document Open Access Logo

Compositionality in Coalgebraic Trace Semantics

Authors Robin Jourde , Henning Urbat , Sergey Goncharov , Stelios Tsampas , Jonas Forster

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.38.pdf
  • Filesize: 0.82 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
Keywords
  • Coalgebra
  • Operational Semantics
  • Process Algebra
  • Abstract GSOS
  • Trace Semantics
  • Rule Formats

Metrics

Abstract

A key requirement on any well-behaved process language is its compositionality: behavioural equivalence of processes should be respected by the constructors of the language. Turi and Plotkin’s abstract GSOS provides an elegant bialgebraic framework for modelling rule formats that guarantee compositionality from the outset. Their original results, however, are restricted to compositionality of strong bisimilarity, a rather fine-grained notion of process equivalence. In the present paper, we demonstrate that Turi and Plotkin’s approach also applies to trace equivalence, which only observes external actions of processes. To this end, we revisit the general compositionality result of their original theory and present it in a refined form with regard to the required naturality conditions. This step makes abstract GSOS applicable over Kleisli categories and thereby enables reasoning about compositionality in the setting of coalgebraic trace semantics. As our main contribution, we introduce De Simone laws, a type of GSOS laws over Kleisli categories, and prove that their operational models are compositional for coalgebraic trace equivalence. This result recovers and explains compositionality of the well-known De Simone rule format for labelled transition systems in a natural categorical setting. As a further application, we derive from our general framework a novel De Simone-type format for probabilistic systems, compositional for probabilistic trace equivalence.

Cite As Get BibTex

Robin Jourde, Henning Urbat, Sergey Goncharov, Stelios Tsampas, and Jonas Forster. Compositionality in Coalgebraic Trace Semantics. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.38

Author Details

Robin Jourde
  • Univ. Savoie Mont Blanc, CNRS, LAMA, Chambéry, France
Henning Urbat
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Sergey Goncharov
  • University of Birmingham, UK
Stelios Tsampas
  • University of Southern Denmark, Odense, Denmark
Jonas Forster
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Urbat, Henning: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 569130867.
  • Goncharov, Sergey: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 527481841.
  • Tsampas, Stelios: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 527481841.
  • Forster, Jonas: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 434050016.

References

  1. Faris Abou-Saleh. A coalgebraic semantics for imperative programming languages. PhD thesis, Imperial College London, UK, 2014. URL: http://hdl.handle.net/10044/1/13693.
  2. Faris Abou-Saleh and Dirk Pattinson. Towards effects in mathematical operational semantics. In Michael W. Mislove and Joël Ouaknine, editors, Mathematical Foundations of Programming Semantics, MFPS 2011, volume 276 of ENTCS, pages 81-104. Elsevier, 2011. URL: https://doi.org/10.1016/j.entcs.2011.09.016.
  3. Faris Abou-Saleh and Dirk Pattinson. Comodels and effects in mathematical operational semantics. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7794 of Lecture Notes in Computer Science, pages 129-144. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37075-5_9.
  4. 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.
  5. Giorgio Bacci and Marino Miculan. Structural operational semantics for continuous state probabilistic processes. In Dirk Pattinson and Lutz Schröder, editors, Coalgebraic Methods in Computer Science, pages 71-89, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-32784-1_5.
  6. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  7. Michael Barr. Coequalizers and free triples. Math. Z., 116:307-322, 1970. Google Scholar
  8. Falk Bartels. GSOS for probabilistic transition systems. In Lawrence S. Moss, editor, Coalgebraic Methods in Computer Science, CMCS 2002, Satellite Event of ETAPS 2002, Grenoble, France, April 6-7, 2002, volume 65 of Electronic Notes in Theoretical Computer Science, pages 29-53. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80358-X.
  9. Falk Bartels. On generalised coinduction and probabilistic specification formats: Distributive laws in coalgebraic modelling. PhD thesis, Vrije Universiteit Amsterdam, 2004. Google Scholar
  10. Bard Bloom. When is partial trace equivalence adequate? Formal Aspects of Computing, 6(3):317-338, 1994. URL: https://doi.org/10.1007/BF01215409.
  11. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. J. ACM, 42(1):232-268, 1995. URL: https://doi.org/10.1145/200836.200876.
  12. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, Beijing, China, September 4-7, 2018, LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.17.
  13. Tomasz Brengos, Marino Miculan, and Marco Peressotti. Behavioural equivalences for coalgebras with unobservable moves. J. Log. Algebraic Methods Program., 84(6):826-852, 2015. URL: https://doi.org/10.1016/j.jlamp.2015.09.002.
  14. Valentina Castiglioni, Ruggero Lanotte, and Simone Tini. Back to the format: A survey on sos for probabilistic processes. Journal of Logical and Algebraic Methods in Programming, 137:100929, 2024. URL: https://doi.org/10.1016/j.jlamp.2023.100929.
  15. Kenta Cho and Bart Jacobs. Disintegration and Bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 29, 2019. arXiv:1709.00322. URL: https://doi.org/10.1017/S0960129518000488.
  16. Dion Coumans and Bart Jacobs. Scalars, monads, and categories. In Quantum Physics and Linguistics - A Compositional, Diagrammatic Discourse, pages 184-216. Oxford University Press, 2013. URL: https://doi.org/10.1093/ACPROF:OSO/9780199646296.003.0007.
  17. R. de Simone. Higher-level synchronising devices in meije-sccs. Theoretical Computer Science, 37(3):245-267, 1985. URL: https://doi.org/10.1016/0304-3975(85)90093-3.
  18. Manfred Droste, Werner Kuich, and Heiko Vogler, editors. Handbook of Weighted Automata. Springer, 2009. Google Scholar
  19. Florian Frank, Stefan Milius, and Henning Urbat. Coalgebraic semantics for nominal automata. In Coalgebraic Methods in Computer Science - 16th IFIP WG 1.3 International Workshop, CMCS 2022, Colocated with ETAPS 2022, Munich, Germany, April 2-3, 2022, Proceedings, volume 13225 of Lecture Notes in Computer Science, pages 45-66. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10736-8_3.
  20. Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370, 2020. arXiv:1908.07021. URL: https://doi.org/10.1016/j.aim.2020.107239.
  21. Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Stateful structural operational semantics. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD'22, volume 228 of LIPIcs, pages 30:1-30:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.30.
  22. Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Towards a higher-order mathematical operational semantics. In 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023), volume 7 of Proc. ACM Program. Lang. ACM, 2023. URL: https://doi.org/10.1145/3571215.
  23. Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Bialgebraic reasoning on stateful languages, 2025. To appear in Proc. ICFP 2025. URL: https://doi.org/10.48550/arXiv.2503.10955.
  24. Jan Friso Groote and Frits W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Inf. Comput., 100(2):202-260, 1992. URL: https://doi.org/10.1016/0890-5401(92)90013-6.
  25. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3(4), 2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.
  26. Bart Jacobs. Trace semantics for coalgebras. Electr. Notes Theor. Comput. Sci., 106:167-184, 2004. URL: https://doi.org/10.1016/j.entcs.2004.02.031.
  27. 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.
  28. Bartek Klin. Bialgebraic methods and modal logic in structural operational semantics. Inf. Comput., 207(2):237-257, 2009. URL: https://doi.org/10.1016/J.IC.2007.10.006.
  29. Bartek Klin. Structural operational semantics and modal logic, revisited. In Proceedings of the Tenth Workshop on Coalgebraic Methods in Computer Science, CMCS@ETAPS 2010, Paphos, Cyprus, March 26-28, 2010, number 2 in Electronic Notes in Theoretical Computer Science, pages 155-175. Elsevier, 2010. URL: https://doi.org/10.1016/J.ENTCS.2010.07.019.
  30. 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.
  31. Bartek Klin and Vladimiro Sassone. Structural operational semantics for stochastic process calculi. In Roberto M. Amadio, editor, 11th International Conference Foundations of Software Science and Computational Structures, FOSSACS'08, volume 4962 of LNCS, pages 428-442. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_30.
  32. Bartek Klin and Vladimiro Sassone. Structural operational semantics for stochastic and weighted transition systems. Inf. Comput., 227:58-83, 2013. URL: https://doi.org/10.1016/J.IC.2013.04.001.
  33. Anders Kock. Commutative monads as a theory of distributions. Theory and Applications of Categories, 26(4):97-131, 2012. URL: http://www.tac.mta.ca/tac/volumes/26/4/26-04abs.html.
  34. Joachim Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151-161, 1968. Google Scholar
  35. Paul Blain Levy and Sergey Goncharov. Coinductive resumption monads: Guarded iterative and guarded elgot. In Proc. 8rd international conference on Algebra and coalgebra in computer science (CALCO 2019), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CALCO.2019.13.
  36. Harald Lindner. Affine parts of monads. Arch. Math., 33(1):437-443, December 1979. Google Scholar
  37. S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, 2 edition, 1978. URL: http://link.springer.com/10.1007/978-1-4757-4721-8.
  38. Marino Miculan and Marco Peressotti. Structural operational semantics for non-deterministic processes with quantitative aspects. Theor. Comput. Sci., 655:135-154, 2016. URL: https://doi.org/10.1016/j.tcs.2016.01.012.
  39. Philip S. Mulry. Lifting theorems for kleisli categories. In Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings, volume 802 of Lecture Notes in Computer Science, pages 304-319. Springer, 1993. URL: https://doi.org/10.1007/3-540-58027-1_15.
  40. 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.
  41. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1), 2013. URL: https://doi.org/10.2168/LMCS-9(1:9)2013.
  42. Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, and Frank Piessens. Abstract congruence criteria for weak bisimilarity. In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science, MFCS'21, volume 202 of LIPIcs, pages 88:1-88:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.88.
  43. Daniele Turi. Categorical modelling of structural operational rules: Case studies. In Category Theory and Computer Science, 7th International Conference, CTCS '97, Santa Margherita Ligure, Italy, September 4-6, 1997, Proceedings, pages 127-146, 1997. URL: https://doi.org/10.1007/BFb0026985.
  44. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In 12th Annual IEEE Symposium on Logic in Computer Science (LICS 1997), pages 280-291, 1997. URL: https://doi.org/10.1109/LICS.1997.614955.
  45. Henning Urbat. Higher-order behavioural conformances via fibrations. Proc. ACM Program. Lang., 10(POPL), January 2026. URL: https://doi.org/10.1145/3776697.
  46. R. J. van Glabbeek. The linear time - branching time spectrum. In CONCUR '90 Theories of Concurrency: Unification and Extension, pages 278-297. Springer, 1990. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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