2 citations · 3 across the 11 of their papers we have counts for
10 papers · 1 filter
UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)
Roman Andriushchenko, Arnd Hartmanns, Joshua Jeppson +5
This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic s…
Shields to Guarantee Probabilistic Safety in MDPs
Linus Heck, Filip Macák, Roman Andriushchenko +2
Shielding is a prominent model-based technique to ensure safety of autonomous agents. Classical shielding aims to ensure that nothing bad ever happens and comes with strong guarant…
Decentralized Planning Using Probabilistic Hyperproperties
Francesco Pontiggia, Filip Macák, Roman Andriushchenko +2
Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected rewar…
Small Decision Trees for MDPs with Deductive Synthesis
Roman Andriushchenko, Milan Češka, Sebastian Junges +1
Markov decision processes (MDPs) describe sequential decision-making processes; MDP policies return for every state in that process an advised action. Classical algorithms can effi…
Policies Grow on Trees: Model Checking Families of MDPs
Roman Andriushchenko, Milan Češka, Sebastian Junges +1
Markov decision processes (MDPs) provide a fundamental model for sequential decision making under process uncertainty. A classical synthesis task is to compute for a given MDP a wi…
Tools at the Frontiers of Quantitative Verification
Roman Andriushchenko, Alexander Bork, Carlos E. Budde +20
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool suppo…