Our paper “Symbolic Counterexample Generation for Discrete-time Markov Chains” was accepted at FACS’12.