模型检测基于概率时间自动机的反例产生研究

模型检测基于概率系统的反例产生问题,在最近引起人们的关注.已有的工作主要围绕模型检测Markov链的反例产生而开展.基于概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展.关注的是模型检测PTA的反例产生问题.首先通过在PTA上寻找概率之和恰好大于λ的κ条最大概率的路径,并根据这些路径和原PTA构造原PTA的一个子图,从而快速找到违背性质的具有较少证据的反例.然后精化此结果——通过逐条加入上述各条最大概率的路径来精确地计算已加入路径所构成的PTA子图的最大概率.由于考虑到符号状态交集对概率系统的影响,可以得到证据更少的反例.

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 th...