Mixing Formal Methods and Learning Techniques for Strategy Synthesis in Partially Observable Markov Decision Processes

• Applicant: Professor Dr. Joost-Pieter Katoen
• Subject Area: Theoretical Computer Science
• Term: since 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 555465011

In this project, we will address the problem of strategy synthesis for partially observable Markov decision processes (POMDPs). Although this problem is generally undecidable, the literature includes partial solutions using semi-algorithms. These approaches either originate from formal methods, relying on partial unfolding of the typically infinite belief space of the POMDP, or from learning techniques, utilizing sampling methods. Formal methods offer strong guarantees but do not scale well to large systems, whereas learning techniques can handle larger systems but lack robust correctness guarantees. In this project, we aim to merge both approaches into a comprehensive framework that can be applied to large systems while maintaining the strong guarantees of formal methods. Our new algorithms will integrate techniques from model-checking and learning, including automata learning techniques, probabilistic model checking, counterexample analysis, probabilistic program refinement techniques, and Monte Carlo tree search with symbolic advice. Additionally, we will explore special cases where decidability can be restored, specifically by demonstrating how multi-environment MDPs and parametric MDPs can be viewed as decidable subclasses of POMDPs.

• DFG Programme: Research Grants
• International Connection: Belgium
• Cooperation Partner: Professor Dr. Jean-Francois Raskin