- 深度策略优化与时序逻辑约束
我们的研究通过将任务规范为线性时间逻辑（LTL）目标并优化额外的标量奖励，提出了一种增强学习代理的任务说明方法。我们的方法将问题转化为单一优化目标，并通过引入 Cycle Experience Replay（CyclER）解决了 LTL 引 - 关于 LTL 目标的 Bellman 方程解的唯一性
在利用贝尔曼方程求解线性时态逻辑目标的规划问题中，我们发现采用两个折扣因子的替代奖励方法能够逼近时态逻辑目标的满足概率，但当一个折扣因子设为 1 时，贝尔曼方程可能存在多解从而导致期望回报评估不准确。我们提出了一个条件，使得贝尔曼方程等式有 - 从演示中学习 LTL 规范的解释整合
该研究探讨了最新的大型语言模型（LLMs）是否能够帮助将人类解释转化为能够支持从演示中稳定学习线性时间逻辑（LTL）的格式。我们提出了一种将 LLMs 和基于优化的方法结合的方法，用于忠实地将人类解释和演示转化为 LTL 规范。通过几个案例 - 偏好基于规划的随机环境：从部分有序时态目标到最受欢迎的策略
使用局部有序偏好对具有时限目标的马尔可夫决策过程进行决策和概率规划，将部分有序偏好通过引入顺序理论映射到这些目标的偏好决策，从而综合出最喜欢的策略。
- 复杂航天器任务的屏蔽深度强化学习
通过使用线性时态逻辑（LTL）来形式化航天器任务和安全需求，以构建奖励函数和确保概率保障的盾牌，本论文研究了自主航天器控制和 SDRL 框架下的任务定义、安全性以及奖励结构的灵活性。
- GPU 上的 LTL 学习
使用 GPU 加速的基于枚举程序合成的 LTL 学习器在处理追踪数据时比现有技术要快 46 倍，并且可以处理比现有学习器多 2048 倍的追踪数据。
- 逻辑规范引导的强化学习智能体的动态任务采样
基于逻辑规范引导的动态任务采样（LSTS）是一个新颖的方法，不像以前的方法，LSTS 不需要关于环境动态或奖励机器的信息，并且通过动态采样有希望导致成功目标策略的任务，来引导代理从初始状态到目标状态。在格局世界的评估中，LSTS 在复杂的顺 - ChIRAAG：ChatGPT 知情快速自动断言生成
通过大语言模型 (LLM) 设计了一种新型流程，从自然语言规范中生成英语语言、线性时态逻辑和 System Verilog Assertion (SVA) 的断言，并使用测试平台验证生成的断言，验证结果表明 LLM 可以简化断言生成工作流程 - MM从示例中学习时间公式是困难的
从样例中学习线性时间逻辑（LTL）公式的问题的计算复杂性进行了研究，发现 LTL 学习问题在全逻辑和几乎所有的片段中都是 NP 完全的。这激发了寻找高效启发式算法的动力，并突显了以简洁的自然语言表达分离性质的复杂性。
- LTLf 任务规范的非确定性和随机服务组合
研究以满足有限轨迹上线性时态逻辑（LTLf）任务规范为目标的服务组合问题，包括非确定性服务和随机服务，以最大化满足 LTLf 规范的概率、同时最小化服务使用成本。将 LTLf 综合、Roman 模型的服务组合、反应式综合和 MDPs 上的双 - 在 MDPs 中用于 LTL 和 ω-regular 目标的 PAC 学习算法
引入了一个基于模型的近似正确（PAC）学习算法，用于解决马尔可夫决策过程中的 omega 正则目标。不同于之前的方法，该算法从系统的采样轨迹中学习，不需要对系统拓扑的先验知识。
- LLM 基于代理的高层行为的形式化规范
通过提出一个简化的高级生成框架，我们旨在减轻设计和实现新代理的困难，该框架允许用户使用线性时态逻辑（LTL）指定期望的代理行为，并通过约束解码器确保产生的输出展现所需的行为，从而迅速设计、实施和尝试不同的以 LLM 为基础的代理，而不必考虑 - 生成强化学习策略解释的实证研究
本文介绍了一组用于政策解释的线性时态逻辑公式，重点是通过这些公式解释政策所实现的最终目标和执行过程中的先决条件。这些基于线性时态逻辑的解释具有结构化表示，特别适用于局部搜索技术。通过模拟夺旗环境显示了我们提出的方法的有效性。最后，提出了未来 - 基于基础模型和形式验证的规范驱动视频搜索
使用视觉和语言模型以及形式方法，本研究论文提出了一种自动高效搜索感兴趣视频事件的方法，通过将文本描述转换为有限轨迹的线性时态逻辑（LTLf）并构建视频信息的自动机，然后使用形式方法验证自动机是否满足规范，如果满足则将相关视频片段添加到搜索结 - 符号化的 LTLf 最佳努力合成
本文研究了代理在非确定性环境中完成任务的问题，提出并比较了多种使用有限轨迹线性时态逻辑的最佳努力合成方法，这些方法基于相同的基本组件，但在组件的组合方式上有所差异，并通过实证评估验证了这种差异对方法性能的重大影响。
- OCTAL：用于 LTL 模型检查的图表示学习
我们提出了一种基于图表示学习的模型检测框架，通过学习系统和规范的图结构表示，将模型检测问题转化为二分类问题，实验证明该方法在两种模型检测场景下取得了令人满意的准确性和速度提升。
- 多智能体规划中的责任预测
预测责任是确定个体行为是否可能导致其对特定结果负责的过程，可用于多智能体规划环境中让智能体在考虑计划时预测责任。该论文定义了主动、被动和贡献性责任的归因，考虑了智能体的变体，并使用此定义了责任预测的概念。该模型证明了我们的预期责任概念可用于 - 从目标导向的 LTLf 公式设计行为树
本文给出了一种将有限路径线性时间逻辑（LTL）中的目标转化为行为树（BT）的方法，其中通过成就取向任务任务语法获得有用的 LTL 公式，为通过运用 LTL 运算符组合任务形成任务提供了可能，这产生了放松的行为综合问题，其中广泛的规划器可以实 - 哥德尔 - 邓梅特线性时间逻辑
该研究探讨了一个版本的线性时态逻辑，其命题片段是 Godel-Dummett 逻辑，并使用了两种自然语义学，一种是真值语义学，另一种是双关系语义学，证明了这些语义定义了相同的逻辑，并提出了决定语句有效性的算法以及一个用于 Godel 临时逻 - 线性时态逻辑规则的基于点的时间解释
这项工作介绍了一种在给定路径规划中评估单个线性时间逻辑（LTL）约束在特定时间的相关性的框架，这是一项我们称之为 “点时解释” 的任务。