符号化 LTLf 合成
本文研究了代理在非确定性环境中完成任务的问题，提出并比较了多种使用有限轨迹线性时态逻辑的最佳努力合成方法，这些方法基于相同的基本组件，但在组件的组合方式上有所差异，并通过实证评估验证了这种差异对方法性能的重大影响。
Aug, 2023
本文提出了一种混合表示方法，利用显式和符号表示状态空间，并有效地利用它们的互补优势，从而提供了一种解决 LTLf 到 DFA 转换过程中三个必要条件的技术，从而解决合成中的瓶颈问题。
Nov, 2019
本文提出了一种新的 AND-OR 图搜索框架，用于合成有限轨迹上的线性时态逻辑（LTLf），并在框架中设计了一种基于 DPLL 算法的程序来生成特定代理 - 环境移动，同时还提出了一种基于状态公式语法等价性的搜索节点等价性检查方法，实验结果表明，这些技术在许多情况下胜过了其他最先进的方法。
Feb, 2023
本文研究了针对任意可达性和安全性属性的环境规范下的 LTLf 综合，考虑了代理任务和环境规范的两种属性，提供了一系列完整的综合算法。针对每种情况，我们设计了一个特定算法（关于问题复杂性最优），并证明了其正确性。这些算法通过不同的方式组合了常见的构建模块。虽然一些情况已经在文献中得到研究，但其他情况本文首次进行了研究。
Aug, 2023
本文提出了一种基于 Satisfiability Modulo Theories 的 Linear Temporal Logic 语言 ——LTLf Modulo Theories，该语言具有高表现力，可用于数据感知过程和规划的模型检验。我们提供了一种基于 SMT 编码的单遍树状表格系统的 LTLfMT 的半决策过程，并在黑色可满足检查工具中实现。实验结果表明了该算法在新型基准测试上的可行性。
Apr, 2022
我们研究可在完全可观察、非确定性领域（FOND）中使用线性时态逻辑有限轨迹（LTLf）表示的目标的尽力策略（又称计划）。我们提出了一种基于博弈论的技术，用于合成利用非确定性规划领域特性的尽力策略。我们在形式上证明了其正确性，并在实验中展示了其有效性，相对于基于将规划领域重新表达为通用环境规范的直接尽力合成方法，其可扩展性大大提高。
Aug, 2023