Conformance Games for Graded Semantics
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916583548387328 |
|---|---|
| author | Forster, Jonas Schröder, Lutz Wild, Paul |
| author_facet | Forster, Jonas Schröder, Lutz Wild, Paul |
| contents | Game-theoretic characterizations of process equivalences traditionally form a central topic in concurrency; for example, most equivalences on the classical linear-time / branching-time spectrum come with such characterizations. Recent work on so-called graded semantics has led to a generic behavioural equivalence game that covers the mentioned games on the linear-time~/ branching-time spectrum and moreover applies in coalgebraic generality, and thus instantiates also to equivalence games on systems with non-relational branching type (probabilistic, weighted, game-based etc.). In the present work, we generalize this approach to cover other types of process comparison beyond equivalence, such as behavioural preorders or pseudometrics. At the most general level, we abstract such notions of behavoiural conformance in terms of topological categories, and later specialize to conformances presented as relational structures to obtain a concrete syntax. We obtain a sound and complete generic game for behavioural conformances in this sense. We present a number of instantiations, obtaining game characterizations of, e.g., trace inclusion, probabilistic trace distance, bisimulation topologies, and simulation distances on metric labelled transition systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_03069 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Conformance Games for Graded Semantics Forster, Jonas Schröder, Lutz Wild, Paul Logic in Computer Science 68Q85 (Primary) F.3.1; F.3.2; F.4.1 Game-theoretic characterizations of process equivalences traditionally form a central topic in concurrency; for example, most equivalences on the classical linear-time / branching-time spectrum come with such characterizations. Recent work on so-called graded semantics has led to a generic behavioural equivalence game that covers the mentioned games on the linear-time~/ branching-time spectrum and moreover applies in coalgebraic generality, and thus instantiates also to equivalence games on systems with non-relational branching type (probabilistic, weighted, game-based etc.). In the present work, we generalize this approach to cover other types of process comparison beyond equivalence, such as behavioural preorders or pseudometrics. At the most general level, we abstract such notions of behavoiural conformance in terms of topological categories, and later specialize to conformances presented as relational structures to obtain a concrete syntax. We obtain a sound and complete generic game for behavioural conformances in this sense. We present a number of instantiations, obtaining game characterizations of, e.g., trace inclusion, probabilistic trace distance, bisimulation topologies, and simulation distances on metric labelled transition systems. |
| title | Conformance Games for Graded Semantics |
| topic | Logic in Computer Science 68Q85 (Primary) F.3.1; F.3.2; F.4.1 |
| url | https://arxiv.org/abs/2411.03069 |