验证超性质的自动化的算法，通过构建一个非确定性多机器人规划实例，确保一个规划存在则满足验证问题。
May, 2024
本文旨在调查多模态和多代理系统是否在理性方面取得进展，通过概述最新的研究成果、鉴别单代理和单模态系统相对于理性的进步以及讨论开放性问题和未来方向。
Jun, 2024
介绍了一种更广泛的策略逻辑，用于在多代理并发游戏中推理策略，证明了其包括 CHP-SL，同时维护可决策模型检查问题。
Dec, 2011
该研究提出了针对强化学习算法的运行时验证技术，用于预测学习阶段是否满足质量和及时性的期望，并提出了三个验证属性和相应的监测与评估步骤。
Nov, 2023
该论文分析了用于真实时间系统的逻辑规范和验证的逻辑符号，分别比较了它们的决策性，公理化程度，表达能力和模型检查等特征。
May, 2010
概率模型检查是一种在不确定性或随机性背景下对软件或硬件系统进行形式化自动推理的技术。该技术综合了来自多个领域的思想和技术，包括逻辑、自动机理论、图论、优化、数值方法和控制。最近，概率模型检查还扩展到整合博弈论中的思想，特别是使用随机博弈模型和均衡解概念来正式验证具有不同目标的多个理性代理之间的交互。这提供了一种灵活推理有关代理以对抗或协作方式行动的手段，并为人工智能、机器人和自主系统等领域解决新问题带来机遇。本文概述了该领域的一些进展，并强调了它们已经被使用的应用。我们讨论了概率模型检查的优势如何应用或有潜力应用于多智能体系统，并概述了在这一领域取得更进一步的关键挑战。
Aug, 2023
本文提出了一种基于动作和信念的模态逻辑形式化描述信念程序的方法，用以表达类似 PCTL 的时态属性，并探讨验证信念程序的可判定性和不可判定性。
Apr, 2022
本研究提出一种基于强化学习的模型自由优化方法来学习行为策略，以最大化符合给定线性时态逻辑规范的概率。通过采用新型的产品 MDP、奖励结构和折扣机制，在各种 MDP 环境中进行实验，证明了其具有改进的样本效率和最优策略收敛性。
May, 2023
本文讨论了在 Markov 决策过程中，使用 LTL 的公式作为代理规划的规范，通过形成多目标优化问题，从 MDP 中演示的行为轨迹中推断 LTL 规范，利用遗传编程解决该问题的有效性进行了证明。
Oct, 2017
本文主要研究了一种称为公共观察逻辑的动态认知逻辑的计算复杂性，并探讨了该模型检查算法的实现，以及其在验证不同特征和交互系统方面的适用性。
May, 2022