基于缩窄的符号可达性分析及密码协议应用

理论计算机科学电子笔记117（2005）153-182www.elsevier.com/locate/entcs基于缩窄的符号可达性分析及其在密码协议验证中的应用我是梅泽格尔和普拉萨纳·塔蒂美国厄巴纳-香槟大学计算机科学系摘要窄化被引入，并且传统上被用于求解初始代数和自由代数中的方程模一组方程E。本文提出了一个泛化的缩小，它可以用来解决重写理论R的初始模型和自由模型中的可达性目标。我们表明，窄化是健全的和弱完整的（即，在关于R的合理的可执行性假设下，我们还表明，在一般情况下，窄化不是强完全的，也就是说，不完全时，一些解决方案可以进一步改写的R。然后，我们确定了几个大类的重写理论，涵盖了许多实际应用，其中缩小是非常完整的。最后，我们说明了一个应用程序的窄化分析的密码协议。保留字：重写逻辑缩小范围可达性安全协议。1介绍本文件讨论了以下技术问题。给定一个重写理论R满足合理的假设，是否有一个一般的演绎过程来解决R的可达性问题？我们所说的（−→x）t→tJ或者，更一般地说，这些可达性目标的存在性量化结合由于R通常指定并发系统或推理，*由ONR Grant N 00014 -02-1-0715和NSF Grant CCR-0234524支持的研究1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.06.024154J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153系统，解决这些目标的意义和利益是相当明显的。项t和tJ表示R的初始模型中的状态集合，我们想知道对于由t表示的状态的哪个子集，我们可以到达由tJ表示的集合。 在有限状态假设下，这类问题可以通过模型检验技术来回答[9]。然而，我们的兴趣在于一般方法不需要有限性假设，可以补充这种模型检查技术。在本文中，我们将窄化从解决等式目标的技术[16，21，23]推广到解决可达性目标的技术;事实上，等式窄化目标可以被视为可达性目标的特殊情况这种更一般意义上的缩小应该被开发为分析并发系统的方法，并且应该适合更广泛的分析能力，这在[12]中首次提出。 人们可以将窄化视为一种新形式的“符号模型检查”，也适用于无限状态系统，其中“符号”一词，而不是具有通过布尔命题表示有限状态集的更严格意义，被扩展为表示可能的有限状态集。这些方法甚至可以在有限状态系统的情况下有有用的应用，这些系统太大而无法通过标准模型检查技术进行分析。确实有许多技术积极研究分析有限状态系统，包括合适子类的模型检查，例如[4，5，15，17]，抽象技术，例如[10，26，19，25，40]，基于树自动机的可达性分析，例如[ 10，26，19，25，40 ]。[18，35]和定理证明，例如，[37、36]。我们认为缩窄是一种有前途的额外技术，有待进一步探索。事实上，缩窄技术已经被证明在密码协议的分析中是有用的[2，22，29]。我们正式定义了有序无条件重写的窄化，形式为R=（E，R），其中E =B，C 我们证明了解决方案的可靠性可达-证明了收缩过程在以下意义下是弱完备的：如果ρ是给定可达性问题的解，且ρ关于重写用规则RmoduloE归一化，则收缩过程找到包含ρmoduloE的解η.这个弱完备性结果在关于给定重写理论的合理可执行性假设下成立。我们还表明，在一般情况下，收缩在以下更强的意义上是不完整的：如果ρ是可达性目标的（不一定是归一化的）解，则收缩过程找到包含ρ模的解ηE. 因此，在缩小的完整性方面存在“弱点”。正如我们通过几个例子所表明的那样，这在一般情况关键是，在等式中，J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153155窄化[23]、并发和终止都是合理的假设; 2相反，指定并发系统的重写规则R通常是非并发和非终止的; 3实际上，终止常常意味着不希望的死锁。所有这一切都意味着，一般来说，重写也可能发生在替换本身，使缩小在强烈的意义上不完整。一个关键的问题是要调查确定有趣的类重写理论，缩小是完整的强意义上。我们证明了几个重要的类，涵盖了许多实际的应用程序有强大的完整的解决方案，可达性目标缩小。第一个重要的这类理论是顶层重写理论，也就是说，这些理论中的项只能在顶层重写。然后我们展示其他大型类重写理论，包括，例如，大多数面向对象的分布式系统，广泛的Petri网模型，语法，和许多以“俄罗斯套娃”体系结构[ 32 ]构造的分布式系统，我们还建立了一个强大的重写理论类R=（R，R，B）的完备性结果，使得B中的方程是正则的（LHS和RHS具有相同的变量集和线性的（LHS和RHS是线性项），R是连续的和终止模B，R是右线性的（RHS是线性的）。作为一个应用程序的例子，我们展示了如何缩小可用于分析的安全协议。许多安全协议的性质，如保密性和真实性，可以被描述为可达性问题。我们展示了如何强完备性的结果，最顶尖的理论可以用来验证协议的保密性时，协议会话的数量有界。这种技术也可以适用于验证其他安全属性，包括真实性。我们的分析技术的一个值得注意的特点是，收缩模方程提供了一个通用的过程，可以统一处理安全协议的分析，这些安全协议采用具有可见代数属性的加密算法，可以被入侵者利用（例如在XOR加密和Difference-Hellman指数化的情况下）[7，8，11，34，39]。2背景一个序排序签名S由一个排序集S，一个子排序包含≤在S上的部分- der关系，以及一个S_n×S-指标族S_n × S -指标族定义。{n，w，s}（w，s）∈Sn×S的运算s.我们通过f：w→s来记f ∈ f，s.我们定义S上的关系156J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153将1ns≤sJ意味着ssJ。 我们假设每一个等价的排序类都包含一个top 1排序，它是该类中所有其他排序的超排序。形式上，对于每一个排序s，我们假设存在一个排序[s]使得s∈sJ蕴涵sJ≤[s]。此外，对于每个f：s1×... × sn→ s我们假设也有一个f：[s1] ×. × [sn] → [s]。我们要求签名是合理的，即，只要我们有f：w → s和f：wJ→ sJ，其中w，wJ的长度相等，则w<$wJ蕴涵s <$sJ。一个S-代数定义为S-指标集族A={As}s∈S，使得s≤sJ蕴涵As<$AsJ，并且对于每个函数f：w→s，其中w=s1×.. . ×sna functionfw，s：As×.. . ×As→As。 此外，我们要求子排序重载操作一致，即， 对于每个f：w → s和（a1，. ，an）∈ Awwe要求f w，s（a1，. ，an）= f [w]，[s]（a1，. ，an），其中如果w = s1×. ×sn，则A A[w]=[s1] ×. × [sn]。我们假设一族X={Xs}s∈S的无限集合，变量，这样的ssJ意味着Xs<$XsJ=<$，X中的变量为与中的常量符号不同我们表示基项的集合和分别由T，s和T（X）s排序s我们把T记作环上基项的-代数，把T（X）记作变量来自集合X的项的-代数。我们使用一个正整数的有限序列，称为位置，来表示一个项中的访问路径。我们让ω在位置上变化 对于t ∈ T∈（X），设Var（t），Pos（t），FuPos（t）分别表示t中的变量、位置和不可变位置的集合。一个项的根在位置。 我们用t表示t在位置ω处的子项|ω。代换是一个映射σ：X→T（X），它将变量映射到项这与X的有限子集Dom（σ）的恒等式不同。我们也用σ表示σ到T∈（X）的同 态 扩 张 。由 σ 引 入 的 变 量 集 是 Ran （ σ ） =Ranx∈Dom （ σ ） Var （ σ（x））。将替换σ限制为一组变量V定义为：⎧<$σ（x）如果x∈ V σ|V（x）=否则，我们说，如果Ran（σ）<$V=，则替换σ远离变量集合V- 是的对于置换σ，ρ使得Dom（σ）<$Dom（ρ）=<$，我们定义它们的并[1]注意，这个顶级排序扮演了一个“错误超级排序”的角色J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153157EEE我我作为如果x∈Dom（σ），则为σ（x）⎨（σρ）（x）=⎪ ρ（x）如果x∈Dom（ρ）我们的服务一个等式是一个形式为t = tJ的表达式，其中t，tJ∈T<$（X）[s]，对于一个合适的[s]。序排序方程逻辑有一个健全而完备的推理系统E（见[31]），它对任何变量集Y都导出一个同余关系=Y关于项t，tJ∈T（Y）： t=YtJ当且仅当E（Y）t = tJ。为了简单起见，我们假设所有的排序都是非空的，也就是说，每一种类型都有一个相应的基项。那样的话如果t，tJ∈T<$（X）<$T<$（Y）则t=XtJ当且仅当t=YtJ.因此，超级-E E脚本符号=Y变得不必要，我们可以写=E。由于我们对签名的假设，t=EtJ，t∈T<$（X）s，且tJ∈T<$（X）sJ蕴涵s<$sJ。一个方程t=TJ称为（i）正则的，如果Var（t）=Var（TJ），（ii）保序的，如果对每个置换σ，我们有σ（t）∈T（X）s当且仅当σ（TJ）∈T（X）s，（iii）减序的，如果对每个置换σ，我们有σ（t）∈T（X）s蕴涵σ（TJ）∈T（X）s，（iv）左（或右）线性的，如果t（resp.tJ）是线性的（即，每个变量出现在一个单一的位置），和（v）线性，如果它是左右线性。一组方程E被称为正则的，或排序递减的，或排序保持的，或（左或右）线性的，如果其中的每个方程都是这样的话。T（X）上的E-包容预序E定义为tEtJ，如果存在一个置换σ使得σ（t）=EtJ;这样的置换σ称为从t到tJ的E-匹配。对于置换σ，ρ和一组变量V，我们定义σ|V=Eρ|V如果σ（x）= Eρ（x），对所有x∈V，且σ|VEρ|V，如果存在置换η，使得ρ|V= E（η σ）|V. 下面是一个有用的引理。引理2.1（[3]）对于置换σ，ρ和变量集V<$W，设Dom（σ）<$W<$V和Ran（σ）<$W=<$.则σ|VEρ|V蕴含σ|WEρ|W.Q一个方程组F是一个表达式的形式t1= tJ. t n= tJ，1NJ其中每个ti= ti是一个π-方程。 我们定义Var（F）=i Var（ti）<$Var（tJ）。F的一个E-单位元是一个置换σ，使得σ（ti）=Eσ（tJ），其中1≤i≤n。对于V=Var（F）<$W，一个置换集CSUE（F，W）被称为F远离W的单位元的完全集，如果• 每个σ∈CSUE（F，W）是F的E-单位元。• 对于F的任意E-单位元ρ，存在σ∈CSU E（F，W），使得σ|VEρ|V.• 对所有的σ∈CSUE（F，W），Dom（σ）<$V和Ran（σ）<$W =<$.⎪158J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153R/ER/E1n我我R/E1我n我2N一个E-单位化算法是完备的，如果对于任何给定的方程组，它生成一个完备的E-单位化器集。 注意，这个集合不需要是有限的。 如果一个统一算法在生成一个有限且完备的解集后终止，那么它被称为有限重写规则是l→r形式的表达式，其中对于适当的[s ]，l，r ∈ T（X）[ s]。一个（无条件的）顺序排序重写理论是一个三元组R=（E，E，R），其中E是顺序排序的签名，E是一组E-方程，R是一组重写规则。 我们只考虑重写理论R，其中对于R中的每个规则l→r，我们有Var（r）<$Var（l）。我们定义T ∈（X）上的一步重写关系如下：t →RtJ，如果存在ω ∈ Pos（t），R中的规则l → r，和替换σ，使得t|ω= σ（l）和tJ= t [ω←σ（r）]。读者可能会发现，由于我们对签名的假设，tJ总是良序的，并且t∈T<$（X）[s]意味着tJ∈T<$（X）[s]。设→R/E为关系式= E→R= E。一项t∈T<$（X）称为R/E-不可约的，如果不存在tJ∈T<$（X）使得t→R/EtJ. 请注意，闭包关系→定义重写理论R通常的顺序式演示的顺序排序版本[30]。 即对于任意t，tJ∈T<$（X）[s]，我们有t→<$tJ当且仅当R <$[t]E→[tJ]E，其中[t]E表示t模E的等价类。对于置换σ，ρ和一组变量V，我们定义σ|V→Rρ|V如果存在x∈V使得σ（x）→Rρ（x），且对所有其他y∈V，我们有σ（y）= ρ（y）。置换关系→R/E定义为= E→R = E。一个代换σ称为R/E-正规化的，如果σ（x）是R/E-不可约的注意，这是一个比说没有替代ρ更强的条件使得σ|X→R/Eρ|X（因为R中的规则不需要是排序递减的）。3可达性目标给定顺序排序重写理论R=（E，E，R），可达性目标G为一个形式为t1→ tJ的合取. 其中，对于1≤i≤n，ti，tJ∈T<$（X）[s]，对于适当的[si].我们说ti是我我目标G，而tJ是目标。我们定义Var（G）=iVar（ti）<$Var（tJ）。一置换σ是G的一个R-解（或简称为解，当R如果σ（ti）→σ（t i），方程组t1=TJσ（tJ），其中1 ≤i≤ n。 我们定义E（G）我... tn= tJ。 我们说σ是平凡的解G，如果它是E（G）的E-单位元我们说G是平凡的，如果恒等式置换id是G的平凡解。因此，σ是G的平凡解当且仅当σ（G）是平凡的。对于目标G：t1→t2. GJ：tJ→ GtJ. t J→1 2 2n−1我们说G= EGj，如果对所有1 ≤i≤2n，ti = Etj。 我们说G→RGJ，如果不J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153159R/E埃克塞特湾埃克塞特湾埃克塞特湾是一个奇i使得ti→RTJ，对于所有j/=i，我们有tj=TJ。的关系I j→R/E超过目标被定义为=E→R=E。引理3.1σ是可达目标G的解当且仅当σ（G）→σ对于一些平凡的目标。Q一个置换集Γ称为G的R-解的完备集，如果（i）每个σ∈ Γ是G的R-解，（ii）对于G的任何R-解ρ，存在一个σ∈ Γ使得σ|Var（G）Eρ|变量（G）。 我们感兴趣的是为给定的目标G和有序（无条件）重写理论R找到一组完备的R-解。由于E-同余类可以是无限的，→R/E-约化是不确定的-总的来说，能。解决这个问题的一种方法是通过使用面向方程和规则的重写组合来例如，Patrick Viry [42]（对于未排序的情况）提出了这种方法。我们在本文中采用这种方法我们假设E=EB使得（i）B是正则的且保排序的，(ii) B有一个有限的和完全的统一算法（注意，这意味着B-匹配是可判定的），并且B有一个完全的（不一定是有限的）统一算法2，（iii）对于每个t=tJ，我们有Var（tJ）<$Var（t），以及（iv）Var是排序递减的，并且是连续的和终止的模B.我们定义T <$（X）上的关系→ψ，B如下：t→ψ，BtJ，如果有一个ω∈Pos（t），l = r在ψ中，和一个替换σ使得t|ω= Bσ（l）和tJ= t [ω←σ（r）]。注意 ， 由 于 B 是 保 排 序 的 ， 而 T 是 减 排 序 的 ， 所 以 tJ 是 良 排 序 的 ， 并 且t∈T<$（X）s意味着tJ∈T<$（X）s。关系→R，B也有类似的定义，由于我们对签名的假设，t→R，BtJ意味着tJ是良序的，t∈T<$（X）[s]意味着tJ∈T<$（X）[s]。我们定义→ R →B为→R，B→B，B。注意，由于B-匹配是可判定的，所以→R，B，→R，B和→R→ R，B是可判定的。这三种关系被提升为目标和替代。B-标准化（以及类似地R、B或R、B-标准化）取代如预期地定义。这个想法是使用→R/E，B在（术语和目标）上实现→ R/E。要做到这一点，我们需要以下额外的假设。• 当t → t时，B与b相邻，即：，t1，t2，t3我们有一个vett1→+t2并且t1=Bt3意味着<$t4，t5使得t2→<$t4，t3→+t5和t4=Et5[2]在某些额外的假设下，如B-coherency of a，B rewriting [23]，这是一种情况，即b-coherencyB有一个完整的统一算法，通过方程窄化。但我们也允许针对B-B的专用统一算法的可能性。160J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153埃克塞特湾埃克塞特湾埃克塞特湾R/E罗塞洛湾R/E阿尔布费拉湾∗[23]第10段。+埃克塞特湾Bt4||E||Et3−→+t5• 当e→R时，B与B是E-共轭的，即. t1，t2，t3表示t1→R，Bt2并且t1=Bt3意味着Bt4使得t3→R，Bt4和t2=Et4.我们还假设→R，B是与h→R，B的E -共轭，即t1，t2，t3分别对应着t1→R，Bt2和∗埃克塞特湾t3蕴涵t4，t5使得t3→t4t4和t4→R，Bt5和t5 = Et2。t1 →R，Bt2t1−→R，B t2⏐||B||Et3 →R，Bt4⏐* *埃克塞特湾∗埃克塞特湾||E→R，Bt4(a) E-→R，B 与B的相容性（b）E-→R，B与→R，B的下面的引理将→R/E与→R，B和→R，B联系起来。它最初是由Patrick Viry为无序无条件重写理论建立的[42]，但以一种直接的方式提升到我们的有序设置。引理3.2设R=（B，B，R）是一个有序重写理论，上面假设的属性 则t1→R/Et2当且仅当t1→ R→R，Bt3对于某个t3= Et2.Q因此，t1→t2当且仅当t1→t2对于某个t3 = Et2。 的读者可以检查，这可以提升到目标，如G1→G2G2当且仅当∗罗塞洛湾对于某个G3= EG2. 所有关于R在本节中，将适用于其余的文件，除非明确提到否则，请执行以下操作。4窄化：合理性和弱完备性T（X ）上的R，B-映射关系如下定义：t~σtJ，如果存在ω ∈ FuPos（t），R中的规则l → r，其中我们假设Var（t）<$Var（l）=<$，且σ∈CSU E（t|ω= l，V），使得tJ= σ（t [ω←r]）。这被提升到可达性目标，如下所示。让G：t1→t2. t2n−1→→tJ... J.J.→tJ得双曲正弦值.1 2 2n−1 2nt1→t2→t1→t3→如果G1→J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153161J超pose有Var（G）V。我们定义G~σR、BGJ，如果有一个奇数i证明了对于某些σthat，t~σtJ对于Var（G）是可解，且对于所有j我我们有i R，Biσ∗J= σ（tj）。 我们写G~GJ如果G=GJ且σ=id，或者存在一个不R、B162J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153R，B R，B n n−1 1R，BR，B罗塞洛湾罗塞洛湾罗塞洛湾导出G~σ1的 序 列 。 . ~σnGJsuchthatσ=σ<$σ你. . . . 好吧类似地，如预期的那样，在术语和目标上定义了R，B-窄化和R，B-窄化关系。众所周知，B-窄化可以为B-窄化提供一个合理而完整的程序[23]。我们表明，R_n，B_narrowing给出了一个声音，但只有弱完整（在下面的意义上精确）的程序计算可达性目标的解决方案。4.1健全性我们首先考虑稳健性问题。按照[23]中的思想，我们将每个R，B-窄化导子与一个R，B-重写导子联系起来，然后诉诸引理3.2来完成论证。首先我们考虑一步缩小项的推导。以下引理的证明与[23]中关于λ，B-窄化和λ，B-重写之间的对应性的Lemma4. 1t~σtJ蕴含σ（t）→tJ。Q这可以提升到缩小目标的推导如下。Lemma4. 2G~σGJ蕴涵σ（G）→σGJ。这就给出了下面的可靠性定理。TheoreM4. 3（soundness）LetG~σ设η是平凡解的解，则η <$σ是G的解。4.2弱完备性证明弱完备性背后的思想是将每个R，B-重写派生与R，B-窄化派生相关联。只有在某些假设下才有可能建立这种对应关系，因此，完整的首先，我们考虑一步重写条款。引理4.4设ρ是一个R ∞，B-正规化代换，V是一个包含Var（t）的有限变量集。设ρ（t）→R∈ R，BtJ利用规则l→r在R中或方程l = r在R中.然后有σ，tJJ，η使得：(i) t~σR_t，B_t，J_J用同样的规则或公式。(ii) η是Rπ，B归一化(iii) η（tJ）=BtJ，以及(iv) ρ|V= B（η σ）|VJ. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153163埃克塞特湾R/E罗塞洛湾接下来，我们将一步R/E-重写与R收缩、B-收缩推导相关联。引理4.5设ρ是一个R∞，B-正规化代换，V是包含Var（t）的有限变量集。 则ρ（t）→R/EtJ意味着存在σ1，σ2，tJJ，η使得：(i) t~σ1~σ2R、BtJJ(ii) η是Rπ，B归一化(iii) η（tJ）=EtJ，以及(iv) ρ|V= E（η <$σ2<$σ1）|V上面的引理可以被提升到缩小目标的推导，如下所示。引理4.6设ρ是R_n，B-正规化代换，V是变量包含Var（G），且令ρ（G）→ <$GJ. 然后，有σ，GJJ，η使得：~σ罗塞洛湾 GJJ(ii) η是Rπ，B归一化(iii) η（GJ）= EGJ.(iv) ρ|V= E（η σ）|V现在我们准备证明弱完备性结果。定理4.7（弱完备性）设ρ是可达目标G的R/E-正规化解，V是包含Var（G）的有限个变量集。然后有σ，GJ使得：~σ罗塞洛湾GJ和GJ有平凡解.(ii) 存在η∈CSU E（E（GJ），V<$Ran（σ））使得（η <$σ）|VEρ|V我们将在后面看到定理4.7对于不是R/E-正规化的置换ρ不必成立，因此窄化仅仅是弱完全的。4.3可达目标的弱完备算法定理4.8对于可达目标G，设V是包含Var（G）的有限变量集，且设Γ是形式为η∈σ的所有替换的集合，其中G~σ <$GJ，η ∈CSU（E（GJ）， V<$Ran（σ））. 这是一个复杂的EG的解关于R/E-正规化解的集合证据 定理4.3和4.7Q(i)G(i)G164J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153这个定理提供了一个通用的算法，它从G开始建立一个缩小树，以找到所有R/E-规范化的解决方案。该树中的节点对应于目标，而边对应于一步R-收缩，B-收缩衍生。由于可以有无限长的窄化推导，算法必须以公平的方式扩展树以覆盖每个可能的推导。此外，注意，对于树中的每个节点，该算法调用一个递归B-统一算法，该算法不需要是无限的，即，统一算法可以返回无限个单位集因此，该统一算法的执行最后，我们注意到，研究适当的策略[3]是很重要的，在保持完整性的同时，使这种缩小过程尽可能有效。4.4狭窄的不完全性窄化仅对于R/E-归一化解是完全的。它一般是不完整的，如下面的例子所示Example4.9LetR=（k，k，R），其中签名k具有单一排序，并且一元函数符号s、f、g和R具有以下两个规则：s（x）→s2（x）f（s2（x））→g（s（x））可达性目标G：f（x）→f_g（x）有解σk={sk（y）/x}，其中k ≥ 1（没有一个是R/E-标准化的）。 但是窄化只返回σ2作为一个解，并且它并不意味着σ2|{x}σ1|{x}。Example4.10ConsiderR=（n， n，R），其中n有一个单值sort，常数a，b，c，d和一个二元函数符号f，R有以下三个规则：a→b a→cf（b，c）→d可达性目标G：f（x，x）→f（d）有σ={a/x}作为解。但G既没有平凡的解，也没有从它开始的缩小的推导5一些强完备性结果这是可能的，以获得强的完整性结果的有用类重写理论。我们考虑几个这样的类，包括最顶层的重写理论，类语义等同于最顶层的重写理论，线性重写理论。J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）1531651n5.1最高重写理论我们说R=（E，E，R）是一个最顶层的重写理论，如果在S/E的一个等价类中，存在一个顶层排序状态，使得：• R中的每个规则重写排序状态的项，即， 对于R中的每个l→r，l∈T（X）态和r∈T（X）态是这样的情况。• 对于每个f：[s1] ×. ×[sn]→s在n中，情况是[si]/=状态，1≤i≤n。这两个条件迫使每次重写都发生在学期的顶部 更准确地说，关系式→R/E和→R，E重合，如果t →R，EtJ，则这种重写发生在t中的位置处。因此，如果我们有一个E-匹配算法，R/E-约简是可判定的，因此第3节中关于重写理论R的假设可以简化如下。我们假设（在（仅本小节）R=（E，E，R）具有以下性质：（i）R是最上面，（ii）E中的方程没有状态变量，以及（iii）E有一个完整的统一算法。(In第3节中的其他假设是不必要的）。我们表明，R，E-窄化提供了一个健全的和强完整的程序，解决重写理论中的可达性目标与上述性质（i）关于合理性的论证与第4节相同。为了完整性，我们首先建立引理4.5的一个更强的版本，其中替代ρ不再需要被归一化。引理5.1设t是不是变量的项，设V是包含Var（t）的变量集合。对于某些替换ρ，令ρ（t）→R/EtJ，在R中，rulel→r。当reeeσ，η，tJJ使得t~σR、EtJJ使用相同的规则，tJJ不是变量，η（tJJ）= EtJ，且ρ|V= E（ησ）|V.利用上面的引理，通过类似于第4节的论证，我们得到下面的定理。定理5.2（最强完备性）设G：t1→TJ我... ∧tn→tJ是可达性目标，使得对于1≤i≤n，ti不是变量，σ∗设ρ是G的一个解.则存在σ，GJ使得G~R，EGj，并且存在η∈CSUE（E（GJ），V<$Ran（σ））使得（η <$σ）|VEρ|V.Q因此，对于一个目标G，没有一个源是变量，所有满足G~σ的子条件η_∞σR、EGJ和η∈CSUE（E（GJ），V Ran（σ）），其中V是包含Var（G）的变量的有限集合，是解决了G.与第4节一样，这给了我们一个计算完整解集的通用算法，从G开始构建一个缩小树。注意，由于E-unification算法可以返回无限个unifier集合，166J. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）1531n1n缩窄树可以无限分支。因此，为了确保完整性，必须以公平的方式扩展收缩树。在实践中，我们经常可以将给定的重写理论转化为在某种意义上等价于它的最顶层重写理论，然后利用上面的完备性结果。在下文中，我们考虑几类可以这样做的理论。最高模结合性、交换性和恒等式（ACU）：一个有序重写理论R=（E，E，R）被称为是最高模ACU，如果在S/E的一个等价类中，有一个顶排序Con fig使得：• R中的每个l→r使得l，r∈T∈（X）Con fig.• 只有一个运算符的arity包含排序s，使得[s] =Con fig，即，n：Config×Con fig→Con fig。运算符是结合的和交换的，并且具有恒等式null。许多指定面向对象系统的顺序排序重写理论是最顶层模ACU，特别是，涉及分布式状态是对象和消息的多集的可扩展配置的面向对象系统通常是最顶层模ACU。另一类例子是由不同类型的Petri网提供的[41]。一个模ACU最高的理论R可以转化为相应的模A的最高理论R=（E，E，R）。 该特性通过添加一个新的顶级排序State和一个新的操作符{}：Config →S ta te扩展了该特性。在R中，对于每个重写规则l→r，{lC}→{rC}，其中C是一个新的类Con fig变量。这个transfor-满足以下等价性。引理5.3设R是最高模ACU的重写理论。然后，对于任意的T，tJ，我们有t→R/EtJ当且仅当{t}→R/E{tJ}。Q上面的引理意味着G：t1→ tjj∈ G的R-解的集合. ∧tn→tJ是G_n的R_n解的一个等价形式：{t1}→t{tJ}_n. . . {tn}→{tJ}。因此，要找到G的R -解的完备集，我们只需找到目标G的R-解的完备集。请注意，abovetransformationR<$→R<$可以很容易地推广到运营商⊗满足同样的假设，除了企业简介只有结合性和交换性（AC）公理，或结合性和单位性（AU）或仅结合性（A）。这使得这些结果也适用于许多字符串处理重写理论，如语法。在每一种情况下，R →RJ. Meseguer，P.Thati/理论计算机科学电子笔记117（2005）153167规则”。例如，对于AC，我们还必须添加规则{l} → {r};对于AU，我们只需添加{C<$l<$CJ} → {C <$r<$CJ};对于A，我们还必须添加{C<$l} →{C<$r}、{l<$C} → {r<$CJ}和{l} → {r}。通过这些修改，上述结果也适用于AC、AU和A情况。俄罗斯套娃不增加深度：许多分布式的基于对象的系统并不是抽象的配置;相反，它们是结构化的配置，在这种配置中，对象和消息的多重集本身可以包含由适当的边界算子封装的嵌套的多重子集Meseguer和Talcott [32]称这种结构化的配置为俄罗斯娃娃，以强调其嵌套和递归特性。由于在这种系统中，重写可以发生在任何嵌套级别，因此刚刚为最高模ACU理论开发的结果并不直接应用。然而，在合理的假设下，方程不会改变嵌套的深度，重写规则不会增加深度，可以将相同的想法扩展到俄罗斯娃娃，因此缩小仍然是一种针对适当目标的强完整分析方法俄罗斯套娃的理论R=（R，E，R）具有以下形式。• 该签名包含排序FlatCon fig和Con fig，其中FlatCon fig

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