Ymer is a tool for verifying probabilistic transient properties of continuous-time Markov chains (CTMCs) and generalized semi-Markov processes (GSMPs). Properties are expressed using the Continuous Stochastic Logic (CSL).
To handle the full generality of GSMPs, Ymer implements statistical techniques, based on discrete event simulation and sequential acceptance sampling, for CSL model checking. Ymer includes support for distributed acceptance sampling, i.e. the use of multiple machines to generate samples, which can result in significant speedup as each sample can be generated independently.
Version 4 of Ymer added support for unbounded until. Eariler versions of Ymer included the hybrid engine from the PRISM tool for CTMC model checking, allowing numerical and statistical techniques to be used in combination to solve nested CSL queries.
The source code for Ymer is hosted on Google Code.
Håkan L. S. Younes, Edmund M. Clake, 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, Marta Kwiatkowska, Gethin Norman, and David Parker. 2005. 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.