|
CMU-CS-13-131
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-13-131
Delta-complete reachability Analysis (Part I)
Sicun Gao, Soonho Kong, Edmund M. Clarke
December 2013
CMU-CS-13-131.pdf
Keywords:
Hybrid Systems, Reachability, Bounded Model Checking
We give a new framework for safety verification of nonlinear hybrid systems, based on delta-decidability of first-order logic formulas over the real numbers. We use expressive logic formulas (which can contain nonlinear ODEs with no analytic solutions) to encode bounded model checking and invariant-based reasoning. Based on the encoding, we solve bounded reachability and invariant validation problems using delta-complete decision procedures. Such techniques allow us to take
into account of robustness properties of a system under delta-bounded numerical perturbations. This report describes Part I of the work, focusing on basic definitions and bounded reachability problems.
16 pages
|