Abstract
In this paper we solve the problem of finding a trajectory that shows that a given hybrid dynamical system with deterministic evolution leaves a given set of states considered to be safe. The algorithm combines local with global search for achieving both efficiency and global convergence. In local search, it exploits derivatives for efficient computation. Unlike other methods for falsification of hybrid systems with deterministic evolution, we do not restrict our search to trajectories of a certain bounded length but search for error trajectories of arbitrary length.
This work was supported by the Czech Science Foundation (GAČR) grant number P202/12/J060 with institutional support RVO:67985807.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abbas, H., Fainekos, G.: Linear hybrid system falsification with descent. Technical Report arXiv:1105.1733 (2011)
Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-taLiRo: A tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011)
Ascher, U.M., Mattheij, R.M.M., Russell, R.D.: Numerical Solution of Boundary Value Problems for Ordinary Differential Equations. SIAM (1995)
Bertsekas, D.P.: Network optimization: continuous and discrete models. Athena Scientific Belmont (1998)
Betts, J.T.: Survey of numerical methods for trajectory optimization. Journal of Guidance, Control, and Dynamics 21(2) (1998)
Branicky, M.S., Borkar, V.S., Mitter, S.K.: A unified framework for hybrid control: Model and optimal control theory. IEEE Transactions on Automatic Control 43(1), 31–45 (1998)
Branicky, M.S., Curtiss, M.M., Levine, J., Morgan, S.: Sampling-based planning, control and verification of hybrid systems. IEE Proceedings-Control Theory and Applications 153(5), 575–590 (2006)
Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods in System Design 34(2), 183–213 (2009)
Dijkstra, E.: A note on two problems in connexion with graphs. Numerische Mathematik 1(1), 269–271 (1959)
Dzetkulič, T., Ratschan, S.: Incremental Computation of Succinct Abstractions for Hybrid Systems. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 271–285. Springer, Heidelberg (2011)
Edelkamp, S., Schuppan, V., Bošnački, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on Directed Model Checking. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol. 5348, pp. 65–89. Springer, Heidelberg (2009)
Fehnker, A., Ivančić, F.: Benchmarks for Hybrid Systems Verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)
Gendreau, M., Potvin, J.-Y. (eds.): Handbook of Metaheuristics, 2nd edn. Springer, Heidelberg (2010)
Hiskens, I., Pai, M.: Trajectory sensitivity analysis of hybrid systems. IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications 47(2), 204–220 (2000)
Lamiraux, F., Ferré, E., Vallée, E.: Kinodynamic motion planning: connecting exploration trees using trajectory optimization methods. In: 2004 IEEE International Conference on Robotics and Automation, Proceedings. ICRA 2004, vol. 4, pp. 3987–3992. IEEE (2004)
LaValle, S.M.: Planning Algorithms. Cambridge University Press (2006)
Locatelli, M., Schoen, F.: Global Optimization–Theory, Algorithms, and Applications. SIAM (2013)
Mosterman, P.J.: An overview of hybrid simulation phenomena and their support by simulation packages. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, p. 165. Springer, Heidelberg (1999)
Nghiem, T., Sankaranarayanan, S., Fainekos, G., Ivančić, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, pp. 211–220. ACM, New York (2010)
Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of LTL safety properties in hybrid systems. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 368–382. Springer, Heidelberg (2009)
Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification by combining motion planning and discrete search. Formal Methods in System Design 34(2), 157–182 (2009)
Pohl, I.: Bi-directional search. Machine Intelligence 6, 124–140 (1971)
Ratschan, S., Smaus, J.-G.: Finding errors of hybrid systems by optimising an abstraction-based quality estimate. In: Dubois, C. (ed.) TAP 2009. LNCS, vol. 5668, pp. 153–168. Springer, Heidelberg (2009)
Rios, L.M., Sahinidis, N.V.: Derivative-free optimization: A review of algorithms and comparison of software implementations. Journal of Global Optimization, 1–47 (2012)
Schoen, F.: Two-phase methods for global optimization. In: Pardalos, P., Romeijn, H. (eds.) Handbook of Global Optimization. Nonconvex Optimization and Its Applications, vol. 62, pp. 151–177. Springer, US (2002)
Zutshi, A., Sankaranarayanan, S., Deshmukh, J.V., Kapinski, J.: A trajectory splicing approach to concretizing counterexamples for hybrid systems. In: CDC 2013 (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Kuřátko, J., Ratschan, S. (2014). Combined Global and Local Search for the Falsification of Hybrid Systems. In: Legay, A., Bozga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2014. Lecture Notes in Computer Science, vol 8711. Springer, Cham. https://doi.org/10.1007/978-3-319-10512-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-10512-3_11
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10511-6
Online ISBN: 978-3-319-10512-3
eBook Packages: Computer ScienceComputer Science (R0)