Copyright (C) 2003--2005 Carnegie Mellon University Copyright (C) 2011-2019 Google Inc
This file is free documentation; the copyright holders give unlimited permission to copy, distribute and modify it.
Ymer is a tool for verifying probabilistic properties of discrete-time Markov chains (DTMCs), 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 multi-threaded acceptance sampling, i.e. the use of multiple threads to generate observations, which can result in significant speedup as each observation 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.
Installation instructions are available in INSTALL.
Ymer is controlled by a command line interface. Run `./ymer --help' for details on available command line options.
If you think you have found a bug, or want to request a feature, file an issue here:
https://github.com/hlsyounes/ymer/issues
Send any other feedback to hlsyounes@gmail.com.