INFAMY: An Infinite-State Markov Model Checker

Ernst Moritz Hahn, Holger Hermanns, Bjorn Wachter, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

18 Citations (Scopus)

Abstract

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism, where performance and dependability properties are analyzable by model checking. We present INFAMY, a model checker for arbitrarily structured infinite-state CTMCs. It checks probabilistic timing properties expressible in continuous stochastic logic (CSL). Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and impossible if the model is infinite. INFAMY only explores the model up to a finite depth, with the depth bound being computed on-the-fly. The computation of depth bounds is configurable to adapt to the characteristics of different classes of models.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings
PublisherSpringer
Pages641-647
ISBN (Electronic)978-3-642-02658-4
ISBN (Print)978-3-642-02657-7
DOIs
Publication statusPublished - 2009
Externally publishedYes
Event21st International Conference on Computer Aided Verification, CAV 2009 - Grenoble, France
Duration: 26 Jun 20092 Jul 2009
Conference number: 21

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume5643
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Conference on Computer Aided Verification, CAV 2009
Abbreviated titleCAV 2009
CountryFrance
CityGrenoble
Period26/06/092/07/09

Fingerprint

Dive into the research topics of 'INFAMY: An Infinite-State Markov Model Checker'. Together they form a unique fingerprint.

Cite this