Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains

Ernst Moritz Hahn

Research output: Contribution to journalArticleAcademicpeer-review

12 Citations (Scopus)


The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism that captures such performance and dependability properties, and makes them analyzable by model checking. In this paper, we focus on time-bounded probabilistic properties of infinite-state CTMCs, expressible in a subset of continuous stochastic logic (CSL). This comprises important dependability measures, such as time-bounded probabilistic reachability, performability, survivability, and various availability measures like instantaneous, conditional instantaneous and interval availabilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This paper presents a method that only explores the model up to a finite depth. The required depth is determined on the fly by an algorithm that is configurable in order to adapt to the characteristics of different classes of models. We provide experimental evidence showing that our method is effective.
Original languageEnglish
Pages (from-to)129-155
JournalFundamenta informaticae
Issue number1
Publication statusPublished - 2009
Externally publishedYes


Dive into the research topics of 'Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains'. Together they form a unique fingerprint.

Cite this