DocumentCode :
2275073
Title :
Time-bounded model checking of infinite-state continuous-time Markov chains
Author :
Zhang, Lijun ; Hermanns, Holger ; Hahn, E. Moritz ; Wachter, Bjorn
Author_Institution :
Dept. of Comput. Sci., Saarland Univ., Saarbrucken
fYear :
2008
fDate :
23-27 June 2008
Firstpage :
98
Lastpage :
107
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.
Keywords :
Markov processes; continuous time systems; formal logic; formal verification; complex concurrent system design; continuous stochastic logic; infinite-state continuous-time Markov chains; time-bounded model checking; timed probabilistic reachability; Availability; Biological system modeling; Biology computing; Network synthesis; Probabilistic logic; Proteins; State-space methods; Stochastic processes; Timing; Transient analysis;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Application of Concurrency to System Design, 2008. ACSD 2008. 8th International Conference on
Conference_Location :
Xian
ISSN :
1550-4808
Print_ISBN :
978-1-4244-1838-1
Electronic_ISBN :
1550-4808
Type :
conf
DOI :
10.1109/ACSD.2008.4574601
Filename :
4574601
Link To Document :
بازگشت