Compositionality in Coalgebraic Trace Semantics
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910232488181760 |
|---|---|
| author | Jourde, Robin Urbat, Henning Goncharov, Sergey Tsampas, Stelios Forster, Jonas |
| author_facet | Jourde, Robin Urbat, Henning Goncharov, Sergey Tsampas, Stelios Forster, Jonas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_18285 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Compositionality in Coalgebraic Trace Semantics Jourde, Robin Urbat, Henning Goncharov, Sergey Tsampas, Stelios Forster, Jonas Logic in Computer Science 68Q85 F.3.2 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. |
| title | Compositionality in Coalgebraic Trace Semantics |
| topic | Logic in Computer Science 68Q85 F.3.2 |
| url | https://arxiv.org/abs/2605.18285 |