# SkiNet: a User-Oriented Tool for Petri Net-based Analysis of Robotic Skills

Baptiste Pelletier, Charles Lesire, Karen Godary-Dejean

► To cite this version:

Baptiste Pelletier, Charles Lesire, Karen Godary-Dejean. SkiNet: a User-Oriented Tool for Petri Net-based Analysis of Robotic Skills. Petri Nets 2025 - 46th International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2025, Paris, France. hal-05072794

HAL Id: hal-05072794

https://hal.science/hal-05072794v1

Submitted on 19 May 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# SkiNet: a User-Oriented Tool for Petri Net-based Analysis of Robotic Skills

Baptiste Pelletier¹, Charles Lesire², and Karen Godary-Dejean³

¹ DCAS, ISAE, 10 Av. Marc Pélegrin, 31055 Toulouse, France
baptiste.pelletier@isae-supaeo.fr

² DTIS, ONERA, Univ. de Toulouse, 2 Av. Marc Pélegrin, 31000 Toulouse, France
charles.lesire@onera.fr

³ LIRMM-CNRS, Univ. de Montpellier, 161 Rue Ada, 34095 Montpellier, France
karen.godary@lirmm.fr

**Abstract.** Despite the rise in applications of formal methods for the design and analysis of robotic systems, their integration into existing frameworks remains a challenge. Part of the problem is due to the important changes in the software architecture of robotic design tools needed to accommodate for formal methods, but another challenge is the inherent difficulty for non-experts to use formal methods. In this work, we present SkiNet, a user-oriented tool which aims to assist in the design of skill-based robotic systems using a formal model based on Petri nets. The main idea for SkiNet is to interpret the user-written specifications and properties, into elements from the formal model, and vice versa. This allows the user to be more independent when diagnosing and validating the specified behavior, without having to directly manipulate the back-end formal tools. An example of the verification process of robotic skills specifications using SkiNet is given to showcase this paradigm.

**Keywords:** Formal methods · Robotics · Model-checking · Software engineering

## 1 Introduction

Recent trends in robotics and autonomous systems have shown a rise in the use of skill-based architectures to describe behaviors [4,16]. Indeed, the design of automation and decision-making functions is simplified by dividing the often complex behavior of a robot into a set of skills it can perform, i.e. modular elementary actions that integrate the sensing or acting capabilities of the robot. On top of this, these skills can run concurrently using abstract resources models for software and hardware components. Domain-specific languages (DSLs) such as SkiROS [15] or Robot-Language [2,1], offer frameworks to design robotic skills.

In parallel, the rise of formal methods applied to autonomous systems allowed an increase in robustness and safety of behaviors, with domains ranging from robotics to autonomous vehicles [13]. However, their integration into frameworks used for the design and analysis of robotic systems, especially for end-user oriented tools, is not as popular. Indeed, high-level skills and mission specification is
still being done using semi-formal methods, such as behavior trees [8] or UML-
based languages [20], or using DSLs such as Robot-Language [1]. In contrast,
approaches relying on formal methods, such as DiNeROS [6], ASPiC [11] or the
work of Ziparo [22], struggle to gain in popularity. The fact that these frame-
works are supposed to be handled by end-users, who often have no experience
with formal methods or robotic programming, makes them less appealing than
their semi-formal counterparts, even if formal verification becomes impossible.
On the other hand, toolchains like the Genom3/Fiacre/Hippo framework [5] are
formally defined, but more expert-oriented. This leads to a need for user-oriented
formal tools, especially when the behaviors become too complex and require a
formal simulation and verification. Related works like VeriPlan [10] or Frama-
C [14] have tried to tackle this issue in their respective domains. However, to
the best of our knowledge, there are no tool who offer, with a user-oriented ap-
proach, an automatic verification of specifications of robotic behaviors, based on
a formal model faithful to the behavior generated from these specifications, not
just the verification of the specifications themselves.

In this work, we tackle robotic skills specified using Robot-Language (RL), a
DSL aimed at users who are familiar with robotics programming and who wish
to create skills for their robots [2,1]. This DSL allows to describe a skillset: a
set of skills defining the elementary actions of the robot, a set of resources ab-
stracting its software and hardware components, and a set of events, considered
uncontrollable, that affect resources states. The RL skillset comes with a tool
for generating a ROS-compliant C++ code that follows the specified behavior
of the skills, with empty functions that need to be filled by the user with the
functional code of the robot. In a previous work [17], we showed how RL skillsets
can be translated into Petri net models and what interesting properties could
be verified via model-checking of the Petri net. The translation and analysis
were integrated in a tool called SkiNet, which we present in this paper, with an
emphasis on user-friendliness.

As the tool started to be used by more and more users with various experience
in robotic skills programming and formal methods, the discrepancy between the
specification language and the PN elements and model-checking results turned
out to be a challenge. This is a known issue, highlighted by Espiau et al. [7],
called the "error diagnosis problem". SkiNet was therefore designed as a high-
level tool, translating the skillset paradigm, manipulated by the user, and the PN
environment, used for simulation and model-checking. The latter partly relies on
Tina, a general PN analysis toolbox [3].

The paper is divided as follows: the SkiNet architecture, and how it interfaces
between the user, the PN model, the RL parser tool and the Tina toolbox,
are presented in Sec. 2. Then, Sec. 3.2 presents a case study of how users can
rely on SkiNet to simulate and diagnose unwanted behaviors. Finally, we will
conclude with our future goals for the tool. The SkiNet tool is available, with
the example skillsets shown in this paper, as well as tutorials, on Gitlab: https:
//gitlab.com/onera-robot-skills/skinet-release.
## 2 SkiNet

In this section, we present in detail the SkiNet tool, how it interfaces with the user, the Robot-Language skillset specification file, the generated PN models and the back-end tools it relies on.

Two domains are tackled by the tool, as shown in Fig 1: the user-space, i.e. what the user interacts with, and the Petri net (PN) space. The user-space is the Robot-Language (RL) skillset specification files (extension .rl), while the PN-space is the PN model and the interfaces with tools from the Tina toolbox. In the center is SkiNet, used either via a command-line interface or the instance of a Python class called `SkillsetNet`. The goal of SkiNet is to assist the user in analyzing its robotic skills, with the PN analysis running in the background, the user being never exposed to the PN-space unless requested.

<figure><img src="image_2.png" /><figcaption>Fig. 1: SkiNet acts as an interpreter between the user-space and the Petri net-space for the user to analyze Robot-Language skills.</figcaption></figure>

### 2.1 Robot-Language (user-space)

A RL skillset [1] contains sets of resources $\mathcal{R}$, events $\mathcal{V}$ and skills $\mathcal{S}$. They have been applied to a variety of robotic systems, such as ground, aerial or underwater vehicles [2,17,18]. In this work, we present a use-case of a skillset used to model a Spot® robot from Boston Dynamics, mounted with a Jaco® manipulator arm from Kinova, as seen in Fig. 2.

Resources $r \in \mathcal{R}$ are state machines with states $S^r = \{S_0^r, S_1^r, ..., S_n^r\}$, with transitions between these states, which help modelling the functional layer. Events $\nu \in \mathcal{V}$ are used to model internal or external changes in the system that would impact the resources states, while skills $s \in \mathcal{S}$ model the elementary actions the robot can do. Both are refined with guards and effects on the resources to specify their execution, and the combination of a guard and an effect is called a skillset transition $\tau$. An example of skill, `safe_poweroff`, taken from the `spot_and_arm rl` skillset, used to turn off the motor power on the Spot® robot, is given in Lst. 1.1. This skill has three preconditions and can only be started if these are met (1.2 to 6), and when started, the motors become busy (resource `control_mode` goes to the `Busy` state, 1.7). Finally, it can end in a success (1.8 to 11), or a failure (1.12), switching `control_mode` back to `Idle`. In case of a success, the resource `power_status` goes to `PowerOff`.
<figure><img src="image_3.png" /><figcaption>Fig. 2: Spot® robot, controlled by a Robot-Language skillset to execute various autonomous missions.</figcaption></figure>

```json
skill safe_poweroff {
  precondition {
    is_sitting : spot_status == Sitting
can_move : lease_status == AutoMode and control_mode == Idle
    is_powered : power_status == PowerOn
  }
  start {control_mode -> Busy}
  success is_poweredoff {
    effect control_mode -> Idle
    postcondition power_status == PowerOff
  }
  failure couldnot_poweroff {effect control_mode -> Idle}
}
```

Listing 1.1: Skill `safe_poweroff`, written in the Robot-Language DSL [1].

## 2.2 Petri Net Generation

The first step to analyze and simulate a RL skillset will be to generate a `SkillsetNet` class instance (`SkN`) from the skillset specification (`.rl` file). This `SkN` instance will contain the skillset elements and its PN model, as shown in Fig. 3. From the specification file, the RL parsing tool is used to obtain a `Skillset` instance, a class describing the skillset content as a tree-like structure, with the skills, resources and events. From this, the PN model of the skillset is generated, giving a `PetriNet` instance, as well as a `.net` file (textual PN extension used by the Tina toolbox). Finally, the `SkN` instance is populated using the places, transitions and arcs from the `PetriNet` instance, by associating them back to elements in the skillset.

In our previous work [17], we have formalized the automated generation of skillsets into PNs modelling their execution. We summarize the important elements here. Resources $r \in \mathcal{R}$ are each modelled with a set of places $p_i^r$ for each of their states $S_i^r$. The transitions of the PN are generated from skillset transitions, generating a set of more than one PN transition $T_\tau$ for each $\tau$, to take into account all possible previous and next states of resources when $\tau$ is triggered.
On top of this, skills $s \in S$ have two states, idle or executing, modeled as PN places $p_i^s$ and $p_e^s$ respectively. As an example, the PN generated from the skill `safe_poweroff` in Lst. 1.1 is given Fig. 4.

<figure><img src="image_4.png" /><figcaption>Fig. 3: SkiNet uses the RL parser with the input file to get a `Skillset` tree-like instance, before generating the PN model and finally the high-level `SkillsetNet`.</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 4: PN generated from the specifications of the `safe_poweroff` skill.</figcaption></figure>

The `SkN` class provides various high-level methods, the middle-level `PetriNet` class methods, as well as lower-level methods which call the tools from the `Tina` toolbox. The latter can be found either in the `PetriNet` class, if the action to be realized can be used for generic PNs, or the `SkN` class, if the action is specialized in the context of robotic skills analysis.

### Manipulating the Generated Petri Net

While the generated PN is initially saved as a `.net`, users can use SkiNet to call the `ndrio` tool from Tina to convert it to another format. This allows expert users to use other tools than Tina and SkiNet, if they are already familiar with other PN analysis tools. The PN can also be exported in the graphical format `.ndr` of Tina using SkiNet. Fig. 5 compares the graphical PN produced by `ndrio` and SkiNet, with the latter being able to position the elements between skills, resources and events. However, as we can see, despite the improved arrangement, the readability is still very difficult.

### Examples

While graphical representation usually makes it easier to simulate the execution of models, it remains challenging to visually follow all simulation
<figure><img src="image_6.png" /><figcaption>Fig. 5: Comparison of the PN graphical representation capabilities.</figcaption></figure>

events and changes for big and complex models. Indeed, some of our skillsets would generate PN models too large for manual simulation, as seen in Tab. 1, with skillsets taken from the *examples* folder of the SkiNet Gitlab repository. We can see that some models can have a lot of PN transitions compared to the number of skillset transitions $τ$, making the PN difficult to manipulate using the former, this discrepancy being due to the concurrency in the resources states. Therefore, a textual simulation using skillset transitions instead of PN transitions can help the user, as we will see in the next section.

## 2.3 Simulation

Textual simulation using SkiNet was designed to help the user by hiding places that are not marked and transitions that are not enabled or firable, in order to only show the "active" elements of the PN. The textual simulation tool *play* of Tina can also be used, however the automated generation of the PN can lead to places and transitions names being hard to read or put back into context, as well as multiple places/transitions being generated from the same skillset element. On top of this, to be really helpful for the user, the simulation process should remind essential keywords or variable names of the user-space (such as resource
<table><caption>Table 1: Examples of RL skillsets used for various robot types. $|R|$, $|S|$ and nb.τ are the number of resources, skills and skillset transitions respectively, $|P|$ and $|T|$ are the number of places and transitions in the generated PN. The state-space size is also given (number of states).</caption><thead><tr><th>Robot type</th><th>RL skillsets files</th><th>|R|</th><th>|S|</th><th>nb. τ</th><th>|P|</th><th>|T|</th><th>States</th></tr></thead><tbody><tr><td>Wheeled</td><td>ugv skillset rl</td><td>3</td><td>5</td><td>44</td><td>24</td><td>60</td><td>37</td></tr><tr><td>Quadruped</td><td>spot rl</td><td>6</td><td>10</td><td>77</td><td>48</td><td>164</td><td>400</td></tr><tr><td>Flying</td><td>uav skillset rl</td><td>6</td><td>10</td><td>116</td><td>54</td><td>297</td><td>1512</td></tr><tr><td>Arm (simple)</td><td>manipulator rl</td><td>4</td><td>6</td><td>68</td><td>49</td><td>266</td><td>51340</td></tr><tr><td>Arm (detailed)</td><td>manipulator_6dof rl</td><td>6</td><td>1</td><td>36</td><td>63</td><td>16089</td><td>16265</td></tr></tbody></table>

states, skill invariants and preconditions, or events). SkiNet will perform the translation of the PN elements back to the user-space.

This simulation is managed as illustrated in Fig. 6: first, the *state* of the skillset is determined from the PN marking, sorting active elements as skill states, resource state places and *frable* skillset transitions, and second, the PN is simulated using the high-level skillset transitions $τ$, rather than the transitions $t \in T_τ$ generated from them.

<figure><img src="image_7.png" /><figcaption>Fig. 6: Skillset state and skillset transition firing sequences.</figcaption></figure>

**Skillset State** The state of a skillset is the set of the active states of each skill (idle or running), and resources (states $S_i^r$). If the place $p_i^s$ of a skill is marked, the skill is considered idle; otherwise, if $p_i^s$ is active, the skill is executing. Similarly, the place $p_i^r$ of a resource $r$ being marked indicates that its state $S_i^r$ is active. This will already help the textual simulation, as only the active states of skills and resources will be shown to the user.

**Skillset Execution** In the user-space, the simulation of the skillset execution is done using the skillset transitions $τ$ of skills or events. In the PN-space, the PN is simulated using the firing of the transitions $t \in T_τ$. This, and the previous skillset state definitions, make for the textual simulation interface that will allow users to simulate their skillsets more intuitively. For instance, if the user decides to start a skill $s$, SkiNet will take the corresponding skillset transition and verify
if a transition $t \in T_\tau$ is firable from the current marking of the PN, and fire it. If none are firable, the skillset transition $\tau$ is directly hidden to the user.

Fig. 7 compares the textual simulation of a skillset with its PN model using Tina and SkiNet. The *play* tool from Tina, taking as input the generated `.net` or `.ndr` file, shows the marking of the PN and the enabled and firable transitions at the given marking. The Skinet interface gives the skillset state, with resources and skill states clearly indicated, as well as the executable skills and events.

<figure><img src="image_8.png" /><figcaption>(a) Interface of *play*, the command line PN (b) Interface of the skillset simulation from player from the Tina toolbox. SkiNet.</figcaption></figure>

<caption>Fig. 7: Comparison of the PN simulation environments.</caption>

# 3 Analysis using SkiNet

Finally, we will showcase how SkiNet can help the user to verify and validate its skillset model, with an example.

## 3.1 Verification Process

Because the skillset specified by the user in the `.rl` file may not match the desired behavior, SkiNet will help with the validation step, i.e. making sure that the skillset can accomplish the desired behaviors, but also with the verification, i.e. checking that the way it accomplishes these behaviors is correct. This analysis is done in two steps: first, the state-space of the skillset must be calculated to generate all the reachable states of the system, and then, model-checking can be performed to check the desired properties. Fig. 8 illustrates how SkiNet serves as interface between the user and the analysis tools from Tina.

For state-space construction, the `sift` tool is used with the PN model to create a Kripke structure [12], stored as a `.ktz` binary file. This Kripke structure is used by the model-checking tools `selt` and `muse` of Tina, for linear temporal logic (LTL) and computational tree logic (CTL) respectively. For each of these tools, a child process is created in the `SkN` instance, namely `selt_child` and `muse_child`, and loaded with the Kripke structure. Once again, manipulating these tools is a challenge for non-expert users. Having to calculate the state-space is not a reflex for most users, so SkiNet will do it automatically for them. On top of this, temporal logics can be challenging to use, and the fact that the tools from Tina are in the PN-space makes them even more challenging, as the
user would have to use the names of places and transitions as they appear in
the generated `.net` file. SkiNet helps in two ways to assist the user, by both
providing generic properties to be verified on the skillset, but also by serving as
an intermediary for the user when verifying temporal logic formulae.

<figure><img src="image_9.png" /><figcaption>Fig. 8: State-space construction and temporal logic verification sequences.</figcaption></figure>

**Generic Properties** Generic properties, defined in our previous work [17], can be called using methods from the `SkN` instance or the command line interface of SkiNet, to verify skillset deadlocks, skill liveness, or the presence of useless elements, defined as skillset transitions $\tau$ where all transitions $t \in T_\tau$ are dead. These methods will call the child processes to verify predefined temporal logic formulae, get the results sent back by the processes, and parse them from the PN-space to the user-space, as seen in Fig. 8.

**User Properties** Users can write, in the user-space, their own properties, using either `CTL` or `LTL`. For `LTL`, the `selt` tool will return a sequence of transitions from the initial state if the property has a counter example. For `CTL`, a set of states verifying the property is returned by `muse`, from which the `pathto` tool from Tina can be used to find the sequence of transitions leading to each state. Then, SkiNet will interpret each transition of these sequences in the user-space, so that the user can see what event or skill execution led to these states.

## 3.2 Example

We consider a user trying to validate a skillset written for the Spot® robot. The specified skillset is the `spot_and_arm.r1` example in the Gitlab repository. Using SkiNet, the user wants to verify a specific property: can the robotic arm be in an unknown state while the Spot® is turning off (skill `safe_poweroff`, Lst. 1.1)? The user writes the property in the user-space, using `CTL`, to find states that would violate the property, giving Eq. 1:

$$ EG \ (safe\_poweroff.executing \ and \ arm\_statusUnknown) \quad (1) $$
SkiNet will convert the property to the PN-space and return the set of states where the property is true, using *muse*, as shown in Fig. 9: four states are found, and SkiNet can return a sequence of transitions leading to each state. For instance, the sequence leading to state n.181 is: the skill `init_power` and `standup` of Spot® succeed, then the `goto_articular` skill of the robotic arm is started, during which the event `end-effector blocked` is triggered, leading to a failure of this skill. After that, if the Spot® uses the `sitdown` skill, followed by the `safe_poweroff` skill, the property will be true. (postcondition of the success, 1.10). The user can then modify the skills and events to fix this behavior.

<figure><img src="image_10.png" /><figcaption>Fig. 9: Result for the verification of Eq. 1 using SkiNet, showing the property to verify, the same property written in the user-space, and the set of states verifying the property. The sequence leading to state n.181 is shown.</figcaption></figure>

## 4 Conclusion

In this work, we have presented SkiNet, a user-oriented tool for the modeling and verification and validation of robotic skills specifications using Petri nets. We have demonstrated the ability of SkiNet to maintain a boundary between the "user-space", where the user only tackles elements from the specifications, and the "Petri net-space". This allows users who are unfamiliar with formal methods to formally simulate, verify and diagnose the skills behaviors.

SkiNet has received positive feedback from developers and users familiar with Robot-Language, familiar with formal methods and model-checking, or both, as well as graduate students who used the tools as part of supervised projects, but a proper case-study should be conducted. On top of this, SkiNet was used to verify skillsets for aerial, ground and underwater robots, with some examples available on the Gitlab repository. Further improvements on SkiNet involve:

- Improve model-checking to go beyond just translating transition sequences, shown Fig. 9, by grouping results to avoid redundant traces.

- Create an ecosystem for verifying robotic skills from other DSLs than RL, or using other formal methods, such as the work of Raïs et al. [19], as well as an interface for planning tools to query SkiNet when solving problems.

- Plugging the LTL/CTL property specification to user-oriented tools such as FRET [9] or LLM-based tools like NL2CTL [21] and VeriPlan [10].

**Disclosure of Interests.** The authors have no competing interests to declare that are relevant to the content of this article.
**Acknowledgements** This research was by the Occitanie Region (France) and the National Research Agency (ANR) grant ANR-22-CE92-0011-02.

References

1. Albore, A., Doose, D., Grand, C., Guiochet, J., Lesire, C., Manecy, A.: Skill-based design of dependable robotic architectures. Robotics and Autonomous Systems **160** (2023). https://doi.org/https://doi.org/10.1016/j.robot.2022.104318

2. Albore, A., Doose, D., Grand, C., Lesire, C., Manecy, A.: Skill-based architecture development for online mission reconfiguration and failure management. In: International Workshop on Robotics Software Engineering (RoSE) (2021). https://doi.org/10.1109/RoSE52553.2021.00015

3. Berthomieu, B., Vernadat, F., dal Zilio, S.: The tina toolbox home page - time petri net analyzer - by laas/cnrs (2004)

4. Bøgh, S., Nielsen, O., Pedersen, M., Krüger, V., Madsen, O.: Does your robot have skills? In: International Symposium on Robotics (2012)

5. Dal Zilio, S., Hladik, P.E., Ingrand, F., Mallet, A.: A formal toolchain for offline and run-time verification of robotic systems. Robotics and Autonomous Systems **159** (2023). https://doi.org/10.1016/j.robot.2022.104301, https://www.scopus.com/inward/record.uri?eid=2-s2.0-85141912955&doi=10.1016%2fj.robot.2022.104301&partnerID=40&md5=0fc8e276f09ce286efe7549f74207eb5, cited by: 3; All Open Access, Bronze Open Access, Green Open Access

6. Ebert, S., Mey, J., Schöne, R., Götz, S., Aßmann, U.: Dineros: A model-driven framework for verifiable ros applications with petri nets. In: International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C) (2023). https://doi.org/10.1109/MODELS-C59198.2023.00127

7. Espiau, B., Kapellos, K., Jourdan, M.: Formal verification in robotics: Why and how? In: Robotics Research (1996)

8. Ghzouli, R., Berger, T., Johnsen, E.B., Dragule, S., Wąsowski, A.: Behavior trees in action: A study of robotics applications. In: International Conference on Software Language Engineering (2020). https://doi.org/10.1145/3426425.3426942

9. Giannakopoulou, D., Mavridou, A., Rhein, J., Pressburger, T., Schumann, J., Shi, N.: Formal requirements elicitation with fret. In: International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020). No. ARC-E-DAA-TN77785 (2020)

10. Lee, C., Porfirio, D., Wang, X.J., Zhao, K., Mutlu, B.: Veriplan: Integrating formal verification and llms into end-user planning. arXiv preprint arXiv:2502.17898 (2025)

11. Lesire, C., Pommereau, F.: Aspic: An acting system based on skill petri net composition. In: International Conference on Intelligent Robots and Systems (IROS) (2018). https://doi.org/10.1109/IROS.2018.8594328

12. Liu, Z., Xing, Z.: Characterizing petri nets with the temporal logicctl. In: Conference on Information Technology and Computer Science (2012). https://doi.org/10.2991/citcs.2012.97

13. Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: A survey. ACM Comput. Surv. **52**(5) (2019). https://doi.org/10.1145/3342355

14. Maroneze, A., Perrelle, V., Kirchner, F.: Advances in usability of formal methods for code verification with frama-c. Electronic Communications of the EASST
77 (Oct 2019). https://doi.org/10.14279/tuj.eceasst.77.1108, https://eceasst.org/index.php/eceasst/article/view/2235

15. Mayr, M., Rovida, F., Krueger, V.: Skiros2: A skill-based robot control platform for ros (2023)

16. Pedersen, M.R., Nalpantidis, L., Andersen, R.S., Schou, C., Bøgh, S., Krüger, V., Madsen, O.: Robot skills for manufacturing: From concept to industrial deployment. Robotics and Computer-Integrated Manufacturing 37 (2016). https://doi.org/10.1016/j.rcim.2015.04.002

17. Pelletier, B., Lesire, C., Doose, D., Godary-Dejean, K., Dramé-Maigné, C.: Skinet, A petri net generation tool for the verification of skillset-based autonomous systems. In: International Workshop on Formal Methods for Autonomous Systems (FMAS) (2022). https://doi.org/10.4204/EPTCS.371.9

18. Pelletier, B., Lesire, C., Grand, C., Doose, D., Rognant, M.: Predictive runtime verification of skill-based robotic systems using petri nets. In: 2023 IEEE International Conference on Robotics and Automation (ICRA). pp. 10580–10586 (2023). https://doi.org/10.1109/ICRA48891.2023.10160434

19. Raïs, S., Brunel, J., Doose, D., Herbreteau, F.: Cross-layer formal verification of robotic systems. In: International Workshop on Formal Methods for Autonomous Systems (FMAS) (2024). https://doi.org/10.4204/eptcs.411.9

20. Thomas, U., Hirzinger, G., Rumpe, B., Schulze, C., Wortmann, A.: A new skill based robot programming language using UML/P statecharts. In: International Conference on Robotics and Automation (ICRA) (2013). https://doi.org/10.1109/ICRA.2013.6630615

21. Zhao, M., Tao, R., Huang, Y., Shi, J., Qin, S., Yang, Y.: Nl2ctl: Automatic generation of formal requirements specifications via large language models. In: Ogata, K., Mery, D., Sun, M., Liu, S. (eds.) Formal Methods and Software Engineering. pp. 1–17. Springer Nature Singapore, Singapore (2024)

22. Ziparo, V.A., Iocchi, L., Lima, P.U., Nardi, D., Palamara, P.F.: Petri net plans: A framework for collaboration and coordination in multi-robot systems. Autonomous Agents and Multi-Agent Systems 23 (2011)