Aug, 2024

基于有效计数的有限轨迹线性时态逻辑的即时合成

HTML
PDF
TL;DR本研究解决了现有有限轨迹线性时态逻辑（LTLf）合成方法中的效率瓶颈，重点突出构建完整确定性有限自动机（DFA）的双指数复杂性问题。通过将LTLf直接转化为基于过渡的DFA（TDFA），本研究提出了一种即时合成框架，并引入了模型引导合成和状态蕴含等优化技术。实验结果表明，所提方法在性能上超过了现有工具，有效提高了合成过程的效率。
发现论文，激发创造
  • 符号化 LTLf 合成

    本文提出了一种基于符号技术的LTLf综合的框架，利用布尔合成的机制实现了策略生成，并在可扩展的基准测试中通过实验证明了符号方法比显式方法更具可扩展性。

    May, 2017

  • 有限时间范围下基于混合组合推理的反应合成

    本文提出了一种混合表示方法，利用显式和符号表示状态空间，并有效地利用它们的互补优势，从而提供了一种解决LTLf到DFA转换过程中三个必要条件的技术，从而解决合成中的瓶颈问题。

    Nov, 2019

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

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

    Oct, 2021

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

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

    Mar, 2022

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

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

    Apr, 2022

  • 前向LTLf合成：DPLL在工作

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

    Feb, 2023

  • 有限路径综合中的策略

    本文研究了线性时间逻辑（LTL）合成工具生成的转换器类型的影响。研究发现，对于模型检查过程，非终止性转换器相较于终止性转换器的复杂度呈指数级增长，因此在LTL合成中应该优先选择终止性转换器。

    May, 2023

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

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

    Jul, 2023

  • 符号化的LTLf最佳努力合成

    本文研究了代理在非确定性环境中完成任务的问题，提出并比较了多种使用有限轨迹线性时态逻辑的最佳努力合成方法，这些方法基于相同的基本组件，但在组件的组合方式上有所差异，并通过实证评估验证了这种差异对方法性能的重大影响。

    Aug, 2023

  • 枚举LTLf公式的最小不可满足核心

    本研究解决了LTLf公式不一致性分析中的空白，通过引入一种新颖的方法来枚举LTLf规范的最小不可满足核心（MUCs）。通过将LTLf公式编码为答案集程序（ASP），实现了高效的MUC枚举，从而推动了解释性人工智能领域的进展。

    Sep, 2024