Analysing navigation paths in constrained graphs using Petri nets

In robotics applications, supporting navigation in dynamic environments (described though a graph) have been addressed multiple times relying on very different approaches. In this work, we are considering the navigation in a pre-defined map, considering different areas (rooms) connected by some pathways. The navigation is constrained by resource availability and specific conditions allowing the movement between adjacent areas. The overall goal is to conclude if, given a specific map and all associated constraints and resources, it is possible to reach a specific location in the map (the ultimate goal) without being trapped in some deadlock or livelock situation. The validation of the proposed approach uses procedurally generated games, where a map is automatically generated considering a set of rooms and doors allowing the movement from a starting room to the ultimate location (end of the game). The player may collect specific resources in the visited rooms, which will be used to allow navigation, namely to unlock passages. In this paper, a strategy based on the translation of the map to a Petri net model is proposed. From the Petri net model, relying on the building of the associated state space (reachability graph) it is possible to conclude about existence of deadlocks and loops (livelocks) and if the ultimate goal is reachable or not. A minimum set of translation rules is presented and validated using a small map and supported by the IOPT-Tools framework, which provides the tools for editing, simulating, generating the associated state space and a query mechanism to conclude about reachability of the ultimate goal, as well as deadlocks.