Journal article icon

Journal article

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

Abstract:

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, suc...

Expand abstract

Actions


Access Document


Publisher copy:
10.3233/FI-2009-145

Authors


Journal:
Fundamenta Informaticae
Volume:
95
Pages:
129-155
Publication date:
2009-01-01
DOI:
ISSN:
1875-8681
URN:
uuid:f73b785b-5f7c-4bff-9435-bcb68a11e246
Local pid:
cs:4765

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP