Simplification of Robotic System Model Analysis by Petri Net Meta-Model Property Transfer

TL;DR

This paper tackles the challenge of formal analysis for robotic systems by introducing the Robotic System Hierarchical Petri Net (RSHPN) meta-model, a six-layer hierarchical Petri Net framework that enables property transfer from meta-models to concrete designs. The authors develop a decomposition-based analysis workflow that isolates subsystems and communication models, significantly mitigating state-space explosion and reducing the need for full re-analysis when creating new robotic systems. They show that core RSHPN properties—safety, conservativeness, and deadlock-freedom—can be preserved across layers, enabling scalable verification and reliable system implementation via the Robotic System Specification Language (RSSL). A case study on a table-tennis ball-collector demonstrates dramatic reductions in analysis complexity while preserving analytical rigor, validating the approach and its potential for rapid, safe robotic system design. The work closes with discussions on extending the methodology to model checking, runtime verification, and environment-driven coordination, underscoring the practical impact for modular, scalable robotics development.

Abstract

This paper presents a simplification of robotic system model analysis due to the transfer of Robotic System Hierarchical Petri Net (RSHPN) meta-model properties onto the model of a designed system. Key contributions include: 1) analysis of RSHPN meta-model properties; 2) decomposition of RSHPN analysis into analysis of individual Petri nets, thus the reduction of state space explosion; and 3) transfer of RSHPN meta-model properties onto the produced models, hence elimination of the need for full re-analysis of the RSHPN model when creating new robotic systems. Only task-dependent parts of the model need to be analysed. This approach streamlines the analysis thus reducing the design time. Moreover, it produces a specification which is a solid foundation for the implementation of the system. The obtained results highlight the potential of Petri nets as a valuable formal framework for analysing robotic system properties.

Figures (17)

• Figure 1: (a): Structure of an embodied agent; (b): 3 communication modes from the perspective of the sending subsystem
• Figure 2: Execution of a HPN represented by a page (example)
• Figure 3: Two places from two different nets fused with each other. When $t_{1,2}$ fires then the token appears in $p_{1,2}$ and in the fused place $p^{\textrm{fusion}}_{(1,2),(3,3)}$ (visible as $p^{\textrm{fusion}}_{(1,2),(3,3)}$ from perspective of $\mathcal{H}_{1}$ and as $p^{\textrm{fusion}}_{(2,1),(3,3)}$ from perspective of $\mathcal{H}_{2}$). Whenever a transition $t_{2,1}$ fires the token disappears from the fused place.
• Figure 4: Method of isolating a PN: (a) Removing connections to higher layers; (b) The first two transformations involve adding an additional transition, connecting it to input and output places, and introducing a token; final transformation replaces pages with places, ensuring isolation from lower layers.
• Figure 5: RSHPN $^{}\mathcal{H}_{}^{}$ modeling activities of a robotic system (adapted from Figat:2022:RAL)