面向即时 LTLf 合成的组合框架

从线性时间逻辑有限迹线 (LTLf) 进行的响应性合成可简化为基于确定性有限自动机 (DFA) 的两人游戏。主要挑战在于 DFA 构造，这在最坏情况下的时间复杂度为 2EXPTIME。现有技术要么在解决游戏前组合构造 DFA，利用自动机最小化来缓解状态空间爆炸问题，要么在游戏求解期间逐步构建 DFA 以避免完全构造 DFA。然而，两种方法都没有占据主导地位。本文引入一种组合化即时合成框架，将两者的优势融合于一起，侧重于实际中常见的较小 LTLf 公式的大型 conjunction。该框架在游戏求解期间而非自动机（游戏场）构造期间应用组合。虽然在最坏情况下组合所有中间结果可能是必要的，但对这些结果进行修剪会简化后续组合，并 enables early detection of unrealizability。具体而言，该框架允许两种组合变体：在组合前修剪以充分利用最小化，或在组合期间修剪以指导即时合成。与最先进的合成求解器相比，我们的框架能够解决其他求解器无法处理的大量实例。详细分析表明，两种组合变体各有独特优势。