TY - GEN
T1 - Bounded verification with on-the-fly discrepancy computation
AU - Fan, Chuchu
AU - Mitra, Sayan
N1 - Funding Information:
The results presented here came about from work supported and funded by the National Science Foundation (NSF CSR 1016791) and the Air Force Office of Scientific Research (AFOSR YIP FA9550-12-1-0336).
Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - 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 piecewise 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.
AB - 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 piecewise 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.
UR - http://www.scopus.com/inward/record.url?scp=84951861790&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84951861790&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-24953-7_32
DO - 10.1007/978-3-319-24953-7_32
M3 - Conference contribution
AN - SCOPUS:84951861790
SN - 9783319249520
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 446
EP - 463
BT - Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Proceedings
A2 - Finkbeiner, Bernd
A2 - Pu, Geguang
A2 - Zhang, Lijun
PB - Springer
T2 - 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
Y2 - 12 October 2015 through 15 October 2015
ER -