Counterexample Generation for Probabilistic Timed Automata Model Checking

Counterexample is a typical topic in model checking. Model checking probabilistic systems have been studied well these years, but counterexample generation for probabilistic system model checking has just drawn some attentions recently. Current works are mainly focusing on the counterexample generation for Markov chain. Probabilistic timed automata （PTA） are the extension of Markov chain with non-determinism and system clocks, and have been used broadly on network protocol modeling and verification. The focus of this paper is on counterexample generation while model is checking PTA. Firstly, a research is made for the k most probable paths whose probability sum is just greater than λ. PTA can be regarded as discrete-time Markov chain （DTMC） in this situation. The sub-graph of PTA constructed from the above paths and the initial PTA is a counterexample which can be obtained quickly with small number of testimonies. When the maximal probability is calculated in a PTA, the contribution to probability not only comes from the contained paths, but also from the symbolic state intersections originated in the existence of system clocks. So refinement can be done as a further step—By adding paths from the above one by one in order to decrease probability, and to calculate the precise maximal probability on the sub-graph of PTA constructed from the added paths and initial PTA, the counterexample occupying less testimonies can be obtained. The refinement process is accomplished through an executable and converging algorithm with high efficiency.