全信息同步系统的 GR(1) 契约符号化构造
计算机科学中的逻辑
2015-08-12 v1 系统与控制
摘要
本文提出一种符号算法，用于构造允许多个智能体协作的假设-保证规范。每个智能体被分配以广义反应秩 1 (GR(1)) 这一线性时序逻辑片段表达的目标。这些目标可能是不可实现的，除非每个智能体对其他智能体的行为做出额外假设。所提算法为每个智能体构造弱公平假设，以确保它们能成功协作。一个必要条件是给定目标具有可协作满足性。我们证明存在这样的博弈：带有状态活性属性的 GR(1) 片段不足以保证从协作获胜集中的任意状态可实现。障碍源于活性目标之间的循环依赖。为防止循环，我们引入嵌套博弈作为表达带条件假设的规范的形式化工具。该算法是符号化的，具有类似于 GR(1) 综合算法的不动点结构，意味着时间复杂度关于状态数多项式，关于递归目标数线性。
引用
@article{arxiv.1508.02705,
title = {Symbolic construction of GR(1) contracts for synchronous systems with full information},
author = {Ioannis Filippidis and Richard M. Murray},
journal= {arXiv preprint arXiv:1508.02705},
year = {2015}
}