CSL Model Checking Algorithms for Infinite-state Structured Markov chains

Anne Remke; Boudewijn R. Haverkort

doi:10.1007/978-3-540-75454-1_24

CSL Model Checking Algorithms for Infinite-state Structured Markov chains

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

6 Citations (Scopus)

90 Downloads (Pure)

Abstract

Jackson queueing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the continuous-time Markov chain (CTMC) that underlies such a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues. We present CSL model checking algorithms for labeled JQNs. To do so, we rely on well-known product-form results for the steady-state probabilities in (stable) JQNs. The transient probabilities are computed using an uniformization-based approach. We develop a new notion of property independence that allows us to define model checking algorithms for labeled JQNs.

Original language	English
Title of host publication	5th International Conference, FORMATS 2007
Editors	J.-F. Raskin, P.S. Thiagarajan
Place of Publication	London
Publisher	Springer
Pages	336-351
Number of pages	16
ISBN (Print)	978-3-540-75453-4
DOIs	https://doi.org/10.1007/978-3-540-75454-1_24
Publication status	Published - 3 Oct 2007
Event	5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007 - Salzburg, Austria Duration: 3 Oct 2007 → 5 Oct 2007 Conference number: 5

Publication series

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

Conference

Conference	5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007
Abbreviated title	FORMATS
Country/Territory	Austria
City	Salzburg
Period	3/10/07 → 5/10/07

Access to Document

10.1007/978-3-540-75454-1_24

ArticleAccepted author version, 235 KB

Cite this

@inproceedings{31fd551858d04012aee9bb4fcf84e586,

title = "CSL Model Checking Algorithms for Infinite-state Structured Markov chains",

abstract = "Jackson queueing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the continuous-time Markov chain (CTMC) that underlies such a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues. We present CSL model checking algorithms for labeled JQNs. To do so, we rely on well-known product-form results for the steady-state probabilities in (stable) JQNs. The transient probabilities are computed using an uniformization-based approach. We develop a new notion of property independence that allows us to define model checking algorithms for labeled JQNs.",

author = "Anne Remke and Haverkort, \{Boudewijn R.\}",

year = "2007",

month = oct,

day = "3",

doi = "10.1007/978-3-540-75454-1\_24",

language = "English",

isbn = "978-3-540-75453-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "336--351",

editor = "J.-F. Raskin and P.S. Thiagarajan",

booktitle = "5th International Conference, FORMATS 2007",

address = "Germany",

note = "5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007, FORMATS ; Conference date: 03-10-2007 Through 05-10-2007",

}

Remke, A & Haverkort, BR 2007, CSL Model Checking Algorithms for Infinite-state Structured Markov chains. in J-F Raskin & PS Thiagarajan (eds), 5th International Conference, FORMATS 2007. Lecture Notes in Computer Science, vol. 4763, Springer, London, pp. 336-351, 5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007, Salzburg, Austria, 3/10/07. https://doi.org/10.1007/978-3-540-75454-1_24

CSL Model Checking Algorithms for Infinite-state Structured Markov chains. / Remke, Anne ; Haverkort, Boudewijn R.
5th International Conference, FORMATS 2007. ed. / J.-F. Raskin; P.S. Thiagarajan. London: Springer, 2007. p. 336-351 (Lecture Notes in Computer Science; Vol. 4763).

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

TY - GEN

T1 - CSL Model Checking Algorithms for Infinite-state Structured Markov chains

AU - Remke, Anne

AU - Haverkort, Boudewijn R.

N1 - Conference code: 5

PY - 2007/10/3

Y1 - 2007/10/3

N2 - Jackson queueing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the continuous-time Markov chain (CTMC) that underlies such a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues. We present CSL model checking algorithms for labeled JQNs. To do so, we rely on well-known product-form results for the steady-state probabilities in (stable) JQNs. The transient probabilities are computed using an uniformization-based approach. We develop a new notion of property independence that allows us to define model checking algorithms for labeled JQNs.

AB - Jackson queueing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the continuous-time Markov chain (CTMC) that underlies such a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues. We present CSL model checking algorithms for labeled JQNs. To do so, we rely on well-known product-form results for the steady-state probabilities in (stable) JQNs. The transient probabilities are computed using an uniformization-based approach. We develop a new notion of property independence that allows us to define model checking algorithms for labeled JQNs.

U2 - 10.1007/978-3-540-75454-1_24

DO - 10.1007/978-3-540-75454-1_24

M3 - Conference contribution

SN - 978-3-540-75453-4

T3 - Lecture Notes in Computer Science

SP - 336

EP - 351

BT - 5th International Conference, FORMATS 2007

A2 - Raskin, J.-F.

A2 - Thiagarajan, P.S.

PB - Springer

CY - London

T2 - 5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007

Y2 - 3 October 2007 through 5 October 2007

ER -

CSL Model Checking Algorithms for Infinite-state Structured Markov chains

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this