Towards Finite Satisfiability Problem for Propositional Dynamic Logic with Loops

Talk by Bartosz Jan Bednarczyk

Location: APB 3027
Start: 15. October 2026 at 11:00 am
End: 15. October 2026 at 12:00 pm
Research group: 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.