Cutting a Parameter Space for a Multi-Legged Robot Based on Model Checking

Abstract

This paper proposes a technique to cut a parameter space in dynamic simulations based on model checking. The design object addressed in this paper is a multi-legged robot which is controlled by a Follow-the-Contact-Point (FCP) gait control. The design parameters are about both the walk controller and the robot construction, but the parameter space is too wide to evaluate by the dynamic simulation. The robot behavior is modelled by timed-automata, and specifications for the robot to successfully walk are described in a computational tree logic (CTL). The proposed method is based on repetition of applying model checking, UPPAAL, to each set of parameters. Its availability is shown by adopting the proposed technique to designing a multi-legged robot.