On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
From International Center for Computational Logic
On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Talk by Tim Lyon
- Location: APB 3027
- Start: 3. April 2025 at 11:00 am
- End: 3. April 2025 at 12:00 pm
- Research group: Computational Logic
- Event series: Research Seminar Logic and AI
- iCal
Propositional dynamic logic (PDL) is an important modal logic used to specify and reason about the behavior of programs. 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 short talk, we discuss PDL, fixed-point equations, and identify a class of PDL formulae arranged into two dual hierarchies for which every fixed-point equation x ≡ ϕ(x) has a solution.
