Probabilistic model checker
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
cudd
examples
glog
gsl
gtest
m4
scripts
src
.gitignore
AUTHORS
COPYING
ChangeLog
INSTALL
Makefile.am
Makefile.in
NEWS
README
aclocal.m4
compile
config.guess
config.h.in
config.sub
configure
configure.ac
depcomp
formulas.h
hybrid.cc
hybrid.h
install-sh
ltmain.sh
missing
mkinstalldirs
sampling.cc
symbolic.cc
test-driver
ylwrap
ymer.cc

README

Copyright (C) 2003--2005 Carnegie Mellon University
Copyright (C) 2011-2015 Google Inc

   This file is free documentation; the copyright holders give
unlimited permission to copy, distribute and modify it.

Ymer 4.2.1
==========

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

Installation instructions are available in INSTALL.


Running Ymer
============

Ymer is controlled by a command line interface.  Run `./ymer --help' for details
on available command line options.