Delta-Complete Analysis for Bounded Reachability of Hybrid Systems

Abstract

We present the framework of delta-complete analysis for bounded reachability problems of general hybrid systems. We perform bounded reachability checking through solving delta-decision problems over the reals. The techniques take into account of robustness properties of the systems under numerical perturbations. We prove that the verification problems become much more mathematically tractable in this new framework. Our implementation of the techniques, an open-source tool dReach, scales well on several highly nonlinear hybrid system models that arise in biomedical and robotics applications.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 16, 2014
Accession Number
ADA613813

Entities

People

  • Edmund M. Clarke
  • Sicun Gao
  • Soonho Kong
  • Wei Chen

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Biomedical
  • C4I
  • Human Systems

DTIC Thesaurus Topics

  • Algorithms
  • Automata
  • Coding
  • Computations
  • Computer Science
  • Differential Equations
  • Hybrid Systems
  • Language
  • Nonlinear Dynamics
  • Nonlinear Systems
  • Numbers
  • Perturbations
  • Prostate Cancer
  • Rational Numbers
  • Real Numbers
  • Time Domain
  • Verification

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Software Engineering.

Technology Areas

  • AI & ML
  • AI & ML - Machine Learning Algorithms
  • Autonomy
  • Autonomy - Autonomous System Control
  • Biotechnology