Symbolic Model Checking of Stochastic Systems: Theory and Implementation

Matthias 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 languageEnglish
Title of host publicationModel Checking Software
Subtitle of host publication13th International SPIN Workshop, Vienna, Austria, March 30 - April 1, 2006. Proceedings
EditorsAntti Valmari
Place of PublicationBerlin
Number of pages19
ISBN (Electronic)978-3-540-33103-2
ISBN (Print)978-3-540-33102-5
Publication statusPublished - 2006
Externally publishedYes
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
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International SPIN Workshop on Model Checking of Software 2006


  • Model checking software
  • Symbolic model checking
  • Performance and dependability analysis
  • Stochastic systems


Dive into the research topics of 'Symbolic Model Checking of Stochastic Systems: Theory and Implementation'. Together they form a unique fingerprint.

Cite this