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 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.


Related Work