Petri net based multi-robot task coordination from temporal logic specifications

We propose a methodology for enforcing a set of coordination rules onto a multi-robot system, based on the use of Petri nets to model the team of robots, safe linear temporal logic to specify a set of coordination rules to be enforced, and supervisory control theory to synthesise a supervisor that enforces the coordination rules. We introduce a composition algorithm that allows us to build a Petri net that represents the largest restriction of the team behaviour that still satisfies the specification. Such a Petri net can be interpreted as a candidate for a supervisor, for which one needs to verify admissibility. We present a general verification procedure for this problem. We also present a syntactic restriction to safe linear temporal logic that guarantees admissibility of the composition a priori. We finish by providing an illustrative example, where we show how the use of temporal logic allows the designer to write the specifications intuitively, and the use of Petri nets allows us to tackle the large state spaces and high concurrency associated with multi-robot systems. (C) 2019 Elsevier B.V. All rights reserved.