Model Checking Interactive Markov Chains

M. Neuhausser; Lijun Zhang

doi:10.1007/978-3-642-12002-2_5

Model Checking Interactive Markov Chains

M. Neuhausser, Lijun Zhang

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

43 Citations (Scopus)

Abstract

Hermanns has introduced interactive Markov chains (IMCs) which arise as an orthogonal extension of labelled transition systems and continuous-time Markov chains (CTMCs). IMCs enjoy nice compositional aggregation properties which help to minimize the state space incrementally. However, the model checking problem for IMCs remains unsolved apart from those instances, where the IMC can be converted into a CTMC. This paper tackles this problem: We interpret the continuous stochastic logic (CSL) over IMCs and define the semantics of probabilistic CSL formulas with respect to the class of fully time and history dependent schedulers. Our main contribution is an efficient model checking algorithm for verifying CSL formulas on IMCs. Moreover, we show the applicability of our approach and provide some experimental results.

Original language	Undefined
Title of host publication	16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010
Editors	J. Esparza, R. Majumdar
Place of Publication	Berlin
Publisher	Springer
Pages	53-68
Number of pages	16
ISBN (Print)	978-3-642-12001-5
DOIs	https://doi.org/10.1007/978-3-642-12002-2_5
Publication status	Published - 1 Apr 2010
Event	16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010 - Paphos, Cyprus Duration: 20 Mar 2010 → 28 Mar 2010 Conference number: 16 http://www.etaps.org/2010/Conf/conf-frame-tacas.html

Publication series

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

Conference

Conference	16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010
Abbreviated title	TACAS
Country/Territory	Cyprus
City	Paphos
Period	20/03/10 → 28/03/10
Internet address	http://www.etaps.org/2010/Conf/conf-frame-tacas.html

Keywords

METIS-270938
EWI-18211
IR-72599

Access to Document

10.1007/978-3-642-12002-2_5

http://eprints.eemcs.utwente.nl/secure2/18211/01/mc_imcs.pdf

Cite this

@inproceedings{225f4f1ecf594dc788c3ef8610ebee0b,

title = "Model Checking Interactive Markov Chains",

abstract = "Hermanns has introduced interactive Markov chains (IMCs) which arise as an orthogonal extension of labelled transition systems and continuous-time Markov chains (CTMCs). IMCs enjoy nice compositional aggregation properties which help to minimize the state space incrementally. However, the model checking problem for IMCs remains unsolved apart from those instances, where the IMC can be converted into a CTMC. This paper tackles this problem: We interpret the continuous stochastic logic (CSL) over IMCs and define the semantics of probabilistic CSL formulas with respect to the class of fully time and history dependent schedulers. Our main contribution is an efficient model checking algorithm for verifying CSL formulas on IMCs. Moreover, we show the applicability of our approach and provide some experimental results.",

keywords = "METIS-270938, EWI-18211, IR-72599",

author = "M. Neuhausser and Lijun Zhang",

note = "10.1007/978-3-642-12002-2_5 ; 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010 ; Conference date: 20-03-2010 Through 28-03-2010",

year = "2010",

month = apr,

day = "1",

doi = "10.1007/978-3-642-12002-2_5",

language = "Undefined",

isbn = "978-3-642-12001-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "53--68",

editor = "J. Esparza and R. Majumdar",

booktitle = "16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010",

url = "http://www.etaps.org/2010/Conf/conf-frame-tacas.html",

}

Neuhausser, M & Zhang, L 2010, Model Checking Interactive Markov Chains. in J Esparza & R Majumdar (eds), 16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010. Lecture Notes in Computer Science, vol. 6015, Springer, Berlin, pp. 53-68, 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Paphos, Cyprus, 20/03/10. https://doi.org/10.1007/978-3-642-12002-2_5

Model Checking Interactive Markov Chains. / Neuhausser, M.; Zhang, Lijun.
16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010. ed. / J. Esparza; R. Majumdar. Berlin: Springer, 2010. p. 53-68 (Lecture Notes in Computer Science; Vol. 6015).

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

TY - GEN

T1 - Model Checking Interactive Markov Chains

AU - Neuhausser, M.

AU - Zhang, Lijun

N1 - Conference code: 16

PY - 2010/4/1

Y1 - 2010/4/1

N2 - Hermanns has introduced interactive Markov chains (IMCs) which arise as an orthogonal extension of labelled transition systems and continuous-time Markov chains (CTMCs). IMCs enjoy nice compositional aggregation properties which help to minimize the state space incrementally. However, the model checking problem for IMCs remains unsolved apart from those instances, where the IMC can be converted into a CTMC. This paper tackles this problem: We interpret the continuous stochastic logic (CSL) over IMCs and define the semantics of probabilistic CSL formulas with respect to the class of fully time and history dependent schedulers. Our main contribution is an efficient model checking algorithm for verifying CSL formulas on IMCs. Moreover, we show the applicability of our approach and provide some experimental results.

AB - Hermanns has introduced interactive Markov chains (IMCs) which arise as an orthogonal extension of labelled transition systems and continuous-time Markov chains (CTMCs). IMCs enjoy nice compositional aggregation properties which help to minimize the state space incrementally. However, the model checking problem for IMCs remains unsolved apart from those instances, where the IMC can be converted into a CTMC. This paper tackles this problem: We interpret the continuous stochastic logic (CSL) over IMCs and define the semantics of probabilistic CSL formulas with respect to the class of fully time and history dependent schedulers. Our main contribution is an efficient model checking algorithm for verifying CSL formulas on IMCs. Moreover, we show the applicability of our approach and provide some experimental results.

KW - METIS-270938

KW - EWI-18211

KW - IR-72599

U2 - 10.1007/978-3-642-12002-2_5

DO - 10.1007/978-3-642-12002-2_5

M3 - Conference contribution

SN - 978-3-642-12001-5

T3 - Lecture Notes in Computer Science

SP - 53

EP - 68

BT - 16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010

A2 - Esparza, J.

A2 - Majumdar, R.

PB - Springer

CY - Berlin

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

Y2 - 20 March 2010 through 28 March 2010

ER -