Codensity games for bisimilarity
Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways, such as bisimulation metric between probabilistic systems. An impor...
| Main Authors: | , , , , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Springer
2022
|
| _version_ | 1797110285125812224 |
|---|---|
| author | Komorida, Y Katsumata, S-Y Hu, N Klin, B Humeau, S Eberhart, C Hasuo, I |
| author_facet | Komorida, Y Katsumata, S-Y Hu, N Klin, B Humeau, S Eberhart, C Hasuo, I |
| author_sort | Komorida, Y |
| collection | OXFORD |
| description | Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways, such as bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive what we call codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric and bisimulation seminorm) as well as new ones (including what we call bisimulation topology). |
| first_indexed | 2024-03-07T07:52:48Z |
| format | Journal article |
| id | oxford-uuid:4b078474-d4d2-4af2-a878-fd8804a474b1 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:52:48Z |
| publishDate | 2022 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:4b078474-d4d2-4af2-a878-fd8804a474b12023-08-03T09:10:30ZCodensity games for bisimilarityJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:4b078474-d4d2-4af2-a878-fd8804a474b1EnglishSymplectic ElementsSpringer2022Komorida, YKatsumata, S-YHu, NKlin, BHumeau, SEberhart, CHasuo, IBisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways, such as bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive what we call codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric and bisimulation seminorm) as well as new ones (including what we call bisimulation topology). |
| spellingShingle | Komorida, Y Katsumata, S-Y Hu, N Klin, B Humeau, S Eberhart, C Hasuo, I Codensity games for bisimilarity |
| title | Codensity games for bisimilarity |
| title_full | Codensity games for bisimilarity |
| title_fullStr | Codensity games for bisimilarity |
| title_full_unstemmed | Codensity games for bisimilarity |
| title_short | Codensity games for bisimilarity |
| title_sort | codensity games for bisimilarity |
| work_keys_str_mv | AT komoriday codensitygamesforbisimilarity AT katsumatasy codensitygamesforbisimilarity AT hun codensitygamesforbisimilarity AT klinb codensitygamesforbisimilarity AT humeaus codensitygamesforbisimilarity AT eberhartc codensitygamesforbisimilarity AT hasuoi codensitygamesforbisimilarity |