Delta-Complete Reachability Analysis (Part 1)

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 2013
Accession Number
ADA600179

Entities

People

  • Edmund M. Clarke
  • Sicun Gao
  • Soonho Kong

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Automata
  • Coding
  • Computer Science
  • Differential Equations
  • Hybrid Systems
  • Notation
  • Numbers
  • Perturbations
  • Polynomials
  • Rational Numbers
  • Real Numbers
  • Standards
  • Switches
  • Time Domain
  • Trajectories
  • Verification

Fields of Study

  • Computer science

Readers

  • Linear Algebra
  • Mathematical Modeling and Probability Theory.