随机多智能体系统中的自然战略能力
本文讨论了针对具有博弈均衡策略的并发多智能体系统进行时间逻辑性质检查的合理性验证问题，并提出了减少验证复杂度的有效方法。同时研究了满足社会福利约束条件的多智能体系统的最优策略问题。
Jul, 2022
本文将ATLES与fixpoint算子、策略分离扩展为具有非确定性控制的AMCDES，其可以灵活地表述时间性质，主要结果是ExpTime上限可满足检测（为ExpTime完全问题），并且Model Checking的上限是QP和NP∪coNP或NP，取决于具体策略的解释。
May, 2023
提出了一种基于类型推理的部分可观测元蒙特卡罗规划方法，在多智能体系统中实现对其他智能体的有效交互和长期规划，相比现有方法计算更快且能够得到更优解。
Jun, 2023
我们提出了一种新的关于多智能体仅信任利用信任基础的语言的语义，并展示了如何将其用于自动检查该语言及其具有私有信念扩展运算符的动态扩展的公式。我们提供了一个依赖于QBF和另一种专用算法的PSPACE模型检查算法，并提出了基于QBF的算法的实现和一个具体实例的计算时间的一些实验结果。
Jul, 2023
概率模型检查是一种在不确定性或随机性背景下对软件或硬件系统进行形式化自动推理的技术。该技术综合了来自多个领域的思想和技术，包括逻辑、自动机理论、图论、优化、数值方法和控制。最近，概率模型检查还扩展到整合博弈论中的思想，特别是使用随机博弈模型和均衡解概念来正式验证具有不同目标的多个理性代理之间的交互。这提供了一种灵活推理有关代理以对抗或协作方式行动的手段，并为人工智能、机器人和自主系统等领域解决新问题带来机遇。本文概述了该领域的一些进展，并强调了它们已经被使用的应用。我们讨论了概率模型检查的优势如何应用或有潜力应用于多智能体系统，并概述了在这一领域取得更进一步的关键挑战。
Aug, 2023
我们研究可在完全可观察、非确定性领域（FOND）中使用线性时态逻辑有限轨迹（LTLf）表示的目标的尽力策略（又称计划）。我们提出了一种基于博弈论的技术，用于合成利用非确定性规划领域特性的尽力策略。我们在形式上证明了其正确性，并在实验中展示了其有效性，相对于基于将规划领域重新表达为通用环境规范的直接尽力合成方法，其可扩展性大大提高。
Aug, 2023
本文研究了代理在非确定性环境中完成任务的问题，提出并比较了多种使用有限轨迹线性时态逻辑的最佳努力合成方法，这些方法基于相同的基本组件，但在组件的组合方式上有所差异，并通过实证评估验证了这种差异对方法性能的重大影响。
Aug, 2023
HyperATLS$^*_S$是ATL$^*$的扩展，可以比较多个战略互动的结果，并强制要求一些代理共用相同策略。它是一个丰富的规范语言，可以捕捉现有逻辑无法达到的重要AI相关属性。我们证明了在并发博弈结构上对HyperATL$^*_S$的模型检查是可判定的，并在一系列基准测试中使用我们的模型检查算法实施，并对其进行评估。
Dec, 2023