On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
Abstract
Propositional dynamic logic (PDL) is an important modal logic used to specify and reason about the behavior of software. A challenging problem in the context of PDL is solving fixed-point equations, i.e., formulae of the form x≡φ(x) such that x is a propositional variable and φ(x) is a formula containing x. A solution to such an equation is a formula ψ that omits x and satisfies ψ≡φ(ψ), where φ(ψ) is obtained by replacing all occurrences of x with ψ in φ(x). In this paper, we identify a novel class of PDL formulae arranged in two dual hierarchies for which every fixed-point equation x≡φ(x) has a solution. Moreover, we not only prove the existence of solutions for all such equations, but also provide an explicit solution ψ for each fixed-point equation.
Details
| Originalsprache | Englisch |
|---|---|
| Titel | Fundamentals of Software Engineering |
| Redakteure/-innen | Hossein Hojjat, Georgiana Caltais |
| Herausgeber (Verlag) | Springer, Cham |
| Seiten | 113-119 |
| Seitenumfang | 7 |
| ISBN (elektronisch) | 978-3-031-87054-5 |
| ISBN (Print) | 978-3-031-87053-8 |
| Publikationsstatus | Veröffentlicht - 2025 |
| Peer-Review-Status | Ja |
Publikationsreihe
| Reihe | Lecture Notes in Computer Science |
|---|---|
| Band | 15593 |
| ISSN | 0302-9743 |
Externe IDs
| Scopus | 105001323082 |
|---|---|
| ORCID | /0000-0003-3214-0828/work/199216619 |