论文标题
通过降低模型验证具有时间逻辑规格的随机混合系统
Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction
论文作者
论文摘要
我们提出了一种可扩展的方法来验证随机混合系统。使用Mori-Zwanzig减少方法，我们构建了一个有限的Markov链减少给定的随机混合系统，并证明该简化的Markov链在分布意义上大致相当于原始系统。随机混合系统及其马尔可夫链还原的近似等效性意味着分析马尔可夫链相对于适当增强的性质，使我们能够得出结论原始的随机混合系统是否符合其时间逻辑规格。我们提出了第一个统计模型检查算法，以验证在线性不等式线性时间逻辑（ILTL）或公表示时间间隔时间逻辑（MITL）中表达的正确性特性的随机混合系统。
We present a scalable methodology to verify stochastic hybrid systems. Using the Mori-Zwanzig reduction method, we construct a finite state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduction means that analyzing the Markov chain with respect to a suitably strengthened property, allows us to conclude whether the original stochastic hybrid system meets its temporal logic specifications. We present the first statistical model checking algorithms to verify stochastic hybrid systems against correctness properties, expressed in the linear inequality linear temporal logic (iLTL) or the metric interval temporal logic (MITL).
