Synthesis Algorithm of Control Strategy for Multi-Robot Systems with Collaborative Behavior under LTL Specifications
Adrien Rigaud · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2013
In this thesis, we present a formal control strategy synthesis algorithm for multirobot systems subject to both individual specications and collaboration requirements. We work in an environment that has been abstracted into nonoverlapping regions. The specications are expressed in Linear Temporal Logic, constructed over some predicates on the actions performed by the robots. Each collaboration requirement is given as a set of complementary actions which are distributed on the robots and must always be performed at the same time. In order to avoid computing a synchronized product of the robot behaviours we consider extracting a satisfying run for each agent. These runs satisfy the individual specications but a priori do not meet the collaboration requirements since they are picked in an individual manner. We study the conditions under which we can enforce these collaboration constraints (synchronize the robots) without violating the specications. Under the reasonnable assumption that all the regions are connected to each other, we prove that this property only depends on the sequences of actions performed by the robots. We formulate sufcient conditions for the property to hold, and propose a procedure for revising the initial sequences to solve the problem. The main contribution of this thesis is that it addresses the formal control of collaborative robots without computing any product between Transition Systems. In particular it proposes a characterization of deadlocks, resulting in a computational framework for their detection and removal.