ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
Imperial College London（帝国理工学院）
本文提出面向无限迹与有限迹语义的 ATL* 符号化模型检测算法，并在 ATL*AS 工具中实现，实验证明其在可扩展性和效率上优于现有方法。
2025-10-21 cs.LO cs.MA
How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract)
我们提出了一个逻辑框架，结合了对多人博弈中代理人通过优化收益或结果偏好来实现定量目标的能力的博弈论研究，以及对玩家实现玩家定性目标的能力的逻辑分析，即，达到或保持具有期望属性的游戏状态。我们丰富的并发游戏模型与支付的范式游戏与模型的状态，并提出了一个定量扩展的逻辑ATL*，使定量和定性推理相结合。
2013-03-04 cs.LO cs.MA
Natural Strategic Ability in Stochastic Multi-Agent Systems
本文提出在随机多智能体系统中使用自然策略框架，分析了 NatPATL 和 NatPATL* 的模型检查复杂性，展示了在确定性策略限制下 NatPATL 的 NP 完全性和 NatPATL* 的 2NEXPTIME 复杂性。
2025-11-26 cs.AI cs.LO
Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems
Institute of Computer Science, Polish Academy of Sciences（波兰科学院计算机科学研究所）；Faculty of Mathematics and Computer Science, Nicolaus Copernicus University（尼古拉·哥白尼大学数学与计算机科学学院）
针对随机多智能体系统中策略能力模型检测的难题，本文提出带不完美信息的概率交替时间时序逻辑的假设-保证验证方案，证明其可靠性并讨论完备性，还提出捕获“最多达成φ”的非概率交替时间逻辑新变体。
2025-10-28 cs.LO cs.MA
Natural Strategic Abilities in Voting Protocols
本文提出一种基于用户策略行为复杂性的分级安全概念，通过电子投票场景的案例研究，建模并分析了投票者维持安全属性所需的策略复杂性、资源消耗及防御攻击的难度。
2023-10-18 cs.LO cs.MA
Strategic (Timed) Computation Tree Logic
本文定义了带战略算子的 CTL 和 TCTL 扩展（SCTL 和 STCTL），证明其表达力优于 ATL，并分析了不同信息与回忆语义下的模型检测复杂度，最终利用 IMITATOR 工具支持 STCTL[ir] 的实际应用。
2023-10-19 cs.LO cs.MA
A Temporal Logic for Strategic Hyperproperties
超属性通常用于计算机安全中，以定义信息流策略和其他要求，这些要求可以推断多个计算之间的关系。在本文中，我们研究了一类新的超性质，其中个人的计算路径选择的多智能体系统中的代理联盟的战略选择。我们介绍HyperATL*，一个扩展的路径变量和策略量词的计算树逻辑。HyperATL* 可以表达策略性的超属性，例如并发系统中的调度器具有避免信息泄漏的策略。HyperATL* 对于指定异步超属性特别有用，即，超属性，其中在不同计算路径上的执行速度取决于调度器的选择。不像其他最近的逻辑规范的异步hyperproperties，我们的逻辑是第一个承认可判定的模型检验的完整的逻辑。我们提出了一个基于交替词自动机的HyperATL* 的模型检验算法，并通过提供一个匹配下界证明了我们的算法是渐近最优的。我们已经为HyperATL* 的一个片段实现了一个原型模型检查器，能够检查小程序的各种安全属性。
2021-07-06 cs.LO
Towards Assume-Guarantee Verification of Strategic Ability
本文提出使用假设-保证推理方法，促进对不完美信息和不完美回忆下的交替时间时序逻辑进行模型检测，以解决战略能力形式化验证的难题。
2023-10-24 cs.LO cs.MA
Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information
针对不完全信息完美记忆下ATL*验证不可判定的问题，本文提出通过生成可判定的子模型-子公式对、结合CTL*模型检验的近似验证方法，证明其复杂度与完全信息下ATL*检验相当，并实现工具给出实验结果。
2021-12-27 cs.LO cs.MA
Refining and Delegating Strategic Ability in ATL
我们建议扩展交替时间时序逻辑（ATL）的运营商<i refines-to G>F表示，代理i可以分配其权力的一组子代理G的方式，满足ATL条件f的战略能力，他们可能形成的联盟，可能与其他代理。证明了以该算子为主要连接符的子公式具有如下形式的公式的模型检验的可判定性<i_1 refines-to G_1>。<i_m refines-to G_m>f，在f中不再出现该运算符。
2014-04-03 cs.GT cs.LO cs.MA
On Angels and Demons: Strategic (De)Construction of Dynamic Models
LIPN, CNRS, Université Sorbonne Paris Nord（巴黎北大学国家科学研究中心信息与网络实验室）；University of Bergen（卑尔根大学）
本文提出三种逻辑用于研究动态图拓扑中策略的构建与破坏，探讨了其表达能力和模型检查复杂性。
2026-01-12 cs.LO
Reasoning about Quality and Fuzziness of Strategic Behaviours
时态逻辑被广泛用于反应系统的持续行为的规范。在这一领域的两个重要发展是传统的时间逻辑的扩展与模态，使规范的多智能体系统中正在进行的战略行为，和过渡的时间逻辑的定量设置，不同的满意度值，使指定形式化的概念，如确定性或质量。我们介绍和研究FSL-SL（战略逻辑），描述战略行为的最自然和最具表现力的逻辑之一的定量扩展。FSL公式的满意度值是[0，1]中的实际值，反映了基本代理人的战略持续目标得到满足的程度。我们展示了FSL在多智能体系统定量推理中的应用，通过展示它如何表达多智能体系统的稳定性概念，以及它如何推广一些模糊时序逻辑。我们还提供了一个模型检查算法，我们的逻辑，基于量化CTL* 的定量扩展。
2019-05-27 cs.LO
Completeness of two fragments of a logic for conditional strategic reasoning
本文证明了合作条件策略推理逻辑（CCSR）的责任片段和能力片段的完备性，方法涉及标准析取、有效性归约条件、抽象博弈形式及其实现，有望推广至CSR及其他策略逻辑。
2025-02-26 cs.LO
Reasoning About Strategies: On the Model-Checking Problem
在开放系统验证中，为了形式化地检查可靠性，需要一个适当的形式主义来建模代理之间的交互，并表示系统的正确性，无论环境如何表现。在这种情况下，一个重要的贡献是由模态逻辑的战略能力，在设置的多智能体游戏，如ATL，ATL \star，等等。最近，Chatterjee，Henzinger和Piterman介绍了策略逻辑，我们在这里表示为CHP-SL，目的是获得一个强大的框架来明确地推理策略。CHP-SL是通过使用一阶量化的策略，并已在非常具体的设置两个代理人轮流为基础的游戏，其中非初等模型检验算法已被提供的调查。虽然CHP-SL是一个非常有表现力的逻辑，我们声称，它并没有完全捕捉多智能体系统的战略方面。在本文中，我们介绍和研究了一个更一般的战略逻辑，表示SL，多智能体并发游戏中的策略推理。我们证明了SL包括CHP-SL，同时保持一个可判定的模型检验问题。特别是，我们提出的算法在计算上并不比已知的最好的CHP-SL。此外，我们证明了这样的问题SL是NonElementarySpace-hard。这个负面的结果促使我们在这里研究SL的语法片段，严格地包含ATL \star，希望得到一个基本的模型检验问题。其中，我们研究子逻辑SL[NG]，SL[BG]和SL[1G]。它们包含特殊前束范式的公式，分别具有嵌套的时间目标、目标的布尔组合和一次一个目标。关于这些逻辑，我们证明了SL[1 G]的模型检验…
2012-02-06 cs.LO cs.MA math.LO
On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
针对交替时间时序逻辑ATL$^*$无法比较多策略交互、无法要求智能体共策略的局限，提出扩展逻辑HyperATL$^*_S$，支持超性质下的策略交互比较与策略共享，证明其模型检测可判定并实现工具HyMASMC完成基准评估。
2024-03-12 cs.AI cs.LO cs.MA
HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
本文提出HyperATL*逻辑，通过引入路径变量和策略量词扩展计算树逻辑，支持在多智能体系统中对战略能力进行推理，统一捕获多种安全概念，并证明了其有穷状态模型检测的可判定性与算法渐近最优性。
2023-05-30 cs.LO
Neighbourhood semantics and axioms for strategic fragment of classical stit logic
STIT语义学是能动模态逻辑中最重要的工具之一，在哲学家和负责任的人工智能学者中广泛使用。STIT逻辑调查代理人的属性，确保某种状态保持不变，而不指定保证这种状态的具体行动。与其他多主体模态逻辑相比，STIT理论的主要优势在于表达能力。STIT逻辑不仅允许研究关于代理执行某些动作的能力的陈述（因为它是在联盟逻辑或命题动态逻辑的变体中），而且还可以研究他们做出的选择以及他们实际上实现的目标。然而，在某些情况下，这种表达可能是多余的。本文考察了经典STIT逻辑的一个特定片段，它只有战略模态算子，代表着这样一个事实，即代理人有能力看到它，一些事态的持有。片段的邻域语义，伴随着健全性，规范性，因此强完备性的结果。此外，本文提出的片段的认知扩展的基本考虑。
2022-03-17 cs.LO
A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability
自从交替时间时序逻辑（ATL）被引入以来，许多逻辑被提出来推理系统中智能体的不同策略能力。特别是，一些逻辑已经被设计成这样的代理商的统一的无记忆策略的原因。这些策略是智能体可以通过只看他们从当前状态观察到的东西来有效地发挥作用的策略。ATL_ir可以被看作是推理这种统一策略的核心逻辑。然而，它的模型检查问题是困难的（它需要对NP预言机的多项式次数的调用），并且解决它的实用算法直到最近才出现。本文提出了一种模型检验统一无记忆策略技术。现有技术通过系统的前向遍历从感兴趣的状态（诸如初始状态）构建策略。另一方面，所提出的方法通过向后遍历从目标状态构建获胜策略，确保只探索统一的策略。然而，从头开始构建策略将其适用性仅限于受限的可达性目标。本文详细介绍了这种方法，并将其与现有的方法实现到一个基于BDD的框架实验比较。这些实验表明，该技术是有竞争力的情况下，它可以处理。
2017-09-07 cs.LO
Formal Verification of Diffusion Auctions
University of Bergen（卑尔根大学）
针对扩散拍卖未被探索的形式化验证与策略推理视角，本文引入捕捉其动态及策略维度的逻辑形式体系，提供模型检测程序并建立算法计算复杂度结果。
2025-11-11 cs.GT cs.LO
Extended Graded Modalities in Strategy Logic
Technische Universitat Wien（维也纳工业大学）；Università degli Studi di Napoli Federico II（那不勒斯费德里科二世大学）
策略逻辑（SL）是多智能体系统中策略推理的逻辑形式。它的主要特点是，它具有与特定代理相关联的策略变量，这些变量具有绑定运算符。我们引入了分级策略逻辑（GradedSL），这是SL在策略变量元组上的分级量词的扩展，即，“存在至少g个不同的元组（x_1，...，其中g是集合N的并集{aleph_0，aleph_1，2 ^aleph_0}中的基数。我们证明了GradedSL的模型检测问题是可判定的。然后，我们转向GradedSL片段的复杂性。当g被限制为有限基数时，写为GradedNSL，模型检查的复杂性并不比SL更难，即，它在量词等级中是非初等的。我们说明了我们的形式主义，显示如何计算的数量不同的策略配置文件是纳什均衡（NE），或子博弈完美均衡（SPE）。通过对具体公式结构的分析，我们得出结论：检验唯一NE或SPE存在性的重要问题都可以在2 ExpTime中解决，这并不比仅仅检验此类平衡点的存在性困难。
2016-07-12 cs.AI cs.GT cs.LO
Big, but not unruly: Tractable norms for anonymous game structures
我们提出了一个新的战略逻辑NCHATL，允许推理规范遵守并发游戏结构，满足匿名性。我们代表这样的游戏结构competencies，避免模型，有指数大小的代理人的数量。然后，我们表明，模型检验可以在多项式时间就这个紧凑的表示，即使是规范的系统，不是匿名的。也就是说，只要潜在的游戏结构是匿名的，模型检验规范公式是易于处理的，即使规范可以规定不同的禁止行为集不同的代理。
2014-05-27 cs.LO cs.MA
Reasoning about Knowledge and Strategies under Hierarchical Information
两个不同的语义已被认为是知识的背景下，战略推理，这取决于球员是否知道对方的战略或没有。分布式合成的问题是已知的认知时间规范是不可判定的，后者的语义，已经在系统的层次信息。然而，对于其他的，不知情的语义，这个问题是决定这样的系统。在这项工作中，我们概括了这一结果，通过引入不完美信息的战略逻辑的认知扩展。知识算子的语义是不知情的，并捕获代理，可以改变观察力，当他们改变策略。我们解决了一类“层次实例”的模型检查问题，这提供了一个解决方案，一个巨大的类的战略问题与认知的时间规范层次系统，如分布式综合或合理的综合。
2018-09-03 cs.LO
Concurrent Game Structures with Roles
在下面的论文中，我们提出了一个新的语义著名的战略逻辑ATL。它基于向并发博弈结构添加角色，即在每个状态下，每个代理都属于一个角色，并且角色指定在该状态下他可以采取什么行动。我们展示了新语义的优势，提供了激励的例子，基于传感器网络，并分析了模型检验的复杂性。
2013-03-04 cs.LO cs.MA
Strategy Logic with Imperfect Information
我们介绍了一个扩展的策略逻辑的信息设置，称为SLii，并研究其模型检测问题。由于这种逻辑自然地捕捉多人游戏的不完美的信息，这个问题是不可判定的，但我们引入了一个语法类的“层次实例”，直观地说，作为一个去语法树的公式，战略量化关注的是更精细的观察模型，我们证明，模型检查SLii限制到层次实例是可判定的。为了建立这个结果，我们通过QCTL，一个中介，“低级”逻辑更适合自动机技术。QCTL是CTL在原子命题上的二阶量化推广。我们将其扩展到不完美的信息设置参数化的二阶量词的意见。虽然QCTLii的模型检查问题是，在一般情况下，不可判定的，我们确定的语法片段的分层公式和证明，使用自动机理论的方法，它是可判定的。我们应用我们的结果来解决复杂的战略问题，在信息不对称的设置。我们首先表明，存在的确定性策略的纳什均衡是可判定的层次信息的游戏。我们还介绍了分布式的合理的合成，一个概括的合理的合成的信息设置。因为它可以很容易地表达在我们的逻辑，我们的主要结果提供了解决这个问题的情况下，层次信息。
2020-03-07 cs.LO
Probabilistic Strategy Logic with Degrees of Observability
University of Aberdeen（阿伯丁大学）；Utrecht University（乌得勒支大学）；Open University Netherlands（荷兰开放大学）
针对现有概率策略逻辑无法表达信息透明性的问题，本文引入可观测性算子扩展 Probabilistic Strategy Logic，提出随机多智能体系统的形式化推理框架，并证明其模型检测问题可判定。
2025-01-06 cs.AI cs.LO
No big deal: introducing roles to reduce the size of ATL models
在下面的论文中，我们提出了一个新的语义著名的战略逻辑ATL。它基于向并发博弈结构添加角色，即在每个状态下，每个代理都属于一个角色，并且角色指定在该状态下他可以采取什么行动。我们展示了新语义的优势，分析了模型检验的复杂性，并证明了标准ATL语义和我们的新方法之间的等价性。
2012-04-16 cs.LO cs.MA
When Natural Strategies Meet Fuzziness and Resource-Bounded Actions (Extended Version)
University of Naples Federico II（那不勒斯费德里科二世大学）
本文提出HumanATLF逻辑，结合模糊语义和资源受限行动，解决自然策略中成本和不确定性的问题，并证明模型检查的复杂性。
2025-12-23 cs.LO cs.MA
A Decidable Fragment of Strategy Logic
策略逻辑（Strategy Logic，简称SL）是Mogavero、Murano和Vardi最近提出的一种有用的形式主义，用于在多智能体并发博弈中明确地推理作为一阶对象的策略。这种逻辑变得非常强大，包含了所有以前研究过的用于战略推理的模态逻辑，包括ATL，ATL* 等。不幸的是，由于它的表达能力，SL有一个非基本可判定的模型检查问题和一个高度不可判定的可满足性问题，特别是$Σ_{1}^{1}$ -Hard。为了得到一个可判定的子逻辑，本文引入并研究了单目标策略逻辑（SL[1G]，简称SL[1G]）。这个逻辑是SL的一个语法片段，严格地包含ATL*，它包含了前束范式中的公式，对于代理的每个策略量化，每次都有一个单一的时间目标。SL[1G]是一个基本可判定的模型检验问题。在这里，我们证明，与SL不同，它具有有界树模型属性，并且它的可满足性问题在2 ExpTime中是可判定的，因此不比ATL* 难。
2012-06-12 cs.LO math.LO
The Alternating-Time μ-Calculus With Disjunctive Explicit Strategies
Friedrich-Alexander-Universität Erlangen-Nürnberg（埃尔朗根-纽伦堡弗里德里希-亚历山大大学）；The Australian National University（澳大利亚国立大学）
本文将ATLES扩展为带不动点算子和策略析取的AMCDES，以更灵活刻画公平性等时序性质及受控非确定性承诺，并证明其可满足性检测为ExpTime完全，模型检测在固定解释下为QP与NP∩coNP、开放解释下为NP。
2023-05-30 cs.AI cs.LO
Unattainability of Common Knowledge in Asymmetric Games with Imperfect Information
本文构建能力极端不对称的双人不完全信息博弈模型，并借助 Kripke 结构与认知逻辑证明当前博弈状态的共同知识无法达成。
2025-01-08 cs.GT cs.LO cs.MA
Reasoning about Strategies: on the Satisfiability Problem
策略逻辑（Strategy Logic，简称SL）是由Mogavero、Murano和Vardi提出的一种有用的形式主义，用于在多智能体并发游戏中明确地推理策略（作为一阶对象）。这种逻辑被证明是非常强大的，包含了所有主要的先前研究的模态逻辑的战略推理，包括ATL，ATL* 等。不幸的是，由于其高表达性，SL具有非基本可判定的模型检查问题，并且可满足性问题是不可判定的，特别是Sigma_1^1。为了得到一个可判定的子逻辑，本文引入并研究了单目标策略逻辑（SL[1G]，简称SL[1G]）。这是SL的一个语法片段，严格地包含ATL*，它包含了前束范式中的公式，每次有一个单一的时间目标，对于每个策略量化的代理。我们证明了SL[1G]与SL不同，SL[1G]具有有界树模型性质，并且它的可满足性问题在2ExpTime中是可判定的，因此并不比ATL* 的可满足性问题难.
2017-03-16 cs.LO
Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems
本文研究多智能体系统修改的验证与综合问题，提出扩展逻辑LAMB以推理模型变化的动态性，并证明其表达能力严格强于ATL且保持P完全的模型检测过程。
2025-04-30 cs.LO cs.MA
