Model checking probabilistic timed automata in the presence of uncertainties

作者：Zhang Junhua^*; Huang Zhiqiu; Cao Zining; Xiao Fangxiong

来源：Journal of Computational Information Systems, 2010, 6(7): 2231-2243.

• Breath-first
• Fault system
• Interval probability
• Key problems
• Markov Decision Processes
• Maximum probability
• Model check
• Network protocol modeling
• Probabilistic systems
• Probabilistic timed automata
• Real time
• State transition probabilities
• Symbolic state
• Transition probabilities

Probabilistic timed automata (PTA) is prevalent to describe real time and probabilistic system. The transition probability in a distribution starting from a state in PTA is fixed, but it is not always coincided with the real world. In this paper, Interval probabilistic timed automata (IPTA) is put forward extending from PTA, which permits the transition probability to vary at an interval. IPTA can be broadly 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.

• 出版日期2010
• 单位南京航空航天大学