Initial Algebra Correspondence under Reachability Conditions
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915479865524224 |
|---|---|
| author | Kori, Mayuko Watanabe, Kazuki Rot, Jurriaan |
| author_facet | Kori, Mayuko Watanabe, Kazuki Rot, Jurriaan |
| contents | Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Markov chains (MCs) coincide whenever the MC at hand is almost surely reachable. In this paper, we present a unifying framework for such reachability conditions that ensures the correspondence of two different semantics. Our categorical framework naturally induces an abstract reachability condition via a suitable adjunction, which allows us to prove coincidences of fixed points, and more generally of initial algebras. We demonstrate the generality of our approach by instantiating several examples, including the almost surely reachability condition for MCs, and the unambiguity condition of automata. We further study a canonical construction of our instance for Markov decision processes by pointwise Kan extensions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_09132 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Initial Algebra Correspondence under Reachability Conditions Kori, Mayuko Watanabe, Kazuki Rot, Jurriaan Logic in Computer Science Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Markov chains (MCs) coincide whenever the MC at hand is almost surely reachable. In this paper, we present a unifying framework for such reachability conditions that ensures the correspondence of two different semantics. Our categorical framework naturally induces an abstract reachability condition via a suitable adjunction, which allows us to prove coincidences of fixed points, and more generally of initial algebras. We demonstrate the generality of our approach by instantiating several examples, including the almost surely reachability condition for MCs, and the unambiguity condition of automata. We further study a canonical construction of our instance for Markov decision processes by pointwise Kan extensions. |
| title | Initial Algebra Correspondence under Reachability Conditions |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.09132 |