On Explicit Solutions to Fixed-Point Equations in Propositional 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 \varphi (x)$ such that $x$ is a propositional variable and $\varphi (x)$ is a formula containing $x$. A solution to such an equation is a formula $\psi$ that omits $x$ and satisfies $\psi \equiv \varphi (\psi )$, where $\varphi (\psi )$ is obtained by replacing all occurrences of $x$ with $\psi$ in $\varphi (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 \varphi (x)$ has a solution. Moreover, we not only prove the existence of solutions for all such equations, but also provide an explicit solution $\psi$ for each fixed-point equation.

Accepted to Fundamentals of Software Engineering (FSEN) 2025