量子计算中的安全性分析方法

理论计算机科学电子笔记153（2006）195-212www.elsevier.com/locate/entcs一种新的基于定量μ-演算的Annabelle McIver安娜贝尔·麦基弗1，2部计算机科学MacquarieUniversitySydney NSW 2109，AustraliaCarroll Morgan卡罗尔·摩根1，3部 比较科学&Eng.新南威尔士大学悉尼NSW2052，澳大利亚摘要定量μ-演算qMμ将Kozen的标准μ -演算[ 5 ]的适用性扩展 在其引入之后[9，4]，我们已经开发了[6，7，8]， 其他人[2]。除了它在定义概率时态逻辑上的自然应用之外，还有许多其他领域也从它的使用中受益。一个应用是随机两个玩家的游戏，本文的贡献是离开通常的概念扩展的动机是基于经济博弈的例子：我们提出了一个qMμ的扩展，以便它们可以被指定;我们表明，扩展可以通过减少表示原来的逻辑，并通过这种减少，我们证明，球员可以发挥最佳的扩展游戏使用无记忆策略。关键词：概率系统，μ演算，定量逻辑，随机博弈，中间不动点，平局和僵局。1我们衷心感谢澳大利亚研究委员会（ARC）通过其发现项目资助DP034557的支持。2电子邮件地址：anabel@ics.mq.edu.au3电子邮件地址：carrollm@cse.unsw.edu.au1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.039196A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）1951引言概率系统结合了计算机系统和随机事件的标准特征，因此它们的大量属性是定量的而不是定性的，并且不能使用标准方法进行验证。定量程序逻辑[4，9，14]的发展是为了克服普通程序逻辑的局限性，特别是考虑到概率行为。特别地，定量μ演算qMμ扩展了Kozen [5]的标准μ演算，通过将项解释为状态的实值函数而不是布尔值函数来获得概率。与标准μ-演算一样，qMμ包含一种具有简单定义语义的建模语言，以及作为两人游戏的操作解释，扩展了Stirling [12]，并建立了与随机奇偶游戏[1]及其相关算法验证方法的正式联系然而，并不是所有的博弈都自然地适合于这个框架，在这篇文章中，我们研究了一个新的博弈，它出现在某些（不一定是概率的）系统的具体化中，并展示了定量μ演算如何成功地适应它。作为我们研究的游戏类型的一个例子，我们考虑两个玩家Max和Min被给予一堆20个1美元硬币彼此分享的情况。他们同意执行以下协议，以确保公平分配：首先，Min选择一个金额s给Max，Max接受或拒绝它。在他接受的情况下，敏然后收到$（20-s）;否则她被迫再次选择。从本质上讲，这个游戏只有两种结果--要么在一定时间后结束游戏，马克斯和敏把硬币分成彼此满意的程度;要么他们玩得不确定，永远无法达成一致。在标准（和定量）μ-演算中，无限次执行是通过固定点来处理的-基本上最大的固定点被解释为Max的绝对胜利，而最小的固定点则相反，即。 敏绝对赢了然而，在上面的协议中，似乎很明显，无限次执行应该被判断为某种“平局”或至少是“僵局”，而不是任何一方的决定性胜利，这种结果不能用一个最小或最大的固定点来我们采用的解决方案使我们提出了一种新的固定点，我们将其视为中间获胜条件。具体而言，我们的贡献可以总结如下。(i) 对定量μ演算的简单扩展，允许直接指定表现出中间3、第二。4）、(ii) 证明了这种游戏在传统意义上的博弈论中确实有很好的定义，我们的意思是玩家可以评估A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195197他们的策略相对于其他参与者的策略的效果，并且两个参与者都可以遵循最佳策略（第二节）。4）、(iii) 一个详细的案例研究的启发，经济应用，和分析方法的基础上，上述理论结果（第二节。5）。该方法的关键将是使用qMμ，并在第二节。2我们回顾了它在概率系统上的解释。在整个过程中，以下符号约定适用。一个固定的'。用于函数应用。我们写S为（固定的）底层状态空间，S为S上的离散概率分布集，其中离散概率分布是一个函数，从m到tval[0，1]，其中ich是n或-将S转化为1;t husS=0{Δ：S→[0，1]|s∈SΔ.s=1}。功能设置从S到实区间[0，1]的距离用ES表示，称为期望在S.S上的实值函数（例如，期望）通过逐点提升实数上的阶≤来排序;函数max和min也同样被提升;我们将常数函数写为x，返回所有状态的实数x，其中通常我们会有0 ≤ x ≤ 1。如果Δ是一个概率分布如果A是S上的可测函数，则ΔA表示期望A的值，其中h小于Δ。当nΔ在S中时，A是一个可靠的值S上的函数，这简化为s：SΔ.s×A.s。2定量qMμ-演算和博弈在本节中，我们总结了μ演算的细节，从语言的定义开始，然后回顾公式如何在概率转移系统上以两种等价的方式解释。逻辑中的公式φ（正形式）构造如下：X|一|{k}φ|φ1Hφ2|φ1Hφ2|φ1GD φ2|（μX·φ）|（νX·φ）在公式的解释中，将给出以下含义• 变量X用于绑定固定点。• 术语A代表ES中的固定函数（通常）。• 项k表示标记的概率转换（如下所述）。• 项G描述S的布尔函数，即（“if”）GD（“else”）。• （μX·φ）和（νX·φ）是极值点，约束φ中的任何自由X我们避免使用分别形成天使-（存在-）和恶魔（普遍-）选择的通常模态，因为它们可以等价地（在我们框架的假设中）通过{k}φ和198A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195H和H。4接下来，我们将展示如何在概率转换系统上解释上述语言。这样一个过渡系统是由从S中的初始状态到S中的最终分布的函数建模的，其中分布对系统中存在的概率特征进行建模。在本文中，我们将使用标签来区分给定结果集中的各种概率分布因此，我们的抽象计算模型是（严格地说）标记的概率转移系统。5设L是标签的（有限）索引集;我们写R.L.S，使得它具有L→S→S型。因此，给定标签和初始状态，结果是S中的单个输出分布，我们称之为转移概率分布。为了解释给定（标记）概率转换系统r∈ R.L.S上的公式，我们使用指称语义学[13]中的标准赋值技术，其工作原理大致如下。给定一个公式φ，赋值V做四件事：（i）它将φ中的每个A映射到ES中的一个固定期望;（ii）它将每个k映射到一个固定标签，从而将{k}映射到由r确定的相应的固定概率转移;（iii）它将每个G映射到S上的一个预测;以及（iv）它通过包含绑定变量X的映射来跟踪固定点的“展开”的当前实例(For在（iv）中，我们允许V接管通常赋予一个单独的“环境”参数的角色公式可以用两种等价的方式来解释[6]：外延上，扩展Kozen [5]，或操作上作为游戏，扩展Stirling [12]。我们现在依次介绍。指称解释给出公式φ的含义为一个函数在ES，概括Kozen设φ为公式，V为赋值。我们写||φ||V的含义由图中给出的规则确定。1.一、公式φ的运算解释是斯特林回合制博弈的推广游戏在两个玩家之间进行，我们称之为Max和Min;Max[4]例如，模态k kφ等价于对形式{ k } φ的所有项的天使选择，其中k在（有限）子集K中。[5]然而，在本文中，标签除了作为方便的“标记”来区分不同的分布之外，没有发挥任何作用A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195199（一）||V =V||V=ˆV. A.∫（二）||V.s=100||V.s=ˆ(iii) ||φJHφJJ||V.s=ˆ||V .||V.V. K.S||V .sMIN||φjj||V .s;||V.s;和||V.S =100||V.s=ˆ(iv) ||φJGDφJJ||V.s=ˆ||V .sMAX||φjj||V .s.||V.s.||V .s if（V.||V.s if(V. G.s）else||φJJ||V.s.(v) ||φ||V=ˆ(lfpε·||φ||V),whereby(lfpε·ex p)wemeanthe[X<$→ε]函数（λε·exp）在ES→ ES中的最小不动点。（vi）||V=V||V=ˆ（gfpε·||V [ X <$→ ε ]）。||V[X›→ε]).注意，在赋值V[X<$→ε]中，变量X被重新映射到期望ε，并且固定点存在，因为ES中的最小期望和最大期望是0和1。Fig. 1. qMμ的Kozen风格指称语义其中，要么是一对（φ，s），其中φ是公式，s是S中的状态，要么是一个单一的（y），对于[0， 1]中的某个实值支付。在斯特林之后，我们将使用一个博弈位置序列称为博弈路径，其形式为（φ0，s0），（φ1，s1），.. （如果有）最后一个支付位置（y）。初始公式φ0是给定的φ，s0是S中的初始状态。从position（φi，si）到o（φi+1，si+1）或到o（y）的移动由Fig的规则s来实现。 二、假设两个参与者按照图2中的规则进行博弈，给定一个公式φ和一个初始状态s0，首先假设没有概率转移。在这种简单的情况下，结果将是记录在游戏期间观察到的游戏位置的实际序列的单个游戏路径，其中球员们已经决定了“在球场上”如何解决他们的选择，因为他们前进。或者，为了达到同样的效果，他们可以事先制定一个策略，根据游戏的进展情况来解决他们的选择。我们称这种策略为预先确定的，并将它们建模为函数σ：paths→ {true，false}，即从有限博弈路径到布尔路径。我们使用的惯例是，true对应于这个想法是，在每个相关的游戏位置，玩家在一个特定的（有限的）游戏之后“查找”他的策略，然后决定是否继续玩左或右分支。由于策略将路径作为参数，因此它们模拟了无限的内存。对于预先确定的策略，我们将σ和σ分别写为Min和Max现在更一般地假设，转换可以是概率性的;这意味着一些移动是由机会决定的。尽管如此，球员们仍然可以根据各自的策略进行比赛，但这次，200A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195如果当前游戏位置是（φ，s），则游戏如下进行：1. 如果φ是A，那么博弈在位置（y）终止，其中y=V。A. S.2. 如果φ是{k}φ，则分布V。k.s用于选择下一个状态S：下一个博弈位置是（φ，sJ）（概率为V。K.S.S.J）。3. 如 果 φ 是 φJHφJJ （ resp.φJHφJJ ） 然 后 Min （ resp. Max ） 选 择 一 个minjuncts（maxjuncts）：下一个游戏位置是（φ，s），其中φ是所选的4. 如果φ是φJGDφJJ，则下一个博弈位置是（φJ，s），如果V。G.s成立，否则为（φJJ，s）。5. 如果φ是（μX·φ）（resp.（v X·φ）），则选择一个新的颜色C，并与公式φ[X<$→C]绑定，其中X已被C取代，以备后用;下一个博弈位置是（C，s）。（这种颜色的使用很容易确定其中递归运算符实际上6. 如果φ是一种颜色C，那么下一个博弈位置是（Φ，s），其中Φ是先前与C绑定的公式。游戏开始于一个封闭的公式。无限游戏总是导致恰好有一种颜色C无限频繁地出现[12，8]。游戏的结果由称为Val的支付函数决定，定义如下。注意，它对有限路径上的颜色和长度都不敏感。7. 路径π是有限的，终止于博弈状态（y）;在这种情况下，π是y。8. 路径π是无限的，并且有（恰好一个）颜色C无限频繁地出现最小）固定点ν（分别为）μ）;在这种情况下，Val.π是1（相应地，0）。图二、随机斯特林博弈的规则他们这样做的结果不是一个单一的可能的游戏路径，而是一组路径，每一个都标有（至少对于有限路径）在游戏中出现的概率。更一般地，该结构表示游戏路径。例如，让公式为（一）={s：=s01/2s：=s1}（1H（μX·X）），其中我们实例化了一个特定的转换（而不是写k），允许它代表它自己，我们使用s0和s1表示S中的状态。 我们也用Pp<$Q来表示概率转移，其中P以概率p被选择，Q以概率1−p被选择。现在让MinA. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195201VVVV∗VC为颜色装订的最小固定点。生成的两条路径，根据她的策略，π0=ππ1=π（（μ，s0），（1H（μX·X），s0），（1）），和（（n，s0），（1H（μX·X），s1），（（μX·X），s1），（C，s1），（C，s1），·· ·），两者发生的概率都是1/ 2。事实上，博弈路径上的概率分布是由著名的测度[3]定义的，该测度由底层转移系统的特殊概率转移生成。我们称这样生成的分布为路径分布。显然，如果Min遵循不同的策略，则会生成不同的路径更一般地说，给定策略序列σ和σ，我们写[φ]]σ，σ.s0，表示Min和Max分别按照σ和σ从s0开始时博弈路径上的结果路径分布。接下来，我们考虑payo函数Val。根据图中的规则在（1）的例子中，我们看到Val.π0= 1，因为它是一条具有最终常数项1的有限路径，但是Val.π1= 0，因为无限出现的颜色C是由一个最小固定点产生的。因此，期望收益与在Min采用上述策略的情况下，1/ 2×Val.π0 + 1/ 2×Val.π1 = 1/ 2一般来说，我们写Vl，对于[[φ]]σ，σ.s0当Min和最大跟随策略序列σ和σ从初始状态s0。它定义得很好，因为Val在博弈路径的σ-代数上可积[14]。我们说，博弈作为一个整体是有明确定义的（在这个意义上，每个参与者都可以理性地博弈，也就是说， 可以评估相对于所有其他参与者的策略的特定策略），如果期望支付的所有可能策略序列上的极大极小等于极大极小。也就是说，对于S中的所有s，我们必须有（2）∫HσHσ∫Val=HσHσVal.[[φ]]σ，σ.s[[φ]]σ，σ.s我们称之为游戏的价值，通常称之为V。 一项战略如果满足以下条件，则σ对于Min是最优的对于所有的Max策略σ，Val≤V[[φ]]σ，σ.s战略σV对于Max是最优的，如果Val≥V对于所有的Min策略σ.[[φ]]σ，σ.s下面的结果总结了SSG202A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195定理2.1在有限状态空间中，由式φ给出的随机Stirling对策是定义良好的，且其值Vφ等于其表示||φ||V.A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195203因此，对于在（1）定义的BSG，相关联的SSG具有值0，因为这是根据图1中列出的规则的它的表示1.一、在参与者策略中，无记忆策略尤为重要，如果一个策略独立于历史，只取决于当前的博弈位置，那么它就是无记忆定理2.2在有限状态空间S中，每个参与者都有一个无记忆的最优策略。我们通常把最优策略写成σ和σ一个后果是。2.2是，给定一个估值V，公式φ中的每个特定H和H都可以被一个特定的布尔选择所取代，其中该选择仅取决于底层状态空间S，因此任何一个参与者所做的所有当参与者采用无记忆策略时，产生的概率结构本质上是一个马尔可夫链[3]。对于图1所给出的博弈，Min的最优策略是“总是选择正确的分支”，这等价于用（· false D·）替换图1中的H，从而得到一个 m ul a j ={ x ： = 0 1 / 2 x ： = 1 } （ 1 fal s e D（μX · X）. Obsere认为，敏以前的选择已经被有效地删除，迫使她遵循实例化的无记忆策略- Thm。2.2保证了新的BJJ-对策的值与原Bjj-对策的值相同。正如我们所看到的，实例化的布尔选择总是选择无限迭代，两条路径的payo均为0更一般地，如果σ（σ）表示Min（Max）的无记忆策略，则我们将公式的φσ（φσ）与H的每个句法出现一起写为（H）由如上所示的由σ（σ3在有限的游戏中在这一节中，我们将介绍SSG的粗略地说，这个想法是扩展Val的定义，以便沿着指定的有限路径，支付不限于0或1，但可以采取严格位于两者之间的其他（常数）值x为了说明，我们回到介绍中描述的Max和Min之间的博弈。首先，我们使用图1中的规则将协议的单个移动编码为qMμ2作为一个向导让敏选择={0}：∈{0. . . 20}，这里我们使用速记从相关的集合中选择最少。接下来，Max可以选择接受s，或者拒绝它并迫使Min再次选择。我们定义实值函数Accept，以返回在204A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195当前状态s，所以如果s= 3，那么实际上也接受s= 3。(That因为状态本身是实值的，在这种情况下，常数期望就是恒等式。）因此，我们可以用子公式Accept H X来模拟马克斯总而言之，这表明了一个公式（τX·{选择}（接受HX）），正式描述了分割货币的理想协议--但在这里，我们引入了一个目前尚未确定的X的固定点绑定τ，因为我们试图决定使用哪一个。关于我们提出的公式，首先要注意的是，支付不受限制于[0， 1]之间 ， 这 是 图 2 中 游 戏 规 则 中 的 假 设 之 一 ： 例 如 ， Min 可 能 会 选 择s=20，Max可以接受。然而，这并不是一个重要的问题，只要所有的支付都位于实数的有界闭子集内。在这种情况下，我们总是可以使用一个简单的转换来转换游戏，6它可以在不改变底层概率转换的情况下移动和缩放支付函数在这种情况下，我们需要做的就是将Accept缩放1/ 20。下一个引理概括地阐述了细节引理3.1考虑一个公式φ和一个赋值，它将φ中的常数期望A映射到某个区间[a，b]（其中a为 5 thenp：=（p− 0. 1）H 0 2/3（p +0. 1）H1 elsep：=（p− 0. 1）H 0 1/2（p +0.1）H1fi;c：=（c− 1）H 0 1/2<$c。算子H和H被方便地用来编码股价和概率的界限。接下来，我们将（上述）过渡系统与投资者的行为和禁止过程相结合，以描述完整的投资者/市场系统。结果是下面的公式（5），我们现在解释其细节。我们使用标签然后，我们将一个月后股票的期望值表示为{month}Sold，当对m进行解释时，将Sold与新股票价格的概率进行平均。例如，如果v是3，p是3/4，c在月初是5，那么一个月后股票的期望值是3/4 × 4+ 1/4 × 2 = 3。5;这正是在state（3， 3/ 4， 5）评估的{month}Sold的含义。函数如果他决定不投资，那么他唯一的其他选择就是等待，然后发生的事情由子公式{month}（XH {month}X）表示;请注意，这是如何通过市场控制下的H选择引入禁止的可能性的把所有的东西收集在一起，212A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）195初始股份价值0 1 2 3 4 5 6 7 8 9 10最佳预期利润0.59 0.57 0.53 0.47 0.40 0.33 0.27 0.23 0.20 0.19 0.18精确描述投资者/市场博弈的公式：（五）Game=（τ0X·利润H {month}（XH {month}X）），其中在子公式{month}（XH {month}X）中，变量X已被绑定到固定点τ0。我们选择τ0是因为我们在有限路径中将投资者的决定等同于然而，请注意，这不是一个标准的SSG，τ0也不仅仅是伪装的最小或最大固定点要看到这一点，请观察利润可以为正值和负值，这取决于股价在特定月份开始时是更有可能上涨还是因此，0既不是最大值，也不是最小值，在整个范围内的支付。为了计算公式（5）的值（以及投资者3.1）;接下来将该游戏转换为标准SSG（Thm.4.8），接下来解决这个游戏（Thm. 2.1），然后再将结果翻译回来（Lem. 3.1）。不幸的是，由于引入了双固定点（特别是如果必须使用迭代方法），这是非常不必要的。然而，在这种情况下，有一个有效的解决方案。我们注意到，在这种情况下，可以通过从0开始迭代来计算值。引理5.1在博弈（τ x X·Φ）中，如果x≤F（x），则V=lim n→∞Fn（x），其中期望-期望函数F是Φ（·）作为X所表示的值的函数的表示。证据在给定的假设下，x-小工具博弈（定义4.3）的值在支付点都在ES中的情况下很容易地简化为limn→∞Fn（x）;一般情况由Lem得出。3.1.Q利用莱姆。5.1我们创建了一个Mathematica脚本，它编码了（5）给出的博弈，并直接从0开始迭代。p的初始值设定为0。5和上限c的最大值为10;下表中列出了一些结果：结果表明，市场总有一定的概率出现上涨，但当初始股价远离上限c时，等待更长时间以获得更有利的p值是可能的。A. 麦基弗角Morgan/Electronic Notes in Theoretical Computer Science 153（2006）1952136结论和进一步的工作在本文中，我们介绍了一种新的定量两人游戏模型的情况下，没有球员赢得决定性的。我们定义了一种新的固定点，作为直接模拟这种情况的方便方法，但显示了原始qMμ实际上可以使用交错固定点对其进行建模将其编码为标准SSG的结果表明，使用为随机奇偶博弈开发的一些技术来开发计算值的算法的可能性[1];然而，我们注意到，在Def.4.3的小工具编码中隐含的交替深度的增加可能会影响它们的效率。这仍然是一个需要进一步调查的问题。引用[1] Chatterjee，K.，M. Jurdzinski和T. A. Henzinger，Quantitat