Bounded verification with on-the-fly discrepancy computation

DOI10.1007/978-3-319-24953-7_32MaRDI QIDQ3460584zbMATH OpenOpenAlexFDO

Authors Chuchu Fan, Sayan Mitra

Publication date 8 January 2016

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1502.01801

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Simulation-based verification algorithms can provide formal safety guarantees for nonlinear and hybrid systems. The previous algorithms rely on user provided model annotations called discrepancy function, which are crucial for computing reachtubes from simulations. In this paper, we eliminate this requirement by presenting an algorithm for computing piece-wise exponential discrepancy functions. The algorithm relies on computing local convergence or divergence rates of trajectories along a simulation using a coarse over-approximation of the reach set and bounding the maximal eigenvalue of the Jacobian over this over-approximation. The resulting discrepancy function preserves the soundness and the relative completeness of the verification algorithm. We also provide a coordinate transformation method to improve the local estimates for the convergence or divergence rates in practical examples. We extend the method to get the input-to-state discrepancy of nonlinear dynamical systems which can be used for compositional analysis. Our experiments show that the approach is effective in terms of running time for several benchmark problems, scales reasonably to larger dimensional systems, and compares favorably with respect to available tools for nonlinear models.

Recommendations

• Proofs from simulations and modular annotations
• Bounded and Unbounded Safety Verification Using Bisimulation Metrics
• Bounded invariant verification for time-delayed nonlinear networked dynamical systems
• Computing bounded reach sets from sampled simulation traces
• Hybrid Systems: Computation and Control

Cited in

(8)

• Approximate partial order reduction
• Bounded invariant verification for time-delayed nonlinear networked dynamical systems
• Proofs from simulations and modular annotations
• Using symmetry transformations in equivariant dynamical systems for their safety verification
• Bounded and Unbounded Safety Verification Using Bisimulation Metrics
• Multi-agent safety verification using symmetry transformations
• Robustness analysis of continuous-depth models with Lagrangian techniques
• Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems

This page was built for publication: Bounded verification with on-the-fly discrepancy computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460584)