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

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

Abstract

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.

Details

OriginalspracheEnglisch
TitelFundamentals of Software Engineering
Redakteure/-innenHossein Hojjat, Georgiana Caltais
Herausgeber (Verlag)Springer, Cham
Seiten113-119
Seitenumfang7
ISBN (elektronisch)978-3-031-87054-5
ISBN (Print)978-3-031-87053-8
PublikationsstatusVeröffentlicht - 2025
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science
Band15593
ISSN0302-9743

Externe IDs

Scopus 105001323082
ORCID /0000-0003-3214-0828/work/199216619

Schlagworte