本文提出了一种基于符号技术的LTLf综合的框架，利用布尔合成的机制实现了策略生成，并在可扩展的基准测试中通过实验证明了符号方法比显式方法更具可扩展性。

May, 2017

本文提出了一种混合表示方法，利用显式和符号表示状态空间，并有效地利用它们的互补优势，从而提供了一种解决LTLf到DFA转换过程中三个必要条件的技术，从而解决合成中的瓶颈问题。

Nov, 2019

本文提出四种算法用于提取LTLf规范中的不可满足核，并采用实验评估了各种算法和工具的可行性、有效性和互补性。

Mar, 2022

本文提出了一种基于Satisfiability Modulo Theories的Linear Temporal Logic语言——LTLf Modulo Theories，该语言具有高表现力，可用于数据感知过程和规划的模型检验。我们提供了一种基于SMT编码的单遍树状表格系统的LTLfMT的半决策过程，并在黑色可满足检查工具中实现。实验结果表明了该算法在新型基准测试上的可行性。

Apr, 2022

本文提出了一种新的AND-OR图搜索框架，用于合成有限轨迹上的线性时态逻辑（LTLf），并在框架中设计了一种基于DPLL算法的程序来生成特定代理-环境移动，同时还提出了一种基于状态公式语法等价性的搜索节点等价性检查方法，实验结果表明，这些技术在许多情况下胜过了其他最先进的方法。

Feb, 2023

本文研究了线性时间逻辑模块理论在有限轨迹上的应用，其中命题使用一阶公式替代，并且可以比较不同时间点引用的一阶变量。我们提出了一种用于LTLfMT表格的完备且有效的修剪规则，该规则在满足有限内存的抽象语义条件的任何LTLfMT公式下，通过增加新规则可以保证表格也能终止。最重要的是，这种技术使我们能够建立关于LTLfMT的多个片段可满足性的新的可判定性结果，并对已知类别给出新的可判定性证明。

Jul, 2023

本文研究了代理在非确定性环境中完成任务的问题，提出并比较了多种使用有限轨迹线性时态逻辑的最佳努力合成方法，这些方法基于相同的基本组件，但在组件的组合方式上有所差异，并通过实证评估验证了这种差异对方法性能的重大影响。

Aug, 2023

自动从系统执行中合成形式规范的学习算法，以实现有效可监控的Metric Temporal Logic (MTL)公式的综合。

Oct, 2023

本研究解决了现有有限轨迹线性时态逻辑（LTLf）合成方法中的效率瓶颈，重点突出构建完整确定性有限自动机（DFA）的双指数复杂性问题。通过将LTLf直接转化为基于过渡的DFA（TDFA），本研究提出了一种即时合成框架，并引入了模型引导合成和状态蕴含等优化技术。实验结果表明，所提方法在性能上超过了现有工具，有效提高了合成过程的效率。

Aug, 2024

本研究解决了LTLf公式不一致性分析中的空白，通过引入一种新颖的方法来枚举LTLf规范的最小不可满足核心（MUCs）。通过将LTLf公式编码为答案集程序（ASP），实现了高效的MUC枚举，从而推动了解释性人工智能领域的进展。

Sep, 2024