Emerson-Lei博弈的符号化求解用于反应式综合
形式语言与自动机理论
2023-10-26 v2 计算机科学与博弈论
摘要
Emerson-Lei条件因其简洁性与组合性近来受到关注。在当前工作中，我们展示了如何以两种不同方式分析具有Emerson-Lei目标的无限时长博弈。首先，我们展示Emerson-Lei条件的Zielonka树自然导出一种新的到奇偶博弈的归约。然而，该归约并未带来最优分析。其次，我们基于首次归约（与Zielonka树）展示了如何提供获胜区域的基于不动点的直接刻画。该基于不动点的刻画允许符号化分析。它推广了具有已知获胜条件（如Büchi、GR[1]、奇偶、Streett、Rabin与Muller目标）的博弈的解，并在这些条件情况下复现了先前已知的符号算法与复杂度结果。我们也展示了所提算法的能力如何在反应式综合中被利用，提出了可符号化处理的LTL的一个新的富于表达力的片段。我们的片段结合了安全规约与活性部分。安全部分不受限，活性部分允许定义关于字母出现的Emerson-Lei条件。符号化处理得益于安全语言情况下确定的简单性以及我们使用的新博弈求解算法。该方法最大化了符号化求解的步骤数，以最大化高效符号实现的潜力。
引用
@article{arxiv.2305.02793,
title = {Symbolic Solution of Emerson-Lei Games for Reactive Synthesis},
author = {Daniel Hausmann and Mathieu Lehaut and Nir Pitermann},
journal= {arXiv preprint arXiv:2305.02793},
year = {2023}
}