Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes

Martin R. Neuhausser, Joost-Pieter Katoen

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

    24 Citations (Scopus)
    3 Downloads (Pure)

    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 languageEnglish
    Title of host publicationCONCUR 2007 – Concurrency Theory
    Subtitle of host publication18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007. Proceedings
    Place of PublicationLondon
    PublisherSpringer
    Pages412-427
    Number of pages16
    ISBN (Electronic)978-3-540-74407-8
    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
    Volume4703
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

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

    Keywords

    • Continuous-time Markov decision process (CTMDP)

    Fingerprint

    Dive into the research topics of 'Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes'. Together they form a unique fingerprint.

    Cite this