A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks

Anne Remke; Boudewijn R. Haverkort

doi:10.1007/978-3-540-85778-5_14

A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks

Anne Remke, Boudewijn R. Haverkort

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

138 Downloads (Pure)

Abstract

We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for these transient probabilities no computational procedures are readily available. The contribution of this paper is the proposal of a new uniformization-based approach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.

Original language	English
Title of host publication	The 6th International Conference on Formal Modelling and Analysis of Timed Systems
Editors	Franck Cassez, Claude Jard
Place of Publication	Berlin
Publisher	Springer
Pages	188-202
Number of pages	15
ISBN (Electronic)	978-3-540-85778-5
ISBN (Print)	978-3-540-85777-8
DOIs	https://doi.org/10.1007/978-3-540-85778-5_14
Publication status	Published - 15 Sep 2008
Event	6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008 - Palais du grand Large, St. Malo, France Duration: 15 Sep 2008 → 17 Sep 2008 Conference number: 6 http://formats08.inria.fr/index.html

Publication series

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

Conference

Conference	6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008
Abbreviated title	FORMATS
Country/Territory	France
City	St. Malo
Period	15/09/08 → 17/09/08
Internet address	http://formats08.inria.fr/index.html

Access to Document

10.1007/978-3-540-85778-5_14

ArticleAccepted author version, 209 KB

Cite this

Remke, A., & Haverkort, B. R. (2008). A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks. In F. Cassez, & C. Jard (Eds.), The 6th International Conference on Formal Modelling and Analysis of Timed Systems (pp. 188-202). (Lecture Notes in Computer Science; Vol. 5215). Springer. https://doi.org/10.1007/978-3-540-85778-5_14

@inproceedings{44cb2bc98b24429eaf2d72657d5a5947,

title = "A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks",

abstract = "We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for these transient probabilities no computational procedures are readily available. The contribution of this paper is the proposal of a new uniformization-based approach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.",

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

year = "2008",

month = sep,

day = "15",

doi = "10.1007/978-3-540-85778-5_14",

language = "English",

isbn = "978-3-540-85777-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "188--202",

editor = "Franck Cassez and Claude Jard",

booktitle = "The 6th International Conference on Formal Modelling and Analysis of Timed Systems",

note = "6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008, FORMATS ; Conference date: 15-09-2008 Through 17-09-2008",

url = "http://formats08.inria.fr/index.html",

}

Remke, A & Haverkort, BR 2008, A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks. in F Cassez & C Jard (eds), The 6th International Conference on Formal Modelling and Analysis of Timed Systems. Lecture Notes in Computer Science, vol. 5215, Springer, Berlin, pp. 188-202, 6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008, St. Malo, France, 15/09/08. https://doi.org/10.1007/978-3-540-85778-5_14

A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks. / Remke, Anne ; Haverkort, Boudewijn R.

The 6th International Conference on Formal Modelling and Analysis of Timed Systems. ed. / Franck Cassez; Claude Jard. Berlin : Springer, 2008. p. 188-202 (Lecture Notes in Computer Science; Vol. 5215).

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

TY - GEN

T1 - A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks

AU - Remke, Anne

AU - Haverkort, Boudewijn R.

N1 - Conference code: 6

PY - 2008/9/15

Y1 - 2008/9/15

N2 - We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for these transient probabilities no computational procedures are readily available. The contribution of this paper is the proposal of a new uniformization-based approach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.

AB - We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for these transient probabilities no computational procedures are readily available. The contribution of this paper is the proposal of a new uniformization-based approach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.

U2 - 10.1007/978-3-540-85778-5_14

DO - 10.1007/978-3-540-85778-5_14

M3 - Conference contribution

SN - 978-3-540-85777-8

T3 - Lecture Notes in Computer Science

SP - 188

EP - 202

BT - The 6th International Conference on Formal Modelling and Analysis of Timed Systems

A2 - Cassez, Franck

A2 - Jard, Claude

PB - Springer

CY - Berlin

T2 - 6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008

Y2 - 15 September 2008 through 17 September 2008

ER -

A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this