Strategy Logic, Imperfect Information, and Hyperproperties
CISPA Helmholtz Center for Information Security（CISPA信息安全研究中心）
本文研究不完全信息策略逻辑（SL$_\text{ii}$）与超策略逻辑（HyperSL）的关系，证明在状态公式不嵌套于路径公式的限定下二者等价，给出双向编码方法，揭示不完全信息与超性质的内在关联。
2025-10-04 cs.AI cs.LO cs.MA
Reasoning about strategies on collapsible pushdown arenas with imperfect information
不完全信息策略逻辑（Strategy Logic with Imperfect Information，SLiR）是一种非常具有表现力的逻辑，旨在表达分布式系统中策略能力的复杂属性。SLiR以前的工作集中在有限系统，并表明，模型检查问题是可判定的，当系统的控制状态的信息是分层的球员或系统的组件，这意味着球员或组件可以完全根据他们各自的状态知识排序。我们表明，从有限到无限的系统产生的可折叠（高阶）下推系统保留可判定性，自然的限制下，堆栈内容是可见的。证明遵循与有限系统相同的路线，但需要使用（可折叠）交替下推树自动机。这种自动机是不可判定的，但半交替下推树自动机被引入并证明是可判定的，研究了两个局中人下推系统的策略问题。为了解决多个球员的层次信息，我们进一步完善这些自动机：我们定义方向引导（可折叠）下推树自动机，并表明它们是稳定的投影，非确定性和缩小。对于后一种操作，用于处理不完美的信息，稳定性在某些假设下保持，当用于具有可见堆栈的系统时，该假设是满足的。然后，我们使用这些自动机来证明我们的主要结果。
2020-07-30 cs.LO
Resource Logics with a Diminishing Resource
模型检查资源逻辑与生产和消费的资源是一个计算困难，往往是不可判定的问题。我们引入了一个简单而现实的假设，即至少有一个递减资源，即不能生产的资源，并且每个行动对该资源的成本都是非零的。这种资源的一个例子是时间。我们表明，有了这个假设，即使是底层的交替时间时态逻辑，如模型检查下不完美的信息和完美的召回，不可判定的问题，成为可判定的资源逻辑与资源减少。
2018-06-24 cs.LO
Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
我们提出了一个形式化证明的不完全信息和完美召回语义下的交替时间时序逻辑的模型检验问题的不可判定性。这个问题被宣布为不可判定的根据个人通信的多人游戏与不完美的信息，但没有正式的证明曾经公布。我们的证明是基于直接减少从非停机问题的图灵机。
2011-02-21 cs.LO cs.MA
The Complexity of Verifying Strategic Abilities in Succinct Multiagent Systems
Griffith University（格里菲斯大学）；CNRS, LIPN, Sorbonne Paris North University（法国国家科学研究中心，LIPN，索邦巴黎北大学）；University of Naples Federico II（那不勒斯费德里科二世大学）；University of New South Wales（新南威尔士大学）
本文研究不完全信息下多智能体系统策略能力验证的复杂性，证明SLK_P和SLK的简洁模型检验为AEXP(poly)完全，目标ATL和ATL*为P^{NEXP}完全，修正了相关旧结果并明确了主观语义下的复杂度性质。
2026-10-13 cs.LO
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
我们介绍MCMAS-SLK，一个基于BDD的模型检查器的验证系统对规格表示在一个新的，认知的战略逻辑的变体。我们给出了规约语言的语法和语义，并介绍了一个标记算法的认知和策略逻辑模态。我们提供的检查器，也可以用于合成代理的策略，使系统满足规格的细节。我们评估的执行效率，通过讨论用餐密码协议和蛋糕切割问题的一个变种所获得的结果。
2014-05-16 cs.LO
An Epistemic Strategy Logic (Extended Abstract)
本文提出了一个扩展的时间认知逻辑与运营商量化的策略。该语言还提供了一种自然的方式来表示代理人会知道什么，如果他们知道其他代理人正在使用的策略。一些例子来激励框架，并讨论了交替时间认知逻辑的几个变种的关系。并对模型检验逻辑的计算复杂性进行了表征。
2014-04-03 cs.LO
A Hennessy-Milner Theorem for ATL with Imperfect Information
我们表明，一个基于历史的变种交替互模拟与不完美的信息允许它与一个变种的交替时间时序逻辑（ATL）的不完美的信息由一个完整的Hennessy-Milner定理。ATL的变体，我们认为有一个共同的知识语义，这要求统一的策略，可用于联盟，以实现某些目标必须是共同的知识联盟内部，而其他语义变体的ATL不完美的信息不适应Hennessy-Milner定理。我们还表明，存在一个基于历史的交替互模拟两个有限的并发博弈结构与不完全信息（iCGS）是不可判定的。
2020-06-26 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
New results on pushdown module checking with imperfect information
开放下推系统的模型检验标准分支时态逻辑（下推模块检查或PMC）最近在文献中被研究，在具有关于系统的完美和不完美信息的环境的上下文中（在最后一种情况下，环境仅具有系统的控制状态和栈内容的部分视图）。对于标准CTL，不完全信息下的PMC是不可判定的。如果堆栈内容被假设为可见的，那么问题是可判定的，并且是2EXPTIME完全的（将PMC的复杂性与CTL的完美信息相匹配）。限制在堆栈内容的深度可见的情况下，具有针对CTL的不完全信息的PMC的可判定性状态是开放的。在本文中，我们表明，与此限制，PMC与不完美的信息对CTL仍然不可判定。另一方面，我们个性化一个有趣的子类OPDS与可见的堆栈内容深度，使PMC与不完善的信息对CTL的存在片段是可判定的，并在2EXPTIME。此外，我们表明，PMC的程序复杂性与不完美的信息和可见的堆栈内容对CTL是2EXPTIME完全的（因此，指数比PMC的程序复杂性与完美的信息，这是已知的EXPTIME完全）。
2011-06-07 cs.LO
An Epistemic Strategy Logic
本文提出了一种扩展的时间认知逻辑与运营商量化代理策略。与以前的工作交替时间认知逻辑，语义与系统的状态明确编码的策略正在使用的每个代理。这提供了一种自然的方式来表达代理人会知道什么，如果他们知道其他代理人正在使用的一些策略。一些例子，依赖于表达一个代理的知识的能力，其他代理所使用的策略，以激励框架，包括推理博弈论均衡，基于知识的程序，和信息理论的计算机安全政策。交替时间认知逻辑的几个变种的关系进行了讨论。模型检验的逻辑和它的几个片段的计算复杂性的特点。
2018-07-11 cs.LO
Alternating (In)Dependence-Friendly Logic
针对 IF 逻辑的参与者不对称、非确定及排中律失效问题，本文提出 ADIF，并给出组合、Herbrand-Skolem 与博弈论语义，证明其确定性、排中律及二阶逻辑表达力。
2023-04-23 cs.LO math.LO
If You're Happy, Then You Know It: The Logic of Happiness... and Sadness
Berlin University of Applied Sciences（柏林应用科学大学）；King’s College（国王学院）
本文提出了一种不完全信息环境下的幸福和悲伤模态的形式语义。它表明，这些模态是不可定义的，通过对方，并给出了一个健全的和完整的公理化的性质。
2021-01-02 cs.AI cs.LO
Towards an Updatable Strategy Logic
本文介绍的是时态多智能体逻辑。这些形式主义中的几个已经提出（ATL-ATL*，ATLsc，SL）。它们能够表达系统中代理的能力，以确保时间属性的满足。特别是，SL和ATLSC使几个代理在一个上下文中混合不同的策略，他们在一个语义游戏中发挥相互作用。我们概括了这种可能性，提出了一种新的形式主义，更新策略逻辑（USL）。在USL中，智能体也可以改进自己的策略。表达能力的提高提高了代理人“可持续能力”的概念。USL是由SL构建的。它主要给SL带来了以下两个方面的修改：语义上，给定状态的后继者不是由每个Agent的一个选择的数据唯一确定的。从语法上讲，我们在语言中引入了一个操作符，称为“unbinder”，它明确地删除了策略与代理的绑定。我们表明，USL是严格的表达比SL。
2013-03-04 cs.LO
Dependences in Strategy Logic
策略逻辑（SL）是一种非常有表现力的逻辑，用于指定和验证多智能体系统的属性：在SL中，人们可以量化策略，将它们分配给智能体，并表达结果的属性。这样一个强大的框架有两个缺点：第一，模型检验SL具有非初等的复杂性;第二，SL的确切语义是相当复杂的，可能不符合预期。在本文中，我们专注于SL的策略依赖，通过跟踪如何存在量化的策略在公式中可能（或可能不）取决于其他策略中选择的公式。我们研究了不同类型的依赖性，改进了[Mogavero等人，关于策略的推理：关于模型检查问题，2014]，并证明它们会产生不同的满意度关系。在设置策略可能只取决于他们所观察到的，我们确定了一个大的片段SL，我们证明模型检验可以在2 EXPTIME。
2017-08-19 cs.LO
Model checking strategy-controlled systems in rewriting logic
本文针对 Maude 内置 LTL 模型检测器无法验证策略控制规约的问题，提出策略感知扩展，并结合表达力分析、应用示例和性能比较验证其有效性。
2024-01-15 cs.LO
Navigability with Imperfect Information
Vassar College（瓦萨学院）
本文研究了自主智能体在迷宫中的可导航性，其中某些房间可能是不可区分的。在以前的工作中，作者已经表明，在这样的设置中的可导航性的属性取决于代理是否具有完美的回忆。具有完美回忆的智能体的可导航性是一种传递关系，而不具有完美回忆的智能体的可导航性是不传递的。本文介绍了一个有限的导航性的概念，并表明，一定形式的传递性持有有限的导航性，即使是没有完美的回忆代理。主要的技术成果是一个健全和完整的逻辑系统，描述了限制通航的属性。
2017-07-26 cs.AI cs.LO
Completeness for Two Left-Sequential Logics
左序贯逻辑提供了一种方法来推理（封闭的）命题项与原子命题，可能有副作用，并从左到右顺序评估。这样的命题术语通常用在程序设计语言中来指导程序的流程。在这篇论文中，我们探讨了两个这样的左序贯逻辑。首先，我们讨论完全求值左序逻辑，它采用完全求值策略，即，为了评估一个项，评估它的每一个原子命题，从而导致其可能的副作用发生。然后，我们转向短路（左序）逻辑，如[BP 10b]所示，其中评估可能是“短路”的，从而防止某些（如果不是全部）被评估的项中的原子命题。我们提出了评估树作为一个自然的语义逻辑，并提供公理化的最小识别的变体。由此，我们定义了一个逻辑与连接词，规定了一个完整的评估策略，以及连接词，规定了短路评估策略。
2012-06-09 cs.LO
A Logic for Strategy Updates
博弈论中的策略概念是静态的，可能是在博弈开始之前构建的。静态的、预先确定的策略概念在分析完美信息博弈时是不够的。因为，即使在完美的信息博弈中，我们人类也不会像这样制定策略--这主要是因为我们在逻辑上不是无所不知的，我们的计算能力有限，记忆有限。在本文中，我们专注于我们所谓的移动更新，其中一些移动在游戏过程中变得不可用。我们在这里的目标是提出一个正式的框架，移动为基础的战略限制扩展战略逻辑，这是由Ramanujam和西蒙。本文提出了一种动态的策略逻辑，证明了它的完备性和可判定性，以及策略逻辑的可判定性问题。我们还提出了一个分析蜈蚣使用我们的逻辑。
2011-07-25 cs.GT cs.LO
Alpaga: A Tool for Solving Parity Games with Imperfect Information
Alpaga是一个求解不完全信息的两人平价博弈的算法。给定博弈的描述，它确定第一个参与者是否能确保获胜，如果是，它构造获胜策略。该工具提供了一个基于反链的最新算法的符号实现。
2009-01-29 cs.GT cs.LO
Reasoning about Knowledge and Strategies: Epistemic Strategy Logic
Laboratoire IBISC -- Unversit\'e d'Evry
在本文中，我们介绍了认知策略逻辑（ESL），策略逻辑的扩展与个人知识的模态算子。这种增强的框架允许我们明确地表示和推理知识代理拥有自己的和其他代理的策略。我们提供了一个语义ESL的认知并发博弈模型，并考虑相应的模型检验问题。我们证明了模型检验ESL的复杂性并不比（非认知的）策略逻辑差
2014-04-03 cs.AI cs.LO
Reachability Games in Dynamic Epistemic Logic
我们定义的可达性游戏的基础上动态认知逻辑（DEL），玩家的行动被精细描述为DEL行动模型。我们首先考虑设置一个外部控制器与完美的信息与环境的相互作用，并旨在达到一些认识的目标状态关于系统的被动代理。我们研究了控制器的策略存在性问题，它概括了经典的认知规划问题，我们解决了几种类型的行动，如公共公告和公共行动。然后，我们考虑一个更丰富的设置，代理人本身是球员，其策略必须基于他们的观察。我们建立了几个（联合国）的分布式策略的存在问题的可判定性结果，根据玩家可以使用的行动类型，并将它们与文献中的结果与不完美信息的多人游戏。
2019-05-29 cs.LO
Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems
针对随机多智能体系统中策略能力模型检测的难题，本文提出带不完美信息的概率交替时间时序逻辑的假设-保证验证方案，证明其可靠性并讨论完备性，还提出捕获“最多达成φ”的非概率交替时间逻辑新变体。
2025-10-28 cs.LO cs.MA
Approximating Strategic Abilities under Imperfect Information: a Naive Approach
交替时间时序逻辑（ATL）允许指定的能力，不同的代理应该（或不应该）在一个多智能体系统中拥有的要求。然而，模型检验ATL规格在现实系统中是计算困难的。特别是，如果代理有不完善的信息，系统的全局状态，复杂性范围从Delta2P到不可判定的，这取决于语法和语义的细节。另一方面，交替认知μ演算的模型检验可以有明显较低的计算复杂性。在这项工作中，我们看看近似前一个问题的验证其“天真”的翻译到后者的想法。换句话说，我们看看当使用（不正确的）不动点算法来验证具有不完美信息的ATL公式时会发生什么。
2016-08-30 cs.LO cs.MA
Synthesising Full-Information Protocols
本文提出一种具有显式通信动作的不完美信息博弈模型，通过从不完美信息到完美信息博弈的通用归约模式及全信息协议构造，解决了正则获胜条件下的策略合成问题，并证明被动观察者数量在表达能力和复杂性上引发严格层级。
2024-02-13 cs.LO
Towards Assume-Guarantee Verification of Strategic Ability
本文提出使用假设-保证推理方法，促进对不完美信息和不完美回忆下的交替时间时序逻辑进行模型检测，以解决战略能力形式化验证的难题。
2023-10-24 cs.LO cs.MA
The Forms of Categorical Proposition
本文对直言命题的性质及其引起的逻辑问题作了详尽的考察。通过对术语逻辑和一阶逻辑的比较分析，指出著名的存在导入问题可以通过两种方式解决：一种是模型自适应策略，通过限制模型来验证对立方;另一种是语言自适应策略，通过扩展直言命题的逻辑形式来验证每个模型中的方。后一种策略是以逻辑的名义提倡的，这意味着每一个模型都是真理。最后，本文需要一些自动的过程，以确定任何一对之间的逻辑关系的性质的256个可用的直言命题。这就需要实现Prolog风格的编程机器。
2022-04-14 cs.LO
An Experiment of Randomized Hints on an Axiom of Infinite-Valued Lukasiewicz Logic
本文给出了一个由无穷值Lukasiewicz逻辑的公理（1）（2）（3）（4）得到公理（5）的自动推理随机提示策略的实验。在实验中，我们随机生成了一组大小从30到60不等的提示，用于指导定理证明器OTTER进行基于超分辨率的搜索。我们成功地在150 * 6个提示列表中找到了最有用的提示列表（包含30个子句）。此外，我们讨论了一个奇怪的非线性增长的生成子句推导公理（5）通过应用我们的随机提示策略。
2022-04-15 cs.LO
Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications
无功综合问题是找到一个有限状态控制器，满足给定的时间逻辑规范，而不管其环境的行为。开发一个正式的规格说明是一个具有挑战性的和乏味的任务，初始规格说明往往是不可实现的。在许多情况下，无法实现的根源是缺乏对系统环境的充分假设。本文考虑通过对环境添加假设来自动纠正线性时态逻辑的广义反应性（1）片段中给出的不可实现规范的问题。当一个时间逻辑规范是不可实现的，合成算法计算一个反策略作为证人。然后，我们的算法分析这种反策略，并合成一组候选环境假设，可用于从环境的可能行为中删除反策略。我们证明了我们的方法与几个案例研究的适用性。
2013-08-19 cs.FL cs.LO
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
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
Regular Games with Imperfect Information Are Not That Regular
研究不完全信息双人博弈中随机化策略的合成问题，提出正则博弈概念，证明在更一般模型中纯策略归约不适用，但在Buechi目标下随机化策略合成可判定。
2024-07-26 cs.GT cs.LO
Algorithms for Omega-Regular Games with Imperfect Information
我们研究了基于观察的策略，两个球员回合制游戏的图与欧米茄定期目标。基于观察的策略依赖于关于戏剧历史的不完全信息，即过去的观察序列。这样的游戏发生在一个控制器的合成中，该控制器看不到植物的私有状态。我们的主要结果是双重的。首先，我们给出了一个不动点算法，用于计算一组状态，从该状态中，玩家可以用确定性的基于观察的策略来赢得任何ω-正则目标。不动点是在状态集的反链格中计算的。该算法具有目标导向和避免在博弈图上构造显式子集的优点。其次，我们给出了一个算法，用于计算一个球员可以赢得概率为1的随机观察为基础的战略Buechi目标的状态集。这个集合很有趣，因为在没有完美信息的情况下，随机策略比确定性策略更强大。我们证明了我们的算法是最佳的匹配下界。
2007-11-02 cs.GT cs.LO
PDL as a Multi-Agent Strategy Logic
命题动态逻辑（PDL）是作为推理常规编程结构的逻辑而发明的。我们提出了一个新的视角PDL作为一个多智能体的战略逻辑（MASL）。这种策略推理逻辑将群体策略作为一等公民，并使博弈逻辑更接近标准模态逻辑。我们证明了MASL可以自然地表达博弈论，社会选择理论和投票理论的关键概念，我们给出了一个健全而完整的证明系统MASL，我们表明，MASL编码联盟逻辑。接下来，我们扩展的语言，认知多智能体战略逻辑（EMASL），我们给出的例子，它可以表达什么，我们建议使用它提出新的问题，在认知社会选择理论，我们给一个演算推理的自然类的认知博弈模型。最后，我们列出了未来研究的途径，并通过追踪与其他一些逻辑的联系来推理策略。
2013-10-23 cs.GT cs.LO
Hyper Strategy Logic
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出超策略逻辑（HyperSL），通过引入超属性支持多策略配置结果比较，捕捉SL无法表达的非干扰性、定量纳什均衡等属性，并提供可判定的模型检测算法及原型实现。
2024-03-20 cs.AI cs.LO cs.MA
Qualitative Concurrent Stochastic Games with Imperfect Information
我们研究了一个模型的游戏，结合并发性，不完美的信息和随机方面。这些是有限状态博弈，在每一轮中，两个参与者同时独立地选择一个行动。然后，根据前一个状态和参与者选择的一对行动，根据某个固定的概率分布来选择后继状态。不完全信息模型如下：两个玩家在状态上有一个等价关系，而不是观察确切的状态，他们只知道它属于哪个等价类。因此，如果某个参与者无法区分两种局部策略，那么他在这两种策略中的行为应该是相同的。我们考虑可达性（戏剧最终会访问最终状态吗？）和Büchi目标（是否发挥访问无限经常一个最终状态？）。我们的主要贡献是证明了以下问题是2-ExpTime完全的：决定第一个玩家是否有一个策略，确保她几乎肯定会赢得任何可能的策略，她oponent。我们还讨论了第一个几乎肯定会赢的玩家所需要的策略。
2011-08-30 cs.FL cs.GT cs.LO
Unattainability of Common Knowledge in Asymmetric Games with Imperfect Information
本文构建能力极端不对称的双人不完全信息博弈模型，并借助 Kripke 结构与认知逻辑证明当前博弈状态的共同知识无法达成。
2025-01-08 cs.GT cs.LO cs.MA
Strategic (Timed) Computation Tree Logic
本文定义了带战略算子的 CTL 和 TCTL 扩展（SCTL 和 STCTL），证明其表达力优于 ATL，并分析了不同信息与回忆语义下的模型检测复杂度，最终利用 IMITATOR 工具支持 STCTL[ir] 的实际应用。
2023-10-19 cs.LO cs.MA
On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts
Institute of Mathematics and Informatics, Bulgarian Academy of Sciences（保加利亚科学院数学与信息学研究所）
本文提出在具有策略上下文的ATL中通过翻译方法处理偏好与量化，以更简洁地表达纳什均衡等博弈解概念，并转化为QCTL进行算法推理。
2026-02-11 cs.LO cs.MA
IMITATOR4AMAS: Strategy Synthesis for STCTL
LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord（索邦巴黎北大学）；Ecole Centrale de Nantes（南特中央理工学院）；Institute of Computer Science, Polish Academy of Sciences（波兰科学院计算机科学研究所）
IMITATOR4AMAS是首个支持在参数时序自动机网络上对STCTL进行记忆less不完全信息策略合成的工具，实验显示其效率显著优于先前方法。
2026-02-11 cs.LO cs.MA
Runtime Verification via Rational Monitor with Imperfect Information
针对传统运行时验证假设信息完美且监控器被动的局限，本文扩展线性时序逻辑属性验证，使监控器在信息不完全时理性决策，并通过机器人系统案例验证了可行性。
2024-08-21 cs.FL cs.LO cs.SE
Together We Know How to Achieve: An Epistemic Logic of Know-How (Extended Abstract)
Vassar College（瓦萨学院）；Lafayette College（拉斐特学院）
达成目标的联盟战略的存在并不一定意味着联盟有足够的信息来知道如何遵循该战略。这也不意味着联合政府知道这种战略的存在。本文研究了分布式知识、联盟策略和联盟“专有技术”策略之间的相互作用。主要的技术成果是一个健全和完整的三模态逻辑系统，描述了这种相互作用的性质。
2017-07-27 cs.AI 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
From rules to runs: A dynamic epistemic take on imperfect information games
Peking University（北京大学）
在博弈论的文献中，对广义博弈的信息集有不同的解释，这可能导致混乱和悖论的情况。我们认为，问题在于混淆了两种解释的广泛形式的游戏结构：游戏规则或游戏运行并不总是一致的。在本文中，我们试图分离和连接这两种观点，提出了一个动态的认知框架，我们可以计算运行一步一步从游戏规则加上给定的假设的球员。我们提出了一种模态逻辑来描述博弈者的知识及其在博弈过程中的变化，并提供了一个完整的公理化。我们还表明，在一定条件下，混合的规则和运行是无害的，由于两者的结构相似性。
2015-12-07 cs.AI cs.GT cs.LO
Tableaux for the Logic of Strategically Knowing How
Nankai University（南开大学）；College of Philosophy, Nankai University（南开大学哲学院）
本文为多智能体策略性知道如何逻辑提出了表推演过程，证明了其可靠性与完备性，并证明该逻辑的可满足性问题可在 PSPACE 内判定。
2023-07-11 cs.AI cs.LO
The Logic of Doxastic Strategies
Institute of Logic and Intelligence, Southwest University（西南大学逻辑与智能研究所）；University of Southampton（南安普顿大学）
本文针对有理由相信可达成目标但无十足把握的策略提出“doxastic（信念）策略”概念，并构建了描述其与信念模态相互作用的可靠完备逻辑系统。
2023-12-13 cs.AI cs.LO
Satisfiability of ATL with strategy contexts
时态逻辑ATL的各种扩展最近被引入到表达多智能体系统的丰富属性。其中，ATLsc扩展了ATL的策略上下文，而策略逻辑具有一阶量化策略。这些逻辑的丰富表现力是有代价的：模型检查是非初等的，可满足性是不可判定的。本文证明了可满足性在几种特殊情况下是可判定的。最重要的一点是限制在回合制游戏中。我们证明，决策性也持有并发游戏，如果移动的数量可供代理是有界的。最后，我们证明了限制策略量化无记忆策略带来了不可判定性。
2013-07-17 cs.GT cs.LO cs.MA
Together We Know How to Achieve: An Epistemic Logic of Know-How
达成目标的联盟战略的存在并不一定意味着联盟有足够的信息来知道如何遵循该战略。这也不意味着联合政府知道这种战略的存在。本文研究了分布式知识、联盟战略和联盟“专有技术”战略之间的相互作用。主要的技术成果是一个健全和完整的三模态逻辑系统，描述了这种相互作用的性质。
2017-06-15 cs.AI cs.GT cs.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
