Model checking Infinite-State Markov Chains

Anne K.I. Remke; Boudewijn R.H.M. Haverkort; Lucia Cloth

doi:10.1007/978-3-540-31980-1_16

Model checking Infinite-State Markov Chains

Anne K.I. Remke, Boudewijn R.H.M. Haverkort, Lucia Cloth

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

25 Citations (Scopus)

27 Downloads (Pure)

Abstract

In this paper algorithms for model checking CSL (continuous stochastic logic) against infinite-state continuous-time Markov chains of so-called quasi birth-death type are developed. In doing so we extend the applicability of CSL model checking beyond the recently proposed case for finite-state continuous-time Markov chains, to an important class of infinite-state Markov chains. We present syntax and semantics for CSL and develop efficient model checking algorithms for the steady-state operator and the time-bounded next and until operator. For the former, we rely on the so-called matrix-geometric solution of the steady-state probabilities of the infinite-state Markov chain. For the time-bounded until operator we develop a new algorithm for the transient analysis of infinite-state Markov chains, thereby exploiting the quasi birth-death structure. A case study shows the feasibility of our approach. The work presented in this paper has been performed in the context of the MC=MC project (612.000.311), financed by the Netherlands Organization for Scientific Research (NWO) and is based on the diploma thesis [18], supported by the German Academic Exchange Service (DAAD).

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005)
Editors	Nicolas Halbwachs, Lenore D. Zuck
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	237-252
Number of pages	16
ISBN (Print)	9783540253334
DOIs	https://doi.org/10.1007/978-3-540-31980-1_16
Publication status	Published - 2005
Event	11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005 - Edinburgh, United Kingdom Duration: 4 Apr 2005 → 8 Apr 2005 Conference number: 11

Publication series

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

Conference

Conference	11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005
Abbreviated title	TACAS
Country/Territory	United Kingdom
City	Edinburgh
Period	4/04/05 → 8/04/05

Access to Document

10.1007/978-3-540-31980-1_16

ArticleAccepted author version, 203 KB

Cite this

Remke, A. K. I., Haverkort, B. R. H. M., & Cloth, L. (2005). Model checking Infinite-State Markov Chains. In N. Halbwachs, & L. D. Zuck (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005) (pp. 237-252). (Lecture Notes in Computer Science; Vol. 3440). Springer. https://doi.org/10.1007/978-3-540-31980-1_16

Remke, Anne K.I. ; Haverkort, Boudewijn R.H.M. ; Cloth, Lucia. / Model checking Infinite-State Markov Chains. Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005). editor / Nicolas Halbwachs ; Lenore D. Zuck. Berlin, Heidelberg : Springer, 2005. pp. 237-252 (Lecture Notes in Computer Science).

@inproceedings{7122c8180d2d40998b5f4fb25e87951a,

title = "Model checking Infinite-State Markov Chains",

abstract = "In this paper algorithms for model checking CSL (continuous stochastic logic) against infinite-state continuous-time Markov chains of so-called quasi birth-death type are developed. In doing so we extend the applicability of CSL model checking beyond the recently proposed case for finite-state continuous-time Markov chains, to an important class of infinite-state Markov chains. We present syntax and semantics for CSL and develop efficient model checking algorithms for the steady-state operator and the time-bounded next and until operator. For the former, we rely on the so-called matrix-geometric solution of the steady-state probabilities of the infinite-state Markov chain. For the time-bounded until operator we develop a new algorithm for the transient analysis of infinite-state Markov chains, thereby exploiting the quasi birth-death structure. A case study shows the feasibility of our approach. The work presented in this paper has been performed in the context of the MC=MC project (612.000.311), financed by the Netherlands Organization for Scientific Research (NWO) and is based on the diploma thesis [18], supported by the German Academic Exchange Service (DAAD).",

author = "Remke, {Anne K.I.} and Haverkort, {Boudewijn R.H.M.} and Lucia Cloth",

year = "2005",

doi = "10.1007/978-3-540-31980-1_16",

language = "English",

isbn = "9783540253334",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "237--252",

editor = "Nicolas Halbwachs and Zuck, {Lenore D.}",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005)",

address = "Germany",

note = "11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, TACAS ; Conference date: 04-04-2005 Through 08-04-2005",

}

Remke, AKI , Haverkort, BRHM & Cloth, L 2005, Model checking Infinite-State Markov Chains. in N Halbwachs & LD Zuck (eds), Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005). Lecture Notes in Computer Science, vol. 3440, Springer, Berlin, Heidelberg, pp. 237-252, 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, Edinburgh, United Kingdom, 4/04/05. https://doi.org/10.1007/978-3-540-31980-1_16

Model checking Infinite-State Markov Chains. / Remke, Anne K.I.; Haverkort, Boudewijn R.H.M.; Cloth, Lucia.
Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005). ed. / Nicolas Halbwachs; Lenore D. Zuck. Berlin, Heidelberg: Springer, 2005. p. 237-252 (Lecture Notes in Computer Science; Vol. 3440).

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

TY - GEN

T1 - Model checking Infinite-State Markov Chains

AU - Remke, Anne K.I.

AU - Haverkort, Boudewijn R.H.M.

AU - Cloth, Lucia

N1 - Conference code: 11

PY - 2005

Y1 - 2005

N2 - In this paper algorithms for model checking CSL (continuous stochastic logic) against infinite-state continuous-time Markov chains of so-called quasi birth-death type are developed. In doing so we extend the applicability of CSL model checking beyond the recently proposed case for finite-state continuous-time Markov chains, to an important class of infinite-state Markov chains. We present syntax and semantics for CSL and develop efficient model checking algorithms for the steady-state operator and the time-bounded next and until operator. For the former, we rely on the so-called matrix-geometric solution of the steady-state probabilities of the infinite-state Markov chain. For the time-bounded until operator we develop a new algorithm for the transient analysis of infinite-state Markov chains, thereby exploiting the quasi birth-death structure. A case study shows the feasibility of our approach. The work presented in this paper has been performed in the context of the MC=MC project (612.000.311), financed by the Netherlands Organization for Scientific Research (NWO) and is based on the diploma thesis [18], supported by the German Academic Exchange Service (DAAD).

AB - In this paper algorithms for model checking CSL (continuous stochastic logic) against infinite-state continuous-time Markov chains of so-called quasi birth-death type are developed. In doing so we extend the applicability of CSL model checking beyond the recently proposed case for finite-state continuous-time Markov chains, to an important class of infinite-state Markov chains. We present syntax and semantics for CSL and develop efficient model checking algorithms for the steady-state operator and the time-bounded next and until operator. For the former, we rely on the so-called matrix-geometric solution of the steady-state probabilities of the infinite-state Markov chain. For the time-bounded until operator we develop a new algorithm for the transient analysis of infinite-state Markov chains, thereby exploiting the quasi birth-death structure. A case study shows the feasibility of our approach. The work presented in this paper has been performed in the context of the MC=MC project (612.000.311), financed by the Netherlands Organization for Scientific Research (NWO) and is based on the diploma thesis [18], supported by the German Academic Exchange Service (DAAD).

U2 - 10.1007/978-3-540-31980-1_16

DO - 10.1007/978-3-540-31980-1_16

M3 - Conference contribution

SN - 9783540253334

T3 - Lecture Notes in Computer Science

SP - 237

EP - 252

BT - Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005)

A2 - Halbwachs, Nicolas

A2 - Zuck, Lenore D.

PB - Springer

CY - Berlin, Heidelberg

T2 - 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005

Y2 - 4 April 2005 through 8 April 2005

ER -

Remke AKI , Haverkort BRHM, Cloth L. Model checking Infinite-State Markov Chains. In Halbwachs N, Zuck LD, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005). Berlin, Heidelberg: Springer. 2005. p. 237-252. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-31980-1_16

Model checking Infinite-State Markov Chains

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this