基于契约的任务规划规范精化与修复
机器人学
2022-11-23 v1 形式语言与自动机理论
软件工程
摘要
我们利用假设-保证契约（assume-guarantee contracts）解决机器人任务的形式化规范建模、精化与修复问题。我们展示了如何在多个抽象层次上对任务规范进行建模，并使用一个预实现规范库来实现它们。假设无法使用库中的组件满足该规范，在此情况下，我们计算出可用库元素生成的、对该规范的最佳近似代理。随后，我们提出一种系统化的方法，以 either 1) 搜索并精化库无法满足的规范“缺失部分”，或 2) 修复当前规范以使现有库能够对其精化。我们用于搜索与修复任务需求的方法论利用了契约之间的商、分离、组合与合并运算。
引用
@article{arxiv.2211.11908,
title = {Contract-Based Specification Refinement and Repair for Mission Planning},
author = {Piergiuseppe Mallozzi and Inigo Incer and Pierluigi Nuzzo and Alberto Sangiovanni-Vincentelli},
journal= {arXiv preprint arXiv:2211.11908},
year = {2022}
}