An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems
An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems
复制标题
DOI：
10.1007/s10009-011-0193-y
复制
发表时间：
2011-10
影响因子：
1.5
通讯作者：
Daisuke Ishii;K. Ueda;H. Hosobe
中科院分区：
文献类型：
--
作者：
Daisuke Ishii;K. Ueda;H. Hosobe
本文提出了一种用于混杂系统的有界模型检验工具。该方法将非线性混合系统的可达性问题转化为一个包含算术约束的谓词逻辑公式，并基于可满足性模理论方法对该公式进行可满足性检验。我们紧密集成（i）增量SAT求解器枚举可能的约束集和（ii）基于区间的求解器的混合约束系统（HCS），以解决公式中描述的约束。HCS求解器通过使用一组框来包围可能导致离散更改的连续状态，来验证离散更改的发生。我们利用HCS求解器计算的盒子中唯一解的存在性作为（i）模型可达性的证明和（ii）过近似细化过程的指导。我们的实现成功地处理了几个例子，包括那些非线性约束。
This paper presents a bounded model checking tool calledfor hybrid systems. It translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints and checks the satisfiability of the formula based on a satisfiability modulo theories method. We tightly integrate (i) an incremental SAT solver to enumerate the possible sets of constraints and (ii) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas. The HCS solver verifies the occurrence of a discrete change by using a set of boxes to enclose continuous states that may cause the discrete change. We utilize the existence property of a unique solution in the boxes computed by the HCS solver as (i) a proof of the reachability of a model and (ii) a guide in the over-approximation refinement procedure. Ourimplementation successfully handled several examples including those with nonlinear constraints.