Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910219151343616 |
|---|---|
| author | Chakraborty, Debraj Majumdar, Anirban Mathew, Prince Mukherjee, Sayan Raskin, Jean-François |
| author_facet | Chakraborty, Debraj Majumdar, Anirban Mathew, Prince Mukherjee, Sayan Raskin, Jean-François |
| contents | Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely, formal synthesis techniques provide correctness-by-construction but often struggle with scalability, as general POMDP synthesis is undecidable. To bridge this gap, we propose a synthesis framework that integrates sampling, automata learning, and model-checking. Inspired by Angluin's $L^*$ algorithm, our approach utilizes sampling as a membership oracle and model-checking as an equivalence oracle. This enables the synthesis of finite-state controllers with formal guarantees, provided the sampling-induced policy is regular. We establish a relative completeness result for this framework. Experimental results from our prototypical implementation demonstrate that this method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. We believe our algorithm serves as a valuable component in a portfolio approach to tackling the inherent difficulty of POMDP synthesis problems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_14440 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning Chakraborty, Debraj Majumdar, Anirban Mathew, Prince Mukherjee, Sayan Raskin, Jean-François Artificial Intelligence Formal Languages and Automata Theory Logic in Computer Science Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely, formal synthesis techniques provide correctness-by-construction but often struggle with scalability, as general POMDP synthesis is undecidable. To bridge this gap, we propose a synthesis framework that integrates sampling, automata learning, and model-checking. Inspired by Angluin's $L^*$ algorithm, our approach utilizes sampling as a membership oracle and model-checking as an equivalence oracle. This enables the synthesis of finite-state controllers with formal guarantees, provided the sampling-induced policy is regular. We establish a relative completeness result for this framework. Experimental results from our prototypical implementation demonstrate that this method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. We believe our algorithm serves as a valuable component in a portfolio approach to tackling the inherent difficulty of POMDP synthesis problems. |
| title | Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning |
| topic | Artificial Intelligence Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2605.14440 |