An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems

Daisuke Ishii*, Kazunori Ueda, Hiroshi Hosobe

*この研究の対応する著者

研究成果: Article査読

23 被引用数 (Scopus)

抄録

This paper presents a bounded model checking tool called for 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. Our implementation successfully handled several examples including those with nonlinear constraints.

本文言語English
ページ(範囲)449-461
ページ数13
ジャーナルInternational Journal on Software Tools for Technology Transfer
13
5
DOI
出版ステータスPublished - 2011 10月

ASJC Scopus subject areas

  • ソフトウェア
  • 情報システム

フィンガープリント

「An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル