Abstract
A Rapidly-exploring Random Tree (RRT) is an algorithm which can search a non-convex region of space by incrementally building a space-filling tree. The tree is constructed from random points drawn from system’s state space and is biased to grow towards large unexplored areas in the system. RRT can provide better coverage of a system’s possible behaviors compared with random simulations, but is more lightweight than full reachability analysis. In this paper, we explore some of the design decisions encountered while implementing a hybrid extension of the RRT algorithm, which have not been elaborated on before. In particular, we focus on handling non-determinism, which arises due to discrete transitions. We introduce the notion of important points to account for this phenomena. We showcase our ideas using heater and navigation benchmarks.
DISTRIBUTION A. Approved for public release; Distribution unlimited. (Approval AFRL PA #88ABW-2016-4898, 30 SEP 2016).
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
References
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. Theoret. Comput. Sci. 138(1), 3–34 (1995)
Bak, S., Bogomolov, S., Henzinger, T.A., Johnson, T.T., Prakash, P.: Scalable static hybridization methods for analysis of nonlinear systems. In: 19th International Conference on Hybrid Systems: Computation and Control (HSCC 2016), pp. 155–164. ACM (2016)
Bak, S., Bogomolov, S., Johnson, T.T.: HyST: a source transformation and translation tool for hybrid automaton models. In: 18th International Conference on Hybrid Systems: Computation and Control, Seattle, Washington. ACM, April 2015
Bhatia, A., Frazzoli, E.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 142–156. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24743-2_10
Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., Wehrle, M.: A box-based distance between regions for guiding the reachability analysis of SpaceEx. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 479–494. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_35
Bogomolov, S., Greitschus, M., Jensen, P.G., Larsen, K.G., Mikucionis, M., Strump, T., Tripakis, S.: Co-simulation of hybrid systems with SpaceEx and Uppaal. In: 11th International Modelica Conference (Modelica 2015), Linköping Electronic Conference Proceedings, pp. 159–169. Linköping University Electronic Press, Linköpings universitet (2015)
Bogomolov, S., Mitrohin, C., Podelski, A.: Composing reachability analyses of hybrid systems for safety and stability. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 67–81. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15643-4_7
Cheng, P., LaValle, S.M.: Resolution complete rapidly-exploring random trees. In: ICRA, pp. 267–272. IEEE (2002)
Dang, T., Nahhal, T.: Randomized simulation of hybrid systems for circuit validation. Technical report (2006)
Esposito, J.M., Kim, J., Kumar, V.: Adaptive RRTs for validating hybrid robotic control systems. In: Erdmann, M., Overmars, M., Hsu, D., van der Stappen, F. (eds.) Algorithmic Foundations of Robotics VI, pp. 107–121. Springer, Heidelberg (2005). doi:10.1007/10991541_9
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). doi:10.1007/978-3-540-24743-2_22
Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30
Lavalle, S.M.: Rapidly-exploring random trees: a new tool for path planning. Technical report (1998)
Plaku, E., Kavraki, L., Vardi, M.: Hybrid systems: from verification to falsification by combining motion planning and discrete search. Formal Methods Syst. Des. 34, 157–182 (2009)
Acknowledgment
This work was partly supported by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award) and by the ARC project DP140104219 “Robust AI Planning for Hybrid Systems”.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Bak, S., Bogomolov, S., Henzinger, T.A., Kumar, A. (2017). Challenges and Tool Implementation of Hybrid Rapidly-Exploring Random Trees. In: Abate, A., Boldo, S. (eds) Numerical Software Verification. NSV 2017. Lecture Notes in Computer Science(), vol 10381. Springer, Cham. https://doi.org/10.1007/978-3-319-63501-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-63501-9_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63500-2
Online ISBN: 978-3-319-63501-9
eBook Packages: Computer ScienceComputer Science (R0)