AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
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

Incremental Search Methods For Reachability Analysis Of Continuous And Hybrid Systems

HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, (2004): 142-156

Cited: 136|Views27
EI

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
Download tables as Excel
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
    Google ScholarLocate open access versionFindings
  • Alur, R., Belta, C., Ivancic, F.: Hybrid modeling and simulation of biomolecular networks. In: Hybrid Systems: Computation & Control. LNCS (2001), 2034:19–32
    Google ScholarLocate open access versionFindings
  • 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
    Google ScholarLocate open access versionFindings
  • Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: ACM Symp on Theory of Computing. (1995) 373–382
    Google ScholarLocate open access versionFindings
  • Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Hybrid Systems Computation & Control. LNCS (2007) 4416:428–443
    Google ScholarLocate open access versionFindings
  • Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems. Proc of IEEE 88(7) (2000) 971–984
    Google ScholarLocate open access versionFindings
  • 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
    Google ScholarLocate open access versionFindings
  • Giorgetti, N., Pappas, G.J., Bemporad, A.: Bounded model checking for hybrid dynamical systems. In: Conf on Decision & Control, Seville, Spain (2005) 672–677
    Google ScholarLocate open access versionFindings
  • 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
    Google ScholarLocate open access versionFindings
  • 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
    Google ScholarFindings
  • Nahhal, T., Dang, T.: Test coverage for continuous and hybrid systems. In: Intl Conf on Computer Aided Verification. LNCS (2007) 4590:449–462
    Google ScholarLocate open access versionFindings
  • 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
    Google ScholarLocate open access versionFindings
  • 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)
    Google ScholarLocate open access versionFindings
  • 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
    Google ScholarLocate open access versionFindings
  • LaValle, S.M., Kuffner, J.J.: Randomized kinodynamic planning. Intl J of Robotics Research 20(5) (2001) 378–400
    Google ScholarLocate open access versionFindings
  • Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Kupferman, O., Vardi, M.: Model checking of safety properties. Formal methods in System Design 19(3) (2001) 291–314 22.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Sistla, A.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing 6 (1994) 495–511 24.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • LaValle, S.M.: Planning Algorithms. Cambridge University Press, MA (2006)
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Plaku, E., Kavraki, L.E., Vardi, M.Y.: Discrete search leading continuous exploration for kinodynamic motion planning. In: Robotics: Science & Systems, Atlanta, GA (2007)
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Ladd, A.M.: Motion Planning for Physical Simulation. PhD thesis, Rice University, Houston, TX (2006)
    Google ScholarFindings
0
Your rating :

No Ratings

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn