IJCAIApr, 2022

有限轨迹上的理论线性时序逻辑 (扩展版)

PDF
TL;DR本文提出了一种基于 Satisfiability Modulo Theories 的 Linear Temporal Logic 语言 ——LTLf Modulo Theories，该语言具有高表现力，可用于数据感知过程和规划的模型检验。我们提供了一种基于 SMT 编码的单遍树状表格系统的 LTLfMT 的半决策过程，并在黑色可满足检查工具中实现。实验结果表明了该算法在新型基准测试上的可行性。
发现论文，激发创造
  • LTLf 模块化理论的决定性片段（扩展版）

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

    Jul, 2023

  • 可扩展的随时学习线性时态逻辑片段算法

    本论文提出了一种新的算法来解决线性时间逻辑（LTL）公式学习问题，可以构建比之前更大的公式，并且可实现任意时刻输出结果，性能较好。通过开源实现和公开基准测试来评估算法性能。

    Oct, 2021

  • 关于带不确定性有限轨迹的时间逻辑（技术报告）

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

    Mar, 2019

  • 学习线性时间属性

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

    Jun, 2018

  • 线性时态逻辑的 Sahlqvist 风格对应定理

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

    Jun, 2022

  • GPU 上的 LTL 学习

    使用 GPU 加速的基于枚举程序合成的 LTL 学习器在处理追踪数据时比现有技术要快 46 倍，并且可以处理比现有学习器多 2048 倍的追踪数据。

    Feb, 2024

  • 前向 LTLf 合成：DPLL 在工作

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

    Feb, 2023

  • 观点线性时间逻辑

    本文提出了一种名为 SLTL 的新逻辑，它将 LTL 的时间特性与 SL 的多角度建模能力相结合，旨在解决多角度情境下的实践推理问题。

    Apr, 2023

  • 概率推理模理论

    我们介绍了一个叫做 SGDPLL（T）的算法，它可以解决概率推理问题，并具有参数化逻辑理论的特点，可以应用于丰富的逻辑语言，如数据结构和关系数据。

    May, 2016

  • 计算 LTLf 规范的不可满足核心

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

    Mar, 2022