Compositionality in Coalgebraic Trace Semantics

TL;DR

This paper extends the abstract GSOS framework to coalgebraic trace semantics, introducing De Simone laws that ensure compositionality for trace equivalence in various process models.

Contribution

It generalizes Turi and Plotkin's approach to trace semantics, introduces De Simone laws over Kleisli categories, and applies this to probabilistic systems.

Findings

Proves De Simone laws are compositional for coalgebraic trace equivalence.

Recovers known compositionality results for labelled transition systems.

Derives a new De Simone-type format for probabilistic systems.

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.