Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods
Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods
复制标题
通过结合不同的封装方法改进混合系统分析的 SAT 模 ODE
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
M. Fränzle
中科院分区：
文献类型：
--
作者：
Andreas Eggers;N. Ramdani;N. Nedialkov;M. Fränzle
针对混杂系统的自动验证与分析技术，提出了一种新的常微分方程组封闭方法与大型布尔组合算术约束的ISAT求解器相结合的方法。在前人工作的基础上，本文的贡献在于将ISAT和VNODE-LP结合起来，作为一种最先进的常微分方程组的封闭方法，并与利用单调性来寻找封闭系统的括号系统相结合，以解决仅靠VNODE-LP无法紧密封闭的问题。我们将我们的方法应用到非线性混合系统的分析中，通过求解归纳稳定性论证的预测编码，并评估了不同方法及其组合的影响。
Aiming at automatic verification and analysis techniques for hybrid systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art enclosure method for ODEs, and with bracketing systems which exploit monotonicity properties to find enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply our method to the analysis of a non-linear hybrid system by solving predicative encodings of an inductive stability argument and evaluate the impact of different methods and their combination.