Chains of Integrators as a Benchmark for Scalability of Hybrid Control Synthesis
Scott C. Livingston, Vasumathi Raman · EPiC series in computing · 2018
Formal methods refers broadly to techniques for the verification and automatic synthesis of transition systems that satisfy desirable properties exactly or within some statistical tolerance. Though historically developed for concurrent software, recent work has brought these methods to bear on motion planning in robotics. Challenges specific to robotics, such as uncertainty and real-time constraints, have motivated extensions to existing methods and entirely novel treatments. However, compared to other areas within robotics research, demonstrations of formal methods have been surprisingly small-scale. The proposed benchmark seeks to motivate advancement of the state of the art toward practical realization by testing scalability of existing tools, and motivating improvements.