本文提出了一种基于 Satisfiability Modulo Theories 的 Linear Temporal Logic 语言 ——LTLf Modulo Theories，该语言具有高表现力，可用于数据感知过程和规划的模型检验。我们提供了一种基于 SMT 编码的单遍树状表格系统的 LTLfMT 的半决策过程，并在黑色可满足检查工具中实现。实验结果表明了该算法在新型基准测试上的可行性。
Apr, 2022
本文提出了一种基于符号技术的 LTLf 综合的框架，利用布尔合成的机制实现了策略生成，并在可扩展的基准测试中通过实验证明了符号方法比显式方法更具可扩展性。
May, 2017
采用逐步缩减分析无法满足的核心方法，可以找出次优解，不仅能够优化稳定模型的计算，也有助于解决问题实例。
Aug, 2016
本文提出了一种新的 AND-OR 图搜索框架，用于合成有限轨迹上的线性时态逻辑（LTLf），并在框架中设计了一种基于 DPLL 算法的程序来生成特定代理 - 环境移动，同时还提出了一种基于状态公式语法等价性的搜索节点等价性检查方法，实验结果表明，这些技术在许多情况下胜过了其他最先进的方法。
Feb, 2023
这篇研究论文解决了测量申明性进程规范不一致性的问题，重点介绍了固定跟踪（LTLff）的线性时间逻辑的不一致性，提出了一种新的不完全一致语义作为不一致性测量的框架。提出两种基于这些语义的不一致性度量，并研究了引入方法的计算复杂性。
Jun, 2022
本文介绍了一种为声明性流程规范设计概率测量的框架。提出了一种测量事件日志上规范满足度的技术，并使用真实数据进行了评估，证明了它在发现、检查和漂移检测方面的适用性。
May, 2023
本论文提出了一种新的算法来解决线性时间逻辑（LTL）公式学习问题，可以构建比之前更大的公式，并且可实现任意时刻输出结果，性能较好。通过开源实现和公开基准测试来评估算法性能。
Oct, 2021
使用 GPU 加速的基于枚举程序合成的 LTL 学习器在处理追踪数据时比现有技术要快 46 倍，并且可以处理比现有学习器多 2048 倍的追踪数据。
Feb, 2024
本文研究了线性时间逻辑模块理论在有限轨迹上的应用，其中命题使用一阶公式替代，并且可以比较不同时间点引用的一阶变量。我们提出了一种用于 LTLfMT 表格的完备且有效的修剪规则，该规则在满足有限内存的抽象语义条件的任何 LTLfMT 公式下，通过增加新规则可以保证表格也能终止。最重要的是，这种技术使我们能够建立关于 LTLfMT 的多个片段可满足性的新的可判定性结果，并对已知类别给出新的可判定性证明。
Jul, 2023
本文研究了针对任意可达性和安全性属性的环境规范下的 LTLf 综合，考虑了代理任务和环境规范的两种属性，提供了一系列完整的综合算法。针对每种情况，我们设计了一个特定算法（关于问题复杂性最优），并证明了其正确性。这些算法通过不同的方式组合了常见的构建模块。虽然一些情况已经在文献中得到研究，但其他情况本文首次进行了研究。
Aug, 2023