Comparative branching-time semantics for Markov chains

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

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

    17 Citations (Scopus)
    97 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 languageEnglish
    Title of host publicationCONCUR 2003 - Concurrency Theory
    Subtitle of host publication14th International Conference, Marseille, France, September 3-5, 2003. Proceedings
    EditorsRoberto Amadio, Denis Lugiez
    Place of PublicationBerlin
    PublisherSpringer
    Pages492-507
    Number of pages16
    ISBN (Electronic)978-3-540-45187-7
    ISBN (Print)978-3-540-40753-9
    DOIs
    Publication statusPublished - 2003
    Event14th International Conference on Concurrency Theory, CONCUR 2003 - Marseille, France
    Duration: 3 Sept 20035 Sept 2003
    Conference number: 14

    Publication series

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

    Conference

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

    Keywords

    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-MC: MODEL CHECKING
    • FMT-PM: PROBABILISTIC METHODS
    • 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