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

Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Research output: Contribution to journalArticle

    21 Citations (Scopus)

    Abstract

    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.

    Original languageEnglish
    Pages (from-to)449-461
    Number of pages13
    JournalInternational Journal on Software Tools for Technology Transfer
    Volume13
    Issue number5
    DOIs
    Publication statusPublished - 2011 Oct

    Fingerprint

    Model checking
    Hybrid systems

    Keywords

    • Bounded model checking
    • Interval analysis
    • Nonlinear hybrid systems
    • Satisfiability modulo theories

    ASJC Scopus subject areas

    • Software
    • Information Systems

    Cite this

    An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems. / Ishii, Daisuke; Ueda, Kazunori; Hosobe, Hiroshi.

    In: International Journal on Software Tools for Technology Transfer, Vol. 13, No. 5, 10.2011, p. 449-461.

    Research output: Contribution to journalArticle

    @article{bd3e93fdf9d24d74a68b0daa52f0c885,
    title = "An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems",
    abstract = "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.",
    keywords = "Bounded model checking, Interval analysis, Nonlinear hybrid systems, Satisfiability modulo theories",
    author = "Daisuke Ishii and Kazunori Ueda and Hiroshi Hosobe",
    year = "2011",
    month = "10",
    doi = "10.1007/s10009-011-0193-y",
    language = "English",
    volume = "13",
    pages = "449--461",
    journal = "International Journal on Software Tools for Technology Transfer",
    issn = "1433-2779",
    publisher = "Springer Verlag",
    number = "5",

    }

    TY - JOUR

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

    AU - Ishii, Daisuke

    AU - Ueda, Kazunori

    AU - Hosobe, Hiroshi

    PY - 2011/10

    Y1 - 2011/10

    N2 - 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.

    AB - 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.

    KW - Bounded model checking

    KW - Interval analysis

    KW - Nonlinear hybrid systems

    KW - Satisfiability modulo theories

    UR - http://www.scopus.com/inward/record.url?scp=80052532801&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=80052532801&partnerID=8YFLogxK

    U2 - 10.1007/s10009-011-0193-y

    DO - 10.1007/s10009-011-0193-y

    M3 - Article

    AN - SCOPUS:80052532801

    VL - 13

    SP - 449

    EP - 461

    JO - International Journal on Software Tools for Technology Transfer

    JF - International Journal on Software Tools for Technology Transfer

    SN - 1433-2779

    IS - 5

    ER -