SkiNet：用于基于技能集自主系统验证的 Petri 网生成工具
形式语言与自动机理论
2022-09-29 v1 机器人学
摘要
在动态与偏远环境中执行任务对自主系统的高层自主性与鲁棒性的需求，推动开发者提出新的软件架构。一种常见架构风格是将机器人系统的能力概括为称为技能的基本动作，并在其上实现技能管理层以结构化、测试并控制功能层。然而，当前可用的验证工具要么仅提供任务特定验证，要么基于未复现系统实际执行的模型进行验证，难以确保其应对意外事件的鲁棒性。为此，开发了工具 SkiNet，将系统的基于技能的架构转换为建模技能状态机行为及其所处理资源的 Petri 网。该 Petri 网允许使用模型检测（如线性时序逻辑（LTL）或计算树逻辑（CTL））供用户分析与验证系统模型。
引用
@article{arxiv.2209.14039,
title = {SkiNet, A Petri Net Generation Tool for the Verification of Skillset-based Autonomous Systems},
author = {Baptiste Pelletier and Charles Lesire and David Doose and Karen Godary-Dejean and Charles Dramé-Maigné},
journal= {arXiv preprint arXiv:2209.14039},
year = {2022}
}
备注
In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181