INFAMY: An Infinite-State Markov Model Checker

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

doi:10.1007/978-3-642-02658-4_49

INFAMY: An Infinite-State Markov Model Checker

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

19 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 language	English
Title of host publication	Computer Aided Verification
Subtitle of host publication	21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings
Publisher	Springer
Pages	641-647
ISBN (Electronic)	978-3-642-02658-4
ISBN (Print)	978-3-642-02657-7
DOIs	https://doi.org/10.1007/978-3-642-02658-4_49
Publication status	Published - 2009
Externally published	Yes
Event	21st International Conference on Computer Aided Verification, CAV 2009 - Grenoble, France Duration: 26 Jun 2009 → 2 Jul 2009 Conference number: 21

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	5643
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Conference on Computer Aided Verification, CAV 2009
Abbreviated title	CAV 2009
Country/Territory	France
City	Grenoble
Period	26/06/09 → 2/07/09

Access to Document

10.1007/978-3-642-02658-4_49

Cite this

@inproceedings{77e2f2c39c0c45699a2484dae416e5c1,

title = "INFAMY: An Infinite-State Markov Model Checker",

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.",

author = "Hahn, {Ernst Moritz} and Holger Hermanns and Bjorn Wachter and Lijun Zhang",

year = "2009",

doi = "10.1007/978-3-642-02658-4_49",

language = "English",

isbn = "978-3-642-02657-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "641--647",

booktitle = "Computer Aided Verification",

address = "Germany",

note = "21st International Conference on Computer Aided Verification, CAV 2009, CAV 2009 ; Conference date: 26-06-2009 Through 02-07-2009",

}

Hahn, EM, Hermanns, H, Wachter, B & Zhang, L 2009, INFAMY: An Infinite-State Markov Model Checker. in Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, Springer, pp. 641-647, 21st International Conference on Computer Aided Verification, CAV 2009, Grenoble, France, 26/06/09. https://doi.org/10.1007/978-3-642-02658-4_49

INFAMY: An Infinite-State Markov Model Checker. / Hahn, Ernst Moritz ; Hermanns, Holger; Wachter, Bjorn et al.
Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Springer, 2009. p. 641-647 (Lecture Notes in Computer Science; Vol. 5643).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - INFAMY: An Infinite-State Markov Model Checker

AU - Hahn, Ernst Moritz

AU - Hermanns, Holger

AU - Wachter, Bjorn

AU - Zhang, Lijun

N1 - Conference code: 21

PY - 2009

Y1 - 2009

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

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

U2 - 10.1007/978-3-642-02658-4_49

DO - 10.1007/978-3-642-02658-4_49

M3 - Conference contribution

SN - 978-3-642-02657-7

T3 - Lecture Notes in Computer Science

SP - 641

EP - 647

BT - Computer Aided Verification

PB - Springer

T2 - 21st International Conference on Computer Aided Verification, CAV 2009

Y2 - 26 June 2009 through 2 July 2009

ER -

INFAMY: An Infinite-State Markov Model Checker

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this