Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908735213928448 |
|---|---|
| author | Hansen, Helle Hvid Poiger, Wolfgang |
| author_facet | Hansen, Helle Hvid Poiger, Wolfgang |
| contents | We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra $\mathbf{A}$ of truth-degrees. More precisely, we work with coalgebraic modal logic via $\mathbf{A}$-valued predicate liftings where $\mathbf{A}$ is a $\mathsf{FL}_{\mathrm{ew}}$-algebra, and interpret actions (abstracting programs and games) as $\mathsf{F}$-coalgebras where the functor $\mathsf{F}$ represents some type of $\mathbf{A}$-weighted system. We also allow combinations of crisp propositions with $\mathbf{A}$-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations that are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for $2$-valued iteration-free PDL with $\mathbf{A}$-valued accessibility relations when $\mathbf{A}$ is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_22851 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility Hansen, Helle Hvid Poiger, Wolfgang Logic in Computer Science Logic We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra $\mathbf{A}$ of truth-degrees. More precisely, we work with coalgebraic modal logic via $\mathbf{A}$-valued predicate liftings where $\mathbf{A}$ is a $\mathsf{FL}_{\mathrm{ew}}$-algebra, and interpret actions (abstracting programs and games) as $\mathsf{F}$-coalgebras where the functor $\mathsf{F}$ represents some type of $\mathbf{A}$-weighted system. We also allow combinations of crisp propositions with $\mathbf{A}$-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations that are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for $2$-valued iteration-free PDL with $\mathbf{A}$-valued accessibility relations when $\mathbf{A}$ is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic. |
| title | Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2512.22851 |