提出一种实时组合合成框架,高效处理复杂逻辑需求。
A Compositional Framework for On-the-Fly LTLf Synthesis
- 在游戏求解过程中动态组合小逻辑公式,避免全量自动机构建
- 通过剪枝优化减少状态空间,提前发现不可实现的约束
- 适合处理大规模逻辑合取场景,对现有工具有明显提升
从有限轨迹上的线性时序逻辑(LTLf)进行反应式合成可转化为在确定性有限自动机(DFA)上的二人博弈。主要挑战在于DFA构造,最坏情况下为2EXPTIME-完全。现有方法要么预先组合构造DFA并利用自动机最小化缓解状态爆炸,要么在博弈求解过程中增量构建DFA以避免完整构造。但两者均无绝对优势。本文提出一种组合式的实时合成框架,结合两者优点,聚焦于实践中常见的多个小LTLf公式的合取。该框架在博弈求解过程中而非自动机构造阶段进行组合。尽管最坏情况下需组合所有中间结果,但通过剪枝可简化后续组合并实现不可实现性的早期检测。具体提供两种组合变体:先剪枝再组合以充分利用最小化,或边组合边剪枝以引导实时合成。与最先进的合成求解器相比,本框架能解决大量其他求解器无法处理的实例。详细分析表明两种变体各有优势。
原文摘要 · Abstract (English)
Reactive synthesis from Linear Temporal Logic over finite traces (LTLf) can be reduced to a two-player game over a Deterministic Finite Automaton (DFA) of the LTLf specification. The primary challenge here is DFA construction, which is 2EXPTIME-complete in the worst case. Existing techniques either construct the DFA compositionally before solving the game, leveraging automata minimization to mitigate state-space explosion, or build the DFA incrementally during game solving to avoid full DFA construction. However, neither is dominant. In this paper, we introduce a compositional on-the-fly synthesis framework that integrates the strengths of both approaches, focusing on large conjunctions of smaller LTLf formulas common in practice. This framework applies composition during game solving instead of automata (game arena) construction. While composing all intermediate results may be necessary in the worst case, pruning these results simplifies subsequent compositions and enables early detection of unrealizability. Specifically, the framework allows two composition variants: pruning before composition to take full advantage of minimization or pruning during composition to guide on-the-fly synthesis. Compared to state-of-the-art synthesis solvers, our framework is able to solve a notable number of instances that other solvers cannot handle. A detailed analysis shows that both composition variants have unique merits.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。