AI helps you reading Science
AI generates interpretation videos
AI extracts and analyses the key points of the paper to generate videos automatically
Go Generating
AI Traceability
AI parses the academic lineage of this thesis
AI Insight
AI extracts a summary of this paper
Weibo:
Incremental Search Methods For Reachability Analysis Of Continuous And Hybrid Systems
HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, (2004): 142-156
EI
Keywords
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; h...More
Code:
Data:
Introduction
- Hybrid systems, which combine discrete and continuous dynamics, provide sophisticated mathematical models being used in robotics, automated highway systems, air-traffic management, computational biology, and other areas [1, 2].
- To handle more complex hybrid systems, alternative methods [9,10,11,12,13] have been proposed that shift from verification to falsification, which is often the focus of model checking in industrial applications [14]
- Even though they are unable to determine that a system is safe, these methods may compute witness trajectories when the system is not safe.
- The authors recently proposed the Hybrid Discrete Continuous Exploration (HyDICE) falsification method [12, 13], which takes advantage of motion planning, but shows significant speedup over related work [10, 11]
Highlights
- Hybrid systems, which combine discrete and continuous dynamics, provide sophisticated mathematical models being used in robotics, automated highway systems, air-traffic management, computational biology, and other areas [1, 2]
- We recently proposed the Hybrid Discrete Continuous Exploration (HyDICE) falsification method [12, 13], which takes advantage of motion planning, but shows significant speedup over related work [10, 11]
- The experiments provide an initial validation of TemporalHyDICE for the falsification of safety properties expressed by syntactically safe linear temporal logic formulas for hybrid systems with nonlinear dynamics
- This paper studies the impact of A (NFA or DFA) on the efficiency of TemporalHyDICE
- This work developed a novel method, TemporalHyDICE, for the falsification of safety properties specified by syntactically safe linear temporal logic formulas for hybrid systems with general nonlinear dynamics
- By effectively combining model checking and motion planning, when a hybrid system is unsafe, TemporalHyDICE may compute a witness trajectory that indicates a violation of the safety property
Results
- The experiments provide an initial validation of TemporalHyDICE for the falsification of safety properties expressed by syntactically safe LTL formulas for hybrid systems with nonlinear dynamics.
- The experiments demonstrate the importance of model checking and the discrete transition model in the computational efficiency of TemporalHyDICE.
- Second-order dynamics for modeling cars, differential drives, and unicycles are associated with each mode.
- When Guardqi,qj is satisfied, a discrete transition occurs.
- While TemporalHyDICE solved all problem instances, RRT[LTL-TSF]
Conclusion
- This work developed a novel method, TemporalHyDICE, for the falsification of safety properties specified by syntactically safe LTL formulas for hybrid systems with general nonlinear dynamics.
- As the authors consider more complex safety properties and high-dimensional continuous systems, it becomes important to further improve the synergistic combination of model checking and motion planning.
- Another direction is to extend the theory developed in [31], which showed probabilistic completeness for reachability analysis in a continuous setting for a motion planner, and show probabilistic completeness for TemporalHyDICE
Tables
- Table1: Reported is the average time in seconds to solve 100 problem instances for each of the LTL formulas. Times for TemporalHyDICE include the construction of M, which took < 1s. Entries marked with X indicate a timeout (set to 400s). b) compares TemporalHyDICE when using NFAs computed by standard tools (scheck [30]), minimal NFAs constructed by hand, or minimal DFAs (scheck -d [30]) for each ¬φn2 . These experiments are motivated by the work in [<a class="ref-link" id="c22" href="#r22">22</a>], which shows significant speedup when using DFAs instead of NFAs in the context of model checking. As shown in Table 1(b), TemporalHyDICE is only slightly faster when using minimal NFAs instead of minimal DFAs, even though the minimal NFAs had significantly fewer states. As concluded in [<a class="ref-link" id="c22" href="#r22">22</a>], DFAs
Funding
- This work is supported by NSF CNS 0615328 (EP, LK, MV), a Sloan Fellowship (LK), and NSFCCF0613889(MV)
- Equipment is supported by NSFCNS0454333 and NSF CNS 0421109 in partnership with Rice University, AMD, and Cray
Reference
- Tomlin, C.J., Mitchell, I., Bayen, A., Oishi, M.: Computational techniques for the verification and control of hybrid systems. Proc of IEEE 91(7) (2003) 986–1001
- Alur, R., Belta, C., Ivancic, F.: Hybrid modeling and simulation of biomolecular networks. In: Hybrid Systems: Computation & Control. LNCS (2001), 2034:19–32
- 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. Theoretical Computer Science 138(1) (1995) 3–34
- Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: ACM Symp on Theory of Computing. (1995) 373–382
- Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Hybrid Systems Computation & Control. LNCS (2007) 4416:428–443
- Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems. Proc of IEEE 88(7) (2000) 971–984
- 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. Intl J of Foundations of Computer Science 14(4) (2003) 583–604
- Giorgetti, N., Pappas, G.J., Bemporad, A.: Bounded model checking for hybrid dynamical systems. In: Conf on Decision & Control, Seville, Spain (2005) 672–677
- Bhatia, A., Frazzoli, E.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Hybrid Systems: Computation & Control. LNCS (2004) 2993:142–156
- Kim, J., Esposito, J.M., Kumar, V.: An RRT-based algorithm for testing and validating multi-robot controllers. In: Robotics: Science & Systems, Boston, MA (2005) 249–256
- Nahhal, T., Dang, T.: Test coverage for continuous and hybrid systems. In: Intl Conf on Computer Aided Verification. LNCS (2007) 4590:449–462
- Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: From verification to falsification. In: Intl Conf on Computer Aided Verification. LNCS (2007) 4590:468–481
- 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 (2008)
- Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.: Benefits of bounded model checking at an industrial setting. In: Intl Conf on Computer Aided Verification. LNCS (2001) 2102:436–453
- LaValle, S.M., Kuffner, J.J.: Randomized kinodynamic planning. Intl J of Robotics Research 20(5) (2001) 378–400
- Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
- Behrmann, G., David, A., Larsen, K.G., Moller, O., Pettersson, P., Yi, W.: Uppaal present and future. In: Conf on Decision & Control, Orlando, FL (2001) 2881–2886 18. Fainekos, G.E., Kress-Gazit, H., Pappas, G.: Temporal logic motion planning for mobile robots. In: IEEE Intl Conf on Robotics & Automation, Barcelona, Spain (2005) 2020–2025 19.
- Batt, G., Belta, C., Weiss, R.: Temporal logic analysis of gene networks under parameter uncertainty. IEEE Trans of Automatic Control 53 (2008) 215–229 20.
- Damm, W., Pinto, G., Ratschan, S.: Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. Intl J of Foundations of Computer Science 18(1) (2007) 63–86 21.
- Kupferman, O., Vardi, M.: Model checking of safety properties. Formal methods in System Design 19(3) (2001) 291–314 22.
- Armoni, R., Egorov, S., Fraer, R., Korchemny, D., Vardi, M.: Efficient LTL compilation for SAT-based model checking. In: Intl Conf on Computer-Aided Design, San Jose, CA (2005) 877–884 23.
- Sistla, A.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing 6 (1994) 495–511 24.
- 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, MA (2005) 25.
- LaValle, S.M.: Planning Algorithms. Cambridge University Press, MA (2006)
- 26. Esposito, J., Kumar, V., Pappas, G.: Accurate event detection for simulation of hybrid systems. In: Hybrid Systems: Computation&Control. LNCS (2001) 204–217 27. 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 & Control. LNCS (2007) 4416:329–342 28.
- Plaku, E., Kavraki, L.E., Vardi, M.Y.: Discrete search leading continuous exploration for kinodynamic motion planning. In: Robotics: Science & Systems, Atlanta, GA (2007)
- 29. Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Hybrid Systems: Computation & Control. LNCS (2004) 2993:326–341 30. Latvala, T.: Efficient model checking of safety properties. In: Model Checking Software. LNCS (2003) 2648:74–88 31.
- Ladd, A.M.: Motion Planning for Physical Simulation. PhD thesis, Rice University, Houston, TX (2006)
Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn