中文摘要：

概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性。本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证。通过2个实例说明检测过程的有效性和高效性。

英文摘要：

Probabilistic timed automata are an extension of timed automata with discrete transition probabilities,and can be used to model timed randomized protocols or fault-tolerant systems. We present a bounded model checking method on SMT for verifying probabilistic timed automata against PTACTL properties. This method adds the transition times and transition probabilities into the ACTL properties and changes the encodings of models and properties in order to verify them,which is come from the SMT-based bounded model checking. We also give two examples to show that this method is effectiveness and efficiency.