Beyond memoryless distributions: model checking semi-Markov chains

Gabriel G. Infante lopez, Holger Hermanns, Joost-Pieter Katoen

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

    38 Citations (Scopus)
    100 Downloads (Pure)

    Abstract

    Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.
    Original languageEnglish
    Title of host publicationProcess Algebra and Probabilistic Methods. Performance Modelling and Verification
    Subtitle of host publicationJoint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001, Proceedings
    EditorsLuca de Alfaro, Stephen Gilmore
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages57-70
    Number of pages14
    ISBN (Electronic)978-3-540-44804-4
    ISBN (Print)978-3-540-42556-4
    DOIs
    Publication statusPublished - 2001
    EventJoint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001 - Aachen, Germany
    Duration: 12 Sep 200114 Sep 2001

    Workshop

    WorkshopJoint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001
    Abbreviated titlePAPM-PROBMIV
    CountryGermany
    CityAachen
    Period12/09/0114/09/01

    Keywords

    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-MC: MODEL CHECKING
    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
    • FMT-PM: PROBABILISTIC METHODS

    Fingerprint Dive into the research topics of 'Beyond memoryless distributions: model checking semi-Markov chains'. Together they form a unique fingerprint.

    Cite this