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

TL;DR

This paper introduces a new class of propositional dynamic logic formulas arranged in dual hierarchies, for which explicit solutions to fixed-point equations are guaranteed and constructed, advancing the understanding of fixed-point solvability in PDL.

Contribution

It identifies a novel class of PDL formulas with guaranteed explicit solutions to fixed-point equations, expanding the theoretical framework of fixed-point solvability.

Findings

Every fixed-point equation in the new class has a solution.

Explicit solutions can be constructed for these equations.

The class is organized in two dual hierarchies.

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 \phi(x)$ such that $x$ is a propositional variable and $\phi(x)$ is a formula containing $x$. A solution to such an equation is a formula $\psi$ that omits $x$ and satisfies $\psi \equiv \phi(\psi)$, where $\phi(\psi)$ is obtained by replacing all occurrences of $x$ with $\psi$ in $\phi(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 \phi(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.