Time-bounded model checking of infinite-state continuous-time Markov chains

Lijun Zhang, Holger Hermanns, Ernst Moritz Hahn, Bjorn Wachter

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

10 Citations (Scopus)

Abstract

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are widely used models for concurrent system designs making it possible to model check such properties. In this paper, we focus on probabilistic timing properties of infinite-state CTMCs, expressible in continuous stochastic logic (CSL). Such properties comprise important dependability measures, such as timed probabilistic reachability, performability, survivability, and various availability measures like instantaneous availabilities, conditional instantaneous availabilities and interval availabilities. Conventional model checkers explore the given model exhaustively which is not always possible either due to state explosion or because the model is infinite. This paper presents a method that only explores the infinite (or prohibitively large) model up to a finite depth, with the depth bound being computed on-the-fly. We provide experimental evidence showing that our method is effective.
Original languageEnglish
Title of host publication2008 8th International Conference on Application of Concurrency to System Design
Place of PublicationPiscataway, NJ
PublisherIEEE
Number of pages11
ISBN (Electronic)978-1-4244-1839-8
ISBN (Print)978-1-4244-1838-1
DOIs
Publication statusPublished - 2008
Externally publishedYes
Event8th International Conference on Application of Concurrency to System Design, ACSD 2008 - Xidian University, Xian, China
Duration: 23 Jun 200827 Jun 2008
Conference number: 8

Conference

Conference8th International Conference on Application of Concurrency to System Design, ACSD 2008
Abbreviated titleACSD 2008
CountryChina
CityXian
Period23/06/0827/06/08

Fingerprint 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