论认知时间战略逻辑：ATEL的理论计算机科学电子笔记126（2005）77-92

理论计算机科学电子笔记126（2005）77-92www.elsevier.com/locate/entcs论认知时间战略逻辑Sieuwert van Otterloo1利物浦大学计算机科学系联合王国利物浦Geert Jonker2乌得勒支大学信息和计算机科学研究所荷兰乌得勒支摘要ATEL是最具表现力的逻辑推理知识，时间和策略之一。围绕这一逻辑的解释的几个问题仍然没有解决。这篇论文有助于正在进行的讨论，表明代理人不必知道做某事的具体策略此外，我们声称，代理人可以拥有所谓的战略知识，这是来自他们的知识正在发挥的战略。为了证明这些说法，我们提出了一种替代的解释ATEL广泛的游戏形式。对于能力的定义，我们使用战略支配，而对于战略知识，我们在模型中包括战略特征我们用几个小例子来说明所提到的解释问题此外，我们展示了完美回忆和完美记忆的特点。关键词：交替时间，认知，时间，策略，逻辑，模型检测1介绍在分析过程中，对知识、时间和策略的推理是重要的多智能体系统已经开发了几种逻辑框架和语言来捕捉这些概念。在本文中，我们讨论一种称为ATEL [15]的语言，它是一种关于知识、时间和1电子邮件：sieuwert@csc.liv.ac.uk2电子邮件：geertj@cs.uu.nl1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.01478S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）77战略布局这种逻辑可以应用于各种系统的形式化分析，例如分布式协议，同步和安全，但也可以应用于任何可以建模为广泛游戏的问题，例如辩论，拍卖或语言游戏。在本文中，我们关注的是ATEL的解释。对语言的原始解释具有吸引人的计算特性，但由于一些违反直觉的特性而受到影响，这导致了许多改进[16，9，8]。在本文中，我们提供了一个新的解释ATEL。为了使事情简单，我们这样做的回合制系统，但我们认为没有理由的方法不能扩展到更一般的类并发系统。ATEL的历史始于计算树逻辑的定义，这是一种用于分支时间模型的逻辑[4]。使用这种逻辑可以表达分布式或并发系统的许多时间属性，例如Biblir和其他人[1]发现，这种逻辑可以扩展到多智能体系统的推理，而不会改变模型检查的复杂性他们用联合运算符扩展了这种语言使用ATL，可以表达这样的属性Van der Hoek和Wooldridge意识到在ATL中推理代理的知识是有用的，并使用称为ATEL的知识运算符扩展了该语言[15]。他们给了knowledge算子一个非常直观的解释系统语义[6]，但没有改变联盟算子中使用的策略的概念其结果是，代理人被认为总是能够在不同的状态下做出不同的选择，即使代理人不能区分这些状态。假设代理可以在他们无法区分的状态中做出不同的选择是违反直觉的[9]，并且Jonker，Van der Hoek和Jamroga [9，8]开发了沿着不完美回忆ATL [13简单地说，ATEL最初假设，如果存在实现某个目标的策略，代理人的联盟可以实现某个目标。这一条件在所引用的资料来源中得到加强：• 一个代理联盟可以实现X，如果他们有一个统一的策略（可行策略，或不完美信息下的策略），实现X[9]。• 一个代理联盟可以达到X，如果他们有一个统一的策略，他们知道它达到X。[9、8]在第2节中，我们正式定义了统一策略的概念，但它可以被认为是一种具有额外限制的策略，因此它不使用事实S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）7779探员不该知道的本文的一个主要观点是，后一个条件太强了一个联盟不必能够确定一个他们知道会成功的战略。一个明智的代理人联盟将选择，如果他们不能确定一个万无一失的策略，他们可以想出最好的策略更准确地说，他们会选择一个不被任何其他策略支配的我们说，一个联盟的代理人可以做X，如果任何非支配策略达到X。我们将在本文后面定义支配。本文的第二个观点是，联盟的知识不仅取决于游戏或系统的状态，而且还取决于他们所采用的策略。似乎可以肯定的是，代理人知道他们采用什么策略，这给了他们关于未来的额外信息。 这种现象可以称为战略知识[5]。这里的解释解决了这个问题，假设所有代理人都知道自己的策略。我们强调，这并不是对这个问题的最终答案，而是作为一个示范，说明如何整合某种形式的战略知识。语言CTL实际上是语言CTL的语法限制子集。ATL和ATL以及ATEL和ATEL也是如此。未加星号的版本受到了最多的关注，因为它们具有较低的模型检查复杂度[16]。然而，在本文中，我们更感兴趣的是语言解释的意义，而不是复杂性。因此，我们更喜欢使用ATEL语言，这种语言没有限制，而不是只为ATEL定义解释在第二节中，我们给出了必要的定义。第3节包含示例。在第4节中，我们定义了对ATEL的解释。第五节用逻辑分析第三节的例子。在第6节中，证明了两个定理，第七节是结论。2广泛的游戏形式游戏是具有不同和可能竞争目标的代理之间交互的模型[12]。 一个广泛的游戏给出了这种互动的详细描述。它显示了为了达到一个结果而做出的决定。它可以用博弈树来表示，每个叶子对应一个结果，每个节点对应一个选项。所有代理人的偏好是一个广泛博弈的一部分。在许多情况下，人们希望研究独立于代理人偏好的博弈结构。在这种情况下，可以使用博弈形式的概念，这是一个没有偏好函数的广泛博弈广泛博弈的概念可以追溯到80S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）77”[11]《礼记》。我们采用了奥斯本的下一个定义[12]。由于结构编码的事实，代理人可能不知道到底是什么，当前的状态是在做决定时，我们说的是一个广泛的游戏与不完美的信息。我们采用了博弈论中流行的符号[12]和联盟逻辑中使用的符号[16]。所有代理的集合表示为r，而r用于代理的子集。单个代理被表示为X、Y。对于游戏形式和游戏形式解释，使用F、G。策略被称为S，T或SΓ，TΓ，以指示策略是针对哪个组的。 一种博弈形式和一种策略一起形成一个模型，用M表示。公式记为φ、φ和原子命题p、q。P是一组命题。这些命题可以用函数π来解释，所以π（h）是在h处成立的命题的集合。动作是a，b，历史是h，HJ或j.为了提高可读性，我们有时会稍微滥用符号，将代理集写成XY{X，Y}。游戏形式一个博弈形式是一个元组（tuple，H，Ow，Ow），其中Ow是代理人的有限集合，H是历史的非空集合。集合H必须是预闭的，这意味着对任何序列ha∈ H，H也∈H。 我们用特殊符号来表示空序列。h之后可用的所有动作的集合被表示为dA（h）={a|ha∈H}。 如果A（h）=H，则Ah是终结的. H的所有终端历史的集合记为Z（H）.函数Ow（h）：H\Z（H）→A定义了哪个玩家选择下一个动作。直觉上，主体Ow（h）拥有历史h，但我们也可以说它决定h、控制h或在h中具有主动权。 对于每个主体X∈X，关系X是历史之间的等价关系，其中h∈Xj表示代理X无法分辨差异在经历了历史h和历史j之后。一个条件适用：如果Ow（h）=X且hJ<$Xh，则Ow（hJ）=X且进一步A（h）=A（hJ）。此条件确保代理知 道 何 时 可 以 选 择 操 作 ， 以 及 哪 些 操 作 可 用 。 这 个 定 义 来 自Osborne。和Rubinstein [12]，定义200.1，在那里它被称为广泛的游戏形式。我们已经扩展了信息集，使得代理人在不负责时也有信息，这是逻辑目的的常见扩展[14，3]。游戏形态解读一个游戏形式的解释被定义为一个元组（，H，Ow，，P，π）。第一个元素（，H，Ow，）是一个游戏形式。集合P包含命题S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）7781和π：H→2P是一个函数，它为每个历史分配在该历史的最终状态下为真的命题集。这个想法是，这些命题可以用来指某些历史，例如历史当一个代理人达到一个特定的目标。战略对于一个联盟Γ，一个策略SΓ是一个函数，它取一个历史h，使得Ow（h）∈Γ，并返回一个非空的动作集SΓ（h），使得SΓ（h）<$A（h）。这意味着策略可以是非确定性的。我们有时称策略SΓ为策略剖面，以表明它包含每个智能体的策略在本文中，战略和战略概况之间没有根本的区别。一个策略SΓ是一致的i ≠对所有的h，j，其中h≠Ow（h）j，这是SΓ（h）=SΓ（j）的情况。 统一战略因此，在历史中规定了代理人无法区分的相同动作为了本文的目的，我们认为一个游戏的形式作为一个众所周知的自治代理之间的交互协议的描述。所有代理都有偏好，并且众所周知，这些偏好是私有的，因此不为其他代理所知。众所周知，具有不同目标的代理人不能在游戏结构之外进行通信。如果一个智能体采取了某种策略，例如达到某个目标，那么智能体本身就知道它在玩什么策略，但其他智能体不知道这一点。如果一个联盟的代理有一个目标，那么它是假设代理有正确的协调手段，以选择一个组策略。心理能力包括在游戏形式的定义中。我们假设，如果一个代理是健忘的，这已经被编码在游戏形式的等价关系因此，博弈形式中的关系在这个假设下，将主体的属性（如第6节中的完美回忆和完美记忆）与等价关系的属性3场景为了说明本文所涉及的ATEL原理，我们首先将看一些例子。我们研究的第一个博弈形式是图1中的博弈形式G1。在这个博弈中，A首先可以在行动1和行动2之间做出选择。2.代理B然后选择动作3或动作4。虚线表示当B必须选择时，代理B不知道代理A做了什么。对于这种博弈形式，我们感兴趣的是智能体B. 在原始ATEL解释中，代理B在t0中具有满足以下条件的策略：82S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）77一1t0 2B3t1 4 3t1 4t2，p，qA一t2t2，pt2，qFig. 1. 一个简单的博弈形式G1Q.如果A选择动作1，它将选择动作3;如果A选择动作2，它将选择动作4。然而，在t1处 ，代理B不知道代理A是否已经执行动作1或2。根据Jonker [9]，代理B没有统一的策略来满足t0中的q。因此，结论是，对于我们有一个唯一的出发点的情况下，要求代理人应该有一个统一的策略是足够的，以获得直观的结果。如果我们从满足t1的两个节点中的一个开始，那么事情就有点不同了。代理B确实有一个统一的策略来实现q，例如在最左边的t1情况下，也有一个统一的策略，在最右边的情况下，但不知道使用哪一个，因为他不知道当前的情况是什么。就Jonker、Van der Hoek和Jamroga而言，它无法确定正确的策略。如果代理B想要满足p，那么它将能够在t1中确定一个统一的策略：选择动作3。但如果B想满足pq呢？在t1，它将不能识别统一策略，因为它不知道代理A是采取了行动1还是2。 然而，它有一个行动3.在代理人看来，这种策略可能会使它达到目标。没有比这个更好的策略了，所以我们称之为非劣势策略。如果存在一种策略，在某些不可区分的状态下表现更好，而在其他状态下表现相同，那么它将是劣势的。我们将在第4节中对此进行更正式的定义。现在让我们假设在行动1之后，我们处于左情形。我们注意到，如果代理B使用他的因此，我们说，代理人B是能够满足p<$q，或者对于试剂B，p<$q是可实现的。图2中的博弈形式G2说明了一个主体可以有几个非劣势策略。 我们假设当前的情况是行动2.代理B希望在接下来的状态中使p为真。智能体有两个行动可供选择，它无法确定哪一个行动最适合实现p.在左边的情况下，适当的策略是行动4。在适当的情况下，适当的战略是行动5。然而，对于中间情况，代理人选择哪种策略并不重要。要么BBS. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）7783B1 2B3BBB4 5 4 5 4 5一啪啪啪啪图二. 博弈形式G2一pQ图三.不完美记忆游戏形式行动导致一个理想的状态。因此，代理人有两个策略，可能使他达到他的目标，他不清楚是否使用一个或另一个，他们都是非劣势的。他能做的最好的就是随机选择其中一个。幸运的是，由于A采取了行动2，B将使用任何非劣策略达到目标。因此，我们说主体B能够满足p，或者主体B能够实现p。在博弈形式G1和G2中，A的选择促进了B达到目标在G1中，我们看到代理B能够满足p和q，因为A选择了行动1。我们说A有能力给B一个满足p和q的能力。代理人A先于代理人B行动的事实并不意味着代理人B不能使代理人A达到某些目标。如果智能体B事先决定采取行动3，它在某种程度上使智能体A有能力（最终）满足p和q。在图3中描绘了另一种游戏形式。这种游戏形式是不寻常的，因为代理人失去信息，根据关系表明。在动作1之后，代理A似乎不记得它选择了这个动作。类似地，B知道历史1和历史2之间的差异，但是一步之后它不能区分历史13和历史23。 在本文的后面，我们将证明，假设A没有完美的回忆，但有完美的记忆。B连记忆力都不好。无论哪种情况，这都表明我们不是在谈论完全理性的主体，因为完全理性的主体能够记住他们所看到和做的一切。 这些属性在第3节和第6节中讨论。12一33AB84S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）77A A11q2 2p见图4。推块图4所示的最后一个场景处理的是代理人是否会通过选择某些策略而失去能力的问题。这是一个小问题，与前面的问题关系不大。然而，它说明了ATEL解释中的一个问题。这种情况背后的故事如下。在右上角和中间的状态下，智能体可以向下推一个块，之后q保持不变，块保持向下。 它也有能力推动块的权利。在最右边的位置，代理不能再向下推块。假设最左边的状态是当前状态。这个模型有趣的特性是，代理有能力在下一个状态中使p为真。根据我们的直觉，它不可能一步摆脱这种能力。如果我们假设主体可以无条件地承诺策略，这样他们以后就不能改变他们的策略，那么A就能够通过承诺进入最右状态，导致自己不能实现p。这不是我们认为的直觉。因此，我们假设代理人总是可以在稍后的时刻改变自己的策略最后，我们再次回到博弈形式G1。考虑这样一个场景：代理人A决定采取行动2的策略。在时间t0，这就要求代理A知道。 例如，它现在知道代理 B不再满足pq。这就是所谓的战略知识[5]。 这是一种暂时的知识;只要一个代理人将遵循它所承诺的战略，它对未来有更多的了解。这同样适用于一个联盟;只要他们遵循相同的战略，并且这是他们之间的共同知识，他们对未来的知识就会增加。 下一节将展示战略知识，与上面解释的其他原理一起，可以使用AtelTM的新解释来形式化。4策略时间认知逻辑语言atel是最小的语言L，使得对于任何公式φ，φ∈L，任何代理人Γ和任何代理人X的联盟，情况是：S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）7785ΓΓΣΣφ<$$>∈L<$φ∈L φ∈L φU<$∈L. φ∈L KX φ∈LΓφ∈L这种语言实际上是AT L逻辑和认知逻辑的混合物[6]。读者会熟悉析取（φ， 时间操作符U和。说说未来φ意味着φ在所有未来状态下都为真。公式φU表示在未来的某个点上φ成为真，并且在此之前φ为真。 下一个国家的运营商。φ表示在下一个状态φ是真的。认知算子KX φ表示施事X知道φ成立。联合算子Γφ表示代理集合Γ可以确保φ成立。我们在模型M和历史h上解释公式φ，并将M，h| = φ，则公式为真。与以前的解释不同，我们在模型中包括了策略。模型M是一个对（F，S），其中F是一个有解释的博弈形式，S是所有代理的策略我们定义中性策略S0为返回所有可用动作的策略：S0（h）=A（h）。不同联盟的策略可以使用函数combine组合成一个更大联盟的函数。策略组合（Γ，SΓ，T）对于Γ中的代理等于SΓ，对于其他代理等于T代理商：⎧如果Ow（h）∈Γ，则Ow（h）是combine（r，Sr，T）（h）=n（h）ifOw（h）∈/Γ模型M=（F，S）包含了代理当前使用的所有策略的信息。特工只知道自己的策略它知道自己将遵循该策略，但假设对其他人的了解仅限于他们遵守中立策略S0。 因此，在评估智能体关于未来的知识时，我们使用的模型是智能体使用其策略的结果，而其他智能体使用中性策略。这种策略实际上是对代理人不可区分的最少限制的策略。我们使用算子k（M，X）来定义它，其定义为k（（F，S），X）=（F，combine（X，S，S0））。函数k用于定义知识经营者的认知。为了定义策略算子Γ的含义，我们使用非劣势策略的概念非正式地，如果S在达到某个目标时严格优于T，则策略S优于T我们假设，如果一个策略是劣势的，那么一个理性主体的联盟就不会采取这个策略。为了定义支配，我们首先需要定义另外两个算子。操作符update类似于k：它返回表示视图的模型86S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）77Σ在采用策略SΓ之后，联盟Γ中的代理的数量。在Γ中的智能体遵守SΓ，但其他智能体可以以他们想要的任何方式行动update（M，Sr）=（F，combine（r，Sr，S0））此外，我们称一个策略SΓ在历史h中成功（success（M，h，SΓ，φ））当且仅当update（M，SΓ），h| = φ。关于模型M、目标φ和历史h，如果满足以下两个条件，则策略SΓ优于策略TΓ：存在历史hJ<$Γh使得成功（M，h，SΓ，φ）但不成功（M，h，TΓ，φ），其次不存在历史j使得成功（M，j，TΓ，φ）但不成功（M，j，SΓ，φ）。这支配的定义使得支配关系是传递的和非对称的。这些性质确保了任何非空的有限策略集合至少包含一个不被集合中另一个策略支配的策略。我们说可实现的（M，h，Γ，φ）如果对所有的非支配策略SΓ，成功（M，h，SΓ，φ）. 我们之所以要量化非支配策略是我们想象一个联盟随机选择任何非支配策略，因为它没有理由喜欢一个非支配策略而不是另一个。因此，只有当所有非劣策略都成功时，才能保证成功。 使用所有这些概念，我们定义了解释以下是ATEL的详细信息M，h |= pi <$p∈ π（h）M，h |=<$φi ≠ M，h| = φM，h| = φi M，h| = φ或M，h|=M，h |= K X φi <$$>hJ：hJ<$Xh =<$k（M，X），hJ|= φM，h|= φU<$i <$$>j∈Z（H（S<$，h））<$i<$k：|H| ≤khJ∈ H（S<$，h）：M，hJ|= φM，h| =. φi <$i a ∈ S<$（h）：M，ha |= φM，h| =的Γφi可实现（M，h，Γ，φ）集合H（S，h）包含H的所有历史，这些历史从h开始并且与策略S一致（在h之后）。它可以递归地定义。H（S，h）是最小集合HJ，使得h∈HJ且<$HJ∈HJ，<$a∈S（HJ）：HJa∈HJ.5示例在第三节中，我们介绍了四种游戏形式。在本节中，我们将使用这些博弈形式来展示示例公式的解释。对于所有实施例S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）7787Σ模型Mi定义为（Gi，S0）。 第一个例子涉及时间特性.M1，|= t0。t1m。 。最初是t0成立，然后是t1，然后是t2M1，|=（t2→ <$t1）如果t2成立，则t 1不成立M1，|= TU t2最终t2成立我们已经论证过，在行动1之后的博弈形式G1中，行为人B可以达到p，但不能达到q。它也可以实现pq，但它不知道它可以实现这个事实。这些事实的翻译在这里给出。在模型G2类似的性质举行，这些也给出了。M1，1 |=B.p代理B可以在下一个状态中使p为M1，1 |=< $ B.Q代理B无法在下一个状态中使q为M1，1 |=B. （pq）代理B可以使p和q在下一个状态M1，1 |=<$K BB.（p<$q）AgentB不知道它可以使p和q为真M2，1 |=< $ B.p代理B无法在下一个状态中使p为M2，2 |=B.p代理B可以在下一个状态中使p为M2，2 |=<$K BB.p代理B不知道它可以在下一个状态中使p为真在博弈形式G3中，A不记得它过去所做的选择。代理B并不总是知道它以前的观察结果。这一点在接下来的陈述中有所体现。M3，|=K AA.p88S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）77代理A知道它可以使p在下一个状态为真M3，|=< $ A. KA p代理A无法知道下一个状态中的pM3，1 |= K B. Q代理B知道q在下一个状态M3，1 |= €。K Bq在下一个状态中，代理B不知道q为真下一个模型，G4，表明代理人一般不能承诺他们自己的行动，反对他们的未来偏好。接下来的公式表明，在这个模型中，代理A不想让p为真，而且A担心将来它可能会做一些违背其当前愿望的事情，p.例如，如果A受到威胁，或者如果A是一个民主委员会，那么当前的成员可能不信任所有未来的成员，就会发生这种情况。M4，|=A.。p代理A可以在第二个下一个状态中使p为真M4，|= € A- A.p代理A不能确保它不能在下一个状态中使p为真它不能仅仅通过采取某种策略来消除能力。M4，|=< $ A. - A.p代理A不能保证下一次它不能使p为真。类似于前面的例子，但多了一个步骤。M4，|=A. - A.p代理A可以确保在两个步骤之后，它不再有能力做出ptrue.回到博弈形式G1，我们给出了一个例子，说明一个智能体如何拥有战略知识。假设代理人A已经承诺采取行动2的策略。然后它知道代理B将无法实现S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）7789满足于满足假设SAB是由A的策略和A的中性策略组成的策略剖面，B. 然后我们可以将上面描述的知识表示为：（G1，S A，B），|=K A<$B.。普什克代理A知道B不能满足pq6完美回忆与完美记忆如果智能体永远不会忘记他们以前的观察和他们选择的行动，那么他们就有完美的回忆。同样，如果他们不忘记他们的观察，他们就有完美的记忆力[10，2]传统上，博弈论关注的是完美回忆代理，但多代理系统中的人工代理通常不具有这些属性。这些人工代理是具有有限内存的计算机程序。对于解决游戏或模型检查时间公式的复杂性，系统是否具有完美记忆的完美回忆是相关的[10，7]。因此，我们在这里提出了两个定理，刻画是否一个游戏形式的解释有完美的回忆和完美的记忆。特别是我们想说明完美回忆和完美记忆之间的区别，因为这种区别不会出现在没有策略的时间逻辑中。利用我们已经包含在模型中的策略轮廓是证明完美召回属性所必需的的作者不确定关于完美回忆的不同定理是否适用于先前对ATEL的解释。可以说，完美回忆不是游戏的属性，而是游戏中参与者然而，我们认为等价关系游戏形式中的X（，H，Ow，[a]a∈）作为代表剂.因此，我们假设代理人的能力已经包含在等价关系中。因此，我们认为完美回忆是一种游戏形式可以或不可以拥有的属性。我们根据观察来定义完美回忆;如果智能体记住了所有的观察，包括它选择的动作，那么它就有完美回忆。 假设OX（h）是返回的函数由代理X在历史h中选择的所有观察和动作的有序列表。然后，代理X有完美召回当且仅当h<$Xj参与OX（h）=OX（j）。函数OX可以递归地定义。ha的观测函数包含h的所有观测，可能还加上动作a（如果Ow（h）=X）和在ha中进行的观测。使用这样的递归定义，90S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）77ΣΣΣΣ完美回忆的性质等同于下面两个性质。ha<$Xjb→h<$XjOw（h）=X<$ha<$Xjb→a=b完美回忆的这个特征就是我们在下一个定理中使用的定理1设F =（λ，H，Ow，[λX] X∈λ），X∈ λ. X在F中有完美召回当且仅当对于每个P，π，每个φ，每个策略S和每个h：（（F，P，π），S），h| = K X. φ→ 。KX φ设X在F中具有完全召回率，且给定P，π，φ，S，h。设G =（F，P，π），且（G，S），h| = K X. φ。 定义MJ=（G，SJ）=k（（G，Sj），X）.设a∈S<$（h），jb<$Xha.从完美的回忆属性，我们知道，hXj。从k的定义可以看出，对于任何hJ，都是S（hJ）<$SJ（hJ）的情况。使用（G，S），h| = K X.我们可以得出结论，MJ，j|= . φ。 如果Ow（h）= X，则Ow（j）= X，我们知道b =a，因此b ∈S<$（h）<$SJ。 如果Ow（h）/=X，则SJ（j）=A（j），因此b∈SJ（j）。 从MJ，j| =. φ和b∈SJ（j），我们可以Σ Σ Σ得出MJ，jb |= φ。由于我们已经证明了任意jb∈X的情况，我们得到（G，S），h |=. K X φ。对于后半部分，假设对于每个P，π，每个φ，每个策略S每个h：（（F，P，π），S），h| = K X. φ→ 。KX φ设G=（F，P，π），ha∈H. 取jb使得haxjb。让P={p}并定义π使得π（jJbJ）={p} i <$h<$XjJ且bJ∈A（jJ）。 令S=S0。这种解释确保（G，S），h| = K X. p.我们可以从以下假设导出：（G，S），h| =.K X p. 因此，对于每个a∈A（h），情况是（G，S），ha| = K X p。由于ha<$Xjb，我们得出结论：（G，S），jb| = p。通过定义π（p），我们得到h<$Xj。设G=（F，P，π），ha∈H使得Ow（h）=X.设jb∈H使得ha<$Xjb.从上一部分我们已经可以得出结论，hXj. 设P={p}，S=S是一个策略，使得S（h）={a}。定义π使得π（jJbJ）={p}i <$bJ=a且jJ<$Xh。这些定义确保（G，S），h| = K X.p.我们可以导出（G，S），h| =.KX p.从下一个的定义我们知道（G，S），哈|=K × p，因此（G，S），jb |=p。通过定义p，我们得出a=b。证明到此结束一个具有完美记忆力的智能体能记住它以前的所有观察结果。设MX（h）是返回历史h中AgentX的所有观测的有序列表的函数（不包括它选择 的 动 作 ） 。我 们 定 义 一 个 智 能 体 X 具 有 完 美 记 忆 当 且 仅 当h<$XjParticipateMX（h）=MX（j）。S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）7791ΣΣΣΣ同样，我们可以递归地定义观测函数M。使用这样的递归定义，不难证明完全记忆的性质等价于ha<$Xjb→h<$Xj。定理2设F =（λ，H，Ow，[λX] X∈λ）是一个对策形式，X∈ λ. X在F中有完美记忆，当且仅当对于每个P，π，每个φ和每个h：（（F，P，π），S0），h |= K X. φ→。KX φ在这个定理中，我们使用中立策略S0来代替任何策略。该策略的一个重要性质是k（（F，S0），X）=（F，S0）.Σ Σ对于证明的前半部分，假设X在F中具有完美记忆，并假设P、π、φ和h都已给出。设M =（（F，P，π），S0），并假设M，h |=K X. φ。设a∈A（h），jb为任意历史，其中jb<$Xha.从完美记忆的性质，我们知道，j xh。我们可以推导出k（M，X），j|=.φ。由于M包含中立策略，k（M，X）= M，因此M，j|=. φ。这意味着M，jb|=φ。由于我们已经证明了对于任意的jb，其中jb <$Xha，我们可以得出结论，|=. K X φ。对于第二部分，假设对于每个P，π，φ和h：（（F，P，π），S0），h |= K X. φ→ 。K X φ。 让我们来看看。 定义P={p}和π使得π（hJaJ）={p}i <$hJ<$Xh且aJ∈A（hJ）。 这个定义确保了M，h| = K X. p.我们可以得出结论，M，h| =. K X p. 从这个公式可以推导出M，ha| = K X p，因此M，jb| = p。这意味着π（jb）={p}，因此j<$Xh。因此X在F中有完美的记忆。7结论和进一步研究提出了战略能力的逻辑，并对战略能力的经营者进行了新的解释。它的优点比以前建议的定义是，意义符合，在作者的意见，最好的自然意义，有一个战略，在一个广泛的游戏。一个典型的特征是，在这种解释下，代理人可能具有他们不知道自己具有的能力。我们已经表明，人们可以描述具有完美的回忆和完美的记忆力。未来的工作可以集中在扩展语言上，例如使用常见的知识。一个有趣的问题是在有限状态系统上评估这种逻辑的复杂性。此外，我们还想看看是否可以为那些立即知道彼此策略的智能体或无法协调行动的联盟提供类似的语义。最后，将这种逻辑应用于示例问题，如俄罗斯纸牌问题[18]和Dining Cryptogra，将会很有趣。92S. van Otterloo，G.Jonker/Electronic Notes in Theoretical Computer Science 126（2005）77phers问题[17].引用[1] R. T.A. A. Henzinger和O.库普弗曼交替时间时序逻辑。在Proceedings of the 38th IEEESymposium on Foundations of Computer Science，pages 100[2] G.博南诺广泛游戏中的记忆和完美回忆。游戏与经济行为，47：237[3] G. 博南诺记忆意味着冯·莫根斯坦博弈。《知识理性与行动》，2004年出版。[4] E.M. Clarke和E.A.爱默生利用分支时间时序逻辑设计与综合同步骨架。计算机科学讲义，131：52[5] S.德鲁伊不完全信息博弈中的知识发展，2002。格罗宁根大学硕士论文。[6] R. Fagin，J. Halpern，Y. Moses和M.瓦迪关于知识的推理麻省理工学院出版社：马萨诸塞州剑桥，1995年。[7] J. Halpern，R van der Meyden和M.瓦迪知识与时间推理的完备公理化。SIAM Journal onComputing，33：674[8] W. Jamroga和W.范德胡克。关于交替时间认知逻辑的几点注记。2003年提交[9] G. 混蛋交替时间时间认知逻辑中的可行策略，2003。乌得勒支大学硕士论文。[10] D. Koller和N.米吉多 二人零和博弈的复杂性。博弈与经济行为4，4：528[11] 库恩。广义博弈与信息问题。Contributions to the Theory of Games，II：193[12] M. J. Osborne和A.鲁宾斯坦博弈论课程。麻省理工学院出版社：马萨诸塞州剑桥，1994年。[13] 皮埃尔-伊夫·朔本斯不完全回忆的交替时间逻辑。在Wiebe van der Hoek，Alessio Lomuscio，Erik de Vink和Mike Wooldrige，编辑，理论计算机科学电子笔记，第85卷。Elsevier，2004年。[14] J. 范·本瑟姆。动态认知逻辑中的博弈Bulletin of Economic Research，53（4）：219[15] W. van der Hoek和M.伍尔德里奇认知目标的易处理多智能体规划。第一届自治代理和多代理系统国际联合会议，第1167-1174页，博洛尼亚，意大利，2002年[16] W. van der Hoek和M.伍尔德里奇合作、知识与时间：交替时间认知逻辑及其应用。StudiaLogica，75（4）：125[17] R. van der Meyden和K.苏符号模型检验密码学中的用餐知识。审查中，2004年。[18] H. P. 范迪特马施。俄罗斯扑克问题Studia Logica，75（4）：31