Three-Valued Abstraction for Continuous-Time Markov Chains

lued Abstraction for Continuous-Time Markov Chains⋆ Joost-Pieter Katoen1 , Daniel Klink1 , Martin Leucker2 , and Verena Wolf3 RWTH Aachen University1 , TU Munich2 , University of Mannheim3 , Germany Abstract. This paper proposes a novel abstraction technique for continuous-time Markov chains (CTMCs). Our technique fits within the realm -valued abstraction methods that have been used successfully itional model checking. The key idea is to apply abstraction on uniform CTMCs that are readily obtained from general CTMCs, and act transition probabilities by intervals. It is shown that this provides a conservative abstraction for both true and false for a threevalued semantics of the branching-time logic CSL (Continuous Stochastic Logic). Experiments on an infinite-state CTMC indicate the feasibility bstraction technique.

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf
• Keywords: Abstraction, CAV 2007, Continuous-time Markov, Continuous-Time Markov Chains⋆, Formal Methods