Our paper “High-level counterexamples for Probabilistic Automata” was accepted at QEST 2013. We also published a technical report including all proofs, which is available here.