Propositional dynamic logic ( \(\textsf{PDL}\) ) is an important modal logic used to specify and reason about the behavior of software. A challenging problem in the context of \(\textsf{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 \(\textsf{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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

  • Tim S. Lyon

摘要

Propositional dynamic logic ( \(\textsf{PDL}\) ) is an important modal logic used to specify and reason about the behavior of software. A challenging problem in the context of \(\textsf{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 \(\textsf{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.