Beyond memoryless distributions: model checking semi-Markov chains

Gabriel G. Infante Lopez; Holger Hermanns; Joost-Pieter Katoen

doi:10.1007/3-540-44804-7_4

Beyond memoryless distributions: model checking semi-Markov chains

Gabriel G. Infante Lopez, Holger Hermanns, Joost-Pieter Katoen

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

45 Citations (Scopus)

108 Downloads (Pure)

Abstract

Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.

Original language	English
Title of host publication	Process Algebra and Probabilistic Methods. Performance Modelling and Verification
Subtitle of host publication	Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001, Proceedings
Editors	Luca de Alfaro, Stephen Gilmore
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	57-70
Number of pages	14
ISBN (Electronic)	978-3-540-44804-4
ISBN (Print)	978-3-540-42556-4
DOIs	https://doi.org/10.1007/3-540-44804-7_4
Publication status	Published - 2001
Event	Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001 - Aachen, Germany Duration: 12 Sept 2001 → 14 Sept 2001

Workshop

Workshop	Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001
Abbreviated title	PAPM-PROBMIV
Country/Territory	Germany
City	Aachen
Period	12/09/01 → 14/09/01

Keywords

FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
FMT-MC: MODEL CHECKING
FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
FMT-PM: PROBABILISTIC METHODS

Access to Document

10.1007/3-540-44804-7_4

Cite this

Infante Lopez, G. G., Hermanns, H., & Katoen, J.-P. (2001). Beyond memoryless distributions: model checking semi-Markov chains. In L. de Alfaro, & S. Gilmore (Eds.), Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001, Proceedings (pp. 57-70). Springer. https://doi.org/10.1007/3-540-44804-7_4

Infante Lopez, Gabriel G. ; Hermanns, Holger ; Katoen, Joost-Pieter. / Beyond memoryless distributions : model checking semi-Markov chains. Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001, Proceedings. editor / Luca de Alfaro ; Stephen Gilmore. Berlin, Heidelberg : Springer, 2001. pp. 57-70

@inproceedings{44090328fcd644658747371e5b2e2313,

title = "Beyond memoryless distributions: model checking semi-Markov chains",

abstract = "Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.",

keywords = "FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-MC: MODEL CHECKING, FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, FMT-PM: PROBABILISTIC METHODS",

author = "{Infante Lopez}, {Gabriel G.} and Holger Hermanns and Joost-Pieter Katoen",

year = "2001",

doi = "10.1007/3-540-44804-7_4",

language = "English",

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

pages = "57--70",

editor = "{de Alfaro}, Luca and Stephen Gilmore",

booktitle = "Process Algebra and Probabilistic Methods. Performance Modelling and Verification",

publisher = "Springer",

address = "Germany",

note = "Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001, PAPM-PROBMIV ; Conference date: 12-09-2001 Through 14-09-2001",

}

Infante Lopez, GG, Hermanns, H & Katoen, J-P 2001, Beyond memoryless distributions: model checking semi-Markov chains. in L de Alfaro & S Gilmore (eds), Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001, Proceedings. Springer, Berlin, Heidelberg, pp. 57-70, Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001, Aachen, Germany, 12/09/01. https://doi.org/10.1007/3-540-44804-7_4

Beyond memoryless distributions: model checking semi-Markov chains. / Infante Lopez, Gabriel G.; Hermanns, Holger; Katoen, Joost-Pieter.
Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001, Proceedings. ed. / Luca de Alfaro; Stephen Gilmore. Berlin, Heidelberg: Springer, 2001. p. 57-70.

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

TY - GEN

T1 - Beyond memoryless distributions

T2 - Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001

AU - Infante Lopez, Gabriel G.

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

PY - 2001

Y1 - 2001

N2 - Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.

AB - Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-MC: MODEL CHECKING

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - FMT-PM: PROBABILISTIC METHODS

U2 - 10.1007/3-540-44804-7_4

DO - 10.1007/3-540-44804-7_4

M3 - Conference contribution

SN - 978-3-540-42556-4

SP - 57

EP - 70

BT - Process Algebra and Probabilistic Methods. Performance Modelling and Verification

A2 - de Alfaro, Luca

A2 - Gilmore, Stephen

PB - Springer

CY - Berlin, Heidelberg

Y2 - 12 September 2001 through 14 September 2001

ER -

Infante Lopez GG, Hermanns H, Katoen JP. Beyond memoryless distributions: model checking semi-Markov chains. In de Alfaro L, Gilmore S, editors, Process Algebra and Probabilistic Methods. Performance Modelling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001, Proceedings. Berlin, Heidelberg: Springer. 2001. p. 57-70 doi: 10.1007/3-540-44804-7_4

Beyond memoryless distributions: model checking semi-Markov chains

Abstract

Workshop

Keywords

Access to Document

Fingerprint

Cite this