Towards Coordination and Control of Multi-robot Systems

摘要

This thesis focuses on control and coordination of mobile multi-robot systems (MRS). In recent years there has been an increasing interest in systems comprised of several autonomous mobile robots. MRS can often deal with tasks that are difficult, if not impossible, to be accomplished by a single robot. In the context of MRS, 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. Temporal logics provide a formal requirement specification mechanism with the capability to define desired behaviors quantitatively due to its similarity to natural languages. 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 multimodal hybrid automata. A finite bisimilar quotient for each of the robots in the network is computed by forming a partition of the environment. Constructing a timed automaton, one for each robot in the network, from the finite bisimilar quotient 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 formulated in Computational Tree Logic (CTL) for a network of multimodal robots. The result is a set of motion plans for the robots which satisfy the requirement specification. Framework II A framework for controller synthesis for a single robot, modeled as a nonlinear system with respect to requirement specification in Linear-time Temporal Logic (LTL) is presented. Dynamic feed-