Probabilistic Model Checking

A core part of my research considers the model-based analysis of (temporal,declaritive) specifications on Markov models such as Continous-Time Markov Chains, Markov Decision Processes, Markov Automata.

Multi-objective, Randomization and Resources

A typical structure in many systems is that the system consumes resources, e.g., battery charge. An important question is to compute the probability that a system runs out of such a resource. We develop effective algorithm that support fast model checking of such systems [1], [2].

Multi-objective model checking asks whether there is a policy that satisfies multiple properties at once. In [3], [4] we consider this problem for Markov automata, a composable variant of continuous-time MDPs. In [5], we looked at a combination of reachability probabilities and randomization constraints. Such constraints enforce that the policy randomizes sufficiently, a property useful for testing and obfuscation.

Hierarchical models

We recently started to support hierarchical MDPs, in particular, by presenting an abstraction-refinement loop that uses similarities between different parts of a hierarchical MDP.

Symbolic model checking

We developed PrIC3 [6], an extension of the hugely successful IC3 methodology to MDPs. While the approach is not yet competitive on the typical benchmarks, the approach shows superior scalability on some benchmarks.

We showed that CEGIS-style approaches to find inductive invariants can be a feasible alternative on (very large) MDPs [7]

Furthermore, probabilistic model checking for finite horizons is related to probabilistic inference in probabilistic programs. In [8], we explored the use of exact inference algorithms for probabilistic model checking and show that the performance is orthogonal to existing approaches.

Tool support

Together with a group of co-developers, we provide state-of-the-art tool support for probabilistic model checking in the tool Storm (missing reference). Storm has a superior performance, as shown on the QCOMP 2019 and QCOMP 2020, and its Python API allows for flexible interfacing.

Besides Storm, I have worked on the development of JANI [9], whose format is the basis for the QCOMP and smaller prototypes that accompany individual papers.

Case studies

Besides the research areas mentioned at the top of the page, we have done some additional case studies, in particular for model checking a wireless token protocol for machine-to-machine communication [10] and model checking behavior learned via Inverse RL [11].

Extensions

Much of my work on

• POMDPs,
• parameter synthesis,
• probabilistic control program sketching, and
• fault trees builds on top of model checking, and often, those applications required extension to the model checking algorithms.

References

1. Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Multi-cost Bounded Reachability in MDP,” in TACAS, 2018.
   
2. Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Multi-cost Bounded Tradeoff Analysis in MDP,” J. Autom. Reason., no. 7, 2020.
   
3. Tim Quatmann, Sebastian Junges, and Joost-Pieter Katoen, “Markov Automata with Multiple Objectives,” in CAV, 2017.
   
4. Tim Quatmann, Sebastian Junges, and Joost-Pieter Katoen, “Markov Automata with Multiple Objectives,” FMSD, 2021.
   
5. Marcell Vazquez-Chanlatte, Sebastian Junges, Daniel J. Fremont, and Sanjit Seshia, “Entropy-Guided Control Improvisation,” in RSS, 2021.
   
6. Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer, “PrIC3: Property Directed Reachability for MDPs,” in CAV, 2020.
   
7. Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja, “Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants,” in TACAS, 2023.
   
8. Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd Millstein, Sanjit A. Seshia, and Guy Van den Broeck, “Model Checking Finite-Horizon Markov Chains with Probabilistic Inference,” in CAV, 2021.
   
9. Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini, “JANI: Quantitative Model and Tool Interaction,” in TACAS, 2017.
   
10. Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, and James Gross, “Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks,” in SRDS, 2016.
    
11. Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, and Mary M. Hayhoe, “Model Checking for Safe Navigation Among Humans,” in QEST, 2018.