Workflow Nets for Multiagent Cooperation

We present a formal framework for robotic cooperation in which we use an extension to Petri nets, known as workflow nets, to establish a protocol among mobile agents based on the task coverage they maintain. Our choice is motivated by the fact that Petri nets handle concurrency and that goal reachability, or soundness, can be theoretically established. In particular, we define a mathematical cooperation operator which turns cooperation problems expressed as workflow nets into algebraic representations. While we do not address the problem of efficiency, we formally demonstrate that this framework guarantees soundness, or goal reachability, using workflow nets.