Apr, 2015

资源有限 ATL 生产与消耗模型检查的技术报告

PDF
TL;DR本文探讨考虑资源限制下的团体能力表达逻辑。前人已经研究了一些逻辑模型，这些模型仅考虑资源的消耗或系统中任何路径中生产或消耗资源的总量有界。本文针对生产和消耗资源无界的情形，研究了 RB-ATL 逻辑的模型检验问题，证明了问题是可判定的，但难度达到指数。同时，本文揭示了该问题的一些可处理情况，并对 RAL 资源逻辑的一种变体进行了详细比较，并提供了新的复杂性结果。
coalitional abilityresource boundsmodel-checking problemrb-clrb-atl
发现论文，激发创造
  • 具有不完全信息和完美回忆的 ATL * 的可决定性结果

    本研究探讨了 ATL * 在不完全信息环境下（ATL * i）扩展的决策问题，首先证明了 ATL *（具有策略背景和不完全信息）的模型检查是可判定决策的，其次证明了当限制到分层实例时该问题是可判定的。

    May, 2018

  • 信息分享系统中战略能力的模型验证

    本文介绍了一种带有私有数据共享能力的不完美信息的并发博弈结构子类，这些结构可以通过特定的 ATL 片段模型检查，被称为 A-cast 系统，可以编码安全领域的复杂问题，如身份验证中的恐怖主义欺诈攻击。

    Apr, 2022

  • 具有析取显式策略的交替时间 μ 演算

    本文将 ATLES 与 fixpoint 算子、策略分离扩展为具有非确定性控制的 AMCDES，其可以灵活地表述时间性质，主要结果是 ExpTime 上限可满足检测（为 ExpTime 完全问题），并且 Model Checking 的上限是 QP 和 NP∪coNP 或 NP，取决于具体策略的解释。

    May, 2023

  • 关于策略的推理：关于模型检查问题

    介绍了一种更广泛的策略逻辑，用于在多代理并发游戏中推理策略，证明了其包括 CHP-SL，同时维护可决策模型检查问题。

    Dec, 2011

  • 关于交替时间逻辑、超属性和策略共享的研究

    HyperATLS$^*_S$ 是 ATL$^*$ 的扩展，可以比较多个战略互动的结果，并强制要求一些代理共用相同策略。它是一个丰富的规范语言，可以捕捉现有逻辑无法达到的重要 AI 相关属性。我们证明了在并发博弈结构上对 HyperATL$^*_S$ 的模型检查是可判定的，并在一系列基准测试中使用我们的模型检查算法实施，并对其进行评估。

    Dec, 2023

  • 由 (条件) 终止证明驱动的资源分析

    该论文提出了一种资源分析方法，它使用终止分析结果驱动成本关系系统（CRS）的生成，并且最终生成的线性有界 CRS（LB-CRS）克服了现有技术产生复杂程序流程的成本函数难以解决的问题，作者还制定了一种名为 MaxCore 的资源分析工具，并针对 C 整数程序的一组基准测试进行了实验，结果显示 MaxCore 优于其他所有资源分析工具。

    Jul, 2019

  • 有理验证的复杂性

    本文讨论了针对具有博弈均衡策略的并发多智能体系统进行时间逻辑性质检查的合理性验证问题，并提出了减少验证复杂度的有效方法。同时研究了满足社会福利约束条件的多智能体系统的最优策略问题。

    Jul, 2022

  • 度量时态逻辑中高效可监测公式的合成

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

    Oct, 2023

  • 实时和概率时态逻辑：一概述

    该论文分析了用于真实时间系统的逻辑规范和验证的逻辑符号，分别比较了它们的决策性，公理化程度，表达能力和模型检查等特征。

    May, 2010

  • 有限信息下的策略逻辑

    研究不完美信息领域中策略逻辑的 SLii 扩展，并研究其模型检查问题，证明其限制为分层实例的模型检查是可判定的，应用此结果解决了分层信息下确定性策略的纳什均衡存在性可判定问题和分布式合理综合问题。

    Mar, 2020