基于概率逻辑的博弈模型及其最大化和最小化策略研究

理论计算机科学电子笔记130（2005）23-37www.elsevier.com/locate/entcs随机对策的无记忆策略研究Carroll Morgan卡罗尔·摩根1，2部新南威尔士大学计算机科学与悉尼2052澳大利亚Annabelle McIver安娜贝尔·麦基弗1，3Macquarie University Sydney2109澳大利亚摘要在形式化方法中，我们使用数学结构来模拟我们想要构建的真实系统，或者进行推理;在本文中，我们主要关注基于游戏的模型。在早期的工作[16]中，我们提出了一种基于概率程序逻辑的随机最小化博弈方法[17，11]。这里的贡献是扩展我们的逻辑方法来最大化游戏。最大化和最小化不是（简单地）重复的，这是因为在这两种情况下都使用了最小固定点，这对迭代程序来说是正常的。 (For在最大化的情况下，我们必须使用最大不动点。这种扩展的意义在于，它在程序逻辑方法和寻找“解决”这类游戏的控制策略保留字：概率语义学，随机博弈，马尔可夫决策过程。1我们感谢澳大利亚研究委员会（ARC）在其发现资助DP0345457下的支持。2 电子邮件地址：carrollm@cse.unsw.edu.au3 电子邮件地址：anabel@ics.mq.edu.au1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.00324C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）231介绍诸如Z[19]和B[1]的技术通过假设其状态的数学模型来建模真实世界系统，并以一种被认为与可以在真实系统上观察或执行的实际操作相对应的在这项工作中，我们关注的是比上述更一般的系统，那些建议（对他们的观察者）玩游戏的过程，可能涉及恶魔的非决定论（环境最近的一个趋势，特别是对于像这样的系统，是将正确性（和细化）不简单地视为解决这类问题的类似地，我们发现已经完成的经典工作可以为我们的编程逻辑设计提供信息，甚至在某些情况下可以提供证明其属性的技术[4]。特别是，我们已经展示了两个玩家回合制恶魔/天使/概率博弈对应于我们的定量μ-演算qM μ[14，15，10]中的表达式，它本身是定量时序逻辑qTL的超集。因此，我们遵循的是一种比Z或B更一般的方法，在Z或B中，我们观察一个系统，将其行为描述为具有操作的状态系统（必然是非正式的步骤），将该描述编码为一个抽象模型，然后使用数学工具（定理）来操纵正式文本（细化等）。最后，我们将结果转换回现实世界，作为对系统行为的预测在这里，我们观察一个系统，将其行为描述为一个博弈（必然是一个非正式的步骤），将该描述编码为一个数学模型（博弈树），然后使用数学工具（定理）来操纵正式文本（通过与树相对应的定量逻辑）。最后，我们再一次将我们的结果转换回现实世界，作为对系统行为的预测C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）2325本文的具体技术结果是展示程序逻辑方法如何预测“玩游戏”的结果2现有的理论和我们的贡献在数学风格中，马尔可夫决策过程解决了与概率环境中的资源争用相关的现实问题。一个（非竞争性的）MDP，以其最抽象的形式，描述了一个孤独的赌徒的行为和他在下注时选择的策略的后果。MDP的使用带来了基于线性规划的长期建立的算法技术，用于量化某些定义明确的属性;然而，即使是简单的论点也可能是复杂的和难以遵循的-主要是因为需要包括每个MDP的所有细节。没有内置的抽象设施。我们解决这个具体化和分析问题的方法是使用定量逻辑来抽象概率系统的属性，其中表达式包含反映底层系统中概率转移的实值。与一般的程序逻辑一样，它导致更简单的规范和分析技术;逻辑的基础是底层系统的域理论模型抽象是自然的。抽象当然是逻辑的本质;在本文中，我们将集中讨论建立这种定量逻辑的域理论模型[14，15，11]。这种域理论的在计算机科学风格中，包含概率和非确定性的早期处理试图引入分布式系统的概率模型，这在澄清与概率和非确定性如何相互作用有关的许多问题方面走了很长的路。[4]这项工作的一个主要贡献是为一般的概率属性[18]和特定的时间属性[20，2，6]提供了具体的语言和验证技术。这样的属性的例子包括后来的工作扩展了应用领域，包括事件之间的平均预期时间和最短路径问题[3]。[4]当我们单独写26C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）23这些处理的一个关键组成部分是提供计算指定属性的实际算法，许多模型检查系统都基于早期工作中提出的思想在本文中，我们处理的问题，但与计算机科学风格的工具，特别是域理论：我们解决的问题表明，存在一个无记忆策略的最大化的参与者在迭代游戏中，其无限行为的值为零（因此最小不动点）。我们使用左关联点“。对于函数应用程序，并按照约束变量然后约束然后项的顺序编写量化，范围是显式的，通过将这些参数（· ··）或参数组合到分支上来指定值{· ··}：您可以选择位置缓存{i：Z|i>0·i3}。3经典观点：马尔可夫决策过程3.1基础知识在本节中，我们阐述了MDP设S是有限状态空间，L是有限标签集，S是S上离散概率分布集。5定义3.1 S上的有限状态马尔可夫决策过程是一对（ρ，ω），其中ρ是L×S→S型的转移系统，ω是L×S→ R型的报酬函数。 转移系统ρ将L中的每个标签l和S中的状态s映射到最终状态上的概率分布ε.l. s，而ω指定一个在状态s中选择标签l之后立即奖励b.l. s。下面的比喻，补充了上述定义，提供了一个基于赌徒玩机会游戏的有用直觉• 从任何位置s，他可以从#S面骰子中选择，每个骰子上都写有S的元素;每个骰子都有一些标签l，并根据分布l. l. s进行偏置。• 每一个骰子的选择都会产生一个直接的成本或奖励。[5]稍后我们将扩展S以包括子分布，即那些和不超过1（而不是正好为1）的子分布。C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）2327∫• 他的总期望赢款由支付函数φ：S→R决定，由他的即时奖励和他掷出所选骰子后达到的最终状态sJ决定：总的来说，他赢得φ.sJ加上奖励。因此，如果在MDP（ρ，ω）中，赌徒从初始状态s开始游戏，并选择掷出标记为l的骰子，则他的总期望一步获胜由下式给出：(1)M.l.s.φ：=M.l.s. φ+M.l.s.公司简介其中我们因此让M代表l，s和φ的函数，（ρ，ω）如上所示。 一般来说，我们写 对于随机的期望值，分布上的变量φ 在有限的情况下，如这里，积分（1）isysJ：S（ρ. l. s. s×φ.s），因为分布是由MDPJ J是唯一的，有限期望值只是加权和。一个赌徒M. H，定义如下：6定义3.2对于MDPM=（ρ，ω），我们定义M. H.φ.s ：=（Hl：L·M.l.l.s. s）=（Hl：L·M.l.l.s.+S公司简介φ）。我们用Filar的一个例子来说明上述定义，在图1中重现（但略有修改）。假设图1中的MDP为M，并考虑由下式给出的支付函数φ：φ.s1：= 10，φ.s2：= 20，φ s3：= 30。那么赌徒M. H.φ.s2=（10 + 1×20）H（5 + 0. 8×10+ 0。2×20）= 30H 17=30。6严格地说，符号“M。H这个非正统但具有启发性的符号在后面会很有用。28C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）23标签l1标签l2状态s1状态 s2状态 s3在这种表示中，框描绘了状态中的动作及其奖励/转换（左上/右下）结果。例如，在上文中，标签l 1的选择导致来自状态s 1的奖励ω.l1.s1= 0，并且转移概率ρ.l1.s1.s1= 0。9，ρ.l1.s1.s2= 0和ρ.l1.s1.s3= 0. 1.如果有不同数量的替代品（例如，在状态S3中只有一个标签），我们认为缺失的标签给出了对于该状态已经存在的标签的效果的“副本”。这样，在理论中，我们可以假设标签的数量是固定的。Fig. 1. 一个可和的马尔可夫决策过程[5，例2.1.1 p10]3.2折扣游戏现在假设赌徒重复玩，在他玩的过程中积累他的奖励，以给出一个整体的“多步”获胜。在每个状态下，他选择一个标签来决定他的下一步行动;让他的策略是σ：S→L，代表提前 赌徒现在是评估他的策略的有效性，如果他遵循它，根据他的总体收益。 策略σ、转移系统ρ和初始状态s共同决定了S中状态序列的一个定义明确的概率分布，赌徒在玩游戏时会观察到这个分布。从该分布可以计算出预期的总奖金，尽管对于某些游戏，它可能会被低估。有一种保证确定性的博弈是贴现成本博弈，我们现在描述它。3.3贴现MDP是一个元组（ρ，ω，β），其中（ρ，ω）是一个（未贴现的）MDP，0≤β 1的额外分量β是贴现因子。游戏是根据上面的一些策略σ进行的，但是奖励是“discounted” according to when they occur: a reward after折扣的效果是，越晚收到奖励，它的价值就越低：因此，它的价值以固定的百分比下降。假设赌徒在第0步从初始状态s0开始玩由（ρ，ω，β）给出的MDP：折扣对于他的第一步是无效的（它是β0），所以他的第一个奖励是（0，1， 0）15（0. 九，零，零。第一章0（0. 八，零。（第2、 0段）5（0，1， 0）1025（0. 九，零。1、C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）2329ω。（σ.s0）.s0，与单步情况相同。对于他的第二步，从概率分布ρ中选择的某个状态s 1。（σ.s0）.s0，他将（仅）获得贴现值β×ω。（σ.s1）.s1;因此，当他达到国家时，他的预期s1是ω。（σ.s0）.s0+β ×ω. （σ.s1）.s1d s1.7ρ. （σ.s0）.s 0类似但越来越复杂的表达式给出了后面步骤的预期总回报。 请注意，这里我们没有使用最终支付函数φ，因为游戏是无限的。一般来说，对于折扣M=（ρ，ω，β），我们将策略为σ的第n步之前的总体预期收益记为M.. n. s。8因此，当n增加时，赌徒按照策略σ进行游戏时，他的总期望赢额就是上述的极限，即lim n →∞ M.. n. s，相应地我们记为M.σ。∞.s.事实证明，对于折扣成本博弈，类σ策略足以实现最大可能的总体预期收益;通过下一个定理，我们概述了传统的证明。(That我们不需要更强大的战略，就像第二章所描述的那样（见下文第3.3段）定理3.4一个赌徒在进行定义3.3中的折扣博弈时，可以通过遵循类σ策略获得最大可能的期望收益。证据标准证明使用线性规划技术;有关详细信息，请参阅Filar [5]。Q在接下来的章节中，我们将研究同一结果的域理论证明，然后我们将其扩展以表明即使在博弈不打折的情况下，该结果也适用。3.3更一般的策略我们上面考虑的[7]按照通常的方式，我们将“d s 1“理解为表示表达式ω的函数抽象。（σ.s1）.s1在其参数s1上。因此，积分符号的辐角是S上的函数，这是应该的。[8]继续我们对符号的滥用，我们在M中使用上标来提醒我们，在这种情况下，我们正在迭代单步M。用σ代替标签表明，标签是根据该策略选择的;我们在之前由payo φφ占据的位置上写上（integer）n，因为两者都与MDP的停止有关。30C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）23≥≥≥≥无记忆的，因为它们只依赖于当前状态，而不依赖于迭代过程M*可能已经通过的任何先前状态然而，还有更一般的策略;一个策略能考虑的信息越多，它就越对我们来说，最有趣的行为是实现最大期望的行为。payo M. H. ∞. 我们在下面给出了一个域理论风格的证明，σ类策略--纯粹的、稳定的和无记忆的--足以做到这一点，只要我们把自己限制在非负的奖励上。这种策略的进一步意义在于，它们将整个问题重新置于有限状态空间的背景下，因为对于有限状态空间S和有限多个标签，只有有限多个这种类型的策略。(On另一方面，即使稍微推广到这意味着，通过这种策略可以获得最佳回报的赌徒可以使用线性规划技术来评估他们的最佳预期收益4计算机科学视角：领域理论我们正在研究我们首先回顾一下域理论的一些基本事实。4.1一个数量函数偏序集是一个对（C，±），其中C是一个集合，±是C上自反、反对称、传递的序。据说订单已经完成如果C中的任何链在C中有一个最小上界，其中链是全序子集。在这里，定义域是一个具有最小元素的完全偏序集。给定一个有限状态空间S，我们构造S上R∞值函数集ES，其中R∞是用顶元完备的非负实数集他们被称为payo。我们在这里使用∞的唯一目的是确保（R∞，≤）是完备的（因此是一个域），也就是说，我们使用的∞的唯一性质是它支配所有真实数。接下来，我们将R∞上的≤提升到ES逐点，定义φ，φJ：ES，φ± φJi ≠（φs：S·φ.s≤φJ.s）。我们使用不同的符号（C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）2331秩序只是部分的。对于实数k，我们将k写为常数值的payo，对于所有状态，值为k因此，ES的最小元素是0，最大元素是∞，我们注意到以下内容：引理4.1空间（ES，±）是一个Domain。我们将看到，MDP的最优值可以作为支付域中的一个“固定点”找到然而，在域理论的背景下，固定点的存在更为直接。一般来说，如果定义域上的函数是“单调的”，则保证称F：C→C是单调的，如果c±CJ蕴涵F.c±F.CJ。 我们写µ.F对于F在C中的最小固定点，它是±最小元素c，使得F. c=c.令人高兴的是，折扣积累游戏，如M。H. ∞，有单调的单步函数M. H在ES上的阶±上，因此我们立即知道它们的最小不动点存在。当然在在某些情况下，最小固定点可能是无限的（如在累积博弈中，如果没有折扣）。取最小固定点似乎是一个武断的决定，但事实上，它与操作规范一致，即参与者在“通过”时只获得由他对ω的吸引力明确确定一个零的薪酬在“无限”等着他。 (Note也就是说，最大的固定点的任何M，使这是一个不太可能的选择。实际上，最小固定点的性质正好证明了线性规划技术中使用的约束条件，这些约束条件通常用于计算最大的总价值。翻译成MDP积累游戏符号。 3.1，lfp归纳性质说，最小固定点的M. H是满足以下条件的最小支付M. H.φ±φ，该不等式是函数的比较，可以解释为一组不等式，状态空间的每个元素对应一个不等式。与累积博弈的联系由以下引理给出引理4.2设M是具有非负报酬函数ω的MDP。 那么迭代博弈的最大期望总收益M是H. ∞最小32C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）23payo-to-payo函数M的固定点。H.类似地，对于策略σ，迭代博弈M的期望收益为.σ。∞是函数M的最小不动点。证据任何一种形式的游戏的价值-无论是M。H. ∞或M∞。H. ∞-是作为无穷和的极限给出的;在相应的不动点的迭代计算中会出现完全相同的和。Q游戏的价值是玩家决定如何玩的基础-如果他玩了一个糟糕的策略，那么他的最终收益将远离游戏的价值。另一方面，如果他使用一个好的策略，那么他的预期收益将接近游戏的价值。线性规划技术[5]可以用来计算他的最优策略;不幸的是，对于许多相当大的系统，巨大的状态空间使得线性编程解决方案不可行，从而需要采用替代的计算策略。在这里，域理论方法将建议使用迭代，这确实是实践中采用的方法（例如PRISM[8，7]）。然而，确定最佳策略仍然是一个问题，我们接下来将把注意力转向这个主题。4.2折扣对策我们首先用域理论的术语定义一个折扣博弈，这样我们就可以研究它的性质。首先，我们定义从状态空间到实数（包括负数）的任何函数f的“ 范数” f。定义4.3函数f：S→R的范数是其余域中的最大绝对值：我们有φ|X.s|）的情况下，哪里|·|表示绝对值。显然，对于有限个S来说，f总是有限的。我们现在定义定义4.4从ES到ES的函数F是压缩映射，因子β，如果0≤β 1，且≤β ×对于所有的payoφ，φJ。现在我们展示如何将折扣MDP视为压缩映射。给定一个未贴现的（ρ，ω）和一个贴现因子β，形成C. 摩根A.McIver/Electronic Notes in Theoretical Computer Science 130（2005）2333×β（同样是未折现的）因为β1我们称它们为子分布;把它们看作一个矩阵（β×ρ）。当M是（ρ，ω）时，我们将（β×ρ，ω）写成M×β;注意，只有转移概率，而不是奖励，由β缩放。请注意，我们立即拥有以下属性。引理4.5由未贴现的MDPM的β标度 M×β由M本身支配：对于所有的payoφ，我们有M×β。H.φ± M. H.φ。因此，我们可以写为M×β。H±M。H.我们现在观察到M×β。H是具有因子β的压缩映射。引理4.6对于任何MDPM，payo ∈ φ，φJ和实数0≤β，我们有：M×β。H.φ − M×β。H.φJ≤β ×。因此，只要β<1，我们就有M×β是关于度量φ·φ的压缩映射。证明（略）假设相反，对于一个矛盾;令是某个实δ。那么对于某些状态s，我们必须有wlogM×β。H.φ.s + β × δ

下载后可阅读完整内容，剩余1页未读，立即下载