Oct, 2021

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

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

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

    Jun, 2018

  • GPU 上的 LTL 学习

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

    Feb, 2024

  • 从示例中学习线性时间公式的复杂性

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

    Feb, 2021

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

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

    Apr, 2022

  • LTLf 模块化理论的决定性片段（扩展版）

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

    Jul, 2023

  • 学习时态逻辑性质：两种最近方法概述

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

    Dec, 2022

  • 教授神经网络时间逻辑

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

    Mar, 2020

  • 度量时态逻辑中高效可监测公式的合成

    自动从系统执行中合成形式规范的学习算法，以实现有效可监控的 Metric Temporal Logic (MTL) 公式的综合。

    Oct, 2023

  • 从示例中学习时间公式是困难的

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

    Dec, 2023

  • 从嘈杂数据中学习线性时间属性：一种 MaxSAT 方法

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

    Apr, 2021