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.

翻译：命题动态逻辑（PDL）是一种重要的模态逻辑，用于规范和推理软件行为。在PDL中，求解不动点方程是一个具有挑战性的问题，即形如$x \equiv \phi(x)$的公式，其中$x$是命题变量，$\phi(x)$是包含$x$的公式。该方程的解是一个不包含$x$的公式$\psi$，且满足$\psi \equiv \phi(\psi)$，其中$\phi(\psi)$是通过将$\phi(x)$中所有$x$的出现替换为$\psi$而得到的。本文识别了一类新颖的PDL公式，它们排列在两个对偶层次结构中，使得每个不动点方程$x \equiv \phi(x)$都存在解。此外，我们不仅证明了所有此类方程解的存在性，还为每个不动点方程提供了显式解$\psi$。