Model checking action- and state-labelled Markov chains

Christel Baier, Lucia Cloth, Boudewijn Haverkort, Matthias Kuntz, Markus Siegle

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

    20 Citations (Scopus)
    1 Downloads (Pure)

    Abstract

    In this paper we introduce the logic asCSL, an extension of continuous stochastic logic (CSL), which provides powerful means to characterise execution paths of action- and state-labelled Markov chains. In asCSL, path properties are characterised by regular expressions over actions and state-formulas. Thus, the executability of a path not only depends on the available actions but also on the validity of certain state formulas in intermediate states. Our main result is that the model checking problem for asCSL can be reduced to CSL model checking on a modified Markov chain, which is obtained through a product automaton construction. We provide a case study of a scalable cellular phone system which shows how the logic asCSL and the model checking procedure can be applied in practice.
    Original languageEnglish
    Title of host publicationProceedings of the 2004 International Conference on Dependable Systems and Networks
    Place of PublicationPiscataway, NJ
    PublisherIEEE
    Pages701-710
    Number of pages10
    ISBN (Print)0-7695-2052-9
    DOIs
    Publication statusPublished - 28 Jun 2004
    EventInternational Conference on Dependable Systems and Networks, DSN 2004 - Florence, Italy
    Duration: 28 Jun 20041 Jul 2004

    Conference

    ConferenceInternational Conference on Dependable Systems and Networks, DSN 2004
    Abbreviated titleDSN
    Country/TerritoryItaly
    CityFlorence
    Period28/06/041/07/04

    Fingerprint

    Dive into the research topics of 'Model checking action- and state-labelled Markov chains'. Together they form a unique fingerprint.

    Cite this