2024/12/05 by Tim S. Lyon, Lyon, Tim S.
Computer Science · #Logic, Reasoning, and Knowledge #Computability, Logic, AI Algorithms
paper · pdf · doi:10.48550/arxiv.2412.04012
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 ≡ ϕ(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 ψ≡ ϕ(ψ), 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 ≡ ϕ(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.