Compositionality in Coalgebraic Trace Semantics

Jourde R, Urbat H, Goncharov S, Tsampas S, Forster J (2026)

Publication Type: Conference contribution

Publication year: 2026

Journal

LIPIcs : Leibniz International Proceedings in Informatics Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Book Volume: 391

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Liverpool GB

ISBN: 9783959774475

DOI: 10.4230/LIPIcs.CONCUR.2026.38

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.

Authors with CRIS profile

Henning Urbat Lehrstuhl für Informatik 8 (Theoretische Informatik) Jonas Forster Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

University of Savoy Mont Blanc / Université Savoie Mont Blanc FR France (FR) University of Birmingham GB United Kingdom (GB) University of Southern Denmark / Syddansk Universitet DK Denmark (DK)

How to cite

APA:

Jourde, R., Urbat, H., Goncharov, S., Tsampas, S., & Forster, J. (2026). Compositionality in Coalgebraic Trace Semantics. In Ana Sokolova, Patrick Totzke (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Liverpool, GB: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Jourde, Robin, et al. "Compositionality in Coalgebraic Trace Semantics." Proceedings of the 37th International Conference on Concurrency Theory, CONCUR 2026, Liverpool Ed. Ana Sokolova, Patrick Totzke, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2026.

BibTeX: Download