理论计算机科学电子笔记149（2006）125-137www.elsevier.com/locate/entcs基于概率模型检测的自动博弈分析：一个案例研究P. Ballarini1，M.费希尔2号，M.J. Wooldridge3英国利物浦大学计算机科学系摘要一段时间以来，人们已经认识到，为分析多智能体系统而开发的各种逻辑与为同一目的而开发的许多博弈论模型之间存在密切联系。在本文中，我们有助于这一新兴的机构的工作，展示了概率模型检测工具可以用于自动分析的游戏样多智能体系统中，代理和环境可以采取行动的不确定性。具体而言，我们展示了如何对Rubinstein的著名交替操作者协商协议的变体进行编码作为PRISM模型检查器的模型，并通过自动验证概率CTL的属性来分析其行为关键词：代理，不确定性，概率模型检验。1引言在博弈论中，谈判被认为是两个参与者就一个或多个项目讨价还价的游戏。玩家每个参与者的效用本质上取决于博弈结果（即达成协议的价值）。 这样一个博弈（即广泛博弈）的一个博弈表示为：根据描述玩家在整个过程中的后续动作的历史1 电子邮件地址：paolo@csc.liv.ac.uk2 电子邮件地址：michael@csc.liv.ac.uk3电子邮件：mike@csc.liv.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.030126P. Ballarini等人/理论计算机科学电子笔记149（2006）125协商讨价还价者可能采取的行动是接受最新的讨价还价者或抛出一个反讨价还价者。玩家的策略决定了他/她在特定历史下的下一步行动（即在货币谈判中，策略也决定了在拒绝最近一次行动的情况下后续行动的价值）。参与人的可能策略也称为纯策略。如果考虑了不确定性，那么概率分布是给纯策略的，我们讨论混合策略，因此是期望效用。博弈论的目的是研究参与者策略的性质。一个使参与者的效用最大化的策略给定一个博弈G，像或者需要研究人员来解决。在本文中，我们专注于著名的鲁宾-斯坦的交替供应商的谈判框架的变化特别是，我们将考虑球员采用混合策略，而不是纯粹的，我们展示了如何，在这种情况下，概率模型检查器可以作为一种替代手段的框架分析。我们考虑了有限数量的策略配置文件，并提供了一个比较分析，在相应的概率分布在一组协议（因此预期效用）。这种方法不同于通常用于游戏分析的模拟和数学分析技术。特别是，我们的方法是自动的，因为是模拟技术，但涵盖了所有可能的行为的系统，TEM，做数学分析技术。因此，我们的方法提供了一种自动的方法来分析一个精确的计算预期有关可能的系统行为。本文的结构如下。在第2节中，我们回顾了协商问题，特别是我们在第4节和第5节中将这两个方面结合在一起，在第4节中描述了讨价还价协议的概率模型，并在第5节中对这种情况进行了一系列验证实验。最后，在第6节中，我们提供简短的结论性意见。2替代供应商谈判框架在过去的二十年中，已经开发了许多协议和相关的多代理系统中的自动协商策略。 其中最早的，也是最具代表性的，是单调让步协议P. Ballarini等人/理论计算机科学电子笔记149（2006）125127≤≤ψRosenschein 和 Zlotkin [10] 从 Harsanyi 和 Zeuthen 以 前 的 工 作 中 改 编 的Zeuthen策略。在这项工作中，作者首次在自动谈判环境中对这种谈判方法进行了真正的评估。最近在自动化谈判方面的工作主要集中在谈判的替代模型上：Rubinstein提出的交替代理模型[8]。在这里，我们简要介绍它指的是有兴趣的读者的文献更多的细节。在鲁宾斯坦的行动者模型中行动可以是（i）提出一个建议（opposer），或（ii）接受最新的建议。 我们选择nts，a和an，谈判发生在一系列回合中，我们假设这些回合由自然数索引。代理a在第0轮开始，提出一个prop_x_0，其中代理a可以接受（A）或拒绝（R）。如果亲P被接受，则交易x0被执行。 否则，谈判就会到另一轮，在那里年龄nta是一个支持者（cou nter-o-changer），年龄nta选择接受或拒绝它。这样一个游戏的历史是一个（可能是无限的）序列（x0，R，x1，R，...，xn，.. . ）和终端 历史是有限的一个以A，（x0，R，x1，R，...， xn，A），其中xn是讨价还价结果。玩家在 Rubinstein的框架中，时间期限被考虑到两个参与者（Ta和Ta），因此排除了无限历史。最后的不同意被认为是最坏的可能结果，因此第一个达到最后期限的玩家将接受最新的结果（即最后的不同意）。所有的历史都是终结者）。此外，在Rubinstein的交替决策框架中代理人a（买方b或卖方s）在时间t（0不Ta）介于其初始价格（IP a）和其保留价格（RP a）之间，定义如下：pt=a→aIPa+φa（t）（RPa−IPa），其中a=b，（1）RP a+（1−φ a（t））（IP a−RP a）， a=s，几个时间相关函数可以通过协商决策函数（NDF）φa（t）来表征，其如下：φa（t）=ka+（1−ka）（t）1（二）不是其中ka确定代理人a在其第一个建议中所要选择的价格通过改变φb（t）的值，可以得到不同类型的策略（参见图1中的φb（t））：对于φb1，我们讨论的是boulware策略（在大多数时间内，φ b非常缓慢地增加/减少，并随着时间期限的临近迅速达到RP），对于φ b=1，我们有线性策略，而对于φ b（t），我们讨论的是boulware策略。.128P. Ballarini等人/理论计算机科学电子笔记149（2006）125M|MM|M当k>1时，我们讨论让步策略。在概率变量中RPbIPb0.20.40.60.8 1Fig. 1. φb（t）的类型在Rubinstein的框架中，我们将在第4节中讨论这方面的问题。3概率模型检测模型检测[4]是一种成熟的方法，用于测试系统的模型是否符合某些时态逻辑公式所表示的属性。模型检查器将模型和公式φ作为输入并返回如果所有执行都满足φ，则通过（即：=φ）或否如果不是（即=φ），在这种情况下，提供检查属性的反例。模型检查技术可以根据它们所涉及的模型类型进行分类。在这个意义上，我们可以区分允许表示非确定性而不包含任何不确定性非概率系统可以用标记转换系统（LTS）来建模，本质上是状态图，其节点附有陈述状态中什么是真的命题。线性时间-时间逻辑[9]及其分支时间扩展，计算树逻辑[3]，允许针对LTS验证定性属性当可以设计关于系统行为的可能性的指示时，则可以构建概率模型。马尔可夫过程[5]是随机过程的一个子类，适用于建模系统，使得可能的概率价格（承认）（线性）（博尔韦尔）t/TbP. Ballarini等人/理论计算机科学电子笔记149（2006）125129M→→→ →∀ ∈转移概率矩阵使得S∈S，L：S → 2 AP是一个标记函数。sJ∈SP（s，sJ）= 1且未来的发展完全取决于当前的状态，而不是过去的历史（即通向未来的道路）。 一个系统的定时也要注意马尔可夫链模型导致离散时间马尔可夫链（DTMC），时间被认为是离散量，或连续时间马尔可夫链（CTMC），当时间被认为是连续的。在过去的几十年中，通过模型检查对马尔可夫链的验证得到了广泛的发展，从而产生了特定的时间逻辑和验证算法的特征：用于DTMC验证的概率计算树逻辑（PCTL）[6]和用于CTMC验证的连续随机逻辑（CSL）[2]。在下文中，我们简要介绍了PCTL模型检查的基本原理，这是我们在这项工作中提到的验证技术。读者可参考文献以了解详细的处理方法。定义3.1给定一组原子命题AP，一个标记DTMCM是一个元组（S，P，L），其中S是一个有限的状态集S，P：S×S→[0，1]是给定DTMC =（S，P，L）中的路径及其概率测度在以下定义中被正式表征。定义3.2从状态s0开始的路径σ是无限序列σ=s0s1...s n. 使得iN，P（si，si+1）>0。给定σ，σ [k]表示σ的第k个元素。一组具有共同有限前缀的无限路径的概率测度σ↑n = s0→. →sn被定义为前缀σ↑n中跃迁概率的乘积。定义3.3设σ↑n = s0→. n是M的有限路径。以σ ↑ n为前缀的（无限）路径集合的概率测度为：n−1概率（σ↑n）=P（si，si+1）i=0时如果n> 0，则Prob（σ ↑ n）=1，如果n = 0。定义3.4（PCTL语法）PCTL状态公式（φ）和路径公式（φ）的语法归纳定义如下：130P. Ballarini等人/理论计算机科学电子笔记149（2006）125PP一组原子命题AP：φ：=a|TT| ¬φ|φ∧φ|Pp（）φ：=φ U≤tφ其中a∈AP，p∈[0，1]，t∈N<$N{∞}且<$N∈{≥，>，≤，}，PCTL的语义与CTL的语义相同，只是概率路径公式不同。式在一个状态s中，如果从s开始并满足条件的路径的概率测度，记为Prob（s，n），满足边界条件，则满足条件p。形式上：S| = Pp（φJU≤tφJJ） i <$Prob（s，（φJU≤tφJJ））<$p其中（φJU≤tφJJ）关于路径σ的语义定义为：σ|= φJU≤tφJJii≤t：σ[i]|= φJJ<$jS RP）≠（tTs）（三）1if（t≥Ts）⎧⎪⎨1if（x<=0）<$（t≥T b）B AP（x，t）=1+S RPx−（B RP+SRP）如果（S RP x B RP）≠（tTb）（四）0if（x>BRP）图3描绘了两个参与者对于在时间期限内接收到的操作者的接受概率（即，图3中的曲线涉及函数3和4在一般时刻t上的投影，即，具有t Ts和tTb的函数S AP（t）和B AP（t<<））。应当注意的是，我们的定义假定买方知道卖方的保留价格（见功能4）。虽然不切实际的这种选择并不妨碍我们的工作，这是表明概率模型检验可以卓有成效地用于分析的目的。游戏的解。不需要侵犯玩家隐私的S AP（）和B AP（）的替代公式在图5中，所描绘的曲线对应于使得卖方和买方保留价格分别为S RP= 1000和S RP= 10000的设置132P. Ballarini等人/理论计算机科学电子笔记149（2006）125∼中标概率1.00.90.80.70.60.50.40.30.20.10.0S_RP=1000x=报价B_RP=10000图三. 接受概率函数：S AP（t），B AP（t）NDF的分段近似在我们的模型中，属于方程2中定义的族的连续NDF（φ（t））由两个分段组成的分段线性函数近似6（见图4）7。该函数有三个参数：第一块的斜率，第二块的斜率和块之间的边界（切换时间）。通过模型配置来选择所需的设置（boulware/concender策略），以便验证不同的策略配置文件（策略组合）（即导出每个可能的谈判结果的概率）。两段线性NDF100090080070060050040030020010000 2 4 6 8 10时间见图4。 NDF[6]两段线是极端讨价还价策略（即，100或100>>1）的一个很好的近似，这是我们在本书中感兴趣的非线性策略类型不那么极端的策略可能更好地近似于多段线，这将需要对我们的模型进行最小的修改才能处理。图7所示曲线对应于工件斜率和切换时间的特定设置。S_AP（x）买 方 - 布 尔 （ 1/500 ） -Tswitch=8卖方-布尔（1/500）-Tswitch=8 买方-浓度（490/1）-Tswitch=2卖方-浓度（490/1）-Tswitch=2要约接受概率->P. Ballarini等人/理论计算机科学电子笔记149（2006）1251335模型在交替操作框架的DTMC模型内编码的概率行为（即，接受概率函数）导致在一个概率分布上的一组可能的结果的假设（即区间[S RP，BRP]），因此在一个战略配置文件的支付。 为了验证我们的模型，我们只考虑设置，S RP B RP，特别是我们的大部分分析都涉及S RP= 10000和S RP= 11000一旦一个策略配置文件（例如Boulware-Boulware或Conceder-Conceder等）已通过配置选择，通过使用PRISM工具验证以下PCTL公式并对照框架模型来确定相应的概率分布：P=？（tt U（agreement）购买=PV AL）（5）上述属性捕获了在讨价还价过程中的某个时刻达成特定价值（PV AL）协议的那些演变。使用PRISM工具，对于每个可能的一致性值（PV AL∈[SRP，B RP]），（5）的验证为我们提供了结果集上的概率分布，因此所得的预期效用可以是直接的-前向派生（为了简洁起见，我们不在这里报告在开始验证阶段之前，需要对模型进行确认。配置需要设置一些参数，其中包括我们想要研究的策略组合（即策略的斜率和双方玩家的切换时间）。可能的策略显然是无限的，但就我们的目的而言，我们只考虑有限数量的组合，我们的目标是通过模型验证的结果进行比较。为了提高模型我们观察到，模型验证的数值结果受所选区间的影响（作为函数（3）和（4）定义的结果）。下面我们报告我们通过验证（5）对任意设定为[10000，11000]的可接受区间（即，宽度：103，o参考集：104）。我们将比较由此产生的概率分布（累积-tive）的不同策略配置文件，指出其中的战略是占主导地位的考虑。 我们提出的结果是根据不同的策略类型进行分组。我们将Lin（x）-Lin（y）表示为非线性策略曲线，其中x和y分别是买方和卖方NDF的第一段斜率134P. Ballarini等人/理论计算机科学电子笔记149（2006）125∼∼∼在切换时间之前相交。另一方面，例如，我们使用Boul（x/xJ）-Conc（y/yJ）来表示一个轮廓，使得玩家线性-线性对称：在此设置中，我们考虑斜率相等的Lin（x）-Lin（y）轮廓（即x = y）。在图5（a）中，比较了不同斜率值（即Lin（10）、Lin（50）和Lin（100））的可能一致性的概率分布该图基本上表明，较大的斜率值导致接受区间内相等值的概率较高。对应的期望值大致相同：Exp（Lin（10））498，Exp（Lin（50））499和Exp（Lin（100））500，显示出较大的斜率倾向对卖家有利。图5（b）中的图表也证实了这一点，该图表代表了三种情况的累积分布函数。图中的曲线表明，从卖方的角度来看，较大的策略110.80.10.60.010.40.0010.20.00011000010100102001030010400105001060010700108001090011000提供价值00100200300400500600700800900 1000提供价值(a) 概率分布（b）累积分布图五. Lin（x）-Lin（y）对称轮廓Linear-Linear asymmetric：这里我们考虑Lin（x）-Lin（y），但斜率值不同为了研究-在谈判的概率结果上的策略梯度的证据中，在图6中，描绘了几个不对称Lin（x）-Lin（y）分布的累积分布。我们观察到，通过增加买方第1001章林（一百）-林（一百）第1050章林（50）-林（10）第1000章林（十）-林（十）林（100）-林（100）林（50）-林验收累积概率接受概率P. Ballarini等人/理论计算机科学电子笔记149（2006）125135卖方）。这一点再次通过观察期望值得到证实，它们显示出相同的趋势 ， Exp （ Lin （ 50 ） Lin （ 10 ） ） <$692 ， 而 Exp （ Lin （ 100 ） Lin（10））<$804。10.80.60.40.2001002003004005006007008009001000提供价值见图6。Lin（x）-Lin（y）非对称分布：累积概率非线性不对称：当我们考虑非线性轮廓时，类似的结论也是有效的，其中NDF在切换后相交，并且斜率不同（对于两个部分）。在图7（a）中，比较了具有不同梯度的非对称Conceder组合的累积概率在那里，我们可以观察到，较早切换到策略的低梯度部分的配置文件倾向于将概率累积到更接近区间的较高效用的一半。例如，如果我们比较图7（a）中的Conc（10/ 1）-Conc（100/ 10）-T sw：4和Conc（10/1）-Conc（100/ 10）-T sw：8中的梯度相等但开关不同的曲线，这是显而易见的，前者对应于卖方的较早开关时间（等于4），后者对应于延迟开关时间（等于8）。类似地，在图7（b）中，将布尔（1/ 100）-浓度（100/ 1）分布的累积概率与图7（b）中的图表证实，对于恒定斜率6结论在本文中，我们展示了一种不同的方法来验证多人游戏，该方法可以用作分析方法和/或模拟的替代方法（或与之结合）。我们已经说明了分析是如何第1010 章 林 （ 一百 ） -林（十）第 1050 章 林 （ 50 ） - 林（10）林 （ 10） -林 （ 10） -林（100）林（50）-林验收累积概率136P. Ballarini等人/理论计算机科学电子笔记149（2006）125110.80.80.60.60.40.40.20浓度（10/1）-浓度（100/10 ）-Ts_sw：4浓度（10/1）-浓度（100/10 ）-Ts_sw：8浓度（100/10）-浓度（10/1 ）-Tb_sw：4浓度（100/10）-浓度（10/1）-Tb_sw：80.200100200300400500600700800900 1000提供价值0100200300400500600700800900 1000提供价值(a) 浓度-浓度不对称（b）Boul-Conc不对称见图7。非线性策略分布特定协商（混合）策略的执行可以通过概率模型检查来进行。这是通过开发一个特定的概率模型来实现的，然后使用PRISM模型检查器对概率属性进行验证。这种分析有助于比较几个战略变量对谈判结果的概率的影响。特别是，我们已经表明，越大的值的OKER函数的斜率导致在更大的预期协议的概率分布接受OKER倾向于累积到接受区间的上确界。此外，对于恒定斜率的非线性策略，最早的切换时间（到分段线性操作器函数的低梯度段）相对于其他切换时间占主导地位据我们所知，这项工作为使用成熟有效的自动验证技术作为游戏分析的模型检查提供了一个新手贡献。虽然我们只提出了所获得的结果的选择，还有很多工作要做，我们相信，这种方法有潜力改进博弈分析，在自动化分析程序，并在复杂的谈判sce- narios的发展。具体而言，我们未来发展的首要任务是通过模型检查解决纳什均衡分析问题鸣谢：本工作得到EC Marie Curie奖学金的支持，合同编号为HPMF-CT-2001-00065。引用[1] R. Alzheimer和T.亨辛格Reactive模块。系统设计中的形式化方法，15（1）：7-48，1999。布尔（1/100）-浓度（100/1）-Tb：20-Ts ： 9 布 尔 （ 1/100 ） - 浓 度（ 100/1 ） -Tb ： 20-Ts ： 6 布 尔（1/100）-浓度（100/1）-Tb：20-验收累积概率验收累积概率P. Ballarini等人/理论计算机科学电子笔记149（2006）125137[2] C.拜尔湾Haverkort，H.赫尔曼和J·P·加藤。连续时间马尔可夫链的模型检验算法。IEEE软件工程学报29（6）：pp. 524-541，2003年6月。[3] E. Clarke，E. Emerson和A. 西斯特拉 使用时态逻辑规范的有限状态并发系统的自动验证。ACMTransactions on Programming Languages and Systems，8（2）：244[4] E. M. Clarke，O.Grumberg和D.A. 佩尔德。模型检查。麻省理工学院出版社，2000年。[5] W.费勒概率论及其应用导论。John Wiley and Sons，1968年[6] H. A. Hansson 和 B. 琼 森 关 于 时 间 和 可 靠 性 的 推 理 框 架 。 在 Proc. 10 thIEEEReal-TimeSystemsSymposium，第102-111页，SantaMonica，Ca.，1989. IEEE计算机学会出版社.[7] M.夸托科夫斯卡湾Norman和D.帕克Probably symbolic model checking with prism：A hybridapproach. International Journal on Software Tools for Technology Transfer（ STTT ） ，2004.[8] M. J. Osborne和A.鲁宾斯坦讨价还价和市场。学术出版社：伦敦，英国，1990年。[9] A.普努埃利程序的时间逻辑。第18届IEEE计算机科学基础研讨会论文集，第46-57页[10] J. S. Rosenschein和G.兹洛金相遇规则：设计计算机之间。麻省理工学院出版社：马萨诸塞州剑桥，1994年。
我的内容管理
展开
