本文研究 Answer Set Programming 中的 past-present 句法子类，其扩展了完成和循环公式的定义，并通过 LTLf 表达式捕捉了一组 past-present 时间程序的时态稳定模型。

Jul, 2023

提出了一种新的基于超定理解的概率时态逻辑，用于处理现实动态系统中的不确定性，探讨了逻辑的特性并提供了基于自动机的推断机制。同时，研究了具有更好计算性质的逻辑片段，可以通过现有的声明性流程发现技术从事件日志数据中发现公式。

Mar, 2019

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

Apr, 2022

基于 Prime Decomposition 定理，本文介绍自动机级联作为自动机复杂系统的一种结构化和模块化方式；并且证明了样本复杂度可以通过组件数量和单个组件的最大复杂度来描述，由此学习表示多组分相互作用的大型动态系统的自动机的数量可以呈指数级增长。

Nov, 2022

本文探讨了线性时态逻辑（LTL）中，一类包括模态算子 F，G，X 和 U 的 Sahlqvist 公式具有一阶语言可定义的框架条件的对应关系。

Jun, 2022

该论文分析了用于真实时间系统的逻辑规范和验证的逻辑符号，分别比较了它们的决策性，公理化程度，表达能力和模型检查等特征。

May, 2010

介绍一些关于非单调推理的逻辑的表格演算，其中包括了 Kraus, Lehmann 和 Magidor 定义的优先、循环累积、累积和理性逻辑，并为所有的 KLM 逻辑给出了一个演算法。这些演算法包括了适当的模态来解释条件语句，为所研究的逻辑提供了一个决策过程，并研究了它们的复杂性。

Nov, 2006

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

Jul, 2023

通过引入分层结构的时态逻辑规范，将传统的机器人规划方法分解为多层组合规范，以提高语法简洁性、可解释性和规划效率，同时开发了一种基于分解的方法来处理具有分层时态逻辑结构的任务，实验结果表明分层形式具有更强的表达潜力，并且所提出的方法具有很好的效果，适用于机器人导航与操纵。

Aug, 2023

该研究论文扩展了 Lewis 关于反事实推理的理论，提出了一个结合时间和反事实操作的逻辑来自动化推理并解决可满足性和追踪检查问题。

Jun, 2023