资 源 简 介
hydlogic translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints, and checks the satisfiability of the formula using a satisfiability modulo theories (SMT) method. We tightly integrate (i) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas and (ii) an incremental
SAT solver to enumerate the possible sets of constraints. The HCS solver verifies an occurrence of a discrete change by enclosing continuous states that may cause the discrete change by a set of boxes.
