Comparative branching-time semantics for Markov chains

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

    Research output: Contribution to journalArticleAcademicpeer-review

    118 Citations (Scopus)
    142 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 characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branchingtime 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
    Pages (from-to)149-214
    Number of pages66
    JournalInformation and computation
    Volume200
    Issue number2
    DOIs
    Publication statusPublished - 2005

    Keywords

    • 2024 OA procedure

    Fingerprint

    Dive into the research topics of 'Comparative branching-time semantics for Markov chains'. Together they form a unique fingerprint.

    Cite this