提出两种新博弈方法，解决有限轨迹时序逻辑的反应式合成问题。
Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis
- 基于自动机构造博弈图，将低阶性质转化为高阶性质求解。
- 引入原生嵌入目标的曼纳-普内利博弈，效率显著提升。
- 适合时序逻辑合成与形式化验证领域的研究者使用。
近期，曼纳-普内利层级被用于定义时序逻辑LTLfp和PPLTLp，使有限轨迹LTLf/PPLTL技术能在无限轨迹场景中应用，同时保持全量LTL的表达能力。本文首次实现了这些逻辑下的反应式合成求解器。基于埃默森-莱博弈的符号化求解器，将低阶性质（保证、安全）转化为高阶性质（重现、持久）后求解。随后提出曼纳-普内利博弈，原生嵌入曼纳-普内利目标于博弈图中，通过组合一系列更简单的埃默森-莱博弈解来求解，实现可证明更高效的策略。我们实现了这些求解器，并在一系列代表性公式上进行了实际评估。结果表明，曼纳-普内利博弈通常表现更优，但并非普遍适用，提示结合两种方法可能进一步提升实际性能。
原文摘要 · Abstract (English)
Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLfp and PPLTLp, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach. We implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。