Behavioural equivalences for coalgebras with unobservable moves
arXiv:1411.0090 · doi:10.1016/j.jlamp.2015.09.002
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.
References in corpus (12)
- A 2-categories companion
- Generalizing determinization from automata to coalgebras
- Generic Trace Semantics via Coinduction
- Relating coalgebraic notions of bisimulation
- Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems
- Presenting Distributive Laws
- Weak bisimulation for coalgebras over order enriched monads
- Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes
- Weak bisimulations for labelled transition systems weighted over semirings
- How to Kill Epsilons with a Dagger -- A Coalgebraic Take on Systems with Algebraic Label Structure
- Morita contexts as lax functors
- Structural operational semantics for non-deterministic processes with quantitative aspects
Cited by in corpus (12)
- Relating Apartness and Bisimulation
- How to Kill Epsilons with a Dagger -- A Coalgebraic Take on Systems with Algebraic Label Structure
- Coalgebraic Infinite Traces and Kleisli Simulations
- A Definition Scheme for Quantitative Bisimulation
- Behavioural equivalences for timed systems
- Structural operational semantics for non-deterministic processes with quantitative aspects
- Lax functors and coalgebraic weak bisimulation
- Better Late Than Never: A Fully Abstract Semantics for Classical Processes
- On the trade-off between labels and weights in quantitative bisimulation
- Endofunctors modelling higher-order behaviours
- A coalgebraic take on regular and -regular behaviours
- Linear Logic, the -calculus, and their Metatheory: A Recipe for Proofs as Processes