可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）215-228www.elsevier.com/locate/entcs具有价格资源代理人的联盟博弈逻辑Dario Della Monica1 玛格丽特那不勒斯2 Mimmo Parente3Dipartimento di InformaticaUniversit`adiSalerno意大利摘要交替时间时序逻辑（ATL）和联盟逻辑（CL）是建立良好的逻辑形式主义，特别适合于对代理的动态联盟（例如，系统和代理）之间的游戏进行建模环境）。 最近，ATL形式主义已被扩展，以考虑有界性执行任务所需的资源。由此产生的逻辑，称为资源绑定ATL（RB-ATL），已经在相当多的场景。针对扩展ATL处理资源边界的模型检验问题通常是不可判定的，提出了一种RB-ATL在本文中，我们介绍了一种新的形式主义，称为PRB-ATL，基于不同的概念的资源界限，我们表明，其模型检测问题仍然是EXPTIME并且具有PSPACE下限。然后，我们解决联盟形成的问题。代理人如何以及为什么应该聚集并不是一个新的问题。问题，并已深入研究，在过去和近年来，在各种框架，例如在算法博弈论，论证设置，和基于逻辑的知识表示。我们在设置具有ATL公式指定的目标的定价资源受限代理时面临这个问题。特别是，我们解决的问题，确定最小成本联盟的代理人采取行动，根据涉及由定价游戏场所表示并满足给定公式的规则。我们证明了这样的问题在计算上并不比用固定联盟验证相同公式的满足性更难关键词：多智能体系统，联盟逻辑，有限资源，模型检测，联盟形成1引言多智能体系统的自动验证是人工智能领域最近文献中的一个重要主题[1]。对这类系统建模的需求激发了逻辑形式主义，最著名的是交替时间时态逻辑[4]和联盟逻辑（CL）[10，11]，面向集体行为的描述1电子邮件：ddellamonica@unisa.it2电子邮件：napoli@dia.unisa.it3电子邮件：parente@unisa.it1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.10.017216D. Della Monica等人/理论计算机科学电子笔记278（2011）215这种逻辑的思想是，智能体可以加入团队（或联盟）并共享资源来完成任务（达到目标）。特别是，交替时间时态逻辑已经在[4]中引入，其中完整的交替时间时态语言，用ATL表示，已经提出，以及两个重要的片段，即ATL和ATL+。这些逻辑是开放系统的自然规范语言，即其行为取决于与外部实体（通常称为环境）的交互的系统。在[9]中，Goranko研究了两种形式主义（的表达能力）之间的关系。特别是，他已经表明，CL可以嵌入ATL。最近，这两种逻辑已被用于多智能体系统（MAS）的验证，其中智能体配备了有限的资源来实现其目标[2，3，6，7]（更多关于这一点在下面的相关工作部分我们在这里提出的框架取决于这些方法，并代表了进一步的形式化，这样的复杂系统：多代理系统，其中代理可以合作执行任务，并受到有限的可用资源，这是一个内在的功能，大多数现实世界的系统。特别是在[2，3，6，7]中提出的形式主义的公式允许人们通过所谓的团队运营商（借用ATL）将资源分配给代理人。然后，问题是要确定是否在支持者团队的代理有一个策略，以执行指定的目标，有界的资源量，无论对手团队的代理做什么。无论如何，这种有界性的处理存在一些缺陷，我们将在下面指出基于自然观察，为了获得一种资源，有一个价格要支付，通常也取决于市场上的资源的可用性，我们建议考虑有限的资源，每个有一个价格要支付的代理人在实现目标。因此，与现有的方法不同，代理人配备了一定数量的资金，而不是资源的禀赋。金钱在某种意义上是一种元资源。 一方面，它的引入是必不可少的，以模拟自然的情况下，获取执行任务所需的资源，有一个价格取决于几个因素：对他们的全球可用性，代理，并在当前的系统状态。另一方面，货币具有“衡量”所有资源价值的特性最小化获得执行任务所需的资源所需的金额）。在以前的方法中，资源有界性的概念在某种程度上是弱的，在这个意义上，资源边界只出现在公式中，并且只应用于支持者团队，但它们根本不在模型中表示。这意味着可以询问一个团队是否可以在给定的资源量下达到目标，但不可能跟踪世界上资源可用性的演变（特别是，由于对手的行动而导致的资源消耗不受控制）。例如，考虑公式[3]中提出的形式主义。 它直观的语义是，团队A可以使用由b限定的资源量来保证p总是保持，而与对手（AG\A）的行为无关。的典范D. Della Monica等人/理论计算机科学电子笔记278（2011）215217这个公式必须包含一个循环，其中A队中的智能体的联合行动不消耗资源，但对手队中的智能体的联合行动可能消耗资源，导致资源的无限消耗。我们认为，这种行为是不现实的。因此，我们引入了一个概念，在市场上（或在自然界中）的资源的全球可用性的发展取决于双方的支持者和对手的行为。这种资源是共享的，在这个意义上，所有的代理人从共享池中提取资源，并且代理人（独立地，如果代理人属于支持者或对手团队）获取资源意味着资源将以较小的数量可用。这里使用的货币概念与[3]中使用的资源概念有几处相似之处。事实上，这里给代理人钱来执行任务（就像[3]中给代理人资源一样此外，对手的金钱消耗不受控制（如[3]中对手的资源消耗与其他资源不同，金钱可以被认为是一种私人（非共享）资源。此外，对手拥有无限的经济力量，在这个意义上，对手大致来说，对方什么都可以买，除了已经不存在的资源另一个在文献中没有充分分析的方面是产生资源的行动一方面，在[2，3]中，动作只能消耗资源;另一方面，在[7]中，作者指出，只要动作可以产生资源，模型检查问题就是不可判定的。可以很容易地说，不确定性来自于资源生产的无限性，因此我们自然地限制了行动生产资源的方式：一个行动生产的资源数量可能不超过迄今为止已经消耗的数量。这样一个概念是有意义的，因为在实践中，它允许人们对重要的现实世界场景进行建模，例如，通过程序获取内存，在旅行期间租赁汽车，以及一般情况下，代理释放先前获得的资源的最后，我们还要解决组建联盟的问题。代理如何以及为什么应该聚合并不是一个新问题，并且在过去和近年来，在各种框架中进行了深入研究，例如在算法博弈论，论证设置和基于逻辑的知识表示中（见[8，5]）。我们在设置具有ATL公式指定的目标的定价资源受限代理时面临这个问题。特别是，我们解决的问题，确定最小成本联盟的代理人按照规则表示的定价游戏舞台，并满足给定的公式。我们证明了模型检测问题和最优联盟问题都是在EXPTIME中的，并且有一个PSPACE下界。相关作品。在[2]中，Alechina等人引入了逻辑RBCL，其语言扩展了CL语言，并显式表示了资源边界。在[3]中，同一作者提出了ATL的类似扩展，称为RB-ATL，并给出了一个218D. Della Monica等人/理论计算机科学电子笔记278（2011）215模型检验程序运行时间为O（|ϕ|2·r +1×S），其中，r是要检查的公式，S是模型，r是资源数。因此，如果资源的数量被视为常数，RB-ATL的模型检测问题是在PTIME中。然而，确定模型检查问题的下限的问题，特别是，是否存在PTIME算法，即使资源的数量不被视为一个恒定的因素是开放的。在[7]中，Bulling和Farwer引入了RAL和RAL。前者代表了Alechina等人的推广。的RB-ATL，后者是ATL的扩展，具有有限的资源。作者研究了几个语法和语义的变体RAL和RAL的模型检测问题的（非）可判定性特别是，虽然以前的方法只考虑消耗资源的行动，但它们引入了产生资源的行动的概念。事实证明，这样一个新的概念，使模型检测问题不可判定。本文的结构如下。在下一节中，我们将考虑定价资源的逻辑形式化，然后在第3节中，我们分析模型检查问题的复杂性，并在第4节中处理寻找最佳联盟的问题。最后，我们对未来的研究方向提出了一些思考。2PRB-ATL的逻辑形式化在本节中，我们定义了逻辑PricedRB-ATL（PRB-ATL）。我们首先介绍一些符号，我们将在本文的其余部分使用。代理的集合是AG ={1，2，...，n}，团队是AG的任何子集。资源类型的集合，也简称为资源，是R ={R1，R2，...，其中，R1表示资 源 “ 时 间 ” 。 本 文 将 使 用 数 字 n 和 r 分 别 表 示 代 理 和 资 源 的 数 量 。 设 M=（ N<${∞} ） r 表 示 市 场 上 （ 或 自 然 界 中 ） 资 源 的 全 局 可 用 性 集 合 ， N=（N<${∞}）n表示代理人的货币可用性集合，其中N是非负整数集合.给定一个货币可用性$∈ N，我们用$[a]表示代理人a的货币可用性，对于每个a∈ AG。最后，集合是原子命题的有限集合。PRB-ATL的公式由以下文法给出：：：= p |¬ϕ |ϕ ∧ ϕ|价格A$|⟨ ⟨A$⟩⟩ϕU ϕ|中国A$中国Q|布其中p∈M，A∈ AG，A ∈ {<，≤，=，≥，>}，b∈ M，$∈ N。直观地说，这类公式测试了市场上资源的当前可用性。公式A $A$，其中∈{，U，Q}，表明团队A有一个策略，使得对于对手（即AG\A）执行的每个动作，都是满意的，并且每个代理人a ∈ A的总费用小于或等于$[a]。在不损失一般性的情况下，我们可以证明对eacha∈/A，该逻辑的公式相对于定价游戏结构和资源的初始可用性（的位置）进行评估直观地说，一个定价博弈结构G是一个图，其顶点（称为位置）由原子命题标记。D. Della Monica等人/理论计算机科学电子笔记278（2011）215219布雷尔在每个位置，每个代理都可以在要执行的非空操作集合中进行选择。任何可能的动作组合都会产生转换，即图的边。一般来说，行动消耗和生产资源。每一种资源的价格都是可变的，并且取决于该资源目前在市场上的可获得性。因此，如果执行动作所需的资源可用，并且团队的代理有足够的钱来获得它们，则可以执行转换。我们将求和操作扩展到向量分量之间的求和。此外，我们使用向量之间的通常分量比较关系，并将k0 s的向量表示为0k当向量的大小明确时，我们将简单地写为0 。 最 后 ， 关 于 和 运 算 的 ∞ 的 行 为 像 往 常 一 样 定 义 ， 即 对 于 每 个 常 数 c ，∞+c=c+∞=∞+∞=∞。形式上，定价博弈结构的定义扩展了[4]和[3]中分别给出的并发博弈结构和资源受限并发博弈结构的定义。定义2.1[定价博弈结构]一个定价博弈结构G被定义为一个元组Q，π，d，qty，δ，ρ，m0，其中：• Q是位置的有限集合。• π：Q→2Π是赋值函数。• d：Q×AG →N是行动函数，它定义了在每个位置q∈Q上每个智能体a∈ AG可以采取的行动。我们假设每个智能体在每个位置至少有一个可用的动作，可以认为这是不做任何事情的动作，并且在不损失一般性的情况下，我们假设它总是第一个，因此用自然数1表示。因此，我们有d（q，a）≥1，对于每个a∈ AG，q∈Q。给定一个团队A，一个行动轮廓αA是一个向量，它为每个智能体a∈A分配一个行动。行动剖面代表一个团队的联合行动。对于每个位置q∈Q并且队A ={a1，...，ak}AG，我们用DA（q）表示在位置q处团队A可用的动作轮廓集，定义为DA（q）={1，.，d（q，a1）}×. × {1，.，d（q，ak）}。为了便于阅读，我们用D（q）表示DAG（q）。给定一个团队A，一个智能体a∈A，和一个动作轮廓αA，我们将向量αA对应于智能体a的分量称为αA（a）。行动（分别为， 通常用α，α1，.表示。（分别地， α，α1，.. . ）.• qty：Q×AG×N→Zr是一个偏函数，定义在三元组（q，a，i）上，其中i∈d（q，a），定义了给定位置的给定代理的可用动作所需的资源量。负成本表示资源消耗，而正成本表示资源生产。此外，我们有qty（q，a，1）=0r，这是其分量都等于0的向量，对于每个q∈Q，a∈ AG（什么都不做既不消耗也不生产资源）。由于符号的滥用，我们也用qty来表示定义数量的函数一个动作轮廓αA∈DA（q）所需的资源，即qty（q，αA）=a∈Aqty（q，a，αA（a））.最后，我们定义函数consd：Q× AG ×N→Nconsd（q，a，α）返回资源的向量，220D. Della Monica等人/理论计算机科学电子笔记278（2011）215被一个代理人a为一个动作a所消耗。这个向量是从qty（q，a，α）中得到的，用零替换表示资源生产的正分量，用绝对值替换表示资源消耗的负分量。• δ：Q×Nn→Q是转移函数，它定义了如果智能体执行动作轮廓α∈Nn，则从q到达的下一个位置。它是定义在对集合（q，α）∈Q×Nn上的部分函数，使得α∈D（q）。• ρ：M×Q× AG →Nr是价格函数，表示每个资源的价格，取决于当前资源的可用性，代理代理和当前位置。在不失一般性的情况下，我们可以假设资源“时间”的价格• m0是资源的初始全局可用性。它表示系统初始状态下市场上为了给出形式语义，我们必须定义以下概念。定义2.2 [配置与计算]定价博弈图G的配置c是一对<$q，m <$∈Q× M。G上的计算是G λ = c1c2. . ，使得对于每个i，如果ci= qi，则mi且ci+1=<$qi+1，mi+1<$$>，则存在跃迁δ（qi，α）= qi+1，其中α=<$a1，.，αn≠ 0，使得mi+1= mi+ qty（qi，α）.设λ = c1c2... 是一个计算。我们用λ[i]表示第i个配置ci在λ和λ [i，j]中，i ≤ j，构造的有限序列cici+1. cjin λ.定义2.3 [策略]一个策略FA是一个函数，它将每个有限的配置序列c1c2. cs，其中s≥ 1，且cs=<$qs，ms<$，作用量分布αA∈ DA（qs）.换句话说，一个策略FA决定了团队A中的行动者的行为，也就是行动轮廓αA。无论如何，对于每个动作轮廓αA和配置c∈Q×M，取决于对手AG\A的不同动作轮廓，下一个配置有几种可能性，称为配置c下αA的结果。在确定这些结果时，我们不考虑提议者的不可行行动概况（分别为，对手）团队，也就是说，消耗的资源量大于当前可用性m或产生的资源量大于m0−m的行动配置文件。（请注意，即使单个主体的每个行动都是可行的，行动轮廓也可能是不可行的）这反映了一个自然概念，即支持者团队不能基于不可行的行动轮廓构思策略。类似地，对手不能通过一个不可行的行动轮廓来阻止支持者实现目标。形式上，给定一个配置c=<$q，m<$，αA在配置c的结果的集合（c，αA）包含<$qJ，mS<$，如果存在αAG扩展αA使得D. Della Monica等人/理论计算机科学电子笔记278（2011）215221Σ·• qJ=δ（q，αAG），• mS=m+qty（q，αAG），• 0≤qty（q，αA）+m≤m0.• 0≤qty（q，αAG\A）+m≤m0，其中αAG\A是αAG对群AG \A的限制.作为上述定义的结果，给定一个配置c，一个策略FA产生一个计算树 计算λ =c1c2. 称之为配置c的策略FA的结果，如果c1= c且ci+1∈ out（ci，FA（λ [1，i]）），对每个i≥ 1.这样的计算的集合由out（c，FA）表示。最后，我们引入了一致性策略的概念，其结果是，在每一种配置中，代理人都有足够的钱来实现它。定义2.4[（$，m0）-策略]设$∈ N，m0∈ M.一个策略FA称为（$，m0）-策略，如果对每个λ = c1c2. . ，其中ci=<$qi，mi<$对于所有i，属于out（c1，FA），对每个i≥1和a∈A，下列条件成立：• 0r≤mi≤m0，ij=1 ρ（mj，qj，a）·consd（qj，a，FA（q1. . qj）（a））≤$[a]。上述两个条件说明了计算关于m和$的一致性，其中点运算符表示向量的通常标量积。注意，在第二个条件下，只测试了团队A的资金可用性。实际上，我们假设对手AG\A总是有足够的钱来做出选择。还请注意，作为第二个条件的另一个结果，产生资源的行动不会导致对代理人的金钱补偿注意，正如处理时间逻辑时通常的那样，我们保证定价博弈结构是非阻塞的，在这个意义上，满足两个条件的计算的有限个前缀总是可以被下一个配置所跟随，而不违反一致性。实际上，A队总是可以选择其代理人的所有不做动作，而对手队的选择不需要比资源可用性更大的资源量我们现在可以给出PRB-ATL公式的语义.PRB-ATL公式的真实性是相对于定价博弈结构G和配置c=q，m定义的。PRB-ATL语义的定义由满意关系的定义完成|=，如下所示：• （G，c）|= p i <$p∈ π（q）• （G，c）|=<$i（G，c）|=• （G，c）|= 12i（G，c）|=1且（G，c）|= 100• （G，c）|存在一个（$，m0）-策略FA使得对于所有λ∈ out（c，FA），则（G，λ [1]）成立|=•（G，c）|存在一个（$，m0）-策略FA使得，对于所有λ∈ out（c，FA），存在i ≥ 0使得（G，λ [i]）|并且，对于所有0 ≤ j Q]，$−$，G，m）<$[]）40：当τ/=σdo41：τ σ42：σ τ（Pre（A，τ，0n第43章：结束44：结束45：[′]σ46：如果结束四十七： 端48：return（<$q，m<$∈[<$]），G，m）[]）算法2Pre（A，[M]，$，G，m）1：res← m′ ≤m2：对所有的n_q，m_q ∈Q×M_0，3：对于所有α A D A（q′）s. t.0qty（q，α A）+mm0do4：ins true5：对于所有的εq′′，m∈D，其中（i）q′′=δ（q′，αAG）对于eαAG∈D（q′）推广了α A，（ii）m=m+qty（q，αAG），以及（iii）0≤qty（q，αAG\A）+m≤m0do6：如果<$q′′，m<$/∈[<$]或<$（0r≤m≤m0）或（$[a] ρ（m，q′，a）consd（q′，a，α（a））对于某个aA，则7：ins false8：如果结束9：结束10：如果ins，则11：res res q′，m12：如果结束13：结束14：结束第15章：回归224D. Della Monica等人/理论计算机科学电子笔记278（2011）215123123123外部的一个（分别为第19和36行）最多执行Sn次，而内部的一个（分别为第21和38行）最多执行|Q ×M ≤m0 |≤ |Q|·Mr次。 以来|Q|≤ |G|，我们有上述的渐近复杂性。注意，函数Pre的复杂度可以忽略，因为它被主算法的复杂度所吸收总而言之，该算法相对于输入的大小定理3.1模型检测PRB-ATL可以在代理和资源数量的指数时间内求解.3.2PSPACE硬度在这里，我们提供了一个下界的复杂性模型检测问题的PRB-ATL。为此，我们将把确定完全量化布尔公式的真值的问题（TQBF问题[12]）简化为PRB-ATL的模型检查问题。一个完全量化的布尔公式是一个布尔公式，其中所有的布尔变量都出现在一个存在或泛量化器的范围内。一个完全量化的布尔公式被称为前趋范式，如果所有的量化器都出现在公式的开头，每个量化器的作用域是它后面的所有东西。任何公式都可以很容易地放入前趋范式，因此我们只考虑这种形式的公式。在不失一般性的情况下，我们还可以假设公式的布尔无量化器部分是合取范式，子句最多有三个文字，其中文字是变量或其否定。例如，y）]和对于所需正规形式的MULA，<$x1<$x2<$x3[（x1<$x2 <$$>x3）<$（<$x1 <$$>x2<$x3）]是完全量化的TQBF是确定一个完全量化的布尔公式是否为真的问题。假设Φ = Q1x1Q2x2. Qkxk [（x1<$x1<$x1）<$. （xhxhxh）]是一个完全量化的布尔公式，其中Qi是量化器，xi是布尔变量，对于1 ≤ i ≤ k，xj，x j，xj是文字，对于1 ≤ j ≤ h。我们必须展示一个定价游戏结构G，G的构型c，以及PRB-ATL公式f，使得（G，c）|=当且仅当Φ为真对应于Φ的定价博弈结构GΦ计算如下。（作为例如，在图1中，由公式Φ=（x1）x2）x3[（x1）x2）x3（<$x1）x2）x3]。位置集由以下位置组成• 3个位置，表示为每个量化器Qi的qi、qiT、qiT，• 位置Qk+1，• 对于每个子句ci的位置qci，• 2个位置，表示为qxi和q<$xi，对于每个变量xi，• 位置qT。存在r= 2·k个资源，每个布尔变量两个，即R={RxT1，RxT1， . ，RxTk，Rxk}，并且只有一个年龄nt（AG={1}）。初始时，每个资源只有D. Della Monica等人/理论计算机科学电子笔记278（2011）21522512K00000 000年q1qx1q1Tq1qc1q<$x1Q2q×2q2Tq2QTq<$x2年q3qc2q×3q3T第三季qx3年q4等于1 μ请注意，由于只有一个agent，因此只有2个可能的团队，即AG和AG。这意味着，减少（和硬度的结果）也适用于扩展的CTL与价格有限的资源。约简的思想是，从任何位置qi开始，只有两个显著的跃迁，导致qiT和qi。导致qiT的过渡的预期含义（分别为，qin），这被称为真跃迁（分别地，假转换），是分配真值真（分别， false）到布尔变量xi。 我们需要一个机器来记住这样的任务。为了实现这一目标，我们利用资源及其有限的可用性：从qi到qiT的过渡（分别为， qi=0）使得资源RxTi的正好1项（分别， Rx{\displaystyleRx{\displaystyleRx{i}是一个简单的过程。类似地，存在从位置q x i开始的转变（相应地，q<$xi），并导致qT。从qxi（相应地，q<$xi）到qT使得资源Rx<$i的恰好1个项（分别地， RxTi）被消耗。在这种情况下，如果在位置Qi为真（分别地，false）已选择过渡，当游戏开始时位置qxi（相应地，qxi），则代理不能选择导致qT的转换，指示文字为假。只存在一个原子命题，即p，它只在位置qT上为真。Fig. 1.定价博弈结构G Φ的图，对应于完全量化的布尔公式Φ=<$x1<$x2<$x3[（x1<$x2<$x3）<$（<$x1<$x2<$x3）]。设Φ是一个有k个布尔变量的全量化布尔公式，设m0是长度为2·k的向量，所有分量都等于1，设φΦ=φ φA0φ φ⟨⟨AG ⟩⟩Ⓧ⟨⟨A⟩⟩Ⓧ⟨⟨AG ⟩⟩Ⓧ... 美国A公司的一个代表处，其中，如果Qi是泛量子数，则Ai=AG，否则，对所有1≤i≤k。可以证明，（GΦ，mΦ1，mΦ0）|当且仅当Φ为真。定理3.2 PRB-ATL的模型检测问题是PSPACE困难的。226D. Della Monica等人/理论计算机科学电子笔记278（2011）215Σ4最优联盟在本节中，我们定义了确定能够满足PRB-ATL公式的最佳联盟的问题在此过程中，我们引入了参数PRB-ATL公式的概念，即，参数团队算子X$可以出现在经典团队算子A$的位置的PRB-ATL公式。如果如果X是一个参数化的团队操作符，那么X是一个团队变量。给定参数PRB-ATL公式，其中团队变量X =X1，...， Xk=1， . ，Ak∈K，我们记为y∈[X/A]，对任意1 ≤ i ≤ k，用Ai代替Xi的每一次出现，得到PRB-ATL公式。 我们用Sol *表示队的向量A的集合，使得（G，c）|[X/A]。最后，我们通过函数fcost将成本与每个PRB-ATL公式相关联，定义如下。假设一个团队A由集合A的特征向量表示，即A是一个由n个二元分量组成的向量，使得第i个分量为1当且仅当代理人i属于团队A，对于每个1≤i≤n。对于每个PRB-ATL公式，包含团队运算符1美元2美元k电子邮件 * 阿维尼翁，阿维尼翁A2 你好，... 你好，Kfcost（i）=（$i·Ai）i=14.1问题在本节中，我们将介绍找到满足给定参数PRB-ATL公式的团队的最佳（关于函数f成本给定参数PRB-ATL公式，定价博弈结构G，G的配置c，PRB-ATL的最优联盟问题（简称OC）包括在寻找向量A时，如果y，则uchat（G，c）|=[X/A]，并最小化函数f cost因此，解决这种问题的算法将以下参数作为输入：• 一个PRB-ATL公式，在组变量X = X1，X2，...， Xk• 定价博弈结构G，• 一个G的构型c，并输出三重的平均值A_n，成本A_n，其中：• res∈ {true，false}为真当且仅当存在一个队A的向量使得（G，c）|=[X/A]，•A是f个队的向量，使得fcos t（X[X/A]）= 米A∈Sol fcost（X[A]）;其如果Sol=，则value未定义，• cost∈N是函数fcost应用于<$[X/A<$]的值。我们的目的是证明OC具有与模型检测相同的复杂性D. Della Monica等人/理论计算机科学电子笔记278（2011）215227PRB-ATL的问题。上限由一个蛮力算法给出，该算法试图解决每个可能的团队向量的模型检查问题。由于存在（2n）k个不同的团队向量，该算法将调用PRB-ATL模型检测算法的（2n）k次。对于下限，考虑OC问题的决策版本：给定参数PRB-ATL公式，定价博弈结构G，G的配置c，以及整数U，决定是否存在向量A，使得（G，c）|=[X/A]，并且如果应用于[X/A]的成本不超过U。 这类问题的难度直接由定理3.2导出。定理4.1判定OC问题介于PSPACE和EXPTIME之间。5讨论在本文中，我们研究了逻辑PRB-ATL的模型检测问题，非常适合于建模的情况下，团队的代理必须执行一项任务，他们受到资源的有界性已经提出了几种形式化来模拟这种真实世界的情况[3，7]。我们的主要贡献是提出了一种新的形式主义，称为PRB-ATL，基于更强的资源边界概念，我们表明，它的模型检测问题我们还介绍了问题，称为最优联盟（OC）问题，找到最优联盟（相对于不同联盟所需的资金量我们已经证明了PRB-ATL的模型检测问题和OC问题都在EXPTIME中，并且有一个PSPACE下界。事实上，为了解决OC问题，我们给出了一个算法，探索整个空间的解决方案，以计算最优。找到计算复杂性的确切特征的问题是一个开放的问题，目前正在调查中进一步的研究方向是研究逻辑的变体，以自然地表达更多种类的场景。作为一个例子，在我们看来，将金钱捐赠视为游戏竞技场的一个组成部分是有趣的（即，该模型），而不是明确地指定新的资金可用性的每一次发生公式中的团队操作员。此外，与这个论点相关的是，人们可以不把货币可用性视为问题的输入，而是将其视为一个参数，以最小化，确定每个代理应该提供多少钱，以执行给定的任务。引用[1] Agotnes，T.，W. vanderHoek和M. Wooldridge，关于联盟游戏的逻辑，在：AAMAS，2006，pp. 153-160。[2] Alechina，N.，B. Logan，N. H. Nga和A. Rakib，A logic for coalitions with bounded resources，in：Proc. of the 21st International Joint Conference on Arti ficial Intelligence，IJCAI659-664.[3] Alechina，N.，B. Logan，N. H. Nga和A. Rakib，Resource-bounded alternating-time temporal logic，in：Proc. 第九届自治代理和多代理系统国际会议：第一卷，228D. Della Monica等人/理论计算机科学电子笔记278（2011）215AAMAS481-488URLhttp://portal.acm.org/citation.cfm?联系电话：021 - 8888888[4]巴尔河，T. A. Henzinger和O.李文，交替时间时序逻辑，北京：计算机科学出版社，2001（2002），pp. 672-713[5] Bulling，N. Dix，Modeling and verifying coalitions using argumentation and ATL，Inteligencia Artificial，Revista Iberoamericana de Inteligencia Arti ficial14（2010），pp.45比73[6] Bulling，N.和B. Farwer，资源受限系统的表达性质：逻辑RTL和RTL，in：J。Dix，M. Fisher和P.Nov'ak，编辑，多代理系统中的计算逻辑（CLIMAX）（2009），pp.22比45[7] Bulling，N.和B.Farwer，关于模型检查资源受限代理的（非）可判定性，在：第19届欧洲人工智能会议，ECAI'10，2010年，pp。567-572.[8] 邓恩，体育，S. Kraus，E. Manisterski和M. Wooldridge，Solving coalitional resource games，Arti ficialIntelligence174（2010），pp. 五五开URLhttp://www.sciencedirect.com/science/article/pii/S0004370209001076[9] Goranko，V.，联盟游戏和交替时间逻辑，在：第八届会议的理性和知识的理论方面，TARK259-272.[10] Pauly ， M. A logical framework for coalitional economicity in dynamic procedures ， Bulletin ofEconomic Research53（2001），pp. 305-324URLhttp://dx.doi.org/10.1111/1467-8586.00136[11] Pauly ， M.A modal logic for coalitional power in games ， Journal of Logic and Computation12（2002），pp.149比166[12] Sipser，M.，
我的内容管理
展开
