Analysis for POMDPs

Partially observable MDPs are a rich modelling formalism to model real world systems. We have considered both verification and controller synthesis approaches to their analysis.

Finite State Controller Synthesis

Finite State Controllers for POMDPs can be computed via parameter synthesis methods for parametric Markov chains [1]. These approaches do generalize to uncertain POMDPs [2], where we showed that we can synthesise robust finite state controllers for POMDPs. We use similar ideas in our work on sketching. To further accelerate finding suitable controllers, it can be helpful to embed a belief-based approach with controller synthesis approaches [3].

We also succesfully applied game-based abstractions to synthesise controllers in a POMDP setting, see [4], [5].

Quantitative Verification

To support reasoning about the absence of a controller satisfying a specification, we need to investigate the underlying infinitely large belief MDP. To make such an analysis feasible, we combine state-of-the-art probabilistic model checking together with an abstraction-refinement loop [6]. The approach is part of Storm.

Qualitative Verification

Finally, we support policy synthesis for a fixed almost-sure reachability property in [7] via an iterative SAT-computation. We applied the obtained policies in the context of runtime enforcement.

Online Planning

Due to the computational complexity, a succesful approach is based on variations of Monte-Carlo Tree Search (MCTS). In [8], we consider such algorithms in the context of many-agent POMDPs, where the challenge is that the number of actions is typically (very) large.

Decentralized Models

We investigated an extension to decentralized controllers for finite horizons in [9].

Benchmarks

Among others, we have a series of gridworld benchmarks that can be used with storm and offer visualisations. See gridworlds for more information.

References

1. Sebastian Junges et al., “Finite-State Controllers of POMDPs using Parameter Synthesis,” in UAI, 2018.
   
2. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen, and Ufuk Topcu, “Robust Finite-State Controllers for Uncertain POMDPs,” in AAAI, 2021.
   
3. Roman Andriushchenko, Alexander Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, and Filip Macak, “Search and Explore: Symbiotic Policy Synthesis in POMDPs,” in CAV, 2023.
   
4. Leonore Winterer et al., “Motion planning under partial observability using game-based abstraction,” in CDC, 2017.
   
5. Leonore Winterer et al., “Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions,” IEEE Trans. Autom. Control., no. 3, 2021.
   
6. Alexander Bork, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Verification of Indefinite-Horizon POMDPs,” in ATVA, 2020.
   
7. Sebastian Junges, Nils Jansen, and Sanjit A. Seshia, “Enforcing Almost-Sure Reachability in POMDPs,” in CAV, 2021.
   
8. Maris Galesloot, Thiago D. Simao, Sebastian Junges, and Nils Jansen, “Factored Online Planning in Many-Agent POMDPs,” in AAAI, 2024.
   
9. Wietze Koops, Sebastian Junges, Nils Jansen, and Thiago Simao, “Recursive Small-Step Multi-Agent A* for Dec-POMDPs,” in IJCAI, 2023.