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 signicant speedup as each sample can be generated independently.
Ymer can also use numerical techniques based on uniformization by approximating a GSMP with a CTMC using phase-type distributions. Ymer includes the hybrid engine from the PRISM tool for CTMC model checking. Numerical and statistical techniques can be used in combination to solve nested CSL queries.
Source code: GZIP (version 3.0; February 1, 2005)
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.
| Håkan L. S. Younes |
|
|
| Last modified: Sat Jun 24 19:52:11 EDT 2006 |