Quantitative bisimulations using coreflections and open morphisms

TL;DR

This paper presents a categorical framework for defining bisimilarity in systems with quantitative information, leveraging coreflections and open morphisms to unify and extend existing bisimulation concepts.

Contribution

It introduces a canonical method for deriving bisimilarity via coreflections, applicable to probabilistic, timed, and hybrid systems, unifying their semantics.

Findings

Recovered path category for probabilistic systems

Derived path category for timed systems

Proposed new path category for hybrid systems

Abstract

We investigate a canonical way of defining bisimilarity of systems when their semantics is given by a coreflection, typically in a category of transition systems. We use the fact, from Joyal et al., that coreflections preserve open morphisms situations in the sense that a coreflection induces a path subcategory in the category of systems in such a way that open bisimilarity with respect to the induced path category coincides with usual bisimilarity of their semantics. We prove that this method is particularly well-suited for systems with quantitative information: we canonically recover the path category of probabilistic systems from Cheng et al., and of timed systems from Nielsen et al., and, finally, we propose a new canonical path category for hybrid systems.