Hybrid systems: From verification to falsification by combining motion planning and discrete search

DOI10.1007/s10703-008-0058-5zbMath1192.68692OpenAlexW1968254796MaRDI QIDQ1039839

Lydia E. Kavraki, Erion Plaku, Moshe Y. Vardi

Publication date: 23 November 2009

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.300.2339

zbMATH Keywords

decompositionnonlinear dynamicshybrid systemsafety propertiesrobot motion planningdiscrete searchsampling-based planning

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Artificial intelligence for robotics (68T40)

Related Items

Motion Planning Under Uncertainty with Complex Agents and Environments via Hybrid Search, OURS: over- and under-approximating reachable sets for analytic time-invariant differential equations, Temporally and spatially flexible plan execution for dynamic hybrid systems, Quantifier-free encoding of invariants for hybrid systems, Factorization of saddle-point matrices in dynamical systems optimization -- reusing pivots, Safety preserving control synthesis for sampled data systems, Falsification of LTL Safety Properties in Hybrid Systems, Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers, Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties

Uses Software

• Kronos
• HyTech
• RSOLVER
• Benchmarks
• Uppaal
• GSL
• HSolver
• d/dt

Cites Work

• On the shortest spanning subtree of a graph and the traveling salesman problem
• The algorithmic analysis of hybrid systems
• Symbolic model checking: \(10^{20}\) states and beyond
• HyTech: A model checker for hybrid systems
• Kronos: A verification tool for real-time systems
• Counterexample-guided predicate abstraction of hybrid systems
• Robust Test Generation and Coverage for Hybrid Systems
• Comparing Forward and Backward Reachability as Tools for Safety Analysis
• Conflict resolution for air traffic management: a study in multiagent hybrid systems
• Computational techniques for hybrid system verification
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Test Coverage for Continuous and Hybrid Systems
• Hybrid Systems: From Verification to Falsification
• Planning Algorithms
• Computer Aided Verification
• Model Checking Software
• Bounded model checking using satisfiability solving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item