本文提出了一种基于动作和信念的模态逻辑形式化描述信念程序的方法，用以表达类似PCTL的时态属性，并探讨验证信念程序的可判定性和不可判定性。
Apr, 2022
本文主要研究了一种称为公共观察逻辑的动态认知逻辑的计算复杂性，并探讨了该模型检查算法的实现，以及其在验证不同特征和交互系统方面的适用性。
May, 2022
本文讨论了针对具有博弈均衡策略的并发多智能体系统进行时间逻辑性质检查的合理性验证问题，并提出了减少验证复杂度的有效方法。同时研究了满足社会福利约束条件的多智能体系统的最优策略问题。
Jul, 2022
介绍了关系型动态系统的建模和验证问题，提出了关系型动作基础（RABs）的通用框架，并通过（近似）基于SMT的反向搜索研究了RABs的参数化安全性，展示了这种方法在数据感知业务流程基准测试中的有效性，最后展示了如何利用通用不变量使得这个过程完全正确。
Aug, 2022
本研究探讨了利用模型检查的方式研究抽象概念来简化argumentation framework，这是解决动态multi-agent系统中的问题的一种方法。
Nov, 2022
提出了一种基于类型推理的部分可观测元蒙特卡罗规划方法，在多智能体系统中实现对其他智能体的有效交互和长期规划，相比现有方法计算更快且能够得到更优解。
Jun, 2023
本研究比较了不同 Zero-suppressed Decision Diagrams 变体在多智能体系统的符号编码中的记忆使用情况，结果表明使用合适的 ZDDs 可以显著减少 BDDs 的记忆使用量。
Jul, 2023
概率模型检查是一种在不确定性或随机性背景下对软件或硬件系统进行形式化自动推理的技术。该技术综合了来自多个领域的思想和技术，包括逻辑、自动机理论、图论、优化、数值方法和控制。最近，概率模型检查还扩展到整合博弈论中的思想，特别是使用随机博弈模型和均衡解概念来正式验证具有不同目标的多个理性代理之间的交互。这提供了一种灵活推理有关代理以对抗或协作方式行动的手段，并为人工智能、机器人和自主系统等领域解决新问题带来机遇。本文概述了该领域的一些进展，并强调了它们已经被使用的应用。我们讨论了概率模型检查的优势如何应用或有潜力应用于多智能体系统，并概述了在这一领域取得更进一步的关键挑战。
Aug, 2023
通过提出一个简化的高级生成框架，我们旨在减轻设计和实现新代理的困难，该框架允许用户使用线性时态逻辑（LTL）指定期望的代理行为，并通过约束解码器确保产生的输出展现所需的行为，从而迅速设计、实施和尝试不同的以LLM为基础的代理，而不必考虑如何实现或执行。
Oct, 2023
通过使用自然策略，模型检测概率时态逻辑在随机多代理系统下的复杂性结果是：当限制主动联盟为确定性策略时，使用自然策略的模型检测是NP完全问题；在不受限制的情况下，使用自然策略的模型检测的复杂度为EXPSPACE。
Jan, 2024