分解具有单例活性保证的 GR(1) 博弈以实现高效综合
计算机科学中的逻辑
2017-09-22 v1
摘要
基于时序逻辑的综合方法通常用于为具有复杂行为的系统中的任务寻找构造正确的轨迹。此类任务的示例包括多智能体混合系统的同步、机器人的反应式运动规划。然而，此类方法的可扩展性令人担忧，在从理论向实践过渡时有时会成为瓶颈。在本文中，我们在线性时序逻辑（LTL）的 GR(1) 片段中识别出一类问题，其中综合问题允许进行能够轻松并行化的分解。这种分解还降低了交替深度，从而实现更高效的综合。我们提出了一个具有协调任务的多智能体机器人网格世界示例，以展示所开发思想的应用，并对基于分解的综合方法进行基准测试的经验分析。
引用
@article{arxiv.1709.07094,
title = {Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis},
author = {Sumanth Dathathri and Richard M. Murray},
journal= {arXiv preprint arXiv:1709.07094},
year = {2017}
}