Ymer: A GSMP Model Checker

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

Released versions of Ymer can be downloaded here.

The source code for Ymer is hosted on GitHub.


Related Work