Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

PROSKILL: A formal skill language for acting in robotics

Félix Ingrand

TL;DR

This work tackles the need for verifiable acting in autonomous robots by introducing ProSkill, a formal skill language that maps to Fiacre for both offline model checking and online execution. ProSkill provides state variables, events, basic and composite skills, with automatic translation into Fiacre objects and processes, enabling rigorous verification via the Tina toolkit and runtime supervision via the Hippo engine. The approach is demonstrated on a UAV survey mission, showing offline verification of large state spaces and successful online deployment, linking specification directly to execution. By unifying acting primitives with a formal verification framework, ProSkill offers a practical pathway to trustworthy robotic behavior, combining design-time guarantees with run-time enforcement, even in the presence of external nondeterminism and timing constraints.

Abstract

Acting is an important decisional function for autonomous robots. Acting relies on skills to implement and to model the activities it oversees: refinement, local recovery, temporal dispatching, external asynchronous events, and commands execution, all done online. While sitting between planning and the robotic platform, acting often relies on programming primitives and an interpreter which executes these skills. Following our experience in providing a formal framework to program the functional components of our robots, we propose a new language, to program the acting skills. This language maps unequivocally into a formal model which can then be used to check properties offline or execute the skills, or more precisely their formal equivalent, and perform runtime verification. We illustrate with a real example how we can program a survey mission for a drone in this new language, prove some formal properties on the program and directly execute the formal model on the drone to perform the mission.

PROSKILL: A formal skill language for acting in robotics

TL;DR

This work tackles the need for verifiable acting in autonomous robots by introducing ProSkill, a formal skill language that maps to Fiacre for both offline model checking and online execution. ProSkill provides state variables, events, basic and composite skills, with automatic translation into Fiacre objects and processes, enabling rigorous verification via the Tina toolkit and runtime supervision via the Hippo engine. The approach is demonstrated on a UAV survey mission, showing offline verification of large state spaces and successful online deployment, linking specification directly to execution. By unifying acting primitives with a formal verification framework, ProSkill offers a practical pathway to trustworthy robotic behavior, combining design-time guarantees with run-time enforcement, even in the presence of external nondeterminism and timing constraints.

Abstract

Acting is an important decisional function for autonomous robots. Acting relies on skills to implement and to model the activities it oversees: refinement, local recovery, temporal dispatching, external asynchronous events, and commands execution, all done online. While sitting between planning and the robotic platform, acting often relies on programming primitives and an interpreter which executes these skills. Following our experience in providing a formal framework to program the functional components of our robots, we propose a new language, to program the acting skills. This language maps unequivocally into a formal model which can then be used to check properties offline or execute the skills, or more precisely their formal equivalent, and perform runtime verification. We illustrate with a real example how we can program a survey mission for a drone in this new language, prove some formal properties on the program and directly execute the formal model on the drone to perform the mission.
Paper Structure (42 sections, 7 figures)

This paper contains 42 sections, 7 figures.

Table of Contents

  1. Introduction and motivation
  2. Acting: state of the art and proposed approaches
  3. Reactive planners and procedural languages
  4. State machines and programming language
  5. Acting/planning framework
  6. Programming skills within a formal framework
  7. Our approach
  8. The ProSkill language
  9. State variables
  10. Events
  11. Basic skills
  12. Composite skills
  13. A formal framework for offline and runtime verification: Fiacre, language, models, and tools
  14. Terminology, models, languages, and tools
  15. Fiacre semantics
  16. ...and 27 more sections

Figures (7)

  • Figure 1: The Fiacre processes modeling the Fiacre specification on Listing \ref{['lst:ftct']}.
  • Figure 2: Illustration of the H-Fiacre program on Listing \ref{['lst:ftch']}.
  • Figure 3: The ProSkill to Fiacre/ Hippo- Tina workflow. Only the data in the blue boxes need to be provided by the programmer. ProSkill (in light red) synthesizes the two models, the rest is fully synthesized. In light green, the workflow for the Hippo runtime verification version, and in light purple, the workflow for the Tina offline verification version.
  • Figure 4: The Offline Verification Basic Skill Automata Fiacre model ( Tina).
  • Figure 5: The Online Verification Basic Skill Automata H-Fiacre model ( Hippo).
  • ...and 2 more figures