On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Aus International Center for Computational Logic
On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Vortrag von Tim Lyon
- Veranstaltungsort: APB 3027
- Beginn: 3. April 2025 um 11:00
- Ende: 3. April 2025 um 12:00
- Forschungsgruppe: 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.
