Model Checking Interval Probabilistic Timed Automata

Interval probabilistic timed automata (IPTA) is put forward extending from probabilistic timed automata, and can be used to model network protocol or fault system with uncertain state transition probability. While we use PTCTL to denote the property of above systems, a solution to model check IPTA against PTCTL is presented. The key problems in the solution are calculating maximum probability and minimum probability on IPTA. To calculate maximum probability on IPTA, we first convert IPTA to interval Markov decision process with loose condition (LIMDP) through backward breath-first traverse based on symbolic state, and then give the strategy to calculate maximum probability on LIMDP. The calculation of minimum probability on IPTA can be converted to calculation of maximum probability on IPTA.