In this paper, we present a sampling-based verification algorithm for embedded robotic systems with continuous dynamics and uncertainty due to adversaries, unmodeled disturbance inputs, unknown parameters, or initial conditions. The algorithm attempts to find inputs (and resulting trajectories) that falsify the specifications of the system thus providing examples of bad inputs to the system. The system is said to be verified if the algorithm cannot find falsifying inputs. The main contribution of the paper is the analysis of the effects of discretization of the state and input spaces that are inherent to sampling-based techniques. We derive conditions that guarantee resolution completeness. These provide sufficient, although conservative, conditions for verifying Lipschitz continuous (but possibly non-smooth) dynamic systems without known analytical solutions. We analyze the effects of transformations of the input and state space on these conditions. The main results of this paper are illustrated with several simple examples.
Alur, R., Henzinger, T.A., Lafferriere, G. and Pappas, G.J. (2000). Discrete abstractions of hybrid systems. Proceedings of the IEEE, 88(7): 917-984.
2.
Asarin, E., Bournez, O., Dang, T. and Malzer, O. (2000). Approximate reachability analysis of piecewise-linear dynamical systems. Hybrid Systems: Computation and Control. Berlin, Springer.
3.
Barraquand, J. and Latombe, J.-C. (1993). Nonholonomic multibody mobile robots: Controllability and motion planning in the presence of obstacles. Algorithmica , 10: 121- 155.
4.
Bertsekas, D.P. (1975). Convergence in discretization procedures in dynamic programming. IEEE Transactions on Automatic Control, 20(3): 415-419.
Bhatia, A. and Frazzoli, E. (2004). Incremental search methods for reachability analysis of continuous and hybrid systems. Hybrid Systems: Computation and Control , Alur, R. and Pappas, G. J. (eds) (Lecture Notes in Computer Science, Vol. 2993) . Berlin, Springer, pp. 67-78.
7.
Bhatia, A. and Frazzoli, E. (2008). Sampling-based resolution-complete algorithms for safety falsification of linear systems. Hybrid Systems: Computation and ControlEgerstedt, M. and Mishra, B. (eds). Berlin, Springer.
8.
Branicky, M., Curtiss, M., Levine, J. and Morgan, S. (2006). Sampling-based planning, control, and verification of hybrid systems. IEEE Proceedings Control Theory and Applications (accepted).
9.
Cheng, P. (2005). Sampling-based motion planning with differential constraints. Ph.D. Thesis, Urbana, IL, University of Illinois.
10.
Cheng, P., Pappas, G. and Kumar, V. (2007). Decidability of motion planning with differential constraints. Proceedings IEEE International Conference on Robotics and Automation.
11.
Cheng, P., Shen, Z. and LaValle, S.M. (2001). RRT-based trajectory design for autonomous automobiles and spacecraft. Archives of Control Sciences, 11(3-4): 167-194.
12.
Choset, H., Lynch, K.M., Hutchinson, S., Kantor, G., Burgard, W., Kavraki, L.E. and Thrun, S. (2005). Principles of Robot Motion: Theory, Algorithms, and Implementations. Cambridge, MA, MIT Press.
13.
Chutinan, A. and Krogh, B. (2001). Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Transactions on Automatic Control, 46: 1401-1410.
14.
Dang, T. and Nahhal, T. (2006). Randomized simulation of hybrid systems for circuit validation. Proceedings of the Forum on Specification and Design Languages.
15.
Donze, A. and Maler, O. (2007). Systematic simulation using sensitivity analysis. Hybrid Systems: Computation and Control. Berlin, Springer, pp. 174-189.
16.
Esposito, J., Kim, J.W. and Kumar, V. (2004). Adaptive RRTs for validating hybrid robotic control systems. Proceedings of the Workshop on Algorithmic Foundations of Robotics, Zeist, The Netherlands.
17.
Girard, A. (2005). Reachability of uncertain linear systems using zonotopes. Hybrid Systems: Computation and Control. Berlin , Springer.
18.
Girard, A. and Pappas, G. (2006). Verification using simulation. Hybrid Systems: Computation and Control. Berlin, Springer.
19.
Goldberg, K.Y. (1994). Completeness in robot motion planning. Proceedings of the Workshop on Algorithmic Foundations of Robotics . Wellesley, MA, A. K. Peters.
20.
Henzinger, T.A., Kopke, P.W., Puri, A. and Varaiya, P. (1998). What's decidable about hybrid automata? Journal of Computer Systems Science, 57: 94-124.
21.
Hsu, C.S. (1987). Cell-to-Cell Mapping. A Method of Global Analysis of Nonlinear Systems. New York, Springer.
22.
Hsu, D., Kindel, R., Latombe, J.-C. and Rock, S. (2002). Randomized kinodynamic motion planning with moving obstacles. The International Journal of Robotics Research , 21: 233-255.
23.
Hsu, D., Latombe, J.-C. and Motwani, R. (1999). Path planning in expansive configuration spaces . International Journal Computational Geometry and Applications , 4: 495- 512.
24.
Kapinski, J., Krogh, B., Maler, O. and Stursberg, O. (2003). On systematic simulation of open continuous systems. Hybrid Systems: Computation and Control. Berlin, Springer.
25.
Kavraki, L.E., Svestka, P., Latombe, J.-C. and Overmars, M.H. (1996). Probabilistic roadmaps for path planning in high-dimensional configuration spaces. IEEE Transactions on Robotics and Automation , 12(4): 566-580.
26.
Khalil, H.K. (2002). Nonlinear Systems. New York , Macmillan.
27.
Ladd, A.M. and Kavraki, L.E. (2005). Motion planning in the presence of drift, underactuation and discrete system changes. Robotics: Science and Systems , Boston, MA, June.
28.
Lafferriere, G., Pappas, G. and Yovine, S. (1999). A new class of decidable hybrid systems. Hybrid Systems: Computation and Control, Vaandrager, F. and van Schuppen, J. (eds). Berlin, Springer.
29.
LaValle, S.M. (2006). Planning Algorithms. Cambrdige , Cambridge University Press. Available at http://planning.cs.uiuc.edu/.
30.
LaValle, S.M., Branicky, M.S. and Lindemann, S.R. (2004). On the relationship between classical grid search and probabilistic roadmaps. The International Journal of Robotics Research, 23(7/8): 673-692.
31.
LaValle, S.M. and Kuffner, J.J. (2001). Rapidly-exploring random trees: progress and prospects. Algorithmic and Computational Robotics: New Directions, Donald, B. R., Lynch, K. M. and Rus, D. (eds). Wellesley, MA, A. K. Peters, pp. 293-308.
32.
Mitchell, I. and Tomlin, C.J. (2003). Overapproximating reachable sets by Hamilton-Jacobi projections. Journal of Scientific Computation, 19(1): 323-346.
33.
Niederreiter, H. (1992). Random Number Generation and Quasi-Monte-Carlo Methods. Philadelphia, PA, Society for Industrial and Applied Mathematics.
34.
Plaku, E., Kavraki, L.E. and Vardi, M.Y. (2007a). Discrete search leading continuous exploration for kinodynamic motion planning. Robotics: Science and Systems, Atlanta, GA.
35.
Plaku, E., Kavraki, L.E. and Vardi, M.Y. (2007b). Hybrid systems: from verification to falsification . Proceedongs of the International Conference on Computer Aided Verification (CAV), Damm, W. and Hermanns, H. (eds). (Lecture Notes in Computer Science, Vol. 4590). Berlin , Springer, pp. 468- 481.
36.
Prajna, S., Jadbabaie, A. and Pappas, G.J. (2007). A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic Control, 52(8): 1415-1429.
37.
Puri, A., Borkar, V. and Varaiya, P. (1996). Epsilonapproximation of differential inclusions. Hybrid Systems III: Verification and Control, Alur, R., Henzinger, T. A. and Sontag, E. D. (eds) (Lecture Notes in Computer Science, Vol. 1066). Berlin, Springer, pp. 362-376.
38.
Tomlin, C.J., Mitchell, I., Bayen, A. and Oishi, M. (2003). Computational techniques for the verification and control of hybrid systems. Proceedings of the IEEE, 91(7): 986- 1001.
