通过提出一个简化的高级生成框架，我们旨在减轻设计和实现新代理的困难，该框架允许用户使用线性时态逻辑（LTL）指定期望的代理行为，并通过约束解码器确保产生的输出展现所需的行为，从而迅速设计、实施和尝试不同的以 LLM 为基础的代理，而不必考虑如何实现或执行。

Oct, 2023

通过给大型语言模型提供关于控制和数据分离的指导，我们探讨了在反应式程序合成中为 LLM 提供指导对于规范生成的影响，发现这种关注点的分离改进了规范生成，并提供了一个基准测试集用于验证未来的 LLM 生成时态逻辑规范的工作。

Jun, 2024

我们提出了一种新的基于文本的时间推理模型 TempGraph-LLM，通过将上下文翻译成时间图，教导大型语言模型 (LLMs) 学习时间概念。我们证明了在其他任务上的预训练对 LLMs 的效益，并通过思路链的引导和特殊数据增强引导 LLMs 进行符号推理，观察到符号推理带来更一致可靠的结果。

Jan, 2024

本文提出了一个基于计算框架的分布式控制策略合成方法，用于处理存在部分观测的异质机器人团队，旨在满足 Truncated Linear Temporal Logic（TLTL）规范，其方法将综合问题表述为一个随机博弈，并采用策略图方法为每个机器人寻找具有内存的控制策略，模拟结果表明其解决方案的有效性和奖励塑形的有效性。

Mar, 2022

本文提出了一种强化学习框架，以从在一个未知的随机环境中，根据给定的线性时间逻辑（LTL）规范合成控制策略，该环境可以被建模为一个马尔可夫决策过程（MDP）。我们学习一种策略，最大化满足 LTL 公式的概率，引入一种新的、基于 LTL 公式的奖励和路径相关的折扣机制，使得（i）最优策略有效地最大化了满足 LTL 目标的概率，（ii）使用这些奖励和折扣因子的无模型强化学习算法保证收敛到这样的策略。最后，我们在两个运动规划案例研究中展示了我们基于强化学习的合成方法的适用性。

Sep, 2019

本研究提出一种基于强化学习的控制策略综合算法，用于最大化满足作为线性时序逻辑公式给出的高级控制目标的概率。该算法将 LTL 规范转换为限制性确定布琦自动机，再与具有不确定工作空间特性、结构和智能体行为的 PL-MDP 合并进行训练，从而生成满足概率的最大值。

Sep, 2019

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

Oct, 2023

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

Oct, 2017

本文提出了第一个针对具有分数折扣因子的 LTL 和 DSRewards 进行综合的声音算法，并在机器人规划领域展示了其效用。

May, 2022

该篇论文提出了一种名为 ``Formal-LLM'' 的新型框架用于基于 LLM 的代理，通过结合自然语言的表现力和形式语言的准确性，使规划过程具有控制性，从而防止代理生成无效和不成功的计划，并且通过实验验证了该框架在任务性能上取得的超过 50% 的整体性能提升，为在规划的有效性至关重要的应用场景中更广泛地利用 LLM 提供了可能性。

Feb, 2024