Out of Control: Reducing Probabilistic Models by Control-State Elimination

Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen

State-of-the-art probabilistic model checkers perform verification on explicit-state Markov models defined in a high-level programming formalism like the PRISM modeling language. T…