×

zbMATH — the first resource for mathematics

Three-valued abstraction for continuous-time Markov chains. (English) Zbl 1135.68476
Damm, Werner (ed.) et al., Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73367-6/pbk). Lecture Notes in Computer Science 4590, 311-324 (2007).
Summary: This paper proposes a novel abstraction technique for continuous-time Markov chains (CTMCs). Our technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key idea is to apply abstraction on uniform CTMCs that are readily obtained from general CTMCs, and to abstract transition probabilities by intervals. It is shown that this provides a conservative abstraction for both true and false for a three-valued semantics of the branching-time logic CSL (Continuous Stochastic Logic). Experiments on an infinite-state CTMC indicate the feasibility of our abstraction technique.
For the entire collection see [Zbl 1119.68005].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
MRMC; PEPA; SIGREF; SMART_
PDF BibTeX XML Cite
Full Text: DOI