Behavioural equivalences for coalgebras with unobservable moves

TL;DR

This paper develops a categorical framework for defining weak behavioural equivalences in coalgebras with unobservable moves, unifying and extending existing concepts across various systems and introducing new equivalences for complex behaviors.

Contribution

It introduces a parametrized saturation categorical framework that generalizes weak behavioural equivalences and applies to a wide range of systems, including complex topological and measurable behaviors.

Findings

Framework unifies existing weak behavioural equivalences

Applicable to systems like weighted LTS, Segala systems, and calculi with names

Introduces new equivalences for topological and measurable spaces

Abstract

We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on parametrized saturation categories, i.e. categories whose hom-sets are endowed with complete orders and a suitable iteration operators; this structure allows us to provide the abstract definitions of various (weak) behavioural equivalence. We show that the Kleisli categories of many common monads are categories of this kind. This allows us to readily instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences. Moreover, we can provide neatly new weak behavioural equivalences for more complex behaviours, like those definable on topological spaces, measurable spaces, etc.