Comparative Branching-Time Semantics for Markov Chains

C Baier, Joost P. Katoen, H. Hermanns, V. Wolf

    Research output: Book/ReportReportProfessional

    55 Downloads (Pure)


    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 languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages64
    Publication statusPublished - Aug 2004

    Publication series

    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)


    • METIS-221297
    • EWI-5774
    • IR-49190

    Cite this