Counterexample Exploration in CTMC Model Checking

 

Tingting Han

 

 

Abstract:

 

In this talk, I will present algorithms for the generation of
counterexamples in CTMC model checking with time-bounded reachability
properties.  Main problems that are considered are the definition of
evidence and a counterexample, and the algorithms for generating the
most informative evidences and counterexamples.  It is shown that
these problems can be solved using uniformization, a standard
technique for CTMCs, and shortest path algorithms.  The main
contribution is a mapping of counter example generation in a
continuous setting to recent algorithms for counterexample generation
for DTMC model checking that is correct up to an a priori fixed
inaccuracy.