Counterexample Generation for Probabilistic Timed Automata Model Checking

This paper presents algorithms on counterexample generation for model checking probabilistic timed automata (PTA). Firstly, the k most probable paths satisfying constraints in a PTA whose probability sum is just greater than a threshold are searched. The sub-graph of the PTA constructed upon above paths is a counterexample with small number of testimonies. Secondly, refinement follows - By adding paths from above one by one in order of decreasing probability, and calculating the precise maximal probabilities on the new PTAs constructed from the added paths, the counterexample occupying least testimonies is derived. The refinement is accomplished through an executable and converging algorithm.