Maude中的μ-Calculus模型检测：重写理论与验证算法统一形式主义

理论计算机科学电子笔记117（2005）135-152www.elsevier.com/locate/entcsMaude中的μ-Calculus模型检测王宝耀中央研究院信息科学研究南港115，台北台湾摘要本文提出了一种检验μ-演算性质的重写理论。我们使用[11]中提出的相同框架，并演示如何将重写逻辑用作从模型指定到验证算法实现的统一形式主义。此外，由于μ-演算比LTL更具表达性，因此这项工作在理论上可以被视为[11]的扩展。我们还开发了一个CTL到µ-calculus的翻译器，以帮助用户更轻松地编写CTL规范。但是，缺少相应的LTL到µ-calculus转换器。[11]中的LTL模型检查器在实践中仍然是首选的。保留字：重写逻辑，模型检查，微演算。1介绍在过去的十年中，模型检测在硬件和软件设计行业中得到了广泛的应用给定一个正式的模型及其规范，模型检查的目标是确定模型是否在形式上符合规范以硬件验证为例。数字电路的形式模型可以是电路本身，它由组合元件和时序元件组成指定可以是其线路上的谓词（例如，读和写不能在任何时候都断言）。使用形式化的验证工具，验证工程师可以检查谓词是否普遍成立。*部分由国家科学委员会NSC 92-2213-E-001 - 023-支持。作者网址：www.iis.sinica。埃德。tw/~bywang1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.06.025136B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135从上面的场景中，我们可以看到模型验证的过程可以分为三个部分：• 模型的具体说明• 财产的具体说明;以及• 根据模型检查属性的机制。事实上，在[23]中进行了观察，作者建议使用Maude [5，18]作为模型检查的验证平台。Maude是一个基于重写逻辑的重写系统。自从重写逻辑在[16]中被引入以来，它一直被用作建模并发的统一形式主义[16，17，19]和逻辑框架[3]。由于重写逻辑的表达能力，来自不同研究社区的研究人员可以在一个单一的形式主义中工作。鉴于重写逻辑中形式主义的统一，问是否有可能在重写逻辑中执行模型验证的所有三个任务可能是一个有趣的挑战。这个挑战在[23]中得到了部分回答，其中验证了主动网络协议在[23]中，协议和属性在对象级别指定。作者使用一个元级理论，用于探索模型的所有可能行为，并根据属性对其进行检查。然而，结果是不令人满意的，因为只有不变的检查下所提出的框架进行了讨论。最近，在[11]中描述了线性时序逻辑（LTL）模型检查器。该模型在Maude中被指定为一个模块。属性指定语言由等式理论定义用户可以用重写理论指定模型，导入指定方程理论编写LTL公式，然后调用内置的模型检测算法来验证模型是否满足LTL公式。模型检测算法是用C++实现的。因此，我们认为，这项挑战尚未得到充分应对。在这项工作中，我们提出了一个新的想法来应对挑战。我们的解决方案使用重写理论来建模规范，如[11]所示而不是LTL，一个更有表现力的规格化逻辑，μ-演算，被使用。此外，我们能够在重写逻辑中构建模型检查器，而不是在C++中实现我们的μ-演算模型检查器。换句话说，我们已经成功地实现了重写逻辑中模型验证的所有三个任务。众所周知，μ-演算严格来说比CTL演算更有表现力。因此，本文的工作可以看作是文[11]结果的推广. 然而，在实践中，首选CTL或LTL公式，因为µ-演算公式有时很难理解。因此，我们提供了一个重写将任何给定的CTL公式转换为等价的μ-演算的理论，B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135137¬ ¬ ≡ ¬ ¬ ¬Qmula。不幸的是，我们仍然不知道如何翻译LTL公式。因此，在实践中仍然需要[11在重写逻辑中实现μ-演算模型检查器的关键是局部模型检查[20，6，22]。与传统的模型检查算法不同，在传统的模型检查算法中，所有满足该属性的状态都被计算出来，局部模型检查试图为初始状态找到一个证明由于证明树是按语法生成此外，状态仅在证明搜索期间必要时才被探索。因此，可以验证无限状态系统的属性，如果它们在不遍历有限数量的状态的情况下被证明。在这份报告中，我们简要回顾了[11]中提出的框架，并专注于为μ-演算局部模型检查器开发Maude理论。本文的结构如下。我们从第二节的“数据库”开始。Maude中模型检查的概述在第3节中给出。第4节介绍了用于µ-演算局部模型检验的Maude理论。第5节中给出了一个将CTL转化为μ-演算的简单理论。最后，我们讨论了一些未来的方向，并在第6节中总结。2初步一个µ-演算公式φ由以下规则生成• 命题变量：X，Y，Z，. . ;• 原子命题（AP）：p，q，r，... . ;• 布尔连接词：<$φ，φ;• 模态次态算符：Qφ;• 最大不动点算子：νX.φ，其中约束变量X为正。像往常一样，我们使用导出算子，如φ（<$$>（<$φ <$）），Qφ（φ）和μX.φ（νX.φ [X/X]）。 在[13]中，允许标记模态下一状态量化器。为了简单起见，这里我们只使用未标记的版本。请注意，该限制的表达能力足以包括CTL[7]。φ的语义定义在Kripke结构K=（S，→，s0，L）上，其中S是状态集，→S×S是转移关系，s0∈S是初始状态，L：S→2AP是将每个状态映射到原子命题子集的标记函数。为了清楚起见，我们写s→t每当（s，t）∈→。赋值ρ是将命题变量映射到S的子集的函数。 设R为S。 我们将赋值映射X记为ρ[X<$→R]，将赋值映射Y记为ρ（Y），对于X/<$Y。给定赋值ρ，语义函数[·]]ρ138B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135|∈∅|{}返回一组满足φ的状态，在赋值ρ下定义如下。• [[X]]ρ=ρ（X）;• [[p]]ρ={s∈S：p∈L（s）};• [[<$φ]]ρ=S\[[φ]]ρ;• [[φ]]ρ=[[φ]]ρ[[]]ρ;• [[Qφ]]ρ={s∈S：t∈S.s→tandt∈ [[φ]]ρ};• [[νX.φ]]ρ=<${R<$S：R<$[[φ]]（ρ[X<$→R]）}。给定一个μ-演算公式φ和一个Kripke结构K=（S，→，s0，L），当s 0[[ φ ]]时，我们记为K，s0=φ。换句话说，K，s0=φ意味着K的s0满足μ演算公式φ。微演算模型检验问题是检验K，s0|= φ。传统上，µ-演算模型检验问题通过计算满足给定µ-演算公式φ的所有状态Sφ并检查s0是否∈Sφ[10，2]来解决。 在这里，我们使用局部模型检查技术来解决问题. 局部模型检验不是计算Sφ，而是试图找到一个证明国家S0。这种证明理论方法在局部探索Kripke结构，更适合于重写逻辑等逻辑框架。局部模型检查器由一组证明规则组成[20，6，22，1]。 它试图根据这些证明规则搜索K，s<$φ的完整证明树。 在这项工作中，我们使用[22]中证明规则的简单扩展。为了提出这一规则，Winskeli引入了一个新的μ-culusformulavX{r<$}φ，其中，{r<$}好的。Itssemannticsisdefinedy：[[νX{r<$}φ]]ρ=<${R<$S：R<${r<$} <$[[φ]]（ρ[X<$→R]）}。注意，νX.φ等价于νX φ。以下证明规则可以在[22]中找到：• （K，s<$p）当p∈L（s）时为真;• （K，s<$p）当p/∈L（s）时为假• （K，s<$T）为真;• （K，s<$F）false;• （K，sφ）b如果（K，sb;• （K，s）b0且（K，sb1;• （K，s）b0或（K，sb1;• （K，s<$Qφ）<$真如果（K，t<$φ）<$真，对于某个t使得s→t;• （K，s<$νX{r<$}φ）-• （K，s<$νX{r<$}φ）<$（K，s<$φ[νX{s，r<$}φ/X]）.B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135139¬¬（fmodMU是排序变量属性公式。子排序变量<公式。子分类Prop<公式。* 原始运算符 * ops TrueFalse：-> Prop.op~_：公式->公式[prec 52]。op_/\_：公式公式->公式[Approc 55]。op_\/_ ： 公式公式->公式[函数prec 59]。op<>_： 公 式 -> 公 式 [prec53]。op' ' ] _ ： 公 式 - > 公 式 [p r e c5 3] 。奥普穆奥普努endfm）：变量公式->公式[prec 61]。：变量公式->公式[prec 61]。Fig. 1. Maude模块MU对任何ν-演算公式φ，证明了（K，s0为真当且仅当K，s| = φ [22]。因此，可以通过在Maude中将这些证明规则指定为方程来解决模型检查问题。但有有几个问题需要解决。为了提高效率，需要相应的μ-算子方程，以及在证明规则中模仿变量替换的机制虽然微演算非常有表现力，但有时很难解释，即使是专家。为了帮助用户编写规范，我们实现了从CTL到µ-calculus的转换。CTL公式α是从以下结构递归构建的[8，9]：• 原子命题：p，q，r;• 布尔连接词：<$α和α<$β;• 存在下一步算子：EXα;• 存在总是算子：EGα;• 存在直到算子：E（αUβ）。其他操作符可以从它们派生出来。例如，AXα（<$$> EX <$α）、EFα（<$E（trueUα））、AGα（<$$> EF <$α）和A（αUβ）（<$<$E（<$βU <$α<$$>β）<$EGβ）。CTL规范用于许多正式的验证工具，[14][15]和[16]。我们的翻译将允许熟悉这些系统的用户轻松采用Maude作为验证平台3Maude中的模型检测我们从μ-演算公式的方程理论开始（图1）。在模块MU中声明了三种类型：变量、属性和公式。μ-演算公式是一种公式。原子命题是一种Prop。最后，命题变量的排序是变量。布尔连接词的定义与往常一样。对于模态算子Q和Q，我们分别使用<>和[]。140B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135∧∨►（modMUTEX是保护药物-INT。排序模式进程令牌会议。子排序令牌进程<会议op：Conf Conf -> Conf[配置文件]。ops waitcritical：->模式。op'[_'，_']：MachineInt模式->处理op*：-> Token。vars m n. var C：Conf.crl [enter]：*[n，wait] [m，critical]=>如果n > 0，则[n - 1，等待] [m +1，临界]。crl[exit]：[n，critical][m，wait]=>* [n - 1，临界][m +1，等待]，如果n > 0。endm）图二. 模块MUTEX算子Mu和Nu分别表示最小和最大不动点算子。作为例子，μ-演算公式νY。Q（Y µZ.pQZ）写为Nu Y（<>（Y/\（Mu Z（p\/<> Z）。对于Kripke结构的具体化，我们遵循[11]中提出的基础结构，并在这里进行简要回顾Kripke结构K=（S，→，s0，L）被指定为重写理论R=（E，E，R）。 让我们成为平等的人。R中s项的lent类。则[s][t]是R的初始模型中的重写证明当且仅当s→t在K中。以图2中的MUTEX模块为例，它是[5]中的一个模块的简单扩展。 会议-类似于[n，critical]，[ m，wait]表示在modedewait中的m预处理。 任何处于等待模式的进程都可以获取令牌（“*”）并进入临界模式。 另一方面，任何处于临界模式的进程都可以通过释放令牌返回到等待模式。例如，配置 *[5，wait][2，critical]可以通过应用规则enter重写为 * *[4，wait][3，critical]。为了定义Kripke结构中的标记函数，我们引入了运算子|-在ENTAILMENT模块中：op |-_ : Environment Term Formula -> Bool [ prec 85 ].LetEbeavariableenvironment （ 稍 后 描 述 ） ， semeta-leveltres表 示states，而对于mula，φ表示我们想检验在环境E下s是否满足φ。注意，状态被表示为元级术语，而不是像[ 11 ]中那样的排序State的元素。由于需要状态的后继者来证明模态算子Q和Q，所以使用元级表示来计算所有后继者。B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135141►（fmod MUTEX-PREDS保护的是药物INT。保护你。保护实体。op crit：MachineInt -> Prop.操作等待：MachineInt ->Prop。op get-critical：TermList -> MachineInt.op get-wait：TermList -> MachineInt.var E：环境。varsn ： MachineInt. 变量T：术语。ceq E T|-crit（n）= true，如果get-critical（T）>= n。ceq E T|-crit（n）= false if get-critical（T）= n。ceq E T|-wait（n）= falseifget-wait（T） Module.op labels：-> QidList.endoscopy）为了实例化模块参数，我们首先定义一个元级模块1在Maude 2中不需要使用元级表示，因为函数MetaXapply可以用来计算后继。2.如果使用对象级表示，我们不需要在Meta级工作142B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135（fmod MUTEX-INT保护的是MUTINE-INT。保护Mutex-Preds保护本地模型[KripkeMUTEX]。操作初始化：->术语。eqinit = up（MUTEX，*[100000，wait][0，critical]）。ops X Y：->变量。ops prop prop0 prop1 prop2 prop3 prop4：-> Bool.eq prop0 = {}init|-Nu X ~（<> ~ X\/（crit（6）。eq prop1 = {}init|-Mu X（<> X\/（crit（6）））。eq prop2 = {}init|-Nu X（[] X/\crit（5））。eq prop3 = {}init|-Nu X（<>True/\[] X）。endfm）图四、Maude模块MUTEX-STUDIOMETA-MUTEX如下。（mod META-MUTEX是保护META-MODERN。OPKRIPKE：-> Module. eqKRIPKE = up（MUTEX）。op labels：-> QidList.eq labels =（'enter 'exit）.endm）然后，我们定义了KripkeMUTEX视图，将KMOTEX映射到META-MUTEX如下（查看KripkeMUTEX从KMONIKO到META-MUTEX是OP KRIPKE到KRIPKE。标签标签标签endv）对于我们的示例性Kripke结构，最初有100，000个进程处于等待模式。 prop1指定在某个计算路径上，最终是否会有超过5个进程处于临界模式。prop0是它的否定。prop2询问最终是否有超过4个进程等待所有计算路径。最有趣的一个是prop3，它指定模型是无死锁的。我们可以通过减少蕴涵来检查prop 0Maude>（red prop0.）重写：5457在480毫秒CPU（510毫秒实）（11368重写/秒）减少在CPU：prop 0。结果Bool：true在本节中，我们将回顾Maudeµ-calculus模型检查器的接口。这与[11]中提出的方法不同因此，Maude的表达能力可以用来模拟复杂的系统，如[11]。与[11]中的黑盒实现相比，我们的模型检查算法是通过重写逻辑来规范的。因此，任何有经验的Maude用户都可以进一步改进该算法，而无需求助于低级C++程序。B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135143--（fmodENVIRONMENT[K：： KMOORY]是保护元级。保护你。保护实体。sort TermSet定义。子排序术语 TermSet。op _U_：TermSet TermSet -> TermSet [aslogid：emptyTermSet]. op_isIn_：Term TermSet -> Bool。ceq TU Tifmeta-reduce（KRIPKE，'_==_[T，T']）==' true}'Bool.等式T isInemptyTermSet=false。ceqTisIn（Tifmeta-reduce（KRIPKE，'_==_[T，T']）==' true}'Bool. ceqTisIn（Tifmeta-reduce（KRIPKE，'_=/=_[T，T']）==“true}"Bool.* 定义op_：= ：Variable Bool TermSet Formula -> Definition [prec 81].* 环境op''}：->环境。op_&_：Environment Environment->Environment [ctor aslogid：{} prec83].endfm）图五. ModuleENVIRONMENT [K：： KMONOW]明.在下面的部分中，我们将详细讨论该实现。4用于μ-演算模型检验的让我们从参数化模块ENVIRONMENT中定义的排序Environment开始（图5）。环境由一系列定义组成每个定义依次包含一个变量、一个布尔值、一组状态（代表由元级术语表示）和公式。为了理解为什么定义是这样定义的，回想一下最大不动点算子的证明规则• （K，s<$νX{r<$}φ）n-树如果s∈{r<$};且d• （K，s<$νX{r<$}φ）<$（K，s<$φ[νX{s，r<$}φ/X]）否则。当遇到mulavX{r<$}φ时，该规则规定了状态是否长到与前mula相关联的状态{ r <$}。 如果是这样，我们就在一起了。另一方面，φ随它的增加而展开。我现在才知道来看看为什么我们定义定义如图5所示。 变量和公式用于替换。布尔值用于区分最大值和144B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135∨最小不动点算子元级术语集用来模拟对象级的集合操作（如元素添加和成员关系）。严格地说，我们对环境的定义并不是最普遍的。它不能用于检查具有多次出现的命题变量的微演算公式考虑公式νZ.ZQQZ。由于环境不区分变量Z的不同出现，我们的模型检查器将产生不正确的结果。这个问题可以通过为命题变量的每次出现保持一个环境来解决。为了简单起见，我们不考虑这样的公式。请注意，状态由元级项表示。 上述集合操作需要在Meta级别执行。此外，Kripke结构的基本方程理论应该被应用。 出于这个原因，我们让模块ENVIRONMENT由Kripke结构参数化，并使用相关集合运算符中的meta-reduce现在我们可以提出证明规则的等式理论对于布尔连接，可以直接写出相应的方程。例如，合取规则的等式是：方程式E s|-f/\g = if（E s|-f）则（E s|-g）否则为假fi。对于每一个µ-演算算子，我们都有一个对应于它的负形式的方程。 这给了我们一个更直接的完全微演算终止的证明[20]。该负方程与其逻辑等价公式具有相同的形式。相应的合取方程为：方程式Es|-~（f/g）=如果（E s|-~ f）then true else（E s|-~ g）fi。对于模态next运算符，请回忆（K，s <$Qφ）为真，如果（K，t <$φ）对某个t为真，使得s →t。这样，E s的所有后继t上的Etφ的结点就减少到D。在这里，我们使用元层次理论来寻找状态s的所有继承者。这解释了为什么我们在定义中使用元级表示。 在图6中，我们展示了[21]中的元级函数allRew的修改版本，以计算给定项的后继项。 有兴趣的读者可以参考[21]了解详情。3有了后继函数，很容易定义下一个模态算子的方程：方程式E s|-<> f = OR（s，E，f，0）。哪里等式OR（s，E，f，n） =if（successor（s，labels，n））==error* thenfalse else if（E（successor（s，labels，n））|（1）true3在Maude 2中，我们可以简单地调用MetaXapply并获得相应的表达式。因此，没有必要使用元层次理论。B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135145(fmod SUCCESSOR [K：： KMONOW]是保护QID-LIST。保护药物-INT。* 变量声明在这里op ~：->TermList。op successor：Term QidList MachineInt -> Term.op lowerRew：Term Qid MachineInt -> Term.oprewArgs：Qid TermList TermList Qid MachineInt->Term. op rebuild：Qid TermList Term TermList -> Term.opmeta-apply '：Term QidMachineInt -> Term. opget-t：ResultPair -> Term。eq successor（T，nil，n）=error*. eq successor（T，LLS，n）=如果meta-applythen successor（T，LS，n）else lowerRew（T，L，n）Fielsemeta-apply '（KRIPKE，T，n）fi.eq get-t（{T，SB}）= T.eq meta_applyget-t（meta-apply（KRIPKE，T，L，none，n））.eq lowerRew（{C}S，L，n）= error*.eqlowerRew（OP[TL]，L，n）= rewArgs（OP，~，TL，L，n）。eq rewArgs（OP，Now，T，L，n）=如果后继者（T，L，n）==error* 则error*else rebuild（OP，Now，successor（T，L，n），~）fi.eq rewArgs（OP，Now，（T，After），L，n）=ifsuccessor（T，L，n）==error*then rewArgs（OP，（Now，T），After，L，n）else rebuild（OP，Now，successor（T，L，n），After）fi.eq rebuild（OP，Now，T，After）=Meta-reduce（KRIPKE，OP[Now，T，After]）。endfm）见图6。ModuleSUCCESSOR [K：： KMOOKER]else OR（s，E，f，n +1）fi fi.对于形式为νX.φ的最大不动点公式，定义X：=tres<$φ被添加到第一次提出的最大不动点公式中。因此，蕴涵Es|-NuX f重写为E&（X：=true s f）s|-f其中X：=true s f记录函数f的定义，最大不动点运算符的布尔值true，以及访问状态s。等式{} s|-Nu X f =（X：= true sf）s|-f.ceq E&（Y：= b S g）s|-Nu X f =E&（Y：= bSg）&（X：= true sf）s|-f，如果X =/= Y。146B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135⇔ ¬ ¬ ¬另一方面，如果公式νX.φ已经被添加到环境中，我们需要确定是否应该展开该公式如[22]，有两种情况。如果同一个状态再次遇到该公式，它将重写为true。否则，状态存储在定义中，公式展开。ceq E&（X：= trueSf）s|-X =true如果s在S中。ceq E&（X：= trueSf）s|-X =E&（X：= true（s U S）f）s|-f if not（s isIn S）.函数isIn检查元级术语s是否属于元级术语的集合S。因此，如果s已被访问，则第一个方程归为真。通过将s添加到集合中，表达式sU S的S. 第二个等式记录当前状态，如果它还没有被访问过。对于具有最小不动点算子的公式，我们可以通过应用对数等价μX.φ νX将它们重写为仅具有最大不动点算子的等价公式。 φ [X/X]递归地。 在这里，我们想采取一种更直接的方法。观察K，s<$$> vX{r<$}<$φ[<$X/X]惠K，s<$$>（<$φ[<$X/X][vX{s，r<$}<$φ[<$X/X]/X]）惠K，s<$φ[<$νX{s，r<$}<$φ[<$X/X]/X]因此，我们可以将μX{r<$}φ定义为e<$vX{r<$}<$φ[<$X/X]，并在K，s<$µX{r<$}φ惠K，s<$$> νX{r<$}<$φ[<$X/X]惠K，s<$φ[<$νX{s，r<$}<$φ[<$X/X]/X]惠K，s<$φ[µX{s，r<$}/X]对于终止条件，考虑K，s<$µX{s}φ。我们有K，s<$µX{s}φ惠K，s<$$> v X{s}<$φ[<$X/X]不优惠（K，s<$v X{s}<$φ[<$X/X]）惠假因此，最小不动点公式的方程为等式{} s|-Mu X f=（X：= false sf）s|-f.ceq（E&（Y：= bSg））s|-MuXf=E&（Y：=b Sg）&（X：= false sf）s|-f，如果X =/= Y。ceq E&（X：= falseSf）s|-X =falseifs is InS. ceqE&（X：= falseSf）s|-X =E&（X：= false（s U S）f）s|-f if not（s isIn S）.前两个方程将最小固定点定义添加到环境中。如果没有遇到状态，第四个方程记录它并展开命题变量。除了定义之外，它们与最大不动点的方程相同。然而，如果状态已经被访问过，则第三个等式归为假B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135147(fmod LOCAL-MODEL-[K：： KMODEL]是保护元级。保护你。保护实体。保护环境[K]. 保护成功者[K].* 变量声明ops OR AND：Term Environment Formula MachineInt -> Bool.方程式E s|-真=真。方程式E s|-假=假。方程式E s|-~ prop = not（E s|-prop）。方程式E s|-~~ f = E s|-f.方程式E s|-f/\g = if（E s|-f）则（E s|-g）否则为假fi。方程式E s|-f1/g = if（E s|-f）then true else（E s|-g）fi。方程式E s|-<> f = OR（s，E，f，0）。等式OR（s，E，f，n） =if（successor（s，labels，n））==error* thenfalse else if（E（successor（s，labels，n））|-f）then true elseOR（s，E，f，n +1）fi fi.方程式E s|-[] f = AND（s，E，f，0）. 等式AND（s，E，f，n） =if（successor（s，labels，n））==error*then true else if（E（successor（s，labels，n））|f）然后AND（s，E，f，n +1）否则就是假的。等式{} s|-Mu X f=（X：= false sf）s|-f.ceq（E&（Y：= bSg））s|-MuXf=E&（Y：=b Sg）&（X：= false sf）s|-f，如果X =/= Y。等式{} s|-Nu X f =（X：= true sf）s|-f.ceq E&（Y：= b S g）s|-Nu X f =E&（Y：= bSg）&（X：= true sf）s|-f，如果X =/= Y。ceq E&（X：=b Sf）s|-X = b，如果s在S中。ceq E&（X：=b Sf）s|-X =E&（X：= b（s U S）f）s|-f ifnot（s isIn S）.* 否定的方程被省略endfm）见图7。Maude模块LOCAL-MODEL-BRANKER [K：： KMOKER]值得注意的是，所有固定点证明规则都有其语义基础[22，1]。从语义上看，我们的方程与文献[20，6，22，1]中的方程基本相同。我们可以通过引入布尔变量来减少方程的数量。例如，最大和最小固定点公式的终止方程可以简化为以下方程：ceq E&（X：=b Sf）s|-X = b，如果s在S中。类似地，我们可以将两个展开方程合并为一个。 我们的µ-calculus局部模型检查器的完整理论如图7所示。148B.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135∧（fmodCTL保护MU。对CTL公式进行排序。subsort Prop< CTLFormula.* 原始运算符 *OP！_： CTLFormula->CTLFormula[prec53] 。 操 作 _&&||_ ： CTLFormulaCTLFormula ->CTLFormula[第55页]。操 作 EX_： CTLFormula -> CTLFormula [prec 53]。操 作 EG_： CTLFormula -> CTLFormula [prec 63]。操作E_U_：CTL公式CTL公式-> CTL公式[prec 63].* 派生运算符 *操作AX_： CTLFormula->CTLFormula[prec53]。ops EF_AF_ AG_：CTLFormula -> CTLFormula [prec63]。操作A_U_：CTL公式CTL公式-> CTL公式[prec 63].* 导出的方程被省略endfm）见图8。 Maude模块CTL我们提出了一个重写理论模型检查μ演算公式。与[11]相比，我们的模型检查器是在重写逻辑中实现的。读者可以通过修改Maude模块LOCAL-MODEL-STANDARD来检查和改进模型检测算法。元级Maude理论可以改进例如，conjunc-已 对 方 程 和 析 取 方 程 进 行 了 修 改 ， 以 便 在 LOCAL-MODEL-DESCRIPTION中使用快捷评估。这些是[11]中黑盒方法所缺少的理想功能5模型检查CTL公式然而，在微演算模型检查中存在一个可接受性问题。在未经训练的人看来，微微积分公式确实很《双城之战》。以死锁自由的具体化为例。微微积分公式νX。Q真QX比相应的CTL公式AGEXtrue更不明显。 如果公式包含相互固定的点，这将更难解释。幸运的是，将任何CTL公式转换为相应的μ-演算公式是很容易的。在本节中，我们将介绍一个Maude方程理论来帮助用户编写CTL规范。如第2节所述，CTL中只有三个原始时间操作符：EX、EG和EU。导出算子AX、EF、AG、AF和AU的定义与通常一样（图8）。由于布尔连接词可以平凡地映射，所以将原始时间算子转换为它们相应的μ-演算公式仍然是一个问题。因此，我们定义了原始时间操作上的平移函数τB.- Y. Wang/Electronic Notes in Theoretical Computer Science 117（2005）135149||作者：• inti =true;• τ（p，c）=p;• τ（<$α，c）=<$τ（α，c）;• τ（α<$β，c）=τ（α，c）<$τ（β，c+θ（α））;• τ（EXα，c）=Qτ（α，c）;• τ（E（αUβ），c）=μXc.τ（β，c+1）<$（τ（α，c+θ（β）+1）<$QXc）;• τ（EGα，c）=νXc.τ（α，c+1）<$QXc.其中θ（α）计算α中所需的不动点运算的数量：• return 0;• n= 0;• θ（<$f）=θ（f）• θ（f<$g）=θ（f）+θ（g）;• θ（EXf）=θ（f）;• θ（EGf）=θ（f）+1;• θ（EfUg）=θ（f）+θ（g）+1;在我们的翻译中，我们增加索引c来创建一个新的命题变量。函数τ（α，c）返回一个等价的µ-演算公式，该公式使用以索引c开始的命题变量。例如，让我们计算τ（AGEXtrue，0）：τ（AGEXtrue，0）=τ（<$EF <$（EXtrue），0）=τ（<$E（trueU（<$（EXtrue），0）=<$τ（E（trueU（<$（EXtrue），0）=<$（µX0.τ（<$（EXtrue），1）<$（true<$QX0））=<$（µX0. <$τ（EXtrue，1）<$QX0）=<$（µX0. <$（Qtrue）<$QX0）。注意，<$（µX0. <$（Qtrue）<$QX0）等价于νX0。Q真QX0如所期望的。设K=（S，→，s0，L）是Kripke结构，α是CTL公式，很容易证明K，s0=α当且仅当K，s0=τ（α，0）.我们基于翻译函数τ定义了模块CTL2MU