INFAMY Tool Homepage
INFAMY is a tool with the purpose of model checking
CSL formulae on infinite state Markov chains in continuous time,
specified in a variant of
the PRISM
language.
INFAMY is capable of handling the time-bounded
subclass of the logic CSL. This is done by exploring the model up
to a certain depth repeatedly, while descending into the nested
CSL formula. We provide different means for finding a stopping
criterion for the state-space exploration. (Currently these are:
Uniform, Layered, FSP, FSP exp. For a comparism, see the papers
given given in the publication
homepage or the case studies.)
This is because there is a tradeoff of when to stop the
state-space exploration and the memory needed to store the finite
truncation of the state space. Apart from
this, INFAMY can also handle certain reward properties.
INFAMY has two sisters, PASS and PARAM, that accept virtually the same language, but have different strengths.
Download and Installation
The latest version of INFAMY can be obtained here:
The version number represents the latest revision in the repository at the time the package was created.
Installation
There in no installation routine; once you have
downloaded the binaries package, you can run the tool in place.
If you wish, you can copy the executables to your bin
directory (~/bin as normal user
or /usr/bin as root to make INFAMY
available system-wide).
Authors
INFAMY was developed by Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang and Björn Wachter.
Contact/Support
For questions, comments and support requests regarding INFAMY, please contact
"emh [at] cs [dot] uni [minus] saarland [dot] de".
