Comparative Branching-Time Semantics for Markov Chains

Christel Baier, Joost-Pieter Katoen, Holger Hermanns, Verena Wolf

    Research output: Book/Report › Report › Professional

    69 Downloads (Pure)

    Abstract

    This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterised in terms of the temporal logics PCTL (Probabilistic Computation Tree Logic) and CSL (Continuous Stochastic Logic). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages64
    Publication statusPublished - Aug 2004

    Publication series

    NameCTIT technical report series
    PublisherUniversity of Twente, CTIT
    No.04-32
    ISSN (Print)1381-3625

    Keywords

    • Comparative semantics
    • Markov chain
    • (Weak) simulation
    • (Weak) bisimulation
    • Temporal logic

    Access to Document

    • ReportFinal published version, 568 KB

      Fingerprint

      Dive into the research topics of 'Comparative Branching-Time Semantics for Markov Chains'. Together they form a unique fingerprint.
      View full fingerprint
      • 1 Conference contribution
      • 1 Article

      • Comparative branching-time semantics for Markov chains

        Baier, C., Katoen, J.-P., Hermanns, H. & Wolf, V., 2005, In: Information and computation. 200, 2, p. 149-214 66 p.

        Research output: Contribution to journal › Article › Academic › peer-review

        Open Access
        File
        118 Citations (Scopus)
        138 Downloads (Pure)

      • Comparative branching-time semantics for Markov chains

        Baier, C., Hermanns, H., Katoen, J.-P. & Wolf, V., 2003, CONCUR 2003 - Concurrency Theory: 14th International Conference, Marseille, France, September 3-5, 2003. Proceedings. Amadio, R. & Lugiez, D. (eds.). Berlin: Springer, p. 492-507 16 p. (Lecture Notes in Computer Science; vol. 2761).

        Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

        Open Access
        File
        17 Citations (Scopus)
        95 Downloads (Pure)

      Cite this