On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
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
| Original language | English |
|---|---|
| Title of host publication | Fundamentals of Software Engineering |
| Editors | Hossein Hojjat, Georgiana Caltais |
| Publisher | Springer, Cham |
| Pages | 113-119 |
| Number of pages | 7 |
| ISBN (electronic) | 978-3-031-87054-5 |
| ISBN (print) | 978-3-031-87053-8 |
| Publication status | Published - 2025 |
| Peer-reviewed | Yes |
Publication series
| Series | Lecture Notes in Computer Science |
|---|---|
| Volume | 15593 |
| ISSN | 0302-9743 |
External IDs
| Scopus | 105001323082 |
|---|---|
| ORCID | /0000-0003-3214-0828/work/199216619 |