Quantitative model checking of continuous-time Markov chains against timed automata specifications

T. Chen, Tingting Han, Joost P. Katoen, Alexandru Mereacre

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

    29 Citations (Scopus)
    48 Downloads (Pure)

    Abstract

    We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.
    Original languageUndefined
    Title of host publication2009 24th Annual IEEE Symposium on Logic In Computer Science
    Place of PublicationPiscataway
    PublisherIEEE Computer Society
    Pages309-318
    Number of pages10
    ISBN (Print)978-0-7695-3746-7
    DOIs
    Publication statusPublished - Aug 2009
    Event24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009 - UCLA, Los Angeles, United States
    Duration: 11 Aug 200914 Aug 2009
    Conference number: 24

    Publication series

    Name
    PublisherIEEE Computer Society Press
    ISSN (Print)1043-6871

    Conference

    Conference24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009
    Abbreviated titleLICS
    CountryUnited States
    CityLos Angeles
    Period11/08/0914/08/09

    Keywords

    • METIS-264047
    • IR-68256
    • EWI-16106
    • FMT-PM: PROBABILISTIC METHODS
    • FMT-MC: MODEL CHECKING

    Cite this

    Chen, T., Han, T., Katoen, J. P., & Mereacre, A. (2009). Quantitative model checking of continuous-time Markov chains against timed automata specifications. In 2009 24th Annual IEEE Symposium on Logic In Computer Science (pp. 309-318). [10.1109/LICS.2009.21] Piscataway: IEEE Computer Society. https://doi.org/10.1109/LICS.2009.21