INFAMY
Subproject |
S3 |
Categories |
Model checker for hard & soft real-time systems, Model checker / solver for probabilistic systems |
Overview |
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. |
E.M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. INFAMY: An infinite-state markov model checker. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification (CAV), volume 5643 of Lecture Notes in Computer Science (LNCS), pages 641-647, 2009. E.M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. Time-bounded model checking of infinite-state continuous-time markov chains. Fundamenta Informaticae, 95:129-155, 2009. L. Zhang, H. Hermanns, E.M. Hahn, and B. Wachter. Time-bounded model checking of infinite-state continuous-time markov chains. In Jonathan Billington, Zhenhua Duan, and Maciej Koutny, editors, Application of Concurrency to System Design (ACSD), pages 98-107, 2008. |
|
Benchmarks |
|
Download |
|
Manual |
|
Status |
Stable |