本文总结了两种不同的问题设置中，从正面或反面的示例中学习 LTL 公式的两种方法，第一种方法假设示例标记有噪声，第二种方法则考虑在仅给出正面示例的情况下推断有意义的 LTL 公式，所提出的方法提供了解决上述问题的不同算法，以及推断时的其他时间性质描述，如信号时间逻辑或确定性有限自动机。

Dec, 2022

本文主要介绍了一种用于从有限集的正面和负面例子中学习复杂系统可解释性描述的算法，通过在 IEEE 标准时间逻辑 PSL (Property Specification Language) 中学习公式来解决此问题，并比较了与现有 LTL 学习算法的效果。

Feb, 2020

该论文提出了两种算法：第一种使用 MaxSAT 求解器在高噪声数据下推导出最小 LTL 公式，第二种算法则基于第一种算法使用决策树学习算法推导出 LTL 公式的决策树。这些算法能够高效地提取简明的 LTL 描述。

Apr, 2021

从样例中学习线性时间逻辑（LTL）公式的问题的计算复杂性进行了研究，发现 LTL 学习问题在全逻辑和几乎所有的片段中都是 NP 完全的。这激发了寻找高效启发式算法的动力，并突显了以简洁的自然语言表达分离性质的复杂性。

Dec, 2023

该论文提出了两种学习 Linear Temporal Logic（LTL）公式的新算法，该算法通过将学习任务简化为命题布尔逻辑中的一系列可满足问题来实现，并且验证了这两种算法在合成基准测试和领导者选举协议的执行理解方面的优异表现。

Jun, 2018

本文讨论了在 Markov 决策过程中，使用 LTL 的公式作为代理规划的规范，通过形成多目标优化问题，从 MDP 中演示的行为轨迹中推断 LTL 规范，利用遗传编程解决该问题的有效性进行了证明。

Oct, 2017

本文探讨了学习线性时序逻辑 (LTL) 公式的计算复杂性，并构建了 LTL 的片段逼近算法，并对许多片段证明了 NP 完全性。

Feb, 2021

该研究探讨了最新的大型语言模型（LLMs）是否能够帮助将人类解释转化为能够支持从演示中稳定学习线性时间逻辑（LTL）的格式。我们提出了一种将 LLMs 和基于优化的方法结合的方法，用于忠实地将人类解释和演示转化为 LTL 规范。通过几个案例研究，我们的实验证明了将解释与演示相结合在学习 LTL 规范方面的有效性。

Apr, 2024

本文提出了一种基于定理证明的方法，在神经网络的训练中规范和生成时间逻辑约束。通过 Isabelle 定理证明器的高阶逻辑，形式化嵌入线性时间逻辑，提出了一个损失函数，并使用 OCaml 版本制作的 PyTorch 模型进行了训练。结果表明，该算法在动态运动中达到预期效果，且避免了直接在 Python 这种编程语言中实现逻辑方面带来的许多风险。

Jul, 2022

本文探讨了神经符号计算中的两个基本问题：深度学习是否能够端到端地解决逻辑中的挑战性问题，以及神经网络是否能够学习逻辑的语义。研究重点是线性时间暂态逻辑（LTL），通过训练 Transformer 来直接预测给定 LTL 公式的解，使用传统求解器产生的经典解决方案生成训练数据，研究表明，使用这些特定的解决方案进行训练已足够。 Transformers 甚至可以预测在文献基准测试中，经典求解器超时的公式的解，它也可以推广到逻辑的语义，虽然与经典求解器找到的解有所不同，但仍可以正确地预测大多数公式的解。

Mar, 2020