Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F25%3A00638085" target="_blank" >RIV/67985807:_____/25:00638085 - isvavai.cz</a>

Výsledek na webu

<a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol342-calco2025/LIPIcs.CALCO.2025.9/LIPIcs.CALCO.2025.9.pdf" target="_blank" >https://drops.dagstuhl.de/storage/00lipics/lipics-vol342-calco2025/LIPIcs.CALCO.2025.9/LIPIcs.CALCO.2025.9.pdf</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.CALCO.2025.9" target="_blank" >10.4230/LIPIcs.CALCO.2025.9</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Popis výsledku v původním jazyce

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 A of truth-degrees. More precisely, we work with coalgebraic modal logic via A-valued predicate liftings where A is an FLew-algebra, and interpret actions (abstracting programs and games) as F-coalgebras where the functor F represents some type of A-weighted system. We also allow combinations of crisp propositions with A-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which 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 A-valued accessibility relations when A is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.

Název v anglickém jazyce

Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Popis výsledku anglicky

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 A of truth-degrees. More precisely, we work with coalgebraic modal logic via A-valued predicate liftings where A is an FLew-algebra, and interpret actions (abstracting programs and games) as F-coalgebras where the functor F represents some type of A-weighted system. We also allow combinations of crisp propositions with A-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which 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 A-valued accessibility relations when A is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/EH23_025%2F0008724" target="_blank" >EH23_025/0008724: Biografie dezinformace s přívlastkem AI: Rizikový fenomén prizmatem moderních věd o člověku</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2025

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

ISBN

978-3-95977-383-6

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

23

Strana od-do

9

Název nakladatele

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Místo vydání

Dagstuhl

Místo konání akce

Glasgow

Datum konání akce

16. 6. 2025

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001585185500009