7 papers
White dwarfs in minimal dilatonic gravity
Denitsa Staicova
We study static, spherically symmetric white dwarfs in minimal dilatonic gravity (MDG) -- a Brans-Dicke theory with fixed coupling and free Compton length . Solving…
Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams
Daniel Basgöze, Kevin Batz, Sebastian Junges +1
Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive verification approaches aim to establish bounds on these q…
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…
Probabilistic Model Checking Taken by Storm
Matthias Volk, Linus Heck, Sebastian Junges +2
This tutorial paper presents a hands-on perspective on probabilistic model checking with the Storm model checker. Storm is a decade-old model checker that excels in performance and…
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…