带公平性与稳定性假设的LTLf合成
人工智能
2019-12-18 v1 形式语言与自动机理论
计算机科学与博弈论
计算机科学中的逻辑
摘要
在合成中，假设是对环境的约束，用以排除某些环境行为。此处一个关键观察是：即便我们考虑具有有限轨迹上LTLf目标的系统，环境假设也需在无限轨迹上表达，因为达成智能体目标可能需要无限多个环境动作。为求解有限轨迹LTLf目标在无限轨迹假设下的合成，我们可将该问题归约为LTL合成。遗憾的是，尽管LTLf与LTL中的合成具有相同的最坏情况复杂度（均为2EXPTIME完全），但实践中可用的LTL合成算法远比LTLf合成算法困难。本工作表明，在一些有趣的情况下，我们可避免此类转向LTL合成而保持LTLf合成的简洁性。具体而言，我们开发了基于BDD的、基于不动点的技术来处理基本形式的公平性与稳定性假设。我们通过实验表明，该技术的表现远优于标准LTL合成。
引用
@article{arxiv.1912.07804,
title = {LTLf Synthesis with Fairness and Stability Assumptions},
author = {Shufang Zhu and Giuseppe De Giacomo and Geguang Pu and Moshe Vardi},
journal= {arXiv preprint arXiv:1912.07804},
year = {2019}
}