4 papers
Symblicit Exploration and Elimination for Probabilistic Model Checking
Ernst Moritz Hahn, Arnd Hartmanns
Binary decision diagrams can compactly represent vast sets of states, mitigating the state space explosion problem in model checking. Probabilistic systems, however, require multi-…
Optimistic Value Iteration
Arnd Hartmanns, Benjamin Lucien Kaminski
Markov decision processes are widely used for planning and verification in settings that combine controllable or adversarial choices with probabilistic behaviour. The standard anal…
A Hierarchy of Scheduler Classes for Stochastic Automata
Pedro R. D'Argenio, Marcus Gerhold, Arnd Hartmanns +1
Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are def…
Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking
Ernst Moritz Hahn, Arnd Hartmanns
In the design of probabilistic timed systems, bounded requirements concerning behaviour that occurs within a given time, energy, or more generally cost budget are of central import…