Multi-Robot system environmental constraint analysis by petri nets

The utilization of multi-robot systems and drones in diverse operational settings is steadily increasing. However, these systems are expected to function reliably despite human-induced failures, particularly in dynamic and evolving environments. This requires robust design methods that account for environmental shifts and contextual uncertainties. This study addresses this challenge by adopting formal methodologies and systematically incorporating environmental constraints (including potential human failures) into both the design and verification phases of multi-robot systems. Specifically, the proposed approach follows a structured three-step strategy- 1)initially transforming the system specification into Petri net (PN) models that reflect both functional behaviors and environmental constraints; 2) model checking the resulting PNs against temporal logic properties in CTL and CSL expressing the influence of environmental contexts on the robot’s task achievement, and 3) deriving extra constraints based on model checking outcomes to manage expected environmental shifts and proactively ensure robust system behavior. Moreover, the framework leverages state-of-the-art large language models to automatically generate temporal logic formulas from natural language system specifications, thereby reducing manual formalization effort. We conducted empirical assessments to validate the approach using a multi-robotic system deployed in airport and hotel environments. The results demonstrate that the framework effectively supports both system modeling and the systematic evaluation of contextual influences on intended operational behavior.