EpCTL逻辑在概率系统推理中的应用

理论计算机科学电子笔记190（2007）95-110www.elsevier.com/locate/entcs外生概率计算树逻辑Pedro Baltazar1，6Paulo Mateus2，6安全和量子信息组，电信和研究所，UividdeTecccicdeLisboa，Lisbon，PortugalRajagopal Nagarajan3，5Nikolaos Papanikolaou4，5英国考文垂华威大学计算机科学系摘要我们定义了一个逻辑EpCTL来推理概率系统的演化。系统状态对应于经典状态的概率分布，系统演化由捕获随机和非确定性转变的概率Kripke结构建模所提出的逻辑是外生概率命题逻辑（EPPL）的时间丰富。分析了EpCTL的模型检验问题，并将其逻辑与PCTL进行了比较;前者的语义是根据命题符号集上的概率分布来定义的，而后者是为了推理可能行为路径上的分布而设计的该逻辑的预期应用是作为通信协议，特别是安全协议的属性的具体形式;为了证明这一点，我们为经典的合同签署协议和所谓的量子一次性密码本指定了相关的安全属性关键词：随机过程，Kripke结构，CTL，PCTL，EPPL1引言在科学中有许多应用，其中关于概率的推理是必要的。在计算中，应用包括概率算法，1电子邮件地址：pbtz@math.ist.utl.pt2电子邮件地址：pmat@math.ist.utl.pt3电子邮件地址：biju@dcs.warwick.ac.uk4电子邮件地址：nikos@dcs.warwick.ac.uk5部分得到欧盟第六框架方案（SecoQC项目：基于量子密码学的安全通信全球网络开发）的支助6由联邦贸易委员会和欧盟联邦经济发展研究所提供部分支助，即通过CLC POCTI（研究股1-601）、QuantLog项目POCI/MAT/55796/2004和SQIG-IT最近的QSec倡议Pedro Baltazar还得到了FCT和欧盟FEDER博士研究金SFRH/BD/22698/2005的支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.07.00796P. Baltazar等人理论计算机科学电子笔记190（2007）95概率系统的计算机建模和验证，包括有和没有安全保证的通信协议。在使用许多不同的方法之前，人们已经研究了概率程序的特性，并且广泛认为，开发用于推理此类程序的形式逻辑是非常有益的，允许系统的设计者和用户对程序可能满足或可能不满足的特性进行在本文中，我们描述了一个时间概率逻辑，EpCTL。我们的方法的特点是使用一个外源的语义，这样的模型的状态公式基本上是概率分布的命题逻辑模型。我们建立在概率状态逻辑EPPL[24]的早期工作之上，通过引入时间扩展;结果是用于概率程序推理的分支时间逻辑。我们的目的是提供一个强大的框架，指定通信协议，特别是安全协议的属性。所提出的逻辑具有足够的表达能力，允许指定相关的安全属性，并使外生语义方法[25]涉及到将基本逻辑的语义结构（例如，命题逻辑），并将它们组合在一起，可能添加新的结构，以提供更高级别逻辑的语义。这种方法已被用来建立概率状态逻辑EPPL和逻辑EQPL的量子信息系统的状态推理。外生语义方法可以被认为是模态逻辑[18]的Kripke可能世界方法的变体，它与[8]中为多值逻辑引入的社会语义和[7]中为次协调逻辑提出的可能翻译语义有关。本文的结构如下。首先，我们研究的语法，语义，然后，我们描述，这些方面依次为时间的扩展，即新的逻辑EpCTL，并提供直观的各种结构。定理的证明已归入附录。2概率状态逻辑CTL[13]、LTL[29]和CTL*[11]等时态逻辑的状态逻辑是经典的命题逻辑。概率时态扩展，如PCTL[16]，也使用经典的命题逻辑的状态逻辑。在这里，我们考虑一个非常不同的状态逻辑，外生概率命题逻辑（EPPL）[23，25，9，24]，这是高度启发Halpern等人的作品。考虑到模型检验的设想应用，我们只考虑有限组命题符号Φ上的在这种情况下，EPPL模型，下面我们称概率结构为对（V，μ），其中V是一组在Φ和μ上的经典赋值7是映射μ：V→[0，1]，其中7 回想一下，Φ上的经典赋值是映射v：Φ→ { 0， 1}。v∈Vμ（v）=1。P. Baltazar等人理论计算机科学电子笔记190（2007）95978对于模型（V，μ），我们称V为可能赋值的集合，μ为概率测度。通过假设不可能的估值是不可能的，可以观察到μ可以扩展到所有估值，即对于任何v∈V \V，μ（v）=0，其中V是所有估值都超过Φ。最后，考虑概率测度是有用的，其中，μ定义为估值集，（V，2V，μ），μ（U）=μU.v∈Uμ（v）对于任何例2.1考虑俄罗斯轮盘赌游戏的一个变体，赌徒投掷一枚硬币，如果结果是正面，枪就会开火。还假设g_ambler具有1/6概率的所述hooot ingbullet。我们将系统与您的需求相结合，命题符号h（人头），b（子弹被射），d（赌徒死了）。被描述为命题符号集合的可能估值是：（所有命题符号都是假的，硬币的结果不是正面）;{h}（硬币的结果是正面，但没有子弹射出）;和{h，b，d}（硬币的结果是正面，子弹射出，赌徒死了）。概率度量是μ（h）=1/2，μ（{h}）=5/12和dμ（{h，b，d}）=1/12。我们继续描述逻辑的语法。2.1语言该语言由两个级别的公式组成。第一级的公式，即经典公式，能够对命题符号进行推理。第二层次的公式，概率状态公式，能够推理概率结构。在概率状态公式中也有概率项用来表示实数。使用BNF表示法表示的语言语法如下所示• 经方γ：= Φ（γγ）• 概率项p：=0<$1<$ y<$（γ）<$（p+p）<$（p p）• 概率状态公式：=（Qγ）经典的状态公式，由γ，γ1，. . ，是由命题符号Φ和经典的选言连接词falsum（ 假 ） 和 implication （ 隐 含 ） 构 成 的 。 像 往 常 一 样 ， 其 他 经 典 的 连 接 词（<$，，，惠）作为缩写引入。例如，（<$γ）代表（γ）。概率项，范围为p，p1，. . ，表示实数的元素。我们还假设一组变量Y={yk：k∈N}，在实数上变化。的term（γ）表示满足γ的赋值集合的测度。概率状态公式，范围由100，1001，. . ，都是由对多个单元（Qγ）的估计，对多个单元（p1≤p2）的估计，以及对多个单元的估计，[8]回想一下概率测度是一个三元组（Ω，F，μ），其中F是Ω上的σ-代数，μ是μ（Ω）=1的测度给定对Φ的无穷假设，在本文中我们将始终使Ω为V，F为V的幂集。98P. Baltazar等人理论计算机科学电子笔记190（2007）95ρρρ（V，μ）ρρ和。当γ对于语义结构中的每个可能赋值都为真时，公式（Qγ）为真。 其他概率连接词（g，n，n，n）也被引入作为一个bbreviatins。对于一个人来说，（g）是一个人，而（g）是一个人。 我们还可以使用（Qγ）作为（g（Q（γ）的缩写。请注意，Q和Q不是模态9。我们都使用一个新的数字资产，这是EPPL的一个重要组成部分有足够的表达能力来指定这些常量。例如，2≤y1可以记作（y2y2=（1 + 1）<$y2≥0）<$y2≤y1。 我们将使用减法，因为它们也可以用EPPL表示，所以可以自由划分，例如x/y = −2可以写成n as（（z+n（1 +1）=0）x=y·z。最后，这一点概率项（γ1|2）是（（γ1<$γ2））/（ γ2）。项p的出现的概念和概率状态公式中的概率状态公式可以很容易地定义。替换零次或多次出现的概率项和概率公式的概念可以类似地定义。为了清楚起见，如果不会引起歧义，我们通常会在公式和术语中去掉括号。例2.2再次考虑例2.2中描述实施例2.1. 硬币是公平的可以用（h= 1/ 2）表示我们可以也可以说，只有当硬币的结果是Q（bh）的人头时，子弹才被射出。类似地，只有当掷硬币的结果是正面，而硬币是反面时，赌徒才是死的，而这可以通过Q（dbh）来实现。最后，事实上，1/ 6的企业可以通过（b）进行融资，|h）=1/6。2.2语义给定V <$V，经典公式γ在V中的范围定义为：|γ|V={v∈V：vDc γ}，其中Dc是经典命题逻辑的满足关系.为了解释概率变量，我们需要赋值的概念。一个分配ρ是一个映射，使得对于每个y∈Y，ρ（y）∈R。给定一个概率结构（V，μ）和一个赋值ρ，概率项的表示和概率状态公式的满足可归纳定义如下。• 概率项·[[0]]（V，μ）= 0·[[1]]（V，μ）= 1·[[y]]（V，μ）=ρ（y）∫·[[（ [001 pdf 1st-31files]|γ|）的情况下进行ρ ρ ρ·[[pl+p2]]（V，μ）=[[pl]]（V，μ）+[[p2]]（V，μ）ρ ρ ρ·[[p1p2]]（V，μ）= [[p1]]（V，μ）×[[p2]]（V，μ）• 概率公式· 对任意v∈V，（V，μ）ρD（Qγ）i ∈vDcγ·（V，μ）ρD（p1≤p2）i <$V <$蕴 涵（[p1]]（V，μ）≤[[p2]]（V，μ））[9]我们没有像Q（Qγ）这样的公式。P. Baltazar等人理论计算机科学电子笔记190（2007）9599·（V，μ）ρρ·（V，μ）ρD（λ1λ2）i λ（V，μ）ρDλ2或（V，μ）ρ λ1只有当所有v∈V都满足γ时，公式（Qγ）才成立。如果用p1表示的项小于p2，则满足公式（p1≤p2）。如果语义模型不满足公式（1）或满足公式（2），则语义模型满足公式（1）。该模型 蕴涵的定义与通常一样：如果（V，μ）ρD <$，则当（V，μ）ρD<$0时，对每个<$0∈<$0.请注意，赋值ρ足以解释概率状态公式的有用子语言：κ：=（a≤a）（κκ）a：= 0 <$1 <$x<$（a + a）<$（aa）。因此，这个子语言的术语将被称为分析术语，公式将被称为分析公式。2.3Model–checking对于模型检查过程，我们假设概率结构和分配使用一个浮动点数据结构来表示。我们假设Φ命题符号的概率结构（V，μ）由实数的V-数组建模; V的大小至多为2 n，其中n =|Φ|. 我们还假设基本的算术运算需要O（1）时间。此外，我们假设我们只使用有限个变量Y，并且赋值是一个大小为实数的向量。|Y|.我们还假设一个经典公式γ或一个概率的长度的定义将公式的符号数作为写入公式所需的符号数。公式的长度（经典或概率）由下式给出：|ξ|.给定概率结构（V，μ），赋值ρ和概率公式首先，这是一个简单的方法，可以让所有的数据都集中在一个节点上。为预处理能力提供支持γ，评估需要|V|· |γ|当我们检查满足以下条件的估值集时，γ。 一旦对项进行了评估，定理2.3假设所有基本算术运算都需要单位时间，则存在一个算法O（|ξ|·|V|）来决定Φ上的概率结构和分配ρ是否满足ρ。Proof. 第一个技术特点是，必须采取措施，以评估这类产品的价值（γ）和（Qγ）。 类型（γ）的项的数目由下式限定：|ξ|. 评价其中一项我们需要O（|V|）时间对应的旅行在所有这些值满足γ，并对所有相关概率求和。 所以，来-2）所有的 （）项都是O（|ξ|. |）时间。|) time. 将得到相同的表达式检查（Qγ）的满足性。100P. Baltazar等人理论计算机科学电子笔记190（2007）95在获得这些值之后，剩余的计算（比较项、求布尔值的反以及在布尔值之间进行蕴涵）最多需要O（|ξ|）时间。因此，决定a是否为概率结构的总时间一个函数O（|ξ|. |+的|ξ|）= O（|ξ|.|. |）.|).Q显然，由于在最坏的情况下，概率分布将涵盖所有可能的估值，我们有|V| = 2n，其中n = |Φ|. 观察到在许多情况下，可能的赋值集很小，并且可以用紧凑的方法来描述这个集合。方式，以及相关的概率，我们将返回到这个讨论，当我们讨论的逻辑的时间扩展的模型检查过程。2.4EPPL的公理化这里给出的EPPL逻辑的公理化完全依赖于[9]中的公理化，并将以概括的方式给出。我们需要两个新的概念的公理化，即概率重言式和有效的分析公式的概念。考虑使用经典连接词和→从可数的命题sym-Q集合构建的命题公式。一个概率公式β称为概率重言式，如果存在Q上的一个命题重言式β，并且一个从Q到概率状态公式集的映射σ，使得σ与βpσ重合（其中βpσ是由β通过替换所有的σ的概率公式而得到的概率公式）。对于我们来说，公式（（y1≤y2））是重言式（例如，从命题重言式q→q）。如第2.2节所述，赋值足以解释所有分析公式。 我们说κ是一个有效的解析公式，如果对任意实闭域K和赋值ρ，κ对ρ为真。显然，一个有效的分析公式适用于EPPL的所有语义结构。这是一个众所周知的事实，从理论的quantier消除[17，3]，一套有效的分析公式，这样定义是可判定的代数有序域上此外，由于实数构成了代数序域的代表模型（也就是说，如果在代数序域中用EPPL项写出的不等式系统存在解，则实数也存在解），因此可判定性结果扩展到实数。我们将不深入这个结果的细节，因为我们只想专注于概率方面的推理。下面列出了EPPL的公理和推理规则• 公理· [CTaut]（Qγ）对于每个有效公式γ;· [PTaut]对于每个概率重言式，·[Lift <$]<$（（Q（γ1<$γ2））<$（Qγ1<$Qγ2））·[Eqv]（（Q））·[参考文献]（Qγ1）（Qγ2））（Q（γ1γ2）P. Baltazar等人理论计算机科学电子笔记190（2007）95101·[RCF]κ{|→y/p→|}当k是分别对概率变量和概率项的mua，→y和d→pae∫·[Meas]（（）=0）·[FAdd]<$（（<$（γ1<$γ2））= 0）<$（γ1<$γ2））=（1）+（γ2）·[Prob]（ T）= 1）·[Mon]（（Q（γ1<$γ2））（（• 推理规则1）≤（γ2）·[CMP]（Qγ1）、（Q（γ1）、（Qγ2））、（Qγ2）·[PMP]100，（101）100，（102）100公理CTaut说，如果γ是一个有效的经典公式，那么（Qγ）是一个公理。公理PTaut说概率重言式是一个公理。由于有效经典公式集和概率重言式集都是递归的，所以不需要详细说明重言式推理的细节公理Lift，Eqv和Ref是联系（局部）经典状态推理和（全局）概率重言式推理的有效公理.Thetermκ{|→y/p→|}在轴向RCF中，是由yi在κ中的所有出现被pi代替所必需的。公理RCF说，如果κ是一个有效的分析公式，那么任何用概率项代替变量得到的公式都是重言式。我们避免详细说明，因为有效的分析公式集是递归的。最大值意味着，最小值为0。axiomFAdd是测度的有限可加性Mon公理将经典连接-概率测度是测度单调性的结果。Prob公理说这个测度是一个概率测度。推理规则CMP和PMP分别是经典蕴涵和概率蕴涵的肯定前件通常我们说，一组公式Γ导出了<$，记作Γ<$<$，如果我们可以以Γ中的公式为假设，从公理和推理规则出发，建立了一个关于Γ的推导式。定理2.4EPPL是可靠的和弱完备的。此外，这组定理是递归的。证据这个结果是由这样一个事实得出的：这里给出的EPPL逻辑是文[9]中给出的EPPL逻辑的一个子语言，文[ 9 ]中给出的EPPL逻辑的相应公理化被证明是可靠的和弱完备的。 详情请看[9]。Q3计算树扩展-EpCTL在本节中，我们定义了EPPL的计算树扩展，我们称之为外生概率计算树逻辑（EpCTL）。我们的想法是考虑几个概率结构以及它们之间的转换关系，换句话说，一个节点是概率结构的Kripke结构。这102P. Baltazar等人理论计算机科学电子笔记190（2007）95由于两个原因，结构特别令人感兴趣。首先，它抓住了概率转移系统研究中出现的思想，即状态空间应该被描述为经典状态的分布[30，14，9]。 其次，这是朝着量子系统推理的一步，因为在这样的系统中，被描述为纯量子态的概率系综（cf. 混合状态，密度算子）。我们将在第4节通过两个详细的例子来探讨这两个方面。我们继续介绍EpCTL的语法。3.1语法EpCTL的语法可以很容易地从EPPL的语法中获得。 我们的想法是，在概率状态公式的水平，我们还介绍了通常的CTL方式。为了清楚起见，我们回顾一下经典公式和概率项的定义。• 经方γ：= Φ（γγ）• 概率项p：=0<$1<$ y<$（γ）<$（p+p）<$（p p）• 外生概率计算树逻辑公式·δ：=（Qγ）（p≤p）（δδ）（EXδ）（AFδ）（E[δUδ]）时间模态的直观语义类似于经典CTL。模态由两个符号组成，其中第一个符号在E或A中选择，第二个符号在X、F、G和双模态U中选择。第二个符号用于时间推理：X代表nex t;F代表未来的某个时候;G代表永远在未来;U代表直到。第一个符号量化所有计算路径：存在路径（E-表示存在）或普适路径（A-表示这两个符号的组合很容易理解。例如，公式EXδ在概率结构（V，p）中成立，如果存在满足δ的（V，p）的一个nex t结构（即，从（V，p）通过一次转移可到达的结构）。通常，所有CTL模态都是从EX、AF和EU获得的缩写。• （AXδ）对于gEX（gδ）;• （EFδ）forrg（E[（g）Uδ]）;• （AGδ）表示g（EF（gδ））;• （EGδ）对于g（AF（gδ））;• A [δ1 U δ2]对于g（E [（g δ2）U（g δ1 δ2）]）（g（EG（g δ2）。例3.1再次考虑例2.1中的俄罗斯轮盘赌变体，其中包含一些时间原语。 首先我们要声明不能为硬币的剩余价值提供支持，因为A[（ b）= 0）U（（ h）>0）]。 假设赌徒总是在玩这个游戏很明显，自杀的概率渐近趋于1，我们可以P. Baltazar等人理论计算机科学电子笔记190（2007）95103J J JJ∫使用（（x1））CRAAF（（ d）> x））。3.2语义一个概率Kripke结构是一个对（P，R），其中P是一个概率结构的集合，R<$P× P是一个全转移关系，即对任何（V，μ）∈P存在（V，μ）使得（V，μ）R（V，μ）.概率Kripke结构的概念是非常普遍的，正如我们将看到的，它能够捕获马尔可夫跃迁（以及更多）以及具有非确定性和概率跃迁的系统例3.2考虑例2.1中的俄罗斯轮盘赌，假设赌徒玩了两次游戏，然后，如果还活着，就停 止 了 。 概 率 Kripke 结 构 是 这 样 的 ， 所 有 涉 及 的 概 率 结 构 都 有 一 组 容 许 的vauationsV={k，{h}，{h，b，d}}。假设有一个不确定的距离，但μ0是μ（μ）=1. V上的概率分布相应地演化为以下随机分布：矩阵矩阵M=因此，假设赌徒的唯一选择是玩两次，如果还活着，则停止，我们有μ 0 R μ 1 and d μ 1（）= 12，μ 1（{ h }）= 5 / 12 and d μ 1（{ h，b，d }）= 1 / 12;最多，μ 1 R μ 2，其中μ 2（）= 11 / 24，μ 2（{ h }）= 55 / 14 and d μ 2（{ h，b，d }）= 23 / 144;最后是μ 2 R μ 2。概率术语的解释与前面一样。时间公式的满足定义在概率Kripke结构（P，R）、概率结构（V，μ）∈P和分配ρ上。• （P，R），（V，μ），ρD（Qγ）i ∈（V，μ），ρD（Qγ）;• （P，R），（V，μ），ρD（p1≤p2）i ∈（V，μ），ρD（p1≤p2）;• （P，R），（V，μ）， ρ/D均为零;• （P，R），（V，μ），ρD（δ1<$δ2）i ∈（P，R），（V，μ），ρ/Dδ1或（P，R），（V，μ），ρDδ2;• （P，R），（V，μ），ρD（EXδ）i ∈（P，R），（VJ，μJ），ρDδwith（V，μ）R（V，μ）;• （P，R），（V，μ），ρD（AFδ）i ∈ R，对于从（V，μ）开始的所有路径π，存在k∈N使得（P，R），πk，ρDδ;• （P，R），（V，μ），ρD（E[δ1Uδ2]），则R上存在从（V，μ）开始的路π，k∈N使得对任意i≤k，（P，R），πk，ρDδ2和（P，R），πi，ρDδ1;其中πi表示路径π的i-元素。我们称（P，R）Dδi ∈（P，R），（V，μ），ρDδ对所有（V，μ）∈P和赋值ρ.例3.3考虑例3.2的概率Kripke结构（P，R）。该结构满足死亡概率不减的性质，151⎢ 2 1212 ⎥⎢⎢ 151 ⎥⎥⎣ 2 1212 ⎦0 01104P. Baltazar等人理论计算机科学电子笔记190（2007）95P∫ ∫即，（P，R）D（（d）=x）ΔG（（d）≥x）。EpCTL与PCTL的关系EpCTL与Hansson和Jonsson提出的逻辑PCTL有关[16]。PRISM工具[19，20]是PCTL的符号模型检查器。在EpCTL和PCTL的语义之间存在根本的差异;PCTL能够推理概率转移系统中路径上的分布，而EpCTL被设计用于推理命题符号的有限集合上的概率分布如何随时间变化后一种方法特别有利于对某些类型的系统进行推理，例如分布式随机算法。根据应用程序，使用路径或命题符号上的分布来建模给定属性可能更好或更差，因为这两种方法都是有效的，但非常不同。 因此，PCTL公式AG>q表示对于调度器的任何选择，满足G的p路径的度量都大于比Q。另一方面，EpCTL公式AG（q> q）意味着对于任何调度器的选择，达到的所有状态分布是这样的，即，等待保持的概率大于Q。假设在PCTL中，概率为在模态中是内生的，似乎不太可能表达更多的复杂类型的属性，例如：AG（（1·2）> q）。有可能设计一个从概率转换系统到概率Kripke结构的映射图中使用了一个涉及盲人的结构，但我们不会在这里详细说明。研究EpCTL和其他逻辑的语义之间的联系无疑是未来工作的一个方向。3.3Model–checking我们现在解决模型检查时态公式的问题遵循CTL的常用Sat（P，R），ρ（δ）：={（V，μ）∈P：（P，R），（V，μ），ρDδ}对于概率Kripke结构（P，R），赋值ρ和公式δ.这就是所谓的全局 在介绍模型检查方法之前在概率Kripke结构（，R）的上下文中，引入一些关系的符号是有用的我们用R−1表示R的逆关系，即（V，μ）R−1（VJ，μJ）i <$（VJ，μJ）R（V，μ）。给定一个概率结构集X <$P，我们用RX表示集合{（V，μ）∈ P：存在（VJ，μJ）∈ X使得（VJ，μJ）R（V，μ）}。 我们现在能够提出一个改编自CTL的常用算法：（一） Sat（P，R），ρ（Qγ）={（V，μ）∈P：（V，μ），ρD（Qγ）};（二） Sat（P，R），ρ（p1≤p2）={（V，μ）∈P：（V，μ），ρD（p1≤p2）};(iii) Sat（P，R），ρ（δ1<$δ2）=（P\Sat（P，R），ρ（δ1）<$Sat（P，R），ρ（δ2）;(iv) Sat（P，R），ρ（EXδ）=R−1Sat（P，R），ρ（δ）;P. Baltazar等人理论计算机科学电子笔记190（2007）9510512(v) Sat（P，R），ρ（AFδ）=固定点[λX.F（AFδ）（X），Sat（P，R），ρ（δ）]，F（AFδ）（X）=X<${（V，μ）∈P：R{（V，μ）}<$X};(vi) Sat（P，R），ρ（E[δ1Uδ2]）=固定点[λX.FE[δ1Uδ2]（X），Sat（P，R），ρ（δ2）]，FE[δUδ]（X）= X<$（Sat（P，R），ρ（δ1）<$R−1X）.一般来说，概率Kripke结构需要指数空间（在命题符号的数量上），因为概率在赋值分布上的指数跨度由于这个原因，模型检查算法在命题符号的数量上花费指数时间，但它在概率Kripke结构的大小和公式的复杂性上是多项式的定理3.4假设所有基本算术运算都需要单位时间，则对于EpC T L的模校验算法需要O（|δ|2·|P|2·2n）time，其中δ用n个命题符号表示.证据算法的时间复杂度为O（|δ|· |P|2）（见[10]详细分析。因此，如果我们把每个（Qγ）和p1≤p2看作是一个命题符号，那么算法的时间复杂度将是O（|δ|· |P|2）的情况。最后，如果满足mua（P ，μ）和ρtakesO（|δ|·2n）（c.f. 定理2.3）我们得到所需的上界。回想一下，算法的时间复杂度为O（1）。Q众所周知，如果将EG作为基本模态而不是AF，则可以获得稍微更好的算法，但我们在这里不这样做。虽然该算法在最坏的情况下是指数的，但它假设估值上的概率显然，对于特定的相关情况，有更有效和紧凑的编码;我们目前正在研究哪些概率分布可以有效地编码。4说明性实例为了证明EpCTL的表达能力，我们考虑了文献中的几个示例，从Ben-Or等人的合同签署协议模型开始。[6]。然后，我们考虑量子密码学领域的一个简单协议示例，量子一次性密码本[ 1 ]，注意到这个特定协议可以完全在概率设置中建模，并且其属性在经典概率（而不是特定的量子）形式主义中表现出来4.1一种合同签署协议合同签署的问题是找到一种方法，让两个用户A和B以这样一种方式承诺合同C，即任何一方都不会错误地说服另一方前者已经签署。换句话说，A和B必须签署106P. Baltazar等人理论计算机科学电子笔记190（2007）95合同在一起，没有一方获得任何优势。这个问题的传统解决方案是A和B同时签署C，但这只有在A和B物理上接近时才有可能。假设A和B虽然在通信协议的不同阶段，一方当事人可能相对于另一方当事人具有相对优势，但是，由于在空间上是分开的，因此，签署合同的唯一途径是通过通信协议。 “公平”合同签署协议的目标BGMR协议假设设置一个用户网络（我们只关注两个用户的情况），并使用一个签名方案假设只有用户U能够可核查性）。该协议假设用户A和用户B都不想被承诺到合同C，除非另一个用户愿意，并且使得A和B可以通过交换承诺来签署合同C。协议的公平性概念被定义为这样的属性，即“B不存在”的条件概率特权”，因为“A是特权”总是很小。在形式上，BGMR协议被称为（v，v）定义4.1合同签署协议对A是（v，n）如果A和B被认为是不诚实的，那么在协议期间必须调用第三方在协议期间，A和B交换以下格式的签名消息m=（C，p，U）=签名，用户U。当消息m被接收时，接收者被称为具有概率p的特权，这意味着调用法官将导致他裁决该合同 C以概率p与A和B结合。如果协议在预先约定的日期D之前没有成功终止我们现在准备详细说明BGMR协议。步骤1(i) A和B双方同意谁先走，并设定终止日期D。我们假设A是第一个。(ii) A方选择“B有特权”而“A没有特权”的条件概率v(iii) 甲方选择参数α >1，条件概率P. Baltazar等人理论计算机科学电子笔记190（2007）95107αβ假设(iv) B方选择β > 1，使得在给定“A是特权的”的情况下“B是特权的”的条件概率至少为1。(v) 协议初始化为λA=λB= 0。符号λA存储了最后从A发送的消息中提到的概率，类似地，λB存储了最后从B发送的消息中提到的概率。(vi) A和B交替执行以下程序：A步 用户A表示由p接收的最后消息中提到的概率。然后检查pλA。如果是，则A设置λA：=max（v，min（1，p·α））。否则，A假定协议已终止。然后A将消息（C，λA，A）发送给B。B步 用户B表示由p接收的最后消息中提到的概率。然后检查pλB是否。如果是，则B设置λB：= min（1，p·β）。否则，B假设协议已经终止。然后B向B发送消息（C，λB，B）。法官的程序和提前停止程序的细节Norman和Shmatikov [27]使用PRISM模型检查器对方案进行了分析。BGMR协议的要点是它确保了特定程度的公平性，其特征在于常数v和ε。在协议结束时，双方都需要特权。在下文中，我们使用EpCTL来形式化（v，v）-公平性的概念我们建立命题常数集合Φ ={A，B}，其中A对应于事件“A是特权的”的真值，同样地，如果“B是特权的”，为了表达公平性，我们将协议参数λ视为一个实变量，即第2节中定义的集合Y的成员。A方在上述步骤（ii）中确定的概率v可以在EpCTL中表示为以下项：. ∫Σv =0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000（A）|在协议的步骤（iii）和（iv）中，A方和B方固定参数α和β，使得以下EpCTL性质为真：（一）（二）.1A.A.|CIBB α. ∫Σ1CIBB|A.A. β（v，v）.. . ∫AGΣΣCIBB> v108P. Baltazar等人理论计算机科学电子笔记190（2007）95. . ∫⊃ΣΣΣ（A）|B≤也就是说，在协议的所有路径中，假定“B是特权的”的概率大于v，则“A不是特权的”的概率在请注意，我们自由地使用了比较器>，这些可以用EpCTL的形式语法中的≤运算符来表示。P. Baltazar等人理论计算机科学电子笔记190（2007）95109211nn4.2Quantum一次性便笺簿量子比特是量子计算中的基本存储单元（就像比特是经典计算中的基本存储单元一样）。量子比特的状态是一对（α，β）复数，使得|α|2个以上|β|2 = 1。量子一次性密码本[1]使用两个密钥（经典）比特以安全的方式加密量子比特：观察加密的量子比特会产生两个结果，两者的概率相等在特殊情况下，α和β是实数的一位密钥表。如果K= 1，则量子比特被加密为对（β，−α），否则它保持不变。我们认为实数α是用浮点表示来编码的，即一个命题向量symbolsα. 我们用α来表示。我们用α=β表示，1N经典公式（α惠β）（a）在任何情况下，下面的程序模拟了这个过程，首先生成一个随机密钥，然后加密量子位（α，β）：(i) 设K=公平伯努利试验的结果;(ii) 如果（K= 1），则(a) γ：=α(b) α：=β(c) β：=−γ假设α和β的初始值分别为c和d（其中c为d）。根据量子信息理论，为了证明安全性，在量子一次性密码本中，它表明加密后α为c的概率为1（因此α为d的概率也为1）。 我们可以用我们的逻辑2 2和模型检查程序，以显示上述考虑的概率Kripke结构诱导的加密程序。假设程序在克里普克结构中引发了一次跃迁，从那一点开始，状态上的概率分布保持不变。因此，量子一次性密码本的安全性等同于检查所有初始状态是否完整。（Q（α=c<$β=d<$（<$（c=d）∫X2（ （α = c））= 1）。5总结和结论在本文中，我们已经介绍了一个概率分支时间逻辑，EpCTL，它可以被视为一个时间扩展的外源概率状态逻辑EPPL。我们已经说明了EPPL的语法和语义，考虑了在这种状态逻辑中公式的模型讨论了EpCTL的可表示性，并给出了一个公理化.我们演示了使用EpCTL作为表达两种安全协议的属性的手段：经典的概率合同签署协议和量子我们的方法受到Halpern早期工作的启发，我们希望概率时态逻辑EpCTL可以作为相关的有用的替代方案。110P. Baltazar等人理论计算机科学电子笔记190（2007）95经典逻辑，如PCTL。未来的工作将包括完善EpCTL的公理化，考虑对模型检查算法的可能改进有必要进一步开展案例研究，特别是为了对担保中通常出现的各类财产进行分类和核实。我们希望这项工作将作为正在进行的工作的基础，在开发一个exogenous，时间量子逻辑模型检查一般量子协议在[23]中提出了一种量子状态逻辑，即外生量子命题逻辑（EQPL）;我们打算提供该逻辑的时间扩展，扩展本文中描述的因此，我们有必要构建一个专用引用[1] Ambainis，A.，M. Mosca，A.Tapp和R.de Wolf，Private Quantum Channels，in：FOCS547号[2] 拜尔角和M.Z. Kwiatkowska，具有公平性的概率分支时间逻辑的模型检查，分布式计算11（1998），pp.125-155网址citeseer.ist.psu.edu/article/kwiatkowska96model.html[3] 巴苏，S.，R. Pollack和R. M.- F. Coise，[4] Beauquier，D.，A. M. Rabinovich和A.Slissenko，一种具有可判定模型检查的概率逻辑，CSL306-321[5] Ben-Ari，M.，Z. Manna和A. Pnueli，分支时间的时序逻辑，在：POPL164-176.[6] Ben-Or ， M. ， O. Goldreich ， S. Micali 和 R. L. Rivest ， A fair protocol for signing contracts ， IEEETransactions on Information Theory36（1990），pp. 40比46[7] Carnielli，W.一、次协调逻辑的可能翻译语义，见：次协调逻辑的前沿（根特，1997），逻辑与计算研究8（2000），第149 - 163页。[8] Carnielli，W. A.和M. Lima-Marques，Society Semantics and33比52[9] 查 达 河 ， P. Mateus 和 A. 概 率 序 列 程 序 状 态 的 推 理 ， [J]. E′sik ， editor ， ComputerScienceLogic2006（CSL06），LectureotesinComputerScience4207， Springer-Verlag，2006 pp.240-255[10] Clarke，E. M.和E. A.陈文生，应用分支时间时序逻辑设计与合成同步框架，载于：程序逻辑研讨会论文集，LNCS131，Springer-Verlag，1981年。[11] Clarke，E.M. 和E.A. 陈文辉，应用分支时间时序逻辑设计与合成同步框架，载于：程序逻辑，工作坊（1982），页.52比71[12] Clarke ， E.M. ， E. A. Emerson 和 A.P. Sistla ， 使 用 时 序 逻 辑 规 范 自 动 验 证 有 限 状 态 并 发 ， ACMTrans.Program。8（1986），pp. 244-263。[13] Clarke，E. M. and J. M. Wing，形式化方法：最新技术和未来方向，ACM Comput。监视器28（1996），pp. 626-643[14] den Hartog，J.和E. de Vink，使用类似于hoare逻辑的概率程序，计算机科学基础国际期刊13（2002），第13页。315-340.P. Baltazar等人理论计算机科学电子笔记190（2007）95111[15] 费 金 河 ， J. Y. Halpern 和 N. Megiddo ， A logic for reasoning about probabilities ， Information andComputation87（1990），pp. 78比128URLciteseer.ist.psu.edu/fagin90logic.html[16] Hansson ， H. 和 B. Jonsson ， A logic for reasoning about time and reliability ， Formal Aspects ofComputing6（1994），pp. 51