Towards a Formalization of the Active Corner Method for Collision Avoidance in PVS
summary
Automatic construction of a quantifier‑free explicit safe region for a convex polygon moving along a piecewise planar trajectory, together with a machine‑checkable PVS proof certificate for correctness. Implementation produces Boolean inequalities from corner trajectories via a Python+Senpai pipeline and generates PVS lemmas proving soundness for squares, diamonds and a hexagon so far. Method handles straight‑line piecewise motion, omits rotation and fully parametric trajectories, and aims to emit certificates that independently verify the algorithmic output. active corner method explicit safe region
AI-written summary · about
chapters (15)
- 0:00Active corner method intro
- 1:02Push-button collision avoidance
- 2:25Talk structure overview
- 3:48Safe region representations
- 6:53Active corners proof approach
- 9:20Soundness proof
- 12:07Proof certificates
- 14:59Algebraic proof in PVS
- 17:47PVS lemmas for diamonds
- 19:10Results and future work
- 20:56Acknowledgments
- 21:17Q&A
- 23:23PVS experience
- 25:28Hybrid system potential
- 26:10Parametric trajectory challenges
related talks
57mReal-Time Decision Making in Hybrid Systems
59mOn Human-robot Interactions via Multimodal Intent Modeling and Reachability-based Safety Assurance
14mMultiparty Motion Coordination: From Choreographies to Robotics Programs
04mSafe and Certified Software for Autonomous Mobility
26mPAARL: An Interactive System for Policy-Aware Planning in Autonomous Agents(…)
43mRobot trajectory planning with hybrid quantum algorithms
24mTopological and Algebraic Invariants to Classify Types of Singularities of Maps relevant to...
19mAirways: Optimization-Based Planning of Quadrotor Trajectories according to High-Level User Goals