www.prismmodelchecker.org
[BKK16] Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller and James Worrell. Markov Chains and Unambiguous Büchi Automata. In Proc. 28th International Conference on Computer Aided Verification (CAV'16). 2016. [Presents techniques for model checking Markov chains against unambiguous automata, implemented as an extension of PRISM.]
Links: [Google] [Google Scholar]

Publications