www.prismmodelchecker.org
[LPST25] Yong Li, Soumyajit Paul, Sven Schewe and Qiyi Tang. Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata. In Proc. 37th International Conference on Computer Aided Verification (CAV'25). 2025. [Proposes novel automata-based techniques for Markov chains, implemented as an extension of PRISM]
Links: [Google] [Google Scholar]

Publications