Numerical Simulation guided Lazy Abstraction Refinement for Nonlinear Hybrid Automata

2006/11/13 by Sumit Kumar Jha, Jha, Sumit Kumar
Computer Science · #B.5.2 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.cs/0611051

11 pages, 2 figures

arxiv created 2006/11/13 · arxiv updated 2011/11/09

Abstract

This draft suggests a new counterexample guided abstraction refinement (CEGAR) framework that uses the combination of numerical simulation for nonlinear differential equations with linear programming for linear hybrid automata (LHA) to perform reachability analysis on nonlinear hybrid automata. A notion of ε- structural robustness is also introduced which allows the algorithm to validate counterexamples using numerical simulations. Keywords: verification, model checking, hybrid systems, hybrid automata, robustness, robust hybrid systems, numerical simulation, cegar, abstraction refinement.

Related

• Design of a Distributed Reachability Algorithm for Analysis of Linear Hybrid Automata
• Computing finite abstractions with robustness margins via local reachable set over-approximation
• Bounded Verification with On-the-Fly Discrepancy Computation
• On verification and constraint generation for families of similar hybrid automata
• Computing Flowpipe of Nonlinear Hybrid Systems with Numerical Methods