# Petri Net Toolbox for Multi-Robot Planning under Uncertainty
## 1 Introduction  
Although the use of multi-robot systems has proven successful in a wide range of real life applications, coordinating these systems at mission-level is still challenging in a number of scenarios. Scientific competitions such as the DARPA subterranean challenge [1] and RoboCup [2, 3] reflect the necessity of progress in this field. Despite the recent advances [4, 5], a considerable amount of behaviors exhibited in these applications still achieve autonomy through hand-crafted rule-based plans [6, 7] or sub-optimal optimizations [8]. These ad-hoc approaches require that a significant engineering effort is placed in every new scenario without even providing any type of formal guarantee on the deployed controllers. Furthermore, as the deployment scale grows, rule-based approaches tend to be harder to define and become more distant from the optimal behavior. In some cases this also leads to many exposed design flaws that have been raising concerns about the safety and reliability of autonomous systems [9, 10]. So far, the most common approach to tackle this problem is through exhaustive testing. This brute-force approach does not produce results as good as formal methods when comparing aspects such as efficiency, robustness, reliability, safety and predictability [11, 12]. Thus, formal methods for synthesizing plans for autonomous systems, have proven to be a successful approach to tackle these concerns. However, the lack of developer-friendly software tools that implement these methods is hindering their adoption. In this work, we introduce a software toolbox that allows: modeling multi-robot systems taking into account time uncertainty; obtaining coordination strategies that guarantee optimality; and executing these strategies in the Robot Operating System (ROS) environment. Theproposed software provides methods that capture system constraints by design, provide algorithms to analyze the obtained plans before execution, and execute them in real robots. Despite the existence of software tools and libraries to model, extract optimal policies and coordinate the execution of multi-robot systems, they were developed and implemented separately and are not interoperable. Moreover, none of them assembles in the same tool the capability of capturing stochastic behavior along with methods to synthesize and execute optimal policies that take into account such uncertainty. PRISM [13] and STORM [14] are open source probabilistic model checkers, that support discrete and continuous time Markov chains, Markov decision processes (MDPs) and generalized stochastic petri nets (GSPNRs). Both these tools allow model analysis, providing reachability properties, conditional probabilities and cost queries, long-run average values, cost-bounded properties and multi-objective queries. However, they are not built specifically for robotic systems and do not allow policy execution. Similarly to PRISM and STORM, Pipe [15] and GreatSPN [16] allow the modeling of Petri nets and provide multiple analysis algorithms that yield logic and performance properties. Moreover, it provides a user-friendly graphical interface to build such models, which reduces the entry barrier for first users and facilitates the modeling step. Still, it does not provide policy synthesis methods neither robot coordination capabilities, through policy execution. Robot coordination under ROS middleware is usually achieved using SMACH [17]. SMACH provides an approach based on nested state machines that has proven effective at building and executing task plans with real robots. Though one of the reasons for the popularity of SMACH is its simplicity, making it restrictive in many applications. Thus SMACH does not provide elements to model uncertainty and stochastic effects that are often present in real robot tasks. Furthermore, it is not able to choose from alternative set of actions, that is a necessary feature to produce policies for the designed models. Finally, Petri Net Plans [18] is the software tool closest to the one proposed in this work.