4 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…
Tractable Hyperproperties for MDPs
Lina Gerlach, Tobias Winkler, Erika Ábrahám +2
Probabilistic hyperproperties describe probabilistic relations between multiple sets of executions in a stochastic system. Prominent examples include information-theoretic characte…
Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
Linus Heck, Filip Macák, Milan Češka +1
The ability to compute reward-optimal policies for given and known finite Markov decision processes (MDPs) underpins a variety of applications across planning, controller synthesis…
Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
Lina Gerlach, Tobias Winkler, Erika Ábrahám +2
Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability proper…