Timed automata based motion planning for a self-assembly robot system

Sambot is a module robot system, with the advantages of self-assembly. A target robotic configuration can be organized by a group of Sambots. A novel motion planning method for Sambot configuration using model checking is presented in this paper. This hierarchical method contains two layers. The abstract logic layer is responsible for the discrete planning of Sambots configuration. The robot and the environment are all modeled as timed automata. System requirements are formalized as Computational Tree Logic (CTL) formulas. Model checking is applied on the system model. The verification result gives the optimal discrete plans for the configuration of Sambot. In physical layer, a sample-based planner generates the trajectory trace considering the dynamics of Sambot and the suggested high level plans. The experiment results illustrate the effectiveness of our approach.