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

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

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

Original languageEnglish
Title of host publicationFundamentals of Software Engineering
EditorsHossein Hojjat, Georgiana Caltais
PublisherSpringer, Cham
Pages113-119
Number of pages7
ISBN (electronic)978-3-031-87054-5
ISBN (print)978-3-031-87053-8
Publication statusPublished - 2025
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science
Volume15593
ISSN0302-9743

External IDs

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

Keywords