Symbolic Model Checking of Stochastic Systems: Theory and Implementation

G.W.M. Kuntz, Markus Siegle

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

    4 Citations (Scopus)
    11 Downloads (Pure)


    This paper presents IM-SPDL, a stochastic extension of the modal logic PDL, which supports the specification of complex performance and dependability requirements. The logic is interpreted over extended stochastic labelled transition systems (ESLTS), i.e. transition systems containing both immediate and Markovian transitions. We define the syntax and semantics of the new logic and show that IM-SPDL provides powerful means to specify path-based properties with timing restrictions. In general, paths can be characterised by regular expressions, also called programs, where the executability of a program may depend on the validity of test formulae. For the model checking of IM-SPDL time-bounded path formulae, a deterministic program automaton is constructed from the requirement. Afterwards the product transition system between this automaton and the ESLTS is built and subsequently transformed into a continuous time Markov Chain (CTMC) on which numerical analysis is performed. Empirical results given in the paper show that model checking IM-SPDL can be realised efficiently in practice.
    Original languageUndefined
    Title of host publicationProceedings of the 13th International SPIN Workshop
    EditorsAntti Valmari
    Place of PublicationBerlin
    Number of pages19
    ISBN (Print)978-3-540-33102-5
    Publication statusPublished - 2006
    Event13th International SPIN Workshop on Model Checking of Software 2006 - Vienna, Austria
    Duration: 30 Mar 20061 Apr 2006
    Conference number: 13

    Publication series

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


    Conference13th International SPIN Workshop on Model Checking of Software 2006


    • model checking software
    • EWI-8961
    • IR-63896
    • METIS-238734
    • Symbolic model checking
    • performance and dependability analysis
    • Stochastic systems

    Cite this