Towards Coordination and Control of Multi-robot Systems

This thesis focuses on control and coordination of mobile multi-robot systems (MRS). MRS can often deal with tasks that are difficult to be accomplished by a single robot. One of the challenges is the need to control, coordinate and synchronize the operation of several robots to perform some specified task. This calls for new strategies and methods which allow the desired system behavior to be specified in a formal and succinct way. Two different frameworks for the coordination and control of MRS have been investigated.

Framework I - A network of robots is modeled as a network of multi-modal hybrid automata. The notion of bisimulations is used to abstract robots in the network. The result is a network of interacting timed automata which allows coordination among the robots and timing constraints to be considered. The model checker UPPAAL is used for formal symbolic model checking against a requirement specification in Computational Tree Logic (CTL) for a network of robots. The result is a set of motion plans for the robots which satisfy the specification.

Framework II - A framework for controller synthesis for a single robot with respect to requirement specification in Linear-time Temporal Logic (LTL) is presented. The notion of bisimulations is used to find an abstraction of the robot. The abstraction is subsequently used for controller synthesis together with the formal specification. Since the abstraction and the original system are bisimilar the discrete controller synthesized for the abstraction will equivalently work for the original system.