Simulation for continuous-time Markov chains

Christel Baier, Joost P. Katoen, Holger Hermanns, Boudewijn Haverkort

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

    19 Citations (Scopus)
    26 Downloads (Pure)

    Abstract

    This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.
    Original languageEnglish
    Title of host publicationCONCUR 2002 — Concurrency Theory
    Subtitle of host publication13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings
    EditorsLuboš Brim, Mojmír Křetínský, Antonín Kučera, Petr Jančar
    Place of Publication978-3-540-45694-0
    PublisherSpringer
    Pages338-354
    ISBN (Electronic)978-3-540-45694-0
    ISBN (Print)978-3-540-44043-7
    DOIs
    Publication statusPublished - 2002
    Event13th International Conference on Concurrency Theory, CONCUR 2002 - Brno, Czech Republic
    Duration: 20 Aug 200223 Aug 2002
    Conference number: 13

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume2421
    ISSN (Print)0302-9743

    Conference

    Conference13th International Conference on Concurrency Theory, CONCUR 2002
    Abbreviated titleCONCUR
    Country/TerritoryCzech Republic
    CityBrno
    Period20/08/0223/08/02

    Keywords

    • FMT-MC: MODEL CHECKING
    • FMT-PM: PROBABILISTIC METHODS
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

    Fingerprint

    Dive into the research topics of 'Simulation for continuous-time Markov chains'. Together they form a unique fingerprint.

    Cite this