Abstract

Bialgebraic semantics is a categorical approach to modelling well-behaved structural operational semantics (SOS), parametrised by notions of syntax and behaviour. Invented by Turi and Plotkin a decade ago, it allows us to derive formats for SOS descriptions of various “kinds” of systems (including labelled transition systems, probabilistic or timed systems etc.) in a systematic way. In each case, the canonical process equivalence related to the “kind”, or behaviour of systems, is guaranteed compositional. The well-known GSOS format can be seen as a special case of the bialgebraic approach, where the behaviour is the one for labelled transition systems and bisimilarity is compositional.

The original bialgebraic setting deals only with a single, canonical equivalence for each behaviour. In this talk I will show how to make the setting more flexible to accommodate other equivalences, e.g., trace or completed trace equivalences for labelled transition systems. To this end, I will show how to combine bialgebraic techniques with the coalgebraic approach to modal logic, to obtain “logical duals” to structural operational semantic descriptions.