VLRL动作公式的线性时态逻辑（LTL）证明模式的研究

理论计算机科学电子笔记117（2005）113-133www.elsevier.com/locate/entcs用Maude模型证明VLRL作用性质米格尔·帕洛米诺和伊莎贝尔·皮塔通过将SistemasInforaticoniversidComplutensedeMadrid摘要重写逻辑验证逻辑（Verification Logic for Rewriting Logic，VLRL）是一种模态动作逻辑，其中重写规则被捕获为动作。本文研究了利用线性时态逻辑（LTL）的Next和Until算子对VLRL动作公式的一种可能表示。特别是，它研究了使用Maude模型检查器来证明VLRL动作公式。 VLRL的动作模式固定了将在一个状态中发生的转换以及它将被应用的上下文，而 LTL运营商则没有。因此，在LTL表示动作模态，有必要将初始重写理论转化为一个新的，其中的状态进行有关使用的过渡和它们发生的上下文的信息。通过将VLRL公式转化为等价的LTL公式，在变换理论中研究了VLRL的性质。关键词：模态逻辑，线性时序逻辑，Maude，重写逻辑，重写逻辑的验证逻辑，理论转换。1介绍重写逻辑的验证逻辑（VLRL）[3，10，11]是一种模态动作逻辑，其中重写规则被捕获为动作。它支持重写逻辑[6，7]中指定的系统属性的验证。为了表达系统的性质，VLRL允许定义系统行为的观测。这样，在每种情况下，都是用户确定他想要强调的系统事实VLRL签名固定了一个指定的排序状态，该状态表示与捕获的更改相关的系统对象。然后，VLRL动作*研究部分得到西班牙CICYT项目MELODIAS TIC 2002 - 01167和MIDAS TIC 2003 -01000的支持。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.06.026114M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113表示那些“原子的”转换，在这种意义上，即使在这种转换期间发生多于一次的重写，也会发生这种情况，因为状态的结构允许同时执行这种重写。VLRL模态语言提供了四种动作模态来表达给定状态的后继者的属性。其中两种模态是不确定的，因为它们需要动作来表示从当前状态的现有转换。其他两项是普遍性的，没有强加这种要求。VLRL允许验证一个特定的重写序列，与线性时序逻辑（LTL）相比，其中所有的计算路径都被探索。有关计算路径的属性通过使用动作模态以自然的方式在VLRL中表示。实际上，VLRL可以用作一个灵活的接口，在其中证明不同分支时间时态逻辑中表达的性质[3]。除了本文所探讨的逻辑的动作部分之外，VLRL还提供了一种用于表达系统各部分属性的空间模态，并且逻辑允许动作和空间模态以极大的自由度组合。本文研究了如何使用LTL的Next和Until算子来表示动作性质，以便使用Maude模型检查器[2]来帮助证明VLRL性质。但是，虽然行动模态固定了将在一个状态及其背景中发生的转变，但LTL操作者没有。因此，为了在LTL中表示动作模态，有必要将初始重写理论转换为一个新的理论，其中状态携带有关所应用的转换及其发生的上下文的信息;这是基于Meseguer先前关于重写理论转换以表达公平和正义属性的工作[8]。然后在变换后的理论中研究VLRL性质，将VLRL公式转化为LTL公式，利用这些附加信息来表达相同的性质。为此，我们使用一个状态谓词来表示动作α何时被应用以获得某个状态，taken（α），另一个状态谓词来表示动作何时被并发地应用，concurrently。两个状态谓词的满足被定义为转换理论的状态。我们用一个简单协议的具体化来说明我们的方法，但是我们的构造适用于具有交换和结合结构的任何系统，并且通过对这里提出的思想进行简单的扩展，它也可以用于任意系统。第2节总结了本文中使用的主要VLRL概念，第3节介绍了重写理论如何转换为具有动作信息第4节解释如何获得原子M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113115命题从观察;然后翻译的VLRL行动公式的LTL公式解释。第5节展示了使用Maude模型检查器来证明一些VLRL公式。最后，附录中包含了本文中给出的例子的完整说明本文假设熟悉重写逻辑和Maude及其LTL模型检查器;关于它们的详细说明可以在[6，1，2]中找到。我们的记法遵循标准惯例：T表示签名上的项的初始代数，T/E是理论（E，E）的项[t我们用t[w/x]来表示在t中用w替换变量x得到的项;有时用上划线来表示表达式序列。2VLRL概述VLRL [3，10，11]是一种像其他模态和时态逻辑[5，4]一样以间接和全局方式谈论变化的逻辑，与重写逻辑相反，重写逻辑是一种变化逻辑。其思想是提供用于观察系统状态的属性和用于说明其基本状态变化的动作符号。2.1验证签名给定重写签名（A，E），验证签名（A+，E+，State，At，L）包括：• 一个杰出的国家，•·定义扩展的附加排序和运算符，以及以保护原始签名的方式将扩展公理化的一组E+使得T +/E+|T/E;• 观察属性的族At，每个观察属性都有一个关联的排序s为+;• 一个集合L的标签索引的字符串排序中。索引对应于出现在规则中的变量的排序序列，该规则定义了与标签相关联的动作。2.2一个简单的互斥例子在下文中，我们用从[1]中借用的一个简单的具体化来说明我们的方法。它描述了一个有两个进程的系统，a和b，共享一个关键资源。每个进程可以是等待的，也可以是处于临界区的，116M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113互斥并且它们通过向彼此传递不同的令牌（$或#）来轮流访问临界区。mod MUTEX是排序名称模式进程令牌配置。子排序令牌进程<会议op none：-> Conf.op ：Conf Conf -> Conf [配置文件id：none]。ops a b：->名称。ops wait critical：->模式。op<_，_>：命名模式->处理ops # $：-> Token。rl [a-enter]：$ =>.rl [b-enter]：# =>.rl [a-exit]： => #. rl[b-exit]： => $.恩德姆我们可以定义两个布尔排序的观察属性，crit-a和crit-b，来检查给定的进程是否处于临界区。与我们将在下面使用的MUTEX的签名（EMUTEX，EMUTEX）相关联的验证签名是+互斥+互斥 ，Conf，{crit-a，crit-b}，L），+互斥使用排序Bool，E+扩展E的扩展，对于布尔运算符，L ={a-enter，b-enter，a-exit，b-exit}。2.3行动我们首先定义预动作α。这些对应于通过以下演绎规则获得的证明项集合• 鉴别：各1个[t]、[t]：[t] →[t]• 替换：对于每个重写规则r：[t（x1，...，X ）] −→ [tJ（x1，.，X ）]及项w1，...，wn，和n nr（w）：[t（w/x）]→[tJ（w/x）]，• f-结构：对于每个f∈f，α1：[t1] −→ [tJ].α ：[t]−→[tJ]1n nn，f（α1， .. . ， α）：[f（t1， . . ， t）]−→[f（tJ， . . ，tJ）]n模以下等式：n1n• Idn t it . ，[tn]）=[f（t1， . . ，tn）]，[1]注意，[t]表示一个状态以及该状态对应的身份转换（，E与M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113117• E中的公理：t（α）= TJ（α），对于E中的每个方程t = TJ.操作是重写排序状态项的预操作。2直观地说，动作（或更一般地，预动作）对应于在[6]中证明了重写理论的初始模型中的任何转换都可以分解为预动作的交织序列。应该注意不要将这个概念与我们也将使用的一步重写一步重写关系，表示为−→1，以区别于一般的重写关系−→，两个项u和vi存在u−→v的一步证明，即，u−→v的证明，其中仅一个重写规则应用于单个子项。换句话说，一步重写是一个预先动作，其中替换规则只应用了一次。Maude模型检查器对于与重写理论相关的Kripke结构的跃迁关系[2]。2.4行动方式VLRL定义了四种动作模态，[α]，[[α]]，[α]和[α]，它们捕获由动作α执行的状态转换。与验证签名相关联的模态语言3由下式给出：：：= true |t1= t2|¬ϕ |ϕ ⊃ ϕ |[α] β |[[α]] |⟨α⟩ϕ |⟨ ⟨α⟩⟩ϕ其中，t1和t2是在用属性作为对应排序的常数扩展的签名n+上给定观测属性的解释I，映射每个JI，σ排序s的属性到从T/E，State到T+/E+，s的函数，值[[[t]]在状态[t]关于I的项tJ和基替换σ是：• [[x]]I，σ[t] =σ（x），• [[at]]I，σ[t]=I（at）（[t]），• [[f（t1， .. . ，tm）]]I，σ[t]=f（[[t1]]I，σ[t]， . ，[[tm]]I，σ[t]）。[t]在给定状态[t]、观察解释I和地面替换σ下，动作模态公式的满足由结构归纳定义：• [t]，I，σ| = VLRLt1= t2i [[[t1]] I，σ [t] =[[t2]] I，σ [t].[2]上述对动作的定义假定R中的规则是无条件的。对条件规则的扩展很简单。[3]实际上，正如在导言中所说的，这只是语言的动作部分：完整的定义见[3118M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113• [t]，I，σ| = VLRL[α]<$i <$[[[α]] σ：[t] → [tJ]蕴含[tJ]，I，σ| = VLRL• [t] ， I ， σ| = VLRL[[α]] i [t] ， I ， σ| = VLRL[α] 和 [t] ， I ， σ| = VLRL[β（α）]，对于所有把α放在上下文中的动作β（α），也就是说，β（α）仅用恒等式和α上的结构规则构造。• [t]，I，σ| = VLRL<$α<$$> i <$[[[α]] σ：[t] → [tJ]和[tJ]，I，σ| = VLRL• [t]，I，σ |= VLRL⟨⟨α⟩⟩ϕ iff either [t],I,σ |= VLRL⟨α⟩ϕ or there is an actionβ（α），将α置于上下文中，使得[t]，I，σ |= VLRL<$β（α）<$β。在其他情况下也是如此注意，[α]和[[α]]是普适模态，要求公式对所有可能的后继者都成立，而不是存在性的α和α动作α是可以解释的，因为它们可能包含变量。我们用[[[α]]σ表示由基作用量给出的状态转移，基作用量是通过将σ代入作用量α而得到的。然后，对于给定的替代动作是确定性的，但部分，即，它们并不适用于每个国家。事实上，一旦实例化，一个动作就只适用于一个状态;这是因为动作本身携带了关于重写规则应用于何处的所有上下文信息。单作用模态[α]和双作用模态[[ α ]]和双作用模态[[α]]之间的区别在于，双模态允许在更广泛的背景下对系统的部分属性进行表述，而不需要由于需要为那些保持不变的子项明确上下文身份转换而使符号也就是说，动作可以发生在表示状态的项中的任何地方例如，MUTEX验证签名的属性的预期解释I是这样的，如果它包含子项a，crit>，则I（crit-a）将排序为Conf的项映射为true<，否则映射为false，并且对于I（crit-b）也是类似的。 在这种解释下，公 式 [[a-enter]] （ crit-a = true ） 和 [[a-enter b-enter]] （ crit-b =true）在$状态下成立，但公式[[b-enter]]（crit-a= true）不成立。3向状态添加操作和上下文一般来说，对于重写理论R来说，直接指定一个形式为（a（y））的谓词持有那些由将动作a应用于某个其他状态而产生的状态，或者一个谓词并发地声明两个动作可以并发地完成，可能是不容易的。 我们所能做的是将一个语义等价的理论RJ与R相关联，该理论具有关于在系统中应用的动作以及触发动作的上下文的信息。然后，我们可以在这个新的理论中推理VLRL的属性，M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113119返回到R得到的结果在本节中，我们通过定义一个理论NEW-MUTEX来说明我们的一般技术，该理论用一些新的排序、运算符和规则扩展了我们的重写理论MUTEX，但也以下面解释的方式修改了原始规则。完整的规格可以在附录中找到3.1新国家NEW-MUTEX中的状态将携带有关创建它们的操作的信息它们被表示为元组{C |R|一|{\ f n M i c r o s o f tY a H e i \ f s 1 4 \ b o r d 1 \ s h a d 0 \ 3 a H C C \ b 0 }其中：• C是表示原始系统MUTEX中的状态的项。• R可以是concur或no-concur，这取决于最后一个动作是否与前一个动作同时执行。对于初始状态，它的值是独立的：我们任意选择concur。• A是已执行的最后一个操作• S是一个标记状态，在这个状态中，那些被最后一个动作改变的子项被标记在@@中。为了帮助理解基本思想，$a，wait > #b，wait >−→a，critical>b，critical>在MUTEX。这种转换可以在动作a-输入后接b-输入的顺序应用、b-输入后接a-输入的应用、或动作a-输入b-输入的单次应用之后出现。在第一种情况下（在第二种情况下也是如此），变换理论中相应的重写如下（运算符 * 和+将在下一节中解释）。{$# |concur |**|$+a，等待>+#+b，等待>}−→1{ #|concur|输入|@ @+#+ }−→1{|不一致|b输入| +@b，临界>@}<请注意，与最后一个状态相关联的操作仅为b-enter，标记的子项b，critical>对应于最后一个操作更改的子项。<第二个状态的第二个论点是平凡的一致，因为它是迄今为止发生的唯一行动。120M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113另一方面，通过以不同的方式执行最后的重写，在变换的理论中模拟单个动作a-enter b-enter{$# |concur |**|$+a，等待>+#+b，等待>}−→1{ #|concur|输入|@ @+#+ }−→1{|concur| a-输入b-输入|@@ + @@}状态的第三个组成部分反映了两个动作同时发生的事实，如第二个参数中出现的concur所示。由于操作a-enter b-enter改变了这两个子项，它们现在都被标记了。似乎令人惊讶的是，并发动作a-enter b-enter实际上对应于转换理论中的两个步骤：这是由于莫德模型检查器通过一步重写来工作的事实而强加给我们的。由于不可能事先预见哪些并发步骤如果一个新的规则将发生，我们所能做的就是将每个原始规则转换为转换后的理论中的一个规则，并依靠它们的交错来允许所有可能的并发行为。正是第二个参数，当它的值为concur时，它告诉我们交织必须被解释为一个并发操作，其完整名称出现在第三个参数中。3.2新种类引入了新的排序来处理操作、标记状态和新状态。排序Action+。排序同意。对Conf+ Conf'进行排序。排序NewConf.subsort Conf Concur。为了捕获由应用演绎的替换规则引起的动作，想法是为每个重写规则l添加：[t（x）] → [tJ（x）]，其中我们假设x =（x1：s1，.，xn：sn），运算符操作l：s_1. s_n -> Action。M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113121由于MUTEX中的规则只涉及基本术语，ops a-enter b-enter a-exit b-exit：-> Action.通过签名结构规则获得的动作通过允许签名的操作符也应用于动作来在我们的案例中，OP none：-> Action.op：ActionAction -> Action [aslogid：none]。我们为动作添加一个新值*，它不同于系统中定义的所有动作。此值在初始状态中用于表示尚未发生任何操作。op *：->Action+。标记状态由Conf+排序项表示;它们由系统状态和操作符op @_@：Conf -> Conf+.op_+_：Conf+ Conf+-> Conf+[配置文件]。第一个操作符是 第二个操作符组合标记的状态以得到另一个标记的状态。最后一个运算符的声明与MUTEX中构造状态的运算符具有相同的属性，除了没有声明以便于定义辅助运算的身份元素。“Conf它由以下操作定义op_._ ：Conf+ Action -> Conf'。op [_]：Conf -> Conf '.op_+ ' _ ： C o n f ' C o n f ' - > C o n f ' [ a s s u m p t i o n ] .等式var S：Conf+.var A：Action。 var C：Conf.eq（S. A）+1C =（（S + C）.A）。第一个操作将关于用于获得状态的动作的信息添加到状态。这些扩展状态是应用原始系统的变换重写规则的结果（参见，例如，规则a-在本节结尾处输入）。第二个操作用于挑出重写规则将应用于的子项。这个操作与最后一个操作结合起来，下面的规则将状态分解为它的组件。最后，排序NewConf用于表示转换理论联系我们|_|_|_}：Conf CONNECT Action+ Conf+-> NewConf.122M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）1133.3新规MUTEX中的原始规则必须进行转换，以便它们仅适用于当前选择的术语，并指出创建了哪些新术语。为此，左侧封装在括号内，右侧由结果进程和标记的令牌组成，以及规则的名称（对应于执行的操作rl[a-enter]：[$a，wait>]=>（@ @. a-enter）。rl[b-enter]：[#b，wait>]=>（@< b，critical> @. b-enter）。rl[a-exit]：[]=>（（@@+@#@）. a-退出）。rl[b-exit]：[b，critical>]=>（（@@+@$@）. b-退出）。然后，NEW-MUTEX包括将状态{C |R|一|{\fnMicrosoftYaHei\fs14\bord1\shad0\3aHCC\b0}进入状态{C '|R'|一个'|其中：• C• R• 如果A和B同时执行，则A• S'是通过标记已经被动作B改变的子项来更新S的结果。用于指定这些步骤的重写规则如下：varsS S '：Conf+.var C：Conf.var R：同意。var A：Action。varA+：Action+。crl [step1]：{ C| R |A+|=>{啊！S'|concur|（一）|（A，A+））|（一）|（S '，S））} f [ C ] =>（S'，S） A）/\（S&' S）。crl [step2]：{ C| R |A+|=>{啊！S'|不一致|一|S ′} i f[ C ] =>（S ′.A）。只有当最后一个动作可以与前一个动作同时执行时，才可以使用规则step1。这是由S' S条件保证的&&op _&_：Conf+ Conf+-> Bool.检查由S'表示的应用动作AM. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113123标记状态S。其基本思想是寻找标记状态在S和S'中都有@ C @备注。如果S和S&新的状态是在辅助运算的帮助下得到的OP！_ ：Conf+ -> Conf.op|：Conf+ Conf+ -> Conf+。op|：Action Action -> Action。第一个是消除一个标记状态的标记。第二个参数更新作为其第二个参数给出的状态的标记，并将其作为其第一个参数给出的标记状态的标记。第三个操作通过将第一个操作与第二个操作相加，从两个操作中构造出一个操作我们用下面的约简来说明它们的行为，这些约简出现在3.1节第二个例子的最后一步：红色！（+ @@）。resultConf：a，critical>b，critical>Maude>红色|（+ @@，@ @ + # +）。resultConf+：@a，critical> @ + @b，critical>@红色|（b-enter，a-enter）。result操作：a-输入b-输入规则step2简单地执行一个新的动作，相对于之前的动作以非并发的方式执行。步骤规则的条件的第一项通过模仿MUTEX中的转换来重写状态。 首先，我们定义一个规则来获得MUTEX的重写规则将应用于的子项。crl[decline]：[C1 C2]=> C1 +' [ C2 ] if C1 =/= none and C2 =/= none.Remark. 重写st→α1的顺序t1→α2·· ·→αntn对应于动作α1，...，αn在MUTEX中有效，当且仅当{t|BA|一|S} →{t1|BA1|alpha1| S1}→ ··· →{tn| 禁 令 |alphan| Sn} 是 NEW-MUTEX中的有效重写序列，其中S是表示将t分解成其令牌和进程的项。124M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）1134在LTL我们本节的目标是，给定观测的解释I，定义从作用公式到LTL的转换，使得在给定的解释下，一个公式在VLRL中的一个状态中成立，当且仅当转换后的公式在变换系统的相应状态中成立我们首先研究如何将原子VLRL公式表示为LTL中的状态谓词，然后考虑如何翻译任意公式。4.1从观察中定义命题其思想是为每个可能的原子VLRL公式（即每个可能的方程）提供一个状态谓词为此，我们将一个超级排序s_n与每个排序s相关联，将排序s的每个属性表示为排序s_n的常数，并定义一个运算符op _=_：s* s* -> Prop.在MUTEX的情况下，mod MUTEX-OBSERVED是保护新木特克斯sort Bool*subsort Bool Bool*.op _=_：Bool* Bool* -> Prop.给定的属性解释I同态地扩展到任意项，如2.4节所解释的，我们可以假设，没有失去一般性，这个扩展可以通过一个算子族interp来等式定义。我们对MUTEX的著名解释I的同态扩张在等式上定义如下。op interp：Conf Bool* -> Bool.关键操作：配置名称->布尔值。var C：Conf.var B1 B2：Bool*.vars N M：Name.var R：同意。var O：Token.var A：Action。var S：Conf+.eq critical（none，N）= false。eq critical（ C，N）=true。eq critical（O C，N）= critical（C，N）。如果N =/= M，则ceqcritical（ C，N）=critical（C，N）。eqcritical（ C，N）=critical（C，N）。M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113125eq interp （ C ， crit-a ） = critical（C，a）。eq interp（C，crit-b）= critical（C，b）。eq interp（C，true）= true。eq interp（C，false）= false。eq interp（C，not B1）= not interp（C，B1）。eq interp（C，B1或B2）= interp（C，B1）或interp（C，B2）。eqinterp（C，B1 and B2）= interp（C，B1）andinterp（C，B2）.然后，原子VLRL公式的语义在LTL中通过以下方式定义：ceq（{C|R|一|{\fnMicrosoftYaHei\fs14\bord1\shad0\3aHCC\b0}|=B1=B2）=true如果interp（C，B1）=interp（C，B2）。ceq（{C|R|一|{\fnMicrosoftYaHei\fs14\bord1\shad0\3aHCC\b0}|如果interp（C，B1）=/= interp（C，B2），则= B1 = B2）=假。恩德姆有了这些定义，我们清楚地知道，对于Conf类的所有基项C和Bool*类的t和t'基项，C我|= VLRLt= t 't 't't {C|R|一|{\fnMicrosoftYaHei\fs14\bord1\shad0\3aHCC\b0}|= LTLt= t'下一步是将从原子到任意VLRL公式的转换扩展4.2定义LTLVLRL公式和LTL公式之间最重要的区别是，前者携带了关于必须应用的过渡的信息。正是出于这个原因，我们不得不对原始系统MUTEX进行改造，以便状态存储有关所采取的行动的信息。此外，现在我们定义了两个谓词来识别这些操作何时发生。occurred：taken top（α），当动作α发生在状态的顶部时为真，taken（α），当动作α应用于表示状态的项的某个子项时为真。op taken-top：Action -> Prop.采取的操作：操作->道具。var C：Conf.var R：同意。var A：Action。var S：Conf+.eq{C|R|一|{\fnMicrosoft YaHei\fs14\bord1\shad0\3aHCC\b0}|=taken（A）=true。ceq{C|R|一|{\fnMicrosoft YaHei\fs14\bord1\shad0\3aHCC\b0}|=taken-top（A）=trueiftop（S）.我们使用一个辅助操作来检查转换是否已经应用于状态之上。为此，只需检查是否标记了状态的所有进程和令牌。op top：Conf+-> Bool.eq top（C）= false。126M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113eq top（@ C @）=true。eq top（C +S）=false。等式top（@ C @ + S）= top（S）。由于动作可能与其他动作同时发生，我们需要一个状态谓词来表达这一事实。我们定义并发谓词如下：op concurrent：-> Prop.eq{C|R|一|{\fnMicrosoft YaHei\fs14\bord1\shad0\3aHCC\b0}|=concurrent=R==concur.通过查看规则step1和step2，可以清楚地看到并发满足以下条件：备注。形式的状态{C |R|一|当且仅当用于构造A的最后一个动作与前面的动作并发执行时，S }满足原子命题并发。现在我们准备好用LTL来表达通用的动作公式，为此我们将使用Next（）和Until（U）时态运算符。直觉上，如果在动作α完成后，结果状态充满了[α]，则[α]在给定的状态中成立。然后，对于非并发操作，所得到的LTL公式简单地为（取顶部（α）→但是，任意操作不能仅用Next操作符捕获，因为它只考虑单步重写;它们可以在LTL中表示，方法是在检查公式的操作是否已执行之前允许多个操作并发执行我们把它翻译成：同时（ConcurrentU（taken top（α））（（concurrentU同时）。第一部分指出，如果采取行动α，则α必须成立，而第二部分考虑α不发生的情况。[4][[α]]的翻译类似，但用taken代替taken top：并发（并发U（taken（α））（（concurrentU<$concurrently）势作用性质通过对偶性转化为普适性质. VLRL中的否定和蕴涵对应于LTL中的否定和4.如果系统中没有死锁（MUTEX就是这种情况），那么这种转换是正确的，因为不可能以无限的方式并发地应用操作，并且并发最终必须为真。在[9]中，证明了重写逻辑中的任何系统都可以通过无死锁理论来指定，所以这不是一个严格的限制。M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）1131275使用模型检查器为了使用Maude模型检查器证明VLRL公式在一个状态下的满足性，我们定义了下面的MUTEX-SAT模块，该模块从一个指定了taken和top的模块MUTEX-SAT中导入带有所有状态谓词的转换理论（见附录），并且我们在其中声明了模型检查器的初始状态。初始状态由两个正在等待的进程a和b以及一个令牌$组成。mod MUTEX-SAT正在保护MUTEX-SAT。包括模型制造商。op init：->NewConf.eq init={< b，wait> $|concur |**|< a，wait>+ +$}。恩德姆我们可以证明满足VLRL性质[[a-enter]]（crit-a=truecrit-b=true），说明在执行动作A-Enter之后，在临界区中存在一个进程。VLRL属性以LTL表示为：（concurrentUtaken（a-enter）同时发生的，同时发生的- 并发），并由模型检查器简化为：reducein mixk-MUTEX：modelCheck（init，O（concurrent U taken（a-enter）/\（crit-a = true\/crit-b = true））\/O（concurrent/\~ taken（a-enter）U ~ concurrent））.rewrites：250in0mscpu（0msreal）（~rewrites/second）result Bool：trueVLRL属性⟨⟨a-enter⟩⟩¬(crit-a=true∧crit-b=true)说明可以执行动作a-enter，并且在执行动作之后，在临界区中没有两个过程，用LTL表示，使用对偶，公式为<$（concurrentU（taken（a-enter）<$（crit-a=true<$crit-b= true）），可以通过reduce inRank-MUTEX：modelCheck（init， ~ O（concurrent U（crit-a =true/\crit-b=true）/\taken（a-enter）。rewrites：272in0ms cpu（0ms real）（~rewrites/second）result Bool：true请注意，按照变换态的第一个参数的重写顺序，很容易得到原始VLRL理论的反例。128M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113最后，财产[a-enter b-enter]false证明了进程A和进程B不能同时进入临界区，reduce inmixk-MUTEX：modelCheck（init， O（concurrent Utaken-top（a-enter b-enter）/\true =false）\/ O（concurrent/\ ~taken-top（a-enterb-输入）U-并发））。rewrites：249in0ms cpu（0ms real）（~rewrites/second）result Bool：true请注意，在这种情况下，操作是在状态的顶部完成的6结论在本文中，我们已经提出了一种技术来证明VLRL的行动性质使用Maude模型检查器;它可以被视为一个案例研究的一般理论的转换Meseguer [8]提出的研究重写逻辑的框架中的公平性。首先，我们将重写理论转化为一个新的理论，其中状态携带有关所使用的转换和它们发生的上下文的信息。然后，通过将VLRL公式转化为等价的LTL公式，在变换理论中研究了VLRL的性质。这个过程使我们能够第一次机械地检查VLRL中公式的有效性，并且它将使我们能够更深入地探索在系统的规范中使用VLRL逻辑的好处。我们还打算在未来探索的另一种选择是开发一种工具，直接处理VLRL，而无需中间翻译为LTL。使用模型检验来证明VLRL公式的主要问题是状态空间的大小，因为对单个转换的研究通常会产生许多不同的计算路径。这一事实反映在我们的转换理论中，例如，在对应于3.1节中解释的转换的三种可能的重写序列中。所提出的过程是通用的，在这个意义上，它可以适用于重写逻辑中指定的任何系统对于一个具有交换和关联结构的规范，如MUTEX示例中的规范，如果有任何变化，变化应该是微小的。对于任意理论来说，其基本思想是相同的，但结构更为复杂。特别是，我们已经能够使用一个单一的sortAction（与一个超级排序一起）来表示操作，因为系统中的规则仅涉及单一种类的术语，Conf。但如果如果规则适用于更多种类，则有必要为每一种种类规定一个预先动作的种类，并以相应的方式将签名中运算符的扩展M. 帕洛米诺岛Pita/Electronic Notes in Theoretical Computer Science 117（2005）113129我们现在正在研究任意理论转换的一般程序的形式化特别是，我们必须检查是否Meseguer此外，我们还致力于将空间VLRL公式转换为LTL公式，其中空间公式是这里考虑的公式的扩展，允许证明在状态的具体部分中发生的属性，特别是定义在