Ymer is a tool for verifying probabilistic properties of continuous-time Markov chains (CTMCs) and generalized semi-Markov processes (GSMPs). Properties are expressed using the Continuous Stochastic Logic (CSL). Ymer also supports verifying PCTL properties of discrete-time Markov chains (DTMCs). Ymer uses a dialect of the PRISM language for model and property specification.
To handle the full generality of GSMPs, Ymer implements statistical techniques for CSL model checking, based on discrete event simulation and sequential acceptance sampling. Ymer includes support for multi-threaded acceptance sampling, which can result in significant speedup as each sample can be generated independently.
Released versions of Ymer can be downloaded here.
The source code for Ymer is hosted on GitHub.
Håkan L. S. Younes, Edmund M. Clarke, and Paolo Zuliani. 2010. Statistical verification of probabilistic properties with unbounded until. In Proceedings of the 13th Brazilian Symposium on Formal Methods, edited by Jim Davies, Leila Silva, and Adenilso Simao, vol. 6527 of Lecture Notes in Computer Science, 144–160, Natal, Brazil. Springer.
Håkan L. S. Younes and Reid G. Simmons. 2006. Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation 204, no. 9: 1368–1409.
Håkan L. S. Younes, Marta Kwiatkowska, Gethin Norman, and David Parker. 2006. Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer 8, no. 3: 216–228.
Håkan L. S. Younes. 2005. Ymer: A statistical model checker. In Proceedings of the 17th International Conference on Computer Aided Verification, edited by Kousha Etessami and Sriram Rajamani, vol. 3576 of Lecture Notes in Computer Science, 429–433, Edinburgh, Scotland. Springer.
Håkan L. S. Younes. 2005. Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Computer Science Department, Carnegie Mellon University, Pittsburgh, Pennsylvania. CMU-CS-05-105.
Håkan L. S. Younes and Reid G. Simmons. 2002. Probabilistic verification of discrete event systems using acceptance sampling. In Proceedings of the 14th International Conference on Computer Aided Verification, edited by Ed Brinksma and Kim Guldstrand Larsen, vol. 2404 of Lecture Notes in Computer Science, 223–235, Copenhagen, Denmark. Springer.