LTL-based decentralized supervisory control of multi-robot tasks modelled as petri nets

We present a decentralized methodology to control multi-robot systems, where each robot behaviour is modelled as a Petri net (PN) and a set of coordination rules between the robots is given as linear temporal logic (LTL) formulas describing safety properties for the system. The LTL formulas are used to define the events and changes in state that must be communicated between robots and to augment the individual PN model of each robot so that it can handle the incoming communications. These augmented PNs are then used, in conjunction with the LTL formulas, to build PN realizations of local supervisors, based on discrete event system theory, that enforce the LTL specifications by construction. The methodology is illustrated through a simulated application example.