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

Tim LyonTim Lyon

Tim Lyon
On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Proceedings of the Eleventh International Conference on Fundamentals of Software Engineering (FSEN), LNCS, to appear. 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.

@inproceedings{L2025,
  author    = {Tim Lyon},
  title     = {On Explicit Solutions to Fixed-Point Equations in Propositional
               Dynamic Logic},
  booktitle = {Proceedings of the Eleventh International Conference on
               Fundamentals of Software Engineering (FSEN)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2025}
}