On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Tim S. Lyon
TL;DR
The paper addresses the challenge of solving fixed-point equations in $\mathsf{PDL}$, a problem with implications for interpolation and verification. It identifies a non-trivial solvable class formed by two dual hierarchies, $\Uppi^{x}$ and $\Upsigma^{x}$, and proves that every equation $x \equiv \varphi(x)$ within this union has a solution. Moreover, it provides explicit witnesses $\lambda_{1}$–$\lambda_{4}$ for the four parity-based subcases and illustrates the method with a concrete example, demonstrating the practicality of obtaining explicit solutions. This work lays groundwork for extending solvable classes and applying fixed-point solutions to interpolation and related verification tasks in dynamic logic.
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 \equiv φ(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 $ψ\equiv φ(ψ)$, 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 \equiv φ(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.