概率命题动态逻辑的表达能力与经典的Hennessy-Milner定理类似

可在www.sciencedirect.com在线获取理论计算机科学电子笔记352（2020）283-304www.elsevier.com/locate/entcsProbablyPDL的Hennessy-Milner结果陶谷亚历山德拉·席尔瓦·法比奥·扎纳西英国伦敦大学学院计算机科学系摘要Kozen在1985年引入了概率命题动态逻辑（Probabilistic Propositional Dynamic Logic，PPDL）作为一个组合框架来推理概率程序。 在本文中，我们研究了PPDL的表达能力，并提供了一系列的结果类似于经典的Hennessy-Milner定理模态逻辑。首先，我们表明，PPDLcharacterises概率自动机（输出）的概率迹等价。其次，我们表明，PPDL可以温和地扩展到产生的概率状态互模拟PPDL模型的特征。第三，我们提供了一个不同的扩展PPDL，这一次表征概率事件互模拟。关键词：概率命题动态逻辑，概率互模拟，Hennessy-Milner性质1介绍概率编程是命令式编程的扩展，可以指定和实现随机网络和安全协议，机器学习和量子算法。各种各样的应用程序最近导致了迅速增长的兴趣在概率的角度来看。关于这些程序正确性的推理，以及更一般地验证诸如收敛和终止之类的属性，是相当复杂的。因此，重要的是要建立正式的技术，使这些形式的推理。概率程序的形式语义的起源可以追溯到20世纪80年代初。 Kozen的开创性工作[13，14]描述了如何使用马尔可夫核给简单的命令式概率程序精确的指称语义。概率程序允许对硬币IP上的条件和迭代参数进行编码：例如，“以概率0执行程序P。3，q的概率为0。7”。因此，它们的语义不仅仅是从输入到输出的关系，而是从初始状态到可能的最终状态的（子）分布的映射关于这类程序正确性的推理不同于https://doi.org/10.1016/j.entcs.2020.09.0141571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。284T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283经典的设置是从一个布尔值开始-一个属性是真还是假- 从定量的角度来看-是一个具有高概率为真的属性概率命题动态逻辑（ProbabilityPropositional Dynamic Logic，PPDL）[14]建立了一个表达和验证概率程序属性的框架，从传统的真值函数解释转向定量解释。概率程序的许多属性，如终止性，可以在PPDL中编码和验证。PPDL中的方块和菱形模态可以被认为是Dijkstra最弱前提的概率模拟McIver和Morgan[15]，以及最近Katoen和Kaminski[12，16]，已经开发了Dijkstra演算的定量除了在验证中的应用外，PPDL还发现了其他领域，例如。它已被用于推理多智能体系统中的不确定性和知识[8]。另一方面，Hennessy和Milner首先注意到标记转移系统（LTS）的互模拟与简单模态逻辑之间的关系，随后被称为Hennessy-Milner逻辑（HML）[10]。特别是，他们证明了HML在像有限LTS类中描述了双相似性（最大的互模拟）：像有限LTS中的两个状态是双相似的，当且仅当它们满足完全相同的HML公式。这种互模拟特性的存在对性质的验证有实际意义：如果一个系统的两个状态属于同一个HM类，那么可以通过查看HML公式来检查它们的互模拟等价性。此外，也许更有趣的是，如果两个状态不是双相似的，那么人们可以找到一个HML公式来证明双相似性的失败（并作为反例）。对于像HML这样的简单逻辑，这是一个相当大的优势。自从Hennessy和Milner的开创性论文以来，类似的特征已经被研究用于其他逻辑和系统。特别是，人们对定量环境的兴趣越来越大。例如，在[3，2]中引入了一种称为L0的HTML风格的简单逻辑，用于描述标记马尔可夫过程（LMP）的状态和事件双相似性。后来，Desharnais等人。[4]提出了一种实值逻辑，该逻辑给出了LMP的相同表征结果。Doberkat[6]研究了随机Kripke模型，并引入了（布尔值）随机PDL来验证此类模型的行为等价性在这项工作中，我们继续这条线的研究，通过研究Hennessy-Milner性质的PPDL。本文的主要贡献（及其技术路线图）如下：(i) 首先，我们证明了PPDL函数（或者更准确地说，具有良好结构程序的PPDL）是PPDL模型的概率迹等价这些都是概率类似的克里普克模型-概率自动机与连续状态空间和多个输出函数（第3节）。不出所料，这里的挑战是证明迹等价意味着PPDL等价。(ii) 在第4节中，我们展示了PPDL的一个小的扩展，其中我们称之为PPDL+，描述了PPDL模型的概率状态双相似性（具有解析T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283285i∈Ii∈I状态空间）。PPDL+使用形式为（−）> r的额外函数构造器（对于布尔函数）扩展了PPDL，其中r是任意非负有理数。(iii) 在第5节中，我们证明了PPDL的一个不同的扩展，我们称之为PPDL，描述了PPDL模型的概率事件双相似性。注意，与状态偏置不同，这个结果不要求状态空间是解析的。2预赛在这一节中，我们固定了一些基本的符号，并回顾了马尔可夫核、PPDL和标记马尔可夫过程的必要背景。2.1可测空间、马尔可夫核和范畴。一个可测空间是一个集合X，在X上有一个σ-代数<$X：<$X<$P（X）是X的子集的集合，使得它包含X，在补下闭，在可数交下闭。当没有混淆出现时，我们常常简单地用它的基本集合来表示可测空间。给定两个可测空间（X，<$X）和（Y，<$Y），我们回想以下概念：• 一个函数f：X→Y是可测的，如果f−1（B）∈<$X，只要B∈<$Y。• 一个函数μ：<$X→ [0，+∞]是一个测度，如果它满足可数可加性性质：对于任何可数族{Ai|i∈I}是X的两两不相交子集，μ。Ai=μ（Ai）特别地，（子）概率度量是使得μ（X）= 1（或μ（X）≤ 1）的概率度量。①的人。• 一个函数h：X×λY→ [0，1]是一个（次）马尔可夫核，如果：(i) h（·，B）：X→[0， 1]是一个可测函数，对任意B∈<$Y.(ii) h（x，·）：<$Y→[0， 1]是对任意x∈X的（次）概率测度。最后，我们回顾一下解析空间的定义--更多细节见例[7]。度量空间M是完备的，如果M中的每个柯西点列在M中有极限;度量空间M是可分的，如果M包含可数稠密子集。波兰空间是完备可分度量空间下的拓扑空间假设（X，<$X）是波兰语。 X的一个子集C在X中解析，如果它是连续象波兰的空间。一个可测空间（Y，<$Y）是解析的，如果它可测同构于波兰空间（X，<$X）中的某个解析集C2.2概率命题动态逻辑现在我们回顾一下[14]中PPDL的基本语法和语义。PPDL签名是一对有限集合（P，F），其中P和F分别是原始集合286T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283程序和原始函数。PPDL的程序、函数和公式定义为：布尔值B：：= 1 |F ∈ F |B|BB|BB程序p，q：：= P∈ P |p; q|B？| p函数f，g：：=1|F∈ F| AF+ BG |B· f|公式φ：：= f≤g|⟨p⟩f formulasφ ::= f ≤ g其中a，b∈ Q ≥0是非负有理数。在上下文清楚的情况下，我们通常会省略运算符“·”和“;”，这样Bf和pq就分别代表B·f和p;q。注意，原函数F∈F也表现为布尔函数。这是因为，正如我们将在下面看到的，原始函数被解释为状态空间上的{0， 1}注2.1在最初介绍PPDL的文章[14]中，允许函数的任意线性组合.在我们的介绍中，为了简单起见注意，消除这样的限制并不影响我们所证明的结果注2.2正如我们将看到的，PPDL公式实际上在下一节的结果中并不起作用，而是围绕PPDL函数。我们在介绍中仍然包括公式，原因有二。首先，坚持PPDL的原始定义，如[14]。第二，为了将公式与我们将在第4节中介绍的函数constructor（−）> r进行对比，请参见下面的注释4.1。为了强调PPDL程序如何捕获标准编程结构，我们还将使用以下缩写：ifBthenpelseq：=（B？; p）+（<$B？;q）whileBdop：=（B？; p）;（<$B）？在本文中，我们将关注结构良好的程序片段，其中线性组合和迭代的使用受到限制：程序p，q：：= P|p; q|B？|而B做p|while B do p这样的限制，已经出现在[14]中，有一个自然的正义。直观地说，程序p的Kleene星p描述了p执行的有限次迭代，对于所有输入，它可能并不总是收敛到一个有限值。的限制 对于结构良好的程序，强制执行p的语义（以及上面给出的所有程序）在任何地方都被定义，并返回[0，1]中的实值（完整的证明参见例如[17]）。每当我们想要强调这种限制时，我们将PPDL的片段称为结构良好的PPDL。用于签名L=（P， F）的PPDL模型是元组X=（X，VX，VP，VF），其中：• （X，<$X）是一个可测空间（称为状态空间），X称为状态集。T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283287（Ⅲ）（P）（Ⅲ）（Ⅲ）<$BB）01（Ⅲ）（Ⅲ）X（Ⅲ）（Ⅲ）.（2）（3）≤ ）（2）XXXi∈N• VP给每个P∈P分配一个次马尔可夫核X×<$X→[0， 1]。• VF赋予每个F∈F一个可测函数X→ {0， 1}。结构良好的程序和函数的语义·X归纳定义如下：• （结构良好的）程序被解释为子马尔可夫核X×<$X→[0， 1]：X=VP（P）X x X<$ifBthenp else q） =<$B？; （p）+<$（<$B）？; q）的p; qX= λ（x，A）.y∈X<$p）（x，dy）·<$q）（y，A）（B？; p）i;（<$B）？）XXB？）= λ（x，A）. B（x）·χA（x）其中（B？p）0=1？，（B？; p）i+1=（B？; p）i;（B？;p），χA是集合A的特征函数。• 布尔函数被解释为{0， 1}值可测量函数：（F）XVF（F）XX= λx。B0XXX(x) B1）XX（十）<$B） = λx. 1 −<$B）（x）<$B0<$B1） = λx。<$B0）（x）<$<$B1）（十）• 函数被解释为可测函数X→[0，+∞）：（1）=λx。1（常数函数为1）F XVF（F）X xX<$af+bg） =λx.a·<$f）（x） +b·<$g）（x）BfXX= λx。BX(x) ·f）X（十）<$p<$f）X=λx。∫y∈X <$f）（y）·<$p）（x，dy）• 公式被解释为{0， 1}值可测量函数：x（x）=1，如果X（x）≤X（x）0否则一个点PPDL模型是一个模型X和一个状态x∈X。我们说两个点模型（X，x）和（Y，y）关于PPDL函数是等价的（记为（X，x）<$PPDL（Y，y）），如果fX（x）=fY（y），对所有函数f。我们还会遇到其他逻辑，它们的语法没有函数，只有公式：对于这样的逻辑L，稍微滥用一下符号，我们将使用L来表示二元关系，即两个（指向的）L-模型关于所有L-公式是等价的XX288T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）2830一0（T）（Ⅲ）2.3标记马尔可夫过程和概率互模拟。给定有限个作用集A，一个标号马尔可夫过程（LMP）是一个A-标号元组（X，<$X ， τa ） a∈A ， 其 中 （ X ， <$X ） 是 一 个 可 测 空 间 ， 对 于 每 个 a∈ A ， τa ：X×<$X→[0， 1]是一个次马尔可夫核。我们将研究两种不同的LMP互模拟概念设（X，<$X，τa）a∈A是LMP.首先，我们引入状态互模拟[18]。对于关系R <$X×X和子集A<$X，我们说A是R-闭的，如果对任意xRxJ，有x∈A当且仅当xJ∈A。关系R <$X×X是一个（LMP）状态互模拟，如果对任意xRxJ，a∈ A，且R-闭A∈<$X，τa（x，A）= τa（xJ，A）.我们说两个指向的LMP（X，x）和（X，XJ）是状态双相似的，表示为（X，x）s（X，xJ），如果存在状态互模拟R <$X × X，使得xRxJ。LMP上还有另一个互模拟的概念，称为事件互模拟[2]。子σ-代数ΛX是事件互模拟，如果（X，Λ，τa）a∈A也是LMP.这样的Λ生成一个二元关系R（Λ），使得（x，xJ）∈R（Λ），如果x∈A恰好当xJ∈A时，对所有A∈Λ。虽然有点滥用术语，但我们也可以将这个R（Λ）称为事件互模拟，当Λ是。我们说两个点LMP（X，x）和（X，XJ）是事件双相似的，记为（X，x）Ae（X，XJ），如果存在事件互模拟Λ使得（x，XJ）∈R（Λ）。值得注意的是，状态和事件互模拟在离散设置和解析状态空间中是一致的。然而，一般来说，这两个概念是正交的[2，20]。从范畴的角度来看，LMP状态互模拟是具有解析状态空间的LMP范畴（被视为余代数）中的跨度。注意，只有当LMP是解析的时，跨度才能被正确定义（作为弱回调）[3，18]。 另一方面，LMP事件互模拟是满射的余跨度在LMP的范畴中，它是可以定义的，而不需要任何分析性限制[2]。2.4LMP的双相似性的逻辑表征对于我们后面的发展，重要的是要回顾两个Hennessy-Milner结果在LMP的背景简单逻辑L0[3]归纳定义如下：φ：：= T|φ∧φ|汽车旅馆（1）其中a∈ A是作用，r是[0，1）中的有理数。 L0的模型是LMP（X，<$X，τa）a∈A. 令（X） 表示X中L0的解释，或简称为<$·）如果上下文清楚。则L0：=X， φφ）：=<$φ）<$<$<$<$），和<$a<$φ）：={x∈¢rX|τa（x，φ）> r}。有两个重要的结果（我们将在第4节和第5节中使用）：（1）如果我们考虑状态空间是解析的LMP，则L0刻画LMP状态双相似性[18]。(2)如果我们一般考虑LMP，T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283289则L0表征LMP事件双相似性[2]。290T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283000命题2.3（[18]）对于可数作用集A，设X=（X，<$X，τa）a∈A是具有解析状态空间的LMP，并且x，y是X中的两个状态。 则（X，x）As（X，y）当且仅当（X，x）<$L0（X，y）。命题2.4（[2]）设X=（X，<$X，τa）a∈A是LMP，且x，y是X中的两个状态。 则（X，x）Ae（X，y）当且仅当（X，x）<$L（X，y）。3PPDL描述迹线等价性在本节中，我们提供PPDL（函数）的Hennessy-Milner性质。首先，我们引入PPDL模型之间的迹等价的概念，这是概率自动机（PA）的迹等价的一般化。然后证明了PPDL具有迹等价的性质.注意迹等价是一个相对弱的概念，所以非平凡的方向是迹等价隐含PPDL等价（Prop.3.6）。第一个要解决的问题是如何定义跟踪等价的概念，PPDL以原则性的方式建模为了这个目的，我们使用的观察，PPDL模型可以被看作是一个具有多个输出函数的（连续）概率自动机（PA）。PA的标准迹语义是其迹分布的集合，每个迹分布都是一个概率分布，为某组迹分配一个概率值[19]。 两个指向的PA是迹线等效的，如果两个状态具有完全相同的迹线分布。受此启发，我们定义了点PPDL模型之间的迹分布和迹等价。由于我们现在在连续情况下工作，迹语义由概率测度集组成（而在离散情况下，我们用概率分布集进行推理为了给出我们的定义，我们固定一个有限签名（P， F）。我们将字母表定义为： B？ 其中B是F∈F的所有布尔组合的集合，并且B？={B？| B ∈ B}; we use Σ∗to denote the set of all finite words over Σ; in particular, ϵ is the empty word.注3.1注意，由于F是有限的，所以在B模逻辑等价中只有有限多个元素。稍微滥用符号，从今以后我们用B？一个字母的集合，包含一个固定的B？从B中的每一个n-等价类。等价类代表的选择并不影响我们的结果。因此，字母表是有限的。定义3.2（迹）PPDL模型X=（X，X，VP，VF）确定，对于每个词ω∈，子马尔可夫核τω：X×X→[0， 1]，归纳如下。为T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283291B？BX（x）= 0或x/∈A任意x∈X和A∈<$X：τ（x，A）：=χA（x）τP（x，A）：=VP（P）（x，A）其中P∈Pτ（x，A）：=.1<$B）X（x）= 1且x∈A0否则，即τω·a（x，A）：=y∈Xτω（x，dy）·τa（y，A），其中ω∈λ，且da∈λ则状态x处的迹是函数ρx：ρπ×F→ R，使得给定ω∈ρπ，F∈F，ρx（ω，F）：=x∈Xτω（x，dy）·VF（F）（y）给定两个点PPDL模型（X，x）和（Y，y），如果ρXn=ρYy，即ρXn和ρYy在所有输入（ω，F）∈φ×F上重合，则称它们是迹等价的（记为（X，x）φtr（Y，y））对于表征结果，我们的第一个观察结果是PPDL等价需要迹等价。命题3.3（X，x）<$PPDL（Y，y）蕴涵（X，x）<$tr（Y，y）。证据根据定义3.2，我们有（X，x）<$tr（Y，y）当且仅当ρx（ω，F）=ρy（ω，F）对任意原函数F∈F和有限字ω∈F成立。注意，每个值ρx（ω，F）都是PPDL公式<$ω<$F在状态x的精确解释，因此（X，x）<$PPDL（Y，y）意味着ρx（ω，F）=ρy（ω，F），对所有ω和F。Q注3.4注意命题3.3的证明也暗示了一个它的函数形式为<$ω<$F，其中ω∈<$<$F，F∈F. 这个逻辑是“极简”的在这个意义上，它可以表示为任何实值逻辑特征跟踪等价。对于相反的方向，即迹等价蕴涵PPDL等价，我们需要下面的因式分解引理。引理3.5（因式分解）每个PPDL函数f等价于某个PPDL函数g（在这个意义上，fX=gX，对于以下形式所有模型X）<$G）：：= 1<$|F）的|B|汽车旅馆（2）g：：= G|AG + BG|B·g其中p是一个程序，a，b ∈ [0，+∞）. 换句话说，人们总是可以将PPDL函数中程序的外观推到“最内层”。证据 通过对PPDL函数复杂性的归纳证明。 我们证明了唯一的非平凡情况，即对于某些f j，f=p<$fJ。 首先，让我们为∫292T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283（2）JJΣ∗ΣΣ（2）（2）PPDL函数之间的语义等价性，即fg，如果fX= gX，对于所有模型X。然后，我们证明的情况下，结构的 FJ。 如果fJ= 1或fJ= F对于一个基元F，则f=<$p<$fJ 已经 是 正确的 形 状 。 若 FJ= af0+ bf1 ， 则 有 f=f_p_f （ af0+bf1 ）a_p_f_f_0+b_p_f_f_1，并可应用关于f0和f1的归纳定理.如果fJ= B·fJJ，注意f =pB？如果你是JJp; B？再一次，我们可以通过对fjj的归纳假设得出结论。最后，如果f J=<$pJ<$f JJ，我们有f =<$p<$pJ<$f JJ<$p; pJ<$f JJ，我们可以通过对f的归纳假设得出结论 。Q现在我们可以证明迹等价蕴涵PPDL等价。命题3.6（X，x）<$tr（Y，y）蕴涵（X，x）<$PPDL（Y，y）。证据 设（X，x）<$tr（Y，y）. 证明了（X，x）和（Y，y）一致 在引理3.5中的所有函数g上。我们用归纳法对g的结构进行推理。我们首先考虑g是某个G的情况，定义如（2）。这有4个子案例：• G=1：平凡。• G是一个本原函数F：由于（X，x）<$tr（Y，y），它们在空字上一致。具体地说，ρx（λ，F）=ρy（λ，F）。• G是一些原函数的布尔组合B这种情况是由B的值完全由它的分量原函数决定的事实得出的。• G=<$p<$F，其中F ∈ F。 我们首先证明，每个程序p都可以写成一个（可数的）字的和。则对任意ω ∈ π π，πpπFX（x）= πpπFY（y）约化为πωπFX（x）= πωπFY（y），这正是迹等价的定义。我们对程序的结构进行归纳推理· 对于p=P和p=B的情况？是微不足道的，因为它们已经在字母表中了。· 至于p=ifBthenp0elsep1和p=whileBdoq的情况，我们只需简单地列出定义。· p= p0; p1。通过归纳假设，p0和p1都可以表示为n中的词和，设p0=i∈Iωi，p1=j∈Jπj，则p0; p1=i ∈ I，j ∈ J ωi; πj.接下来我们考虑g的其余两种情况，即g=ag0+bg1和g=B·gJ。两者都可以通过直接应用归纳假说来证明Q命题3.6和3.3一起产生所需的Hennessy-Milner性质，PPDL：定理3.7（PPDL刻画迹等价）对于任意点PPDL模型（X，x）和（X，y），（X，x）<$PPDL（X，y）当且仅当（X，x）<$tr（X，y）。例3.8设签名为P ={a，b}，F ={F1，F2}. 考虑T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）2832932下面两个点PPDL模型（X，x0）和（Y，y0）：x0的a，1C1b，1C2b，1y2s，y0a，1C1ZY3此外，定义F1（x2）=F1（y2）=F1（y3）= 1，F2（x2）=F2（y2）= 1，对于所有其他未提及的情况，F1和F2的值为0。则（X，x0）和（Y，y0）不是迹等价的。定理3.7 告 诉 我 们 ， 存 在 一 个 PPDL 函 数f ， 它 在 x0 和 y0 上 有 不 同 的 值 . 例 如 ， 设f=<$a<$$>b<$$>（F1<$F2），则X1 1 1Y1 1 1 1<$f）（x0）=2×3×1=6<$f）（y0）=2×2×1 +2×2×0=44扩展的PPDL刻画了状态的双相似性定理3.7用PPDL刻画了迹等价。这是一个自然的问题，问什么额外的逻辑结构是需要的，以保证状态双相似性和事件双相似性的PPDL模型。在本节中，我们将重点放在状态互模拟上（事件互模拟留到下一节）。为此，我们引入了PPDL的一个适当的扩展，称为PPDL+，并表明，它的特点是在PPDL模型与解析状态空间的状态双相似性4.1PPDL+我们首先介绍作为PPDL扩展的逻辑PPDL+。我们的想法是，由于L0的特点LMP状态的双相似性（命题2.3），我们扩展PPDL，使它可以解释L0公式的功能。在下面的语法中，我们指出哪些子句与PPDL中的子句相同，以强调两种逻辑之间的差异。PPDL+定义为PPDL+B ooleansB：：=1|F∈F|B|BB|BB|f>rPPDL+程序p，q：：=P∈P|p;q|B？|ap+bq|pPPDL+函数f，g：：=B|AF+BG|B·f|PPDL+，对于mφ：：=f≤g其中a，b∈ [0，+∞），r是[0，+∞）中的任意有理数。与PPDL的情况一样，我们可以将PPDL +限制为具有良好结构的程序。所得到的逻辑PPDL+具有与PPDL相同的程序集，但具有形式为（−）> r的额外函数构造器（用于布尔函数）。注4.1注意，这个新的函数构造函数显然类似于PPDL公式的构造函数的形状，但它具有不同的性质：对于每个有理数r∈Q≥0，（−）> r是固定的，它产生一个函数，而PPDL语法中的（−）≤（−）作用于两个变量参数，它产生一个公式。b，1423XX2y294T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283一一本文给出了一个{0，1}值函数，满足<$f>r）X（x）=1if<$f）X（x）>r，逻辑PPDL+也在PPDL模块中解释。（boolean）函数f>r否则为0（即，如果4.2状态互模拟f）X（x）≤r）。我们现在开发状态双相似性的表征结果。为了提醒本小节，我们将自己限制在那些状态空间是解析的LMP（和PPDL模型）PPDL模型的状态互模拟的概念被定义为通过考虑额外的权重结构，在底层LMP上扩展相同的概念。定义4.2（PPDL模型的状态互模拟）设X是PPDL模型。X上的状态互模拟是等价关系R<$X×X，使得如果xRxJ，则(i)VP（P）（x，A）=VP（P）（xJ，A），对任意P∈P和R-闭A∈X（R-闭包的定义见第2节）.(ii) VF（F）（x）=VF（F）（xJ），对任意F∈F.给定两个状态x，XJ∈ X，我们称两个点PPDL模型（X，x）和（X，XJ）是状态双相似的（记为（X，x）s（X，XJ）），如果存在一个状态互模拟R <$X×X使得xRxj.注4.3回想一下，在定义迹等价（定义3.2）时，我们让本原函数（及其布尔组合）是LMP的标签这使我们能够解释形式B？的测试，其中B是原始函数的布尔组合。只有在这种设置下，作为结果的跟踪等价概念才意味着逻辑等价。对于互模拟，这种额外的标签结构是不必要的，因此上面的定义。虽然上面的定义只涉及单个模型X，但对于两个模型X和Y之间的互模拟，可以简单地将定义应用于它们的不相交并集X Y。直接观察到上述条件（i）可以推广到τω，对任意程序ω∈τω（其中τ = PB？ 第3节定义）：引理4.4If（X，x）s（X，xJ）乘R，则对任意ω ∈ π，τω（x，A）= τω（xJ，A）和R-闭A∈ <$X.证据 我们用关于ω的归纳法证明了这个命题。• ω=π：我们需要证明x∈A当且仅当xJ∈A，这是因为XRXJ且集合A是R-闭的.• ω=P，其中P∈P：我们需要证明VP（P）（x，A）=VP（P）（xJ，A），这已经是状态互模拟的定义（部分）。• ω=B？，其中B∈ B：所需方程化为VF（B）（x）=VF（B）（xJ），且x∈A当且仅当xJ∈A。它们直接由定义4.2中的条件2得出，并且A是R-闭的。T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283295∫∫一Fn·xωFy∈X∫22X• ω= ωJ·a，其中ωJ∈ ω j和a ∈ ω j：有两种子情况。(i) a=P∈ P。首先，回想一下τω′·P（x，A）=y∈Xτω′（x，dy）·VP（P）（y，A）。注意，（VF（P）（−，A）） −1（r）总是R-闭的，对于任意r∈[0， 1]。根据归纳假设，τω′（x，VF（a）（−，A）−1（r））=τω′（xJ，VF（a）（−，A）−1（r））这意味着两个积分是等价的。(ii) a=B？，其中B∈ B。同样，注意τω′·B？（x，A）= y∈Xτω′（x，dy）·τB？（y，A），且（τB？（−，A））−1（r）总是R-闭的，对任意r∈[0， 1]。Q下一个观察结果是，在非概率设置，状态bisimulation-灰意味着跟踪等价。引理4.5（X，x）s（X，xJ）蕴含（X，x）<$tr（X，xJ）。证据 假设R <$X × X是X上的状态互模拟，使得xRxJ。本文对ω∈F作了一个特例，证明了对任意F∈F，ρx（ω，F）=ρx′（ω，F）• ω= π：ρx（π，F）= VF（F）（x），根据定义4.2，VF（F）（x）= VF（F）（xJ）。ω非空：ρ（ω，F）=τ （x，dy）V（F）（y）=y∈V（F）−1（1）τω（x，dy）= τω（x，VF（F）−1（1））.注意，VF（F）−1（1）显然R-闭的，所以根据引理4.4我们有τω（x，VF（F）−1（1））=τω（xJ，VF（F）−1（1））。Q上面的观察，与我们在PPDL（定理3.7）方面对迹等价的描述相结合，产生了一个问题，即PPDL如何不能解释更强的状态双相似性概念，从而使PPDL +的引入成为必要。下面的例子说明了这一点。例4.6考虑PPDL签名（P ={a，b}， F ={F}）和以下两个点模型（X，x0）和（Y，y0）：a，1x0x1，sb，1Zx2b，1b，1y0a，1C1Cc3 4y3，sZY4其中F（x1）=F（x2）=F（x3）=F（y1）=F（y3）= 1， F（x4）=F（y4）= 0，和a，12b，12yX296T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283F（x0）= F（y0）= 0. 我们称x0<$PPDLy0. 根据定理3.7， 检查（X，x0）和（Y，y0）是迹等价的。 例如，ρx0（a，F）=1 12×1 +2× 1 = 1，ρy0（a，F）= 1× 1 = 1。 然而，这两个模型不是状态双相似的。这是因为如果这样的R存在，那么R也应该包含（x1，y1）和（x2，y1），但这不起作用，因为y1有一个非平凡的概率分支，而x1和x2都没有。T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283297L一一（）（）JJfJ≥r。 Sup pose（X，x）As（X，y）. 通过归纳，我们得到<$FJ）（x）=<$FJ）（y），所以对于表征的非平凡方向，即PPDL+意味着状态双相似性，其思想是从一些简单的逻辑L开始，类似于L0（见第2节），例如PPDL+意味着状态双相似性。 如果我们能证明PPDL+能表示L，那么PPDL+就意味着PPDL，我们就完成了。这促使我们引入L1作为0的扩展，基于观察到PPDL模型和LMP之间的主要区别是前者具有一些额外的权重结构（即VF）。与L0不同，在L1中，我们有F中的那些原函数F作为原公式：L13φ：：= T|F|φ∧φ|（3）其中F∈F，P∈P，r是[0，1）中的任意有理数。逻辑L1在PPDL模型上解释，语义类似于LMP上的L0特别是（X，x）<$F，如果VF（F）（x）= 1。 对于PPDL模型，我们可以证明下面的命题作为命题2.3的类似物。证据可以在附录A中找到。命题4.7设X =（X，<$X，VP，VF）是具有解析空间的PPDL模型，x，y是X中的两个状态. 则（X，x）s（X，y）当且仅当（X，x）<$L1（X，y）。然后，为了表明PPDL+等式意味着状态互相似性，它可以表明PPDL+可以编码L1（定义见（3））。在下面的翼引理中，令φ f表示Mulas和PPDL+（boolean）函数的L1之间的二元关系，使得φf当且仅当它们在语义上等价：对于任何PPDL模型X和x∈X ，X， x <$φif和o<$fif）X（x）=1，并且X， x/<$φif和o <$fifXf）（x）=0.引理4.8F或每个L1公式φ，其结果是一个函数f，因此，φ≠f。证据我们对L1公式φ进行归纳推理.注意T <$1;F<$F;φ1<$φ2<$f1<$f2，其中φi<$fi，i= 1， 2。对于φ=ar的情况，通过归纳假设假设f。然后，可以检查ar（af）> r。Q现在我们准备证明这一小节的主要结果定理4.9（PPDL+c刻画了状态互相似y）F或任意点PPDL模型X具有解析状态空间和状态x，y∈X，（X，x）s（X，y）当且仅当（X，x）<$PPDL+（X，y）.证据 对于正向，我们通过函数f的归纳进行推理。给定引理4.5和命题3.6，只剩下证明f=f（x）≥r当且仅当 f（y）≥r. 这需要 f> r（x）=f> r（y）。对于另一个方向，假设（X，x）<$PPDL+（X，y）。我们构造一个二元关系R<$X× X，并检查定义4.2中的两个条件。 根据引理4.8，（X，x）<$PPDL+（X，y）蕴涵（X，x）<$L1（X，y）。所以简单地让R是L1，xRy。然后应用命题4.7，我们知道在互模拟R下（X，x）As（X，y）。Q298T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283.Σx0的Y00−33F>31F>32F>31例4.10我们回想一下例4.6，其中（X，x0）和（X，y0）不是状态双相似的。 然后定理4.9 意味着 存 在 某 个 PPDL+函数可以区分这两个点模型。例如，令f=ab（F）>1> 2。然后可以计算出：b2X（x）=1 b2X（x）= b2Y（y）= 0这意味着，（Y，y0）。<$f）（x）= 1andf）（y） =0. Sof可以区分（X，x）5扩展的PPDL描述事件的双相似性本节致力于展示PPDL的另一个温和扩展可以用于验证PPDL模型的事件双相似性。事件互模拟的概念是在[2]中提出的，作为一种比状态互模拟更合适的方式来定义LMP的行为等价性，因为它不需要底层状态空间是解析的。在下文中，我们首先介绍新的逻辑，然后是PPDL模型的事件互模拟概念，最后展示它们的对应关系。5.1PPDL描述PPDL模型的事件双相似性的逻辑称为PPDL。直观地说，PPDL是通过以“最小”方式将L0添加到PPDL而获得的：与PPDL +不同，当re（）> r可以应用于任意函数时，在PPDL中仅允许f > r的某些实例。更确切地说，PPDL程序p，pJ和PPDL函数f定义如下，其中我们突出显示语法与PPDL具有相同子句的情况。PPDL布尔B：：= 1|F∈ F |BB| BB|（4）PPDL布尔函数C：：=B|P|C<$C（5）PPDL程序p：：= P∈ P |p; p|B？| p|p∗PPDL函数g，gJ：：=B|ag+bgJ|B·g|（6）PPDL函数f：：=g|C（7）PPDL公式φ：：=f≤g在PPDL的情况下，我们总是限制在结构良好的程序。注意PPDL函数f被定义为PPDL函数g，或者函数C，其中可能出现新的函数构造函数P（·）> r。直观地说，考虑PPDL而不是PPDL+的原因是，每个二进制化都是为了提供任意的pPDL函数，这也是由PPDL+syntax得出的，而是要求函数享有一些结构属性，如引理3.5为PPDL函数所保证的。PPDL的语义基于PPDL模型：所有的程序和函数都被解释为PPDL，而新的函数构造T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283299则是300T. Gu et al. /Electronic Notes in Theoretical Computer Science 352（2020）283.（1）（2）（3）（4）（1）L一（2）X1111111（Ⅲ）1解释为可测量的{0， 1}值函数P（C）> r（x）=1，如果 P（x，{u∈X| C（u）= 1}）> r。0否则5.2事件互模拟至于状态互模拟，我们可以将PPDL模型的事件互模拟定