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-…