Model Checking Interactive Markov Chains

M. Neuhausser, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 languageUndefined
Title of host publication16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010
EditorsJ. Esparza, R. Majumdar
Place of PublicationBerlin
PublisherSpringer
Pages53-68
Number of pages16
ISBN (Print)978-3-642-12001-5
DOIs
Publication statusPublished - 1 Apr 2010
Event16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010 - Paphos, Cyprus
Duration: 20 Mar 201028 Mar 2010
Conference number: 16
http://www.etaps.org/2010/Conf/conf-frame-tacas.html

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume6015
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010
Abbreviated titleTACAS
CountryCyprus
CityPaphos
Period20/03/1028/03/10
Internet address

Keywords

  • METIS-270938
  • EWI-18211
  • IR-72599

Cite this

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 (pp. 53-68). (Lecture Notes in Computer Science; Vol. 6015). Berlin: Springer. https://doi.org/10.1007/978-3-642-12002-2_5
Neuhausser, M. ; Zhang, Lijun. / Model Checking Interactive Markov Chains. 16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010. editor / J. Esparza ; R. Majumdar. Berlin : Springer, 2010. pp. 53-68 (Lecture Notes in Computer Science).
@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",
year = "2010",
month = "4",
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",

}

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 proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Model Checking Interactive Markov Chains

AU - Neuhausser, M.

AU - Zhang, Lijun

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

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

ER -

Neuhausser M, Zhang L. Model Checking Interactive Markov Chains. In Esparza J, Majumdar R, editors, 16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010. Berlin: Springer. 2010. p. 53-68. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-12002-2_5