Abstract
This paper develops a novel approach for the falsification of safety properties given by a syntactically safe linear temporal logic (LTL) formula \({\phi}\) for hybrid systems with nonlinear dynamics and input controls. When the hybrid system is unsafe, the approach computes a trajectory that indicates violation of \({\phi}\) . The approach is based on an effective combination of model checking and motion planning. Model checking searches on-the-fly the automaton of \({\neg\phi}\) and an abstraction of the hybrid system for a sequence σ of propositional assignments that violates \({\phi}\) . Motion planning incrementally extends trajectories that satisfy more and more of the propositional assignments in σ. Model checking and motion planning regularly exchange information to find increasingly useful sequences σ for extending the current trajectories. Experiments that test LTL safety properties on a robot navigation benchmark modeled as a hybrid system with nonlinear dynamics and input controls demonstrate the computational efficiency of the approach. Experiments also indicate significant speedup when using minimized DFA instead of non-minimized NFA for representing \({\neg\phi}\) .
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Tomlin C.J., Mitchell I., Bayen A., Oishi M.: Computational techniques for the verification and control of hybrid systems. Proc. IEEE 91(7), 986–1001 (2003)
Alur R., Courcoubetis C., Halbwachs N., Henzinger T.A., Ho P.H., Nicollin X., Olivero A., Sifakis J., Yovine S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995)
Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: ACM Symp on Theory of Computing, pp. 373–382 (1995)
Chutinan C., Krogh B.H.: Computational techniques for hybrid system verification. IEEE Trans. Autom. Control 48(1), 64–75 (2003)
Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Hybrid Systems: Computation and Control. LNCS, vol. 4416, pp. 428–443 (2007)
Alur R., Henzinger T.A., Lafferriere G., Pappas G.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)
Clarke E., Fehnker A., Han Z., Krogh B., Ouaknine J., Stursberg O., Theobald M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583–604 (2003)
Giorgetti, N., Pappas, G.J., Bemporad, A.: Bounded model checking for hybrid dynamical systems. In: Conference on Decision and Control, Seville, Spain, pp. 672–677 (2005)
Branicky M.: Universal computation and other capabilities of continuous and hybrid systems. Theor. Comput. Sci. 138(1), 67–100 (1995)
Branicky M.S., Curtiss M.M., Levine J., Morgan S.: Sampling-based planning, control, and verification of hybrid systems. IEE Proc. Control Theory Appl. 153(5), 575–590 (2006)
Bhatia, A., Frazzoli, E.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Hybrid Systems: Computation and Control. LNCS, vol. 2993, pp. 142–156 (2004)
Esposito, J.M., Kim, J., Kumar, V.: Adaptive RRTs for validating hybrid robotic control systems. In: Workshop on Algorithmic Foundations of Robotics, Zeist, Netherlands, pp. 107–132 (2004)
Kim, J., Esposito, J.M., Kumar, V.: An RRT-based algorithm for testing and validating multi-robot controllers. In: Robotics: Science and Systems, Boston, pp. 249–256 (2005)
Nahhal T., Dang T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods Syst. Des. 34(2), 183–213 (2009)
Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification. In: International Conference on Computer Aided Verification. LNCS, vol. 4590, pp. 468–481 (2007)
Plaku E., Kavraki L.E., Vardi M.Y.: Hybrid systems: from verification to falsification by combining motion planning and discrete search. Formal Methods Syst. Des. 34(2), 157–182 (2009)
Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.: Benefits of bounded model checking at an industrial setting. In: International Conference on Computer Aided Verification. LNCS, vol. 2102, pp. 436–453 (2001)
Cheng P., Kumar V.: Sampling-based falsification and verification of controllers for continuous dynamic systems. Int. J. Robot. Res. 27(11–12), 1232–1245 (2008)
Bhatia, A., Frazzoli, E.: Sampling-based resolution-complete safety falsification of linear hybrid systems. In: IEEE Conference on Decision and Control, New Orleans, pp. 3405–3411 (2007)
Bhatia, A., Frazzoli, E.: Sampling-based resolution-complete algorithms for safety falsification of linear systems. In: Hybrid Systems: Computation and Control. LNCS, vol. 4981, pp. 606–609 (2008)
LaValle S.M., Kuffner J.J.: Randomized kinodynamic planning. Int. J. Robot. Res. 20(5), 378–400 (2001)
Clarke E., Grumberg O., Peled D.: Model Checking. MIT Press, Cambridge (1999)
Behrmann, G., David, A., Larsen, K.G., Mller, O., Pettersson, P., Yi, W.: Uppaal—present and future. In: Conference on Decision and Control, Orlando, Florida, pp. 2881–2886 (2001)
Fainekos G.E., Girard A., Kress-Gazit H., Pappas G.J.: Temporal logic motion planning for dynamic mobile robots. Automatica 45(2), 343–352 (2009)
Fainekos, G.E., Kress-Gazit, H., Pappas, G.: Temporal logic motion planning for mobile robots. In: IEEE International Conference on Robotics and Automation, Barcelona, Spain, pp. 2020–2025 (2005)
Kloetzer M., Belta C.: A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans. Autom. Control 53(1), 287–297 (2008)
Kress-Gazit H., Fainekos G., Pappas G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robot. 25(6), 1370–1381 (2009)
Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning for dynamical systems. In: IEEE Conference on Decision and Control, Shanghai, China, pp. 5997–6004 (2009)
Kloetzer M., Belta C.: Temporal logic planning and control of robotic swarms by hierarchical abstractions. IEEE Trans. Robot. 23(2), 320–331 (2007)
Batt G., Belta C., Weiss R.: Temporal logic analysis of gene networks under parameter uncertainty. IEEE Trans. Autom. Control 53, 215–229 (2008)
Damm W., Pinto G., Ratschan S.: Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. Int. J. Found. Comput. Sci. 18(1), 63–86 (2007)
Kupferman O., Vardi M.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001)
Sistla A.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6, 495–511 (1994)
Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Hybrid Systems: Computation and Control. LNCS, vol. 2993, pp. 326–341 (2004)
Armoni, R., Egorov, S., Fraer, R., Korchemny, D., Vardi, M.: Efficient LTL compilation for SAT-based model checking. In: International Conference on Computer-Aided Design, San Jose, pp. 877–884 (2005)
Alpern B., Schneider F.: Recognizing safety and liveness. Distrib. Comput. 2, 117–126 (1987)
Choset H., Lynch K.M., Hutchinson S., Kantor G., Burgard W., Kavraki L.E., Thrun S.: Principles of Robot Motion: Theory, Algorithms, and Implementations. MIT Press, Cambridge (2005)
LaValle S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)
Esposito, J., Kumar, V., Pappas, G.: Accurate event detection for simulation of hybrid systems. In: Hybrid Systems: Computation and Control. LNCS, pp. 204–217 (2001)
Julius, A.A., Fainekos, G.E., Anand, M., Lee, I., Pappas, G.J.: Robust test generation and coverage for hybrid systems. In: Hybrid Systems: Computation and Control. LNCS, vol. 4416, pp. 329–342 (2007)
Plaku, E., Kavraki, L.E., Vardi, M.Y.: Discrete search leading continuous exploration for kinodynamic motion planning. In: Robotics: Science and Systems, Atlanta, Georgia, pp. 326–333 (2007)
Latvala, T.: Efficient model checking of safety properties. In Ball, T., Rajamani, S., (eds.) Model Checking Software. LNCS, vol. 2648, pp. 74–88 (2003)
Ladd, A.M.: Motion planning for physical simulation. PhD thesis, Rice University, Houston (2006)
Author information
Authors and Affiliations
Corresponding author
Additional information
A preliminary version of this work appeared in the Intl Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), LNCS vol. 5505, pp. 368–382.
Rights and permissions
About this article
Cite this article
Plaku, E., Kavraki, L.E. & Vardi, M.Y. Falsification of LTL safety properties in hybrid systems. Int J Softw Tools Technol Transfer 15, 305–320 (2013). https://doi.org/10.1007/s10009-012-0233-2
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-012-0233-2