Ymer: A GSMP Model Checker

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)

Publications

Related Work


Håkan L. S. Younes Valid CSS! Valid XHTML 1.0!
Last modified: Sat Jun 24 19:52:11 EDT 2006