Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems
Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems
复制标题
DOI：
10.1007/978-3-319-19249-9_32
复制
发表时间：
2015-06
期刊：
影响因子：
--
通讯作者：
A. Sogokon;Paul B. Jackson
中科院分区：
文献类型：
--
作者：
A. Sogokon;Paul B. Jackson
本文研究约束条件下多项式常微分方程系统偶发性（一种活性）时间性质的证明方法。这个问题是一个更普遍的兴趣混合系统验证，推理的时间属性的连续片段往往是一个瓶颈。在处理连续系统的困难很大程度上源于这样一个事实，即封闭形式的解决方案，非线性常微分方程是很少可用的。我们提出了一种证明偶然性性质的通用方法，该方法直接适用于微分方程，而无需计算其解。我们的方法直观上是简单的，但比以前报道的方法保守得多，使其非常适合作为一个规则的推理，在一个正式的证明演算的混合动力系统。
This paper is concerned with proof methods for the temporal property of eventuality (a type of liveness) in systems of polynomial ordinary differential equations (ODEs) evolving under constraints. This problem is of a more general interest to hybrid system verification, where reasoning about temporal properties in the continuous fragment is often a bottleneck. Much of the difficulty in handling continuous systems stems from the fact that closed-form solutions to non-linear ODEs are rarely available. We present a general method for proving eventuality properties that works with the differential equations directly, without the need to compute their solutions. Our method is intuitively simple, yet much less conservative than previously reported approaches, making it highly amenable to use as a rule of inference in a formal proof calculus for hybrid systems.