On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic

Tim LyonTim Lyon

DOI Link

Tim Lyon
On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
In Hossein Hojjat, Georgiana Caltais, eds., Proceedings of the Eleventh International Conference on Fundamentals of Software Engineering (FSEN), volume 15593 of LNCS, 113-119, 2025. Springer

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

The final publication is available at Springer via http://dx.doi.org/https://doi.org/10.1007/978-3-031-87054-5_8.

@inproceedings{L2025,
  author    = {Tim Lyon},
  title     = {On Explicit Solutions to Fixed-Point Equations in Propositional
               Dynamic Logic},
  editor    = {Hossein Hojjat and Georgiana Caltais},
  booktitle = {Proceedings of the Eleventh International Conference on
               Fundamentals of Software Engineering (FSEN)},
  series    = {LNCS},
  volume    = {15593},
  publisher = {Springer},
  year      = {2025},
  pages     = {113-119},
  doi       = {https://doi.org/10.1007/978-3-031-87054-5_8}
}