Bi-Weekly Talk: Tobias Winkler: Out of Control: Reducing Probabilistic Models by Control-State Elimination

Mittwoch, 18.11.2020, 10.30 Uhr

Ort: Online session 

Vortragender: Tobias Winkler

 

Abstract: 

In this talk, I present some recent work on a new, simple technique to reduce state space sizes in probabilistic model checking when the input model is defined in a programming formalism like the PRISM modeling language.
Intuitively, the idea is to eliminate control-flow structures that are indispensable for the programmer but may blowup the underlying Markov model that needs to be fed into the model checker. Unlike various reduction techniques, our approach is property-directed and can thereby achieve reductions beyond bisimilarity. In many cases, it suffices to compute the reduced program only once to analyze it for many different parameter configurations—a rather common workflow in probabilistic model checking. Despite its conceptual simplificity, experiments demonstrate that control-state reduction yields a state-space reduction of up to one order of magnitude on practically relevant benchmarks.
This is joint work with Joost-Pieter Katoen and our UnRAVeL student assistant Johannes Lehmann.