Performance analysis := (process algebra + model checking) x Markov chains

Holger Hermanns; Joost-Pieter Katoen

doi:10.1007/3-540-44685-0

Performance analysis := (process algebra + model checking) x Markov chains

Holger Hermanns
, Joost-Pieter Katoen

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

48 Downloads (Pure)

Abstract

Markov chains are widely used in practice to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This tutorial paper shows how successful model specification and analysis techniques from concurrency theory can be applied to performance evaluation. The specification of CTMCs is supported by a stochastic process algebra, while the quantitative analysis of these models is tackled by means of model checking. Process algebra provides: (i) a high-level specification formalism for describing CTMCs in a precise, modular and constraint-oriented way, and (ii) means for the automated generation and aggregation of CTMCs. Temporal logic model checking provides: (i) a formalism to specify complex measures-of-interest in a lucid, compact and flexible way, (ii) automated means to quantify these measures over CTMCs, and (iii) automated measure-driven aggregation (lumping) of CTMCs. Combining process algebra and model checking constitutes a coherent framework for performance evaluation based on CTMCs.

Original language	English
Title of host publication	CONCUR 2001 - Concurrency Theory
Subtitle of host publication	12th International Conference, Aalborg, Denmark, August 20-25, 2001 Proceedings
Editors	Kim G. Larsen, Mogens Nielsen
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	59–81
ISBN (Electronic)	978-3-540-44685-9
ISBN (Print)	978-3-540-42497-0
DOIs	https://doi.org/10.1007/3-540-44685-0
Publication status	Published - 2001
Event	12th International Conference on Concurrency Theory, CONCUR 2001 - Aalborg, Denmark Duration: 20 Aug 2001 → 25 Aug 2001 Conference number: 12

Publication series

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

Conference

Conference	12th International Conference on Concurrency Theory, CONCUR 2001
Abbreviated title	CONCUR
Country/Territory	Denmark
City	Aalborg
Period	20/08/01 → 25/08/01

Keywords

2023 OA procedure

Access to Document

10.1007/3-540-44685-0

ArticleFinal published version, 290 KBLicence: Taverne

Cite this

Hermanns, H., & Katoen, J.-P. (2001). Performance analysis := (process algebra + model checking) x Markov chains. In K. G. Larsen, & M. Nielsen (Eds.), CONCUR 2001 - Concurrency Theory: 12th International Conference, Aalborg, Denmark, August 20-25, 2001 Proceedings (pp. 59–81). (Lecture Notes in Computer Science; Vol. 2154). Springer. https://doi.org/10.1007/3-540-44685-0

@inproceedings{a658ab1fc5a14b39aa6a4ec211cb0fa7,

title = "Performance analysis := (process algebra + model checking) x Markov chains",

abstract = "Markov chains are widely used in practice to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This tutorial paper shows how successful model specification and analysis techniques from concurrency theory can be applied to performance evaluation. The specification of CTMCs is supported by a stochastic process algebra, while the quantitative analysis of these models is tackled by means of model checking. Process algebra provides: (i) a high-level specification formalism for describing CTMCs in a precise, modular and constraint-oriented way, and (ii) means for the automated generation and aggregation of CTMCs. Temporal logic model checking provides: (i) a formalism to specify complex measures-of-interest in a lucid, compact and flexible way, (ii) automated means to quantify these measures over CTMCs, and (iii) automated measure-driven aggregation (lumping) of CTMCs. Combining process algebra and model checking constitutes a coherent framework for performance evaluation based on CTMCs.",

keywords = "2023 OA procedure",

author = "Holger Hermanns and Joost-Pieter Katoen",

year = "2001",

doi = "10.1007/3-540-44685-0",

language = "English",

isbn = "978-3-540-42497-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "59–81",

editor = "Larsen, \{Kim G.\} and Mogens Nielsen",

booktitle = "CONCUR 2001 - Concurrency Theory",

address = "Germany",

note = "12th International Conference on Concurrency Theory, CONCUR 2001, CONCUR ; Conference date: 20-08-2001 Through 25-08-2001",

}

Hermanns, H & Katoen, J-P 2001, Performance analysis := (process algebra + model checking) x Markov chains. in KG Larsen & M Nielsen (eds), CONCUR 2001 - Concurrency Theory: 12th International Conference, Aalborg, Denmark, August 20-25, 2001 Proceedings. Lecture Notes in Computer Science, vol. 2154, Springer, Berlin, Heidelberg, pp. 59–81, 12th International Conference on Concurrency Theory, CONCUR 2001, Aalborg, Denmark, 20/08/01. https://doi.org/10.1007/3-540-44685-0

Performance analysis := (process algebra + model checking) x Markov chains. / Hermanns, Holger; Katoen, Joost-Pieter.
CONCUR 2001 - Concurrency Theory: 12th International Conference, Aalborg, Denmark, August 20-25, 2001 Proceedings. ed. / Kim G. Larsen; Mogens Nielsen. Berlin, Heidelberg: Springer, 2001. p. 59–81 (Lecture Notes in Computer Science; Vol. 2154).

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

TY - GEN

T1 - Performance analysis := (process algebra + model checking) x Markov chains

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

N1 - Conference code: 12

PY - 2001

Y1 - 2001

N2 - Markov chains are widely used in practice to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This tutorial paper shows how successful model specification and analysis techniques from concurrency theory can be applied to performance evaluation. The specification of CTMCs is supported by a stochastic process algebra, while the quantitative analysis of these models is tackled by means of model checking. Process algebra provides: (i) a high-level specification formalism for describing CTMCs in a precise, modular and constraint-oriented way, and (ii) means for the automated generation and aggregation of CTMCs. Temporal logic model checking provides: (i) a formalism to specify complex measures-of-interest in a lucid, compact and flexible way, (ii) automated means to quantify these measures over CTMCs, and (iii) automated measure-driven aggregation (lumping) of CTMCs. Combining process algebra and model checking constitutes a coherent framework for performance evaluation based on CTMCs.

AB - Markov chains are widely used in practice to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This tutorial paper shows how successful model specification and analysis techniques from concurrency theory can be applied to performance evaluation. The specification of CTMCs is supported by a stochastic process algebra, while the quantitative analysis of these models is tackled by means of model checking. Process algebra provides: (i) a high-level specification formalism for describing CTMCs in a precise, modular and constraint-oriented way, and (ii) means for the automated generation and aggregation of CTMCs. Temporal logic model checking provides: (i) a formalism to specify complex measures-of-interest in a lucid, compact and flexible way, (ii) automated means to quantify these measures over CTMCs, and (iii) automated measure-driven aggregation (lumping) of CTMCs. Combining process algebra and model checking constitutes a coherent framework for performance evaluation based on CTMCs.

KW - 2023 OA procedure

U2 - 10.1007/3-540-44685-0

DO - 10.1007/3-540-44685-0

M3 - Conference contribution

SN - 978-3-540-42497-0

T3 - Lecture Notes in Computer Science

SP - 59

EP - 81

BT - CONCUR 2001 - Concurrency Theory

A2 - Larsen, Kim G.

A2 - Nielsen, Mogens

PB - Springer

CY - Berlin, Heidelberg

T2 - 12th International Conference on Concurrency Theory, CONCUR 2001

Y2 - 20 August 2001 through 25 August 2001

ER -

Performance analysis := (process algebra + model checking) x Markov chains

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this