Model Checking Interactive Markov Chains

M. Neuhausser, Lijun Zhang

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    42 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