面向概率ZIA时序及度量性质的检测研究

摘要 带数据约束的概率系统是指一种既带有概率约束，又带有数据变量约束的计算系统，应用非常广泛.对这类系统而言，确保其正确性和可靠性是至关重要的.目前对带数据约束的概率系统模型的规范及验证研究较少，本文提出了一种针对概率系统的带数据约束的规范.对于传统的时序逻辑如计算树逻辑和概率计算树逻辑来说，尽管这些逻辑很强大，但是只能反映系统的时序性质，为了解决这些局限性，本文提出一个新的形式化语言来表达度量性质查询，同时保留表达时序性质的能力.最后，文章给出针对概率系统度量性质的检测算法并通过实例说明本文提出的方法可行有效