# SkiNet, A Petri Net Generation Tool for the Verification of Skillset-based Autonomous Systems

arXiv: https://arxiv.org/abs/2209.14039 · HTML: https://mlsanity.com/paper/2209.14039/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Sep 2022.

## Built on by (most cited first, 1 of 1)

- [Model-Based AI planning and Execution Systems for Robotics](https://mlsanity.com/paper/2505.04493/) (2025)

## Abstract (arXiv)

The need for high-level autonomy and robustness of autonomous systems for missions in dynamic and remote environment has pushed developers to come up with new software architectures. A common architecture style is to summarize the capabilities of the robotic system into elementary actions, called skills, on top of which a skill management layer is implemented to structure, test and control the functional layer. However, current available verification tools only provide either mission-specific verification or verification on a model that does not replicate the actual execution of the system, which makes it difficult to ensure its robustness to unexpected events. To that end, a tool, SkiNet, has been developed to transform the skill-based architecture of a system into a Petri net modeling the state-machine behaviors of the skills and the resources they handle. The Petri net allows the use of model-checking, such as Linear Temporal Logic (LTL) or Computational Tree Logic (CTL), for the user to analyze and verify the model of the system.