Motion planning in multi-robot systems using timed automata

This paper describes how interacting timed automata can be used to model, analyze, and verify motion planning problems for systems with multiple mobile robots. The method assumes an infra-structure of simple unicycle type robots, moving on a planar grid. The motion of the robots, including simple kinematics, is captured in an automata formalism that allows formal composition and symbolic reasoning. The verification software UPPAAL is used to verify specification requirements formulated in computational tree logic (CTL), generating all feasible trajectories that satisfy specifications. The results of the planning are demonstrated in a testbed that allows execution of the planned paths and motion primitives by synchronizing the planning results from UPPAAL with actual robotic vehicles. The planning problem may be modified online by moving obstacles in the physical environment, which causes a re-planning and modified execution.