Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes

M. Neuhausser, Joost P. Katoen

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

    20 Citations (Scopus)

    Abstract

    This paper introduces strong bisimulation for continuous-time Markov decision processes (CTMDPs), a stochastic model which allows for a nondeterministic choice between exponential distributions, and shows that bisimulation preserves the validity of CSL. To that end, we interpret the semantics of CSL - a stochastic variant of CTL for continuous-time Markov chains - on CTMDPs and show its measure theoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory.
    Original languageUndefined
    Title of host publication18th International Conference on Concurrency Theory (CONCUR)
    Place of PublicationLondon
    PublisherSpringer
    Pages412-427
    Number of pages16
    ISBN (Print)978-3-540-74406-1
    DOIs
    Publication statusPublished - Sep 2007
    Event18th International Conference on Concurrency Theory, CONCUR 2007 - Lisbon, Portugal
    Duration: 3 Sep 20078 Sep 2007
    Conference number: 18

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    NumberSupplement
    Volume4703

    Conference

    Conference18th International Conference on Concurrency Theory, CONCUR 2007
    Abbreviated titleCONCUR
    CountryPortugal
    CityLisbon
    Period3/09/078/09/07

    Keywords

    • IR-64519
    • METIS-245846
    • EWI-11539

    Cite this

    Neuhausser, M., & Katoen, J. P. (2007). Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. In 18th International Conference on Concurrency Theory (CONCUR) (pp. 412-427). [10.1007/978-3-540-74407-8_28] (Lecture Notes in Computer Science; Vol. 4703, No. Supplement). London: Springer. https://doi.org/10.1007/978-3-540-74407-8_28