Towards Finite Satisfiability Problem for Propositional Dynamic Logic with Loops

Towards Finite Satisfiability Problem for Propositional Dynamic Logic with Loops

Vortrag von Bartosz Jan Bednarczyk

• Veranstaltungsort: APB 3027
• Beginn: 15. Oktober 2026 um 11:00
• Ende: 15. Oktober 2026 um 12:00
• Forschungsgruppe: Computational Logic
• Event series: Research Seminar Logic and AI
• iCal

Propositional Dynamic Logic (PDL) is a well-established modal logic of programs. Among its many extensions, the loop operator stands out for capturing the cyclic behaviour of programs: a world satisfies loop(pi) precisely when it can return to itself along a path matching the regular expression pi. While the satisfiability problem for the resulting logic LoopPDL was settled already in the 1980s, the decidability of its finite satisfiability problem has remained open ever since. The core difficulty is inherent to the finite setting: requiring and forbidding cycles at once is easily reconciled over arbitrary models, but over finite ones it defeats the existing finite-model-theoretic techniques.

During the talk, I will provide a high-level overview of my ongoing work with my PhD student, Mikołaj Swoboda, a substantial part of which is currently under submission. In this work, we solve the problem for a large fragment of LoopPDL and are currently extending our approach towards a solution for the full problem.