Correct Software Synthesis for Stable Speed-Controlled Robotic Walking

Abstract

We present a software synthesis method for speed- controlled robot walking based on supervisory control of a context-free Motion Grammar. First, we use Human-Inspired control to identify parameters for fixed speed walking and for transitions between fixed speeds, guaranteeing dynamic stability. Next, we build a Motion Grammar representing the discrete- time control for this set of speeds. Then, we synthesize C code from this grammar and generate supervisors¹ online to achieve desired walking speeds, guaranteeing correctness of discrete computation. Finally, we demonstrate this approach on the Aldebaran NAO, showing stable walking transitions with dynamically selected speeds.