Tools Overview Contact Us Publications Case Studies Home

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.


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


INFAMY was developed by Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang and Björn Wachter.


For questions, comments and support requests regarding INFAMY, please contact "emh [at] cs [dot] uni [minus] saarland [dot] de".

Valid XHTML 1.1 Valid CSS! Powered by PHP