  Binary decision diagrams can compactly represent vast sets of states,
mitigating the state space explosion problem in model checking. Probabilistic
systems, however, require multi-terminal diagrams storing rational numbers.
They are inefficient for models with many distinct probabilities and for
iterative numeric algorithms like value iteration. In this paper, we present a
new "symblicit" approach to checking Markov chains and related probabilistic
models: We first generate a decision diagram that symbolically collects all
reachable states and their predecessors. We then concretise states one-by-one
into an explicit partial state space representation. Whenever all predecessors
of a state have been concretised, we eliminate it from the explicit state space
in a way that preserves all relevant probabilities and rewards. We thus keep
few explicit states in memory at any time. Experiments show that very large
models can be model-checked in this way with very low memory consumption.
