Comparative branching-time semantics for Markov chains

Christel Baier, H. Hermanns, Joost P. Katoen, Verena Wolf

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

    12 Citations (Scopus)
    72 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 and CSL. Apart from presenting various existing branching-time relations in a uniform manner, our contributions are: (i) weak simulation for DTMCs is defined, (ii) weak bisimulation equivalence is shown to coincide with weak simulation equivalence, (iii) logical characterisation of weak (bi)simulations are provided, and (iv) a classification of branching-time relations is presented, elucidating the semantics of DTMCs, CTMCs and their interrelation.
    Original languageUndefined
    Title of host publicationConcurrency Theory (CONCUR)
    EditorsRoberto Amadio, Denis Lugiez
    Place of PublicationBerlin
    PublisherSpringer
    Pages492-507
    Number of pages16
    ISBN (Print)978-3-540-40753-9
    DOIs
    Publication statusPublished - 2003
    Event14th International Conference on Concurrency Theory, CONCUR 2003 - Marseille, France
    Duration: 3 Sep 20035 Sep 2003
    Conference number: 14

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer-Verlag
    NumberXI
    Volume2761
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference14th International Conference on Concurrency Theory, CONCUR 2003
    Abbreviated titleCONCUR
    CountryFrance
    CityMarseille
    Period3/09/035/09/03

    Keywords

    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-MC: MODEL CHECKING
    • FMT-PM: PROBABILISTIC METHODS
    • METIS-217628
    • IR-47300
    • EWI-6537

    Cite this

    Baier, C., Hermanns, H., Katoen, J. P., & Wolf, V. (2003). Comparative branching-time semantics for Markov chains. In R. Amadio, & D. Lugiez (Eds.), Concurrency Theory (CONCUR) (pp. 492-507). (Lecture Notes in Computer Science; Vol. 2761, No. XI). Berlin: Springer. https://doi.org/10.1007/978-3-540-45187-7_32