In this paper we propose an automated method for planning a team of mobile robots such that a Boolean-based mission is accomplished. The task consists of logical requirements over some regions of interest for the agents' trajectories and for their final states. In other words, we allow combinatorial specifications defining desired final states whose attainment includes visits to, avoidance of, and ending in certain regions. The path planning approach should select such final states that optimize a certain global cost function. In particular, we consider minimum expected traveling distance of the team and reduce congestions. A Petri net (PN) with outputs models the movement capabilities of the team and the regions of interest. The imposed specification is translated to a set of linear restrictions for some binary variables, the robot movement capabilities are formulated as linear constraints on PN markings, and the evaluations of the binary variables are linked with PN markings via linear inequalities. This allows us to solve an Integer Linear Programming problem whose solution yields robotic trajectories satisfying the task.

In this paper, we develop an automated framework for formal verification of timed continuous Petri nets (ContPNs). Specifically, we consider two problems: (1) given an initial set of markings, construct a set of unreachable markings and (2) given a Linear Temporal Logic (LTL) formula over a set of linear predicates in the marking space, construct a set of initial states such that all trajectories originating there satisfy the LTL specification. The starting point for our approach is the observation that a ContPN system can be expressed as a Piecewise Affine (PWA) system with a polyhedral partition. We propose an iterative method for analysis of PWA systems from specifications given as LTL formulas over linear predicates. The computation mainly consists of polyhedral operations and searches on graphs, and the developed framework was implemented as a freely downloadable software tool. We present several illustrative numerical examples.

This paper proposes a method exploiting the advantages of Petri net (PN) and Büchi automata models, by joining them in a newly defined Composed Petri net representation. Based on the latter model, collision-free trajectories are computed for a team of robots. The path planning algorithm is divided into two steps: computing a solution in a reduced PN model, and projecting it to the PN assigned to the environment. The results, given by a set of Mixed Integer Linear Programming (MILP) problems, yield lower computational complexity when compared with previous approaches.