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 special order enriched categories, i.e. categories whose hom-sets are endowed with suitable complete orders. Using this structure we provide an abstract notion of saturation, which allows us to define various (weak) behavioural equivalences. We show that the Kleisli categories of many common monads are categories of this kind. On one hand, this allows us to 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; on the other, we can readily provide new weak behavioural equivalences for more complex behaviours, like those definable on presheaves, topological spaces, measurable spaces, etc.
Original language | English |
---|---|
Journal | Journal of Logical and Algebraic Methods in Programming |
Volume | 84 |
Issue number | 6 |
Pages (from-to) | 826-852 |
DOIs | |
Publication status | Published - Nov 2015 |
Externally published | Yes |
Keywords
- Formal methods
- Process calculi
- Behavioural Theory
- Weak behavioural equivalences
- Coalgebraic semantics
- Quantitative methods
- Quantitative models
- Programming Languages
- Semantics