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


Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu