Abstract
In this paper we present algorithms and tools for fast and efficient reachability analysis, applicable to continuous and hybrid systems. Most of the work on reachability analysis and safety verification concentrates on conservative representations of the set of reachable states, and consequently on the generation of safety certificates; however, inability to prove safety with these tools does not necessarily result in a proof of unsafety. In this paper, we propose an alternative approach, which aims at the fast falsification of safety properties; this approach provides the designer with a complementary set of tools to the ones based on conservative analysis, providing additional insight into the characteristics of the system under analysis. Our algorithms are based on algorithms originally proposed for robotic motion planning; the key idea is to incrementally grow a set of feasible trajectories by exploring the state space in an efficient way. The ability of the proposed algorithms to analyze the reachability and safety properties of general continuous and hybrid systems is demonstrated on examples from the literature.
The research leading to this work was supported by the NSF Embedded and Hybrid Systems program, under the direction of Dr. Helen Gill, through grant CCR-0208891 (with Branicky and LaValle). Any opinions, findings, conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the National Science Foundation.
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
Alur, R., Dang, T., Esposito, J., Hur, Y., Ivančić, F., Kumar, V., Lee, I., Mishra, P., Pappas, G.J., Sokolsky, O.: Hierarchical modeling and analysis of embedded systems. Proceedings of the IEEE 91, 11–28 (2003)
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3–34 (1995)
Henzinger, T., Ho, P.H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control 43, 540–554 (1998)
Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool KRONOS. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, Springer, Heidelberg (1996)
Chutinan, A., Krogh, B.H.: Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Hybrid Systems: Computation and Control, Springer, Heidelberg (1999)
Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, p. 202. Springer, Heidelberg (2000)
Alur, R., Dang, T., Ivančić, F.: Reachability analysis of hybrid systems via predicate abstraction. In: Tomlin, C.J., Greenstreet, M.R. (eds.) Hybrid Systems: Computation and Control, pp. 35–48. Springer, Heidelberg (2002)
Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Alur, R., Dang, T., Ivanc̆ić, F.: Counter-example guided predicate abstraction of hybrid systems. In: 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003)
Blondel, V., Tsitsiklis, J.N.: The boundedness of all products of a pair of matrices is undecidable. Systems and Control Letters 41, 135–140 (2000)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proceedings of the 27th ACM Symposium on Theory of Computing (STOC), pp. 373–382 (1995)
Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computation 32, 231–253 (2001)
LaValle, S.M.: Rapidly-exploring random trees: A new tool for path planning. Technical Report 98-11, Iowa State University, Ames, IA (1998)
LaValle, S., Kuffner, J.: Randomized kinodynamic planning. In: Proceedings of the 1999 IEEE International Conference on Robotics and Automation (1999)
Branicky, M.S., Curtiss, M.M., Levine, J., Morgan, S.: Sampling-based planning and control. In: Proceedings of the 12th Yale Workshop on Adaptive and Learning Systems, New Haven, CT (2003)
Reif, J.: Complexity of the mover’s problem and generalizations. In: FOCS, pp. 421–427 (1979)
LaValle, S.M., Branicky, M.S.: On the relationship between classical grid search and probabilistic roadmaps. In: Workshop on the Algorithmic Foundation of Robotics (WAFR), Nice, France (2002)
LaValle, S.M., Branicky, M.S., Lindemann, S.R.: On the relationship between classical grid search and probabilistic roadmaps. International Journal of Robotics Research (2003) (to appear)
Kavraki, L., Svestka, P., Latombe, J., Overmars, M.: Probabilistic roadmaps for path planning in high-dimensional configuration spaces. IEEE Transactions on Robotics and Automation 12, 566–580 (1996)
Hsu, D., Kavraki, L., Latombe, J., Motwani, R., Sorkin, S.: On finding narrow passages with probabilistic roadmap planners. In: Proceedings of the 1998 Workshop on Algorithmic Foundations of Robotics, Houston, TX (March 1998)
Hsu, D., Latombe, J.C., Motwani, R.: Path planning in expansive configuration spaces. Int. J. Comp. Geometry and Applications 9, 495–512 (1999)
Hsu, D., Kindel, J., Latombe, J.C., Rock, S.: Randomized kinodynamic motion planning with moving obstacles. In: Proc. Workshop on Algorithmic Foundations of Robotics (WAFR 2000), Hanover, NH (2000)
Bohlin, R., Kavraki, L.: Path planning using lazy PRM. In: Proceedings of the International Conference on Robotics and Automation, pp. 521–528 (2000)
LaValle, S.M., Kuffner, J.J.: Randomized kinodynamic planning. International Journal of Robotics Research 20, 378–400 (2001)
Cheng, P., LaValle, S.M.: Resolution complete rapidly-exploring random trees. In: Proc. IEEE Int’l Conf. on Robotics and Automation (2002)
Nijmeijer, H., Van der Schaft, A.J.: Nonlinear Dynamical Control Systems. Springer, Heidelberg (1990)
Sastry, S.: Nonlinear Systems: Analysis, Stability, and Control. IAM, vol. 10. Springer, New York (1999)
Barber, C.B., Dobkin, D.P., Huhdanpaa, H.T.: The Quickhull algorithm for convex hulls. ACM Transactions on Mathematical Software (1996)
Aubin, J.P.: A survey on viability theory. SIAM Journal of Control and Optimization 28, 749–789 (1990)
Tomlin, C., Lygeros, J., Sastry, S.: A game theoretic approach to controller design for hybrid systems. Proceedings of the IEEE 88, 949–970 (2000)
Mitchell, I., Tomlin, C.: Level set methods for computation in hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 310–323. Springer, Heidelberg (2000)
Merz, A.W.: The game of two identical cars. Journal of Optimization Theory and Applications 9, 324–343 (1972)
Mitchell, I.: Games of two identical vehicles. SUDAAR 740, Department of Aeronautics and Astronautics, Stanford University, Stanford, CA (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bhatia, A., Frazzoli, E. (2004). Incremental Search Methods for Reachability Analysis of Continuous and Hybrid Systems. In: Alur, R., Pappas, G.J. (eds) Hybrid Systems: Computation and Control. HSCC 2004. Lecture Notes in Computer Science, vol 2993. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24743-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-24743-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21259-1
Online ISBN: 978-3-540-24743-2
eBook Packages: Springer Book Archive