从ATL到STIT
From ATL to Stit
摘要：
我提出了一个技术嵌入到STIT理论的交替时间时序逻辑。
英文摘要：
I present a technical embedding of alternating-time temporal logic into stit theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
相关论文
交替时序逻辑ATL +中构造性可满足性测试和模型综合的最优表格法
Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temporal Logic ATL+
我们开发了一个健全的，完整的，实际上可实现的基于表格的决策方法建设性的可满足性测试和模型合成的片段ATL+的完整交替时间时序逻辑ATL*。该方法扩展了一个基本的方式以前开发的基于表格的ATL的决策方法和工程在2EXPTIME，这是最佳的最坏情况下的可满足性问题的ATL+的复杂性。我们还讨论了如何适当的参数化和语法限制输入ATL+公式类可以降低可满足性问题的复杂性。
cs.LO
交替时间时态逻辑的博弈论语义
Game-Theoretic Semantics for Alternating-Time Temporal Logic
我们介绍了交替时间时态逻辑（ATL）的博弈论语义（GTS）的版本。在GTS中，真理被定义为在语义评估博弈中获胜策略的存在，因此博弈论的视角出现在ATL的框架中的两个语义层面上：在策略算子的标准语义中的对象层面上，以及在元层面上，博弈论的逻辑语义被应用于ATL。我们统一这两个角度到专门为ATL设计的语义评估游戏。博弈论的角度，使我们能够确定新的变体的ATL语义的基础上限制的时间资源提供给验证者和证伪者的语义评估游戏。我们介绍和分析一个无界和（序数）有界的GTS，并证明这些是等价的标准（塔斯基风格）的成分语义。我们证明了在这两个版本的GTS中，ATL公式的真值总是可以在有限时间内确定的，即，而不需要构建无限的路径。我们还介绍了一个不等价的有界语义，并认为这是自然的逻辑和博弈论的角度来看。
cs.GTcs.LOmath.LO
多变量分支和交替时序逻辑的复杂性和表达性
Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
我们证明了分支时间时序逻辑CTL和CTL*，以及交替时间时序逻辑ATL和ATL*，在具有单个命题变量的语言中与在完整语言中一样具有语义表达性，即，有无限的命题变量由此可见，对于CTL和ATL，用单个变量的可满足性是EXPTIME-完全的，而对于CTL* 和ATL*，用单个变量的可满足性是2 EXPTIME-完全的，即，对于这些逻辑，只有一个变量的公式的可满足性与任意公式的可满足性一样困难。
cs.LO
具有有限存储策略的交替时序逻辑
Alternating-time temporal logic with finite-memory strategies
不完全信息的交替时序逻辑ATL和ATL* 的模型检查对于完美召回语义是不可判定的。然而，当限制到无记忆策略的模型检查问题变得可判定。在本文中，我们考虑其他两种类型的语义有限记忆策略的基础上。一种是允许的内存大小有界，另一种是内存大小无界（但必须是有限的）。这是由具有完美召回语义的模型检查的高复杂性和无记忆策略的严重限制所激发的。我们表明，这两种类型的语义介绍是不同的完美召回和无记忆语义和下一个重点的可判定性和复杂性的模型检查在完整和不完整的信息游戏ATL/ATL*。特别是，我们证明了模型检测的复杂性与有界记忆语义是Delta_2 p-完全的ATL和PSPACE-完全的ATL* 在不完全信息的游戏，就像在无记忆的情况下。我们还提出了一个证明，ATL和ATL* 模型检查是不可判定的n >= 3的球员与有限记忆语义的不完全信息游戏。
cs.GTcs.LO
不完全信息下ATL的Hennessy-Milner定理
A Hennessy-Milner Theorem for ATL with Imperfect Information
我们表明，一个基于历史的变种交替互模拟与不完美的信息允许它与一个变种的交替时间时序逻辑（ATL）的不完美的信息由一个完整的Hennessy-Milner定理。ATL的变体，我们认为有一个共同的知识语义，这要求统一的策略，可用于联盟，以实现某些目标必须是共同的知识联盟内部，而其他语义变体的ATL不完美的信息不适应Hennessy-Milner定理。我们还表明，存在一个基于历史的交替互模拟两个有限的并发博弈结构与不完全信息（iCGS）是不可判定的。
cs.LOcs.MA
使用交替时序逻辑（ATL）为信念-愿望-意图（BDI）智能体生成计划
Generating Plans for Belief-Desire-Intention (BDI) Agents Using Alternating-Time Temporal Logic (ATL)
Department of Systems and Computer Engineering（系统与计算机工程系）；Carleton University（卡尔顿大学）
本文提出一种基于交替时序逻辑（ATL）自动生成BDI智能体计划的工具，以支持多智能体系统中的竞争与合作，并通过协作游戏验证了计划能够帮助智能体成功实现共同目标。
cs.AIcs.LOcs.MA
更多相关论文收起更多论文
为学习而博弈，或为保密而博弈：交替时序逻辑遇见信息论
Playing to Learn, or to Keep Secret: Alternating-Time Logic Meets Information Theory
本文提出逻辑ATLH，基于哈特利不确定性度量扩展交替时序逻辑，用于量化智能体关于事实的知识不确定性，并证明其与ATLK表达力相同但指数级更简洁。
cs.LOcs.MA
ATL +的博弈语义及其在模型检测中的应用
Game-Theoretic Semantics for ATL+ with Applications to Model Checking
我们开发了完整的交替时间时态逻辑ATL* 的片段ATL+的博弈论语义（GTS），基本上扩展了最近推出的GTS ATL。我们首先表明，新的博弈论语义是等价的ATL+的标准语义（基于完美的召回策略）。然后，我们提供了一个分析，基于新的语义，模型检查ATL+所需的内存和时间资源。基于此，我们确定仅使用非常有限的内存量的策略就足以满足ATL+的需求。此外，使用GTS，我们提供了一个新的算法模型检查的ATL+和确定一个自然的层次结构的易处理的片段ATL+扩展ATL。
cs.GTcs.LOmath.LO
认知$μ$ -微积分的表达能力
The Expressive Power of Epistemic $μ$-Calculus
虽然$μ$演算臭名昭著地包含交替时间时序逻辑（ATL），我们发现，认知$μ$演算不submergentATL与不完美的信息（ATL $_i$）的同步完美召回语义。为了证明这一点，我们首先建立跳跃奇偶校验树自动机（JTA），最近推出的交替奇偶校验树自动机的扩展，表示等价于认知$μ$ -演算，这对任何知识语义。利用这一结果，我们还表明，对于有界记忆语义，认知$μ$演算是不是比标准的$μ$演算更有表现力，它的可满足性问题是EXPTIME完全的。
cs.LO
单计数器博弈模型的模型检验定量交替时序逻辑
Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models
我们考虑定量扩展的交替时间时序逻辑ATL/ATL称为定量交替时间时序逻辑（QATL/QATL），其中计数器的值可以比较使用等式，不等式和模约束的常数。我们解释这些逻辑在一个计数器的游戏模型，这是无限的持续时间的游戏有限的控制图，每个过渡可以增加或减少一个无界计数器的值。也就是说，这些游戏的状态空间通常是无限的。我们考虑的模型检验问题的逻辑QATL和QATL的一个计数器的游戏模型与VASS语义，我们开发的算法，并提供匹配的下界。我们的算法是基于减少的模型检验问题的模型检验游戏。这种方法使我们很容易处理扩展的逻辑语言以及无限的状态空间。该框架一方面概括了定性问题，如有限状态系统的ATL/ATL模型检验、单计数器过程上的分支时间时序逻辑CTL和CTL的模型检验以及LTL规范的可实现性问题。另一方面，QATL/QATL的模型检验问题推广了定量问题，如能源博弈（在QATL的情况下）和能源平价博弈（在QATL的情况下）的固定初始信用问题。我们的结果是积极的，因为我们表明，泛化是不是太昂贵的复杂性。作为一个副产品，我们获得了新的结果的复杂性模型检验CTL在一个计数器的过程中，并表明，决定赢家在一个计数器的游戏与LTL的目标是2 ExpSpace完成。
cs.LO
鲁棒交替时间时序逻辑
Robust Alternating-Time Temporal Logic
本文提出扩展自ATL/ATL*的鲁棒交替时间时序逻辑rATL与rATL*，通过多值语义实现多智能体系统鲁棒策略推理，验证其模型检测与可满足性问题未增加计算复杂度。
cs.LO
论ATL的表达性和复杂性
On the Expressiveness and Complexity of ATL
ATL是面向多代理系统中属性的规范和验证的时态逻辑。它允许的原因上存在的战略联盟的代理人，以执行一个给定的属性。在本文中，我们首先精确地描述了交替迁移系统和并发博弈结构上的ATL模型检测的复杂性时，代理的数量是不固定的。我们证明了它是Δ^P_2 -和Δ ^P_3-。3-完整，取决于底层的多代理模型（分别为ATS和CGS）。我们还考虑了ATL的一些扩展的相同的问题。然后，我们考虑表达问题。我们展示了ATS和CGS是如何相关的，并提供这些模型之间的翻译。交替互模拟我们还证明了ATL的标准定义（建立在模态“Next”，“Always”和“Until”上）不能表达其模态的连续性：有必要明确地添加模态“Release”。
cs.GTcs.LOcs.MA
带析取显式策略的交错时间μ-演算
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。
cs.AIcs.LO
ATL * 在不完全信息和完全召回下的判定性结果
Decidability results for ATL* with imperfect information and perfect recall
交替时间时序逻辑（ATL*）是多智能体系统的核心逻辑。它的扩展到不完美的信息设置（ATL*i）是众所周知的，有一个不可判定的模型检查问题时，代理有完美的回忆。因此，研究主要集中在没有记忆的代理，或替代语义检索决策。在这项工作中，我们建立了新的决策结果与完美的回忆代理：我们首先证明了一个元定理，允许转移的决策结果类的多人游戏与不完美的信息，如游戏与层次观察，ATL*i的模型检查问题。然后，我们建立了模型检验ATL* 的战略背景和不完善的信息是可判定的限制时，层次实例。
cs.LO
在具有策略上下文的交替时间时序逻辑中关于定性偏好的问题
On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts
Institute of Mathematics and Informatics, Bulgarian Academy of Sciences（保加利亚科学院数学与信息学研究所）
本文提出在具有策略上下文的ATL中通过翻译方法处理偏好与量化，以更简洁地表达纳什均衡等博弈解概念，并转化为QCTL进行算法推理。
cs.LOcs.MA
不完全信息和完全召回语义下的模型检验ATL是不可判定的
Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
我们提出了一个形式化证明的不完全信息和完美召回语义下的交替时间时序逻辑的模型检验问题的不可判定性。这个问题被宣布为不可判定的根据个人通信的多人游戏与不完美的信息，但没有正式的证明曾经公布。我们的证明是基于直接减少从非停机问题的图灵机。
cs.LOcs.MA
带有平均收益保证的交替时间时序逻辑
Alternating-Time Temporal Logic with Mean-Payoff Guarantees
Heriot-Watt University（赫瑞-瓦特大学）
本文提出带合取平均收益约束的ATL*扩展ATL*_mp，分析其模型检验复杂度、记忆层级等性质，证明有限记忆策略可实现低于完美记忆上确界的所有阈值，还关联了合作理性验证。
cs.GTcs.LOcs.MA
将认知ATL的效度还原为认知CTL的效度
Reducing Validity in Epistemic ATL to Validity in Epistemic CTL
Institute of Mathematics；Informatics Bulgarian Academy of Sciences Sofia, Bulgaria
我们提出了一个有效性保持翻译的一个子集的认知交替时间时序逻辑（ATL）的认知计算树逻辑（CTL）。已知所考虑的认知ATL子集具有有限模型性质和可判定的模型检验。这需要有效性的可判定性，但隐含的算法是不可行的。将有效性问题减少到相应的CTL系统中，使得该逻辑的自动演绎技术可用于处理明显更复杂的ATL系统。
cs.AIcs.LOcs.MA
论交替时间时序逻辑、超性质与策略共享
On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
针对交替时间时序逻辑ATL$^*$无法比较多策略交互、无法要求智能体共策略的局限，提出扩展逻辑HyperATL$^*_S$，支持超性质下的策略交互比较与策略共享，证明其模型检测可判定并实现工具HyMASMC完成基准评估。
cs.AIcs.LOcs.MA
MsATL：一个基于SAT的ATL可满足性检查工具
MsATL: a Tool for SAT-Based ATL Satisfiability Checking
本文提出MsATL工具，结合SAT求解器与ATL模型检查器，支持判定不完美信息下ATL的可满足性及游戏合成。
cs.LOcs.MA
ATL中战略能力的提炼与委派
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中不再出现该运算符。
cs.GTcs.LOcs.MA
不完全信息下的战略能力近似：一种朴素的方法
Approximating Strategic Abilities under Imperfect Information: a Naive Approach
交替时间时序逻辑（ATL）允许指定的能力，不同的代理应该（或不应该）在一个多智能体系统中拥有的要求。然而，模型检验ATL规格在现实系统中是计算困难的。特别是，如果代理有不完善的信息，系统的全局状态，复杂性范围从Delta2P到不可判定的，这取决于语法和语义的细节。另一方面，交替认知μ演算的模型检验可以有明显较低的计算复杂性。在这项工作中，我们看看近似前一个问题的验证其“天真”的翻译到后者的想法。换句话说，我们看看当使用（不正确的）不动点算法来验证具有不完美信息的ATL公式时会发生什么。
cs.LOcs.MA
基于交替Büchi下推系统的共享资源有界系统的模型检验
Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems
资源受限的多智能体系统的验证一般是不可判定的。在许多这样的设置中，资源对于代理是私有的。本文研究了基于交替时序逻辑（ATL）的资源逻辑在共享资源下的模型检验问题。资源可以被消耗和生产到任何数量。我们表明，模型检验问题是不可判定的，如果两个或两个以上的这样的无界资源。我们的主要技术成果是，在一个单一的共享资源的情况下，问题变得可判定。虽然直观，可判定性的证明是不平凡的。我们减少模型检验的问题交替Büchi下推系统。一个中间结果连接到一般的基于自动机的验证：我们表明，模型检验计算树逻辑（CTL）（紧凑）交替Büchi下推系统是可判定的。
cs.LO
通过 Effectivity Frames 实现 Alternating-Time μ-Calculus 的高效模型检测
Efficient Model Checking for the Alternating-Time μ-Calculus via Effectivity Frames
本文探讨基于 effectivity frames 实现 alternating-time μ-calculus 模型检测，发现大型系统中转换开销可被后续检测收益抵消，性能优于传统方法。
cs.LO
多智能体系统中战略能力逻辑的表格决策方法
Tableau-based decision procedures for logics of strategic ability in multi-agent systems
University of the Witwatersrand（威特沃特斯兰德大学）
我们开发了一个增量的基于表的决策过程的交替时间时序逻辑ATL和它的一些变种。虽然在理论上建立的复杂性上限内运行，我们声称，我们的画面实际上是更有效的平均情况下，比其他决策程序ATL已知的。此外，其适应ATL的变体的容易性证明了所提出的程序的灵活性。
cs.AIcs.LOcs.MA
技术报告：资源约束的ATL模型检验及资源的生产和消耗
Technical Report: Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources
文献中已经提出并研究了几种表示资源约束下联盟能力的逻辑。已有的工作表明，如果只考虑资源的消耗，或者系统中任意路径上产生或消耗的资源总量是有界的，那么几种标准逻辑（如资源有界联合逻辑（RB-CL）和资源有界交替时序逻辑（RB-ATL））的模型检验问题是可判定的.然而，对于具有无限资源生产和消费的联盟逻辑，只知道一些不可判定性结果。本文证明了资源无限生产和无限消耗的RB-ATL的模型检验问题是可判定的，但是EXPSPACE困难的.我们还调查了一些易于处理的情况下，并提供了一个详细的比较，资源逻辑RAL的一个变种，连同新的复杂性结果。
cs.LOcs.MA
具有知识、不完全信息、完全回忆和通信联盟的交替时序逻辑的模型检验
Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
我们提出了一个变体的ATL与分布式知识运营商的基础上同步和完善的召回语义。这种逻辑中的联盟模式是基于对完整历史的部分观察，并结合了联盟成员之间的合作形式，其中代理基于该联盟的系统历史的分布式知识发布其行动。我们表明，模型检验是可判定的这种逻辑。该技术利用两个变种的游戏与不完美的信息和部分可观察的目标，以及一个子集的建设，用于识别状态的历史是无法区分的考虑联盟。
cs.LOcs.MA
通过约束求解学习CTL和ATL中的分支时间性质
Learning Branching-Time Properties in CTL and ATL via Constraint Solving
本文研究从Kripke结构和并发博弈结构样本中学习CTL与ATL公式的问题，通过将学习问题编码为可满足性问题并结合不动点模型检测算法进行符号化求解，并在Python原型中验证了方法的有效性。
cs.LO
简洁多智能体系统中策略能力验证的复杂性
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}完全，修正了相关旧结果并明确了主观语义下的复杂度性质。
cs.LO
CGAAL：具备启发式方法的分布式即时ATL模型检验器
CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics
本研究提出分布式即时ATL模型检验器CGAAL，通过带否定边的扩展依赖图编码ATL，结合多种定制启发式搜索策略，在多类案例中性能显著优于PRISM-games及传统搜索策略。
cs.LO
一种面向自然策略能力的模型检测器
A Model Checker for Natural Strategic Ability
本文提出并实现了一个集成于开源模型检测器VITAMIN中的NatATL模型检测工具，支持无记忆与带回忆策略，将有限理性策略推理理论转化为可实际验证多智能体系统的框架。
cs.LOcs.MA
若我能的话：多智能体系统中行动动态的推理
I Would If I Could: Reasoning about Dynamics of Actions in Multi-Agent Systems
University of Bergen（卑尔根大学）；Örebro University（厄勒布鲁大学）；CNRS（法国国家科学研究中心）；Université Sorbonne Paris Nord（索邦巴黎北大学）
本文提出ATL-D和ATEL-D，用于建模智能体行动的动态授予与撤销过程及其对知识的影响，探讨了逻辑表达力、规范系统关系及计算复杂性。
cs.LOcs.MA
带抽象的 Timed ATL 的即时符号算法
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions
本文在 ADG 框架中提出 TATL 的即时符号验证算法，并通过推广包含检查与新型抽象显著加速，性能优于朴素方法及 Uppaal Tiga。
cs.LO
学习时序性质的复杂性
The Complexity of Learning Temporal Properties
本文研究LTL、CTL和ATL时序逻辑被动学习问题的计算复杂性，证明无界二元运算符情况下均为NP完全，并揭示有界情况下不同逻辑间的复杂性差异。
cs.LO
平坦余代数不动点逻辑的完备性
Completeness of Flat Coalgebraic Fixpoint Logics
模态不动点逻辑传统上在计算机科学中起着核心作用，特别是在人工智能和并发性中。μ演算和它的亲属是这类逻辑中最具表现力的。然而，流行的定点逻辑倾向于用表达性来换取简单性和可读性，事实上，它经常存在于μ演算的单个变量片段中。这种平坦定点逻辑的家族包括，例如，LTL、CTL和常识逻辑。将这一概念扩展到共代数逻辑的通用语义框架，使得能够覆盖标准μ演算之外的广泛逻辑，例如，分级μ演算和交替时间μ演算（如交替时间时序逻辑ATL）的平坦片段，以及概率和单调不动点逻辑。我们给出了一个通用的完整性证明的Kozen-Park公理化这样平坦的余代数不动点逻辑。
cs.LO
博弈策略：时间与认知视角
Strategies in Sabotage Games: Temporal and Epistemic Perspectives
Technical University of Denmark（丹麦技术大学）
本文从时间视角用ATL$^\ast$分析Sabotage游戏，并探讨其认知扩展中的玩家不确定性，为动态图的时间属性推理提供新框架。
cs.LOcs.MA
并发多人博弈中联盟目标分配的时序逻辑
The temporal logic of coalitional goal assignments in concurrent multi-player games
我们介绍和研究交替时间时序逻辑ATL的自然扩展，称为联盟目标的时序逻辑（TLCGA）。它的特点是只有一个，但很有表现力，联盟战略运营商，即联盟目标分配运营商，这是基于映射分配给游戏中的每组球员的联盟目标，形式化的TLCGA语言的路径公式，即一个公式前缀与时间运营商X，U，或G，代表相应的联盟的时间目标，描述满足该目标的策略的属性。建立了TLCGA的μ-演算扩展中时间目标分配的不动点刻画，讨论了它的表达性并举例说明，证明了它相对于适当定义的互模拟概念的互模拟不变性和Hennessy-Milner性质，构造了TLCGA的一个完善的公理系统，并通过有限模型性质得到了它的可判定性.
cs.GTcs.LOcs.MA
