理论计算机科学电子笔记238（2009）139-154www.elsevier.com/locate/entcs减少重写理论Lars Helge Hairs1和Thomas Noll2软件建模与验证组亚琛工业大学52056德国摘要状态空间的组合爆炸是应用模型检测方法的最大问题并发系统。在本文中，我们提出了一种新的状态空间约简技术，该技术适用于重写逻辑中的系统规范，重写逻辑是一种基于条件项重写模方程理论的统一并发语义框架。其思想是在方程中隐藏通过显式转换来改变状态（例如通信操作）。 我们展示了这种优化可以通过转换重写逻辑规范来实现，避免构建完整的状态空间。 此外，我们建立我们的技术的正确性证明，原来的和简化系统是弱双相似的，并通过将其应用于并发函数式程序设计语言Erlang来证明其可用性.关键词：状态空间约简，方程抽象，弱双相似1引言在本文中，我们将讨论软件验证的问题，集中在验证过程的第一部分，即要检查的（transition-system）模型的构建。这项工作是在J.Meseguer在[9]和[10]中介绍的重写逻辑框架的背景下进行的，该框架已被证明是许多具体规范和编程语言的适当建模形式主义[8]。在这种方法中，系统的状态由以给定方程组为模的项的等价类表示，并且转换对应于重写代表的操作。因此重写逻辑支持编程形式主义的定义，并通过使用（等式）项重写方法，执行或模拟具体系统。1电子邮件：hass@cs.rwth-aachen.de2电子邮件：noll@cs.rwth-aachen.de1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.05.017140L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139\在这里，我们将使用方程来定义抽象映射，这些映射减少了系统的状态空间。更具体地说，这个想法是把某些transi- 将代表系统行为的“不重要”细节的问题转化为方程。因此，这些转换被“隐藏”在当前状态中，通常减少了状态的数量，这反过来又使大型并发系统变得形式上可验证。从技术上讲，给定重写逻辑规范的修改是通过选择一个特殊的动作标签τ来实现的，该动作是无声的或不可观察的动作（通常用于CCS [12]等演算中，用于表示内部操作），用于区分系统的内部计算和那些应该由显式转换表示的计算。我们将说明在哪些限制条件下，可以通过将τ-跃迁转化为方程，使所得的跃迁系统等价于原始的跃迁系统，来修改给定的重写逻辑规范。这里等价性必须被解释为弱互模拟，这意味着原始系统的每一步都可以被简化系统的相应动作模拟，反之亦然，其中τ-跃迁被忽略。这种等价的结果是，我们的抽象是健全的和完整的具体形式主义，不能区分弱双相似系统. 具有此属性的时态逻辑的示例是CTL\X和CTL\X其中下标X\X操作员（详见[3]）。在这里，对于这样一个逻辑的每个公式，该性质在抽象系统中成立，当且仅当它能在原始系统中得到保证。因此，模型检测的效率可以通过考虑抽象而不是原始系统来提高。我们工作的一个重要方面是，抽象转换不是在实际的变迁系统本身上进行的，而是在其“紧凑描述”上进行的， 重写逻辑规范。这与需要完整原始系统的设置非常不同，例如通过删除ε-转换将非确定性有限自动机转换为确定性有限自动机，并且通常降低了峰值内存需求。本文的其余部分组织如下。第2节介绍重写逻辑框架，然后在第3节中使用该框架来形式化Erlang编程语言的操作语义。在第4节中，我们介绍了我们的抽象技术，在第5节中演示了它在Erlang中的应用，并在第6节中证明了它的正确性。最后，第7节以一些评论结束。2重写逻辑方法本节介绍我们的建模形式主义，重写逻辑，它是基于条件项重写模方程理论。为了支持重写理论的有效实现，我们将提出[10]中原始定义的一个变体，该变体已在[6，7]中得到发展L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139141∪ΣΣα1ΣΣΣΣΣΣ标签的有限集合，和R。TP（X）×L ×TP（X）+是（条件）的有限集α2.1标签重写理论的我们的目标是对由（动态创建的）顺序进程组成的并发系统进行建模。因此，我们区分表示单个进程的术语和表示并发进程系统的术语定义2.1设f是一个签名，X=X P X S是一组（过程和系统）变量。在X上的过程项的集合，用T P（X）表示，归纳地定义为X P<$T P（X），并且f（t1，...，t n）∈ T P（X），当t1，.，t n∈ T P（X）且f∈N（n）. 设λ∈/λmore是一个二元函数系统。所述一组系统X上的项，记为TS（X），归纳定义为XS<$TP（X）<$TS（X），Σ Σ Σ当t1，t2∈ TS（X）时，t1<$t2∈ TS（X）.在这些描述之后，我们可以引入标记重写理论的语法作为我们的建模形式。定义2.2标记重写理论（LRT）是一个四元组T =（E，E，L，R）其中，f是签名，ETP×TP是（过程）方程的有限集合，L是Σ转换规则，每个表示为C→dΣ... Cαkd1 1k→kl→αr因此，转移规则表示由项l表示的（子）系统如何能够演化到r，只要组成过程ci具有各自的后继状态di，对于每个1≤i≤k。2.2标签重写理论归约系统是一种抽象的数学模型，我们用它来表示任意系统的计算。我们感兴趣的是特定的还原系统，其中某些标签附在还原物上，以指示还原物的类型。还原，并且其中元素被区分为初始状态。定义2.3标记跃迁系统（LTS）是四元组（S，s0，L，→），其中S是一组被称为状态的对象，s0∈S是初始状态，L是一组有限的标签，所以=α∈L→ 是一个跃迁关系，对每个α ∈ L，都有S ×S。这里我们假设标签集L包含一个可区分元素τ。此标签指示没有侧效应的局部评估步骤，即，不“本质上”修改当前状态的转变从现在起，我们将使用符号a来表示（可能）涉及侧效应的跃迁，即a∈L\{τ}。基于这个定义，我们现在可以用标记迁移系统给出标记重写理论的（操作）语义。它形式化了一种理解，即当前状态由项s（或其某些E-等价物）表示的并发系统可以进化到状态t，只要存在142L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139α0α1→ΣnΣΣΣΣΣαiΣα∈L，n∈N一个转换规则，其左手边匹配s模E的子项，并且其条件被满足。这个直观的概念可以正式描述如下。定义2.4标记重写理论T的转移关系，→T = →T <$TS（X）/E×L ×TS（X）/E，通过y→αT：=α，αc→d... Cαkd→Tn+1 ：= {（[s] E，α，[t]E）|∃11k→kl→αr∈R，w ∈Pos（s），σ∈Sub使得s|w= Elσ，t= Es[w ← rσ]，这里且[ci σ] ETn[di σ] E，对于每一个1≤i≤ k}。• T S（X）/E：= {[t]E|t∈T S（X）}是T S（X）对t的商。 E，• [t]E：= {s∈T S（X）|s=Et}表示t的E-等价类，• Pos（s）是s的位置的集合，• S |w表示s在位置w ∈Pos（s）处的子项，• s [w ← t]是从s通过替换s获得的|w乘t，以及• 子：= {σ|σ：X→T S（X）}是置换的集合。此外，n被称为相应过渡的深度。注意，由LRT导出的转移关系作用于系统项，并且在替换和上下文下是封闭2.3弱互模拟我们的最终目标是减少由给定重写理论引起的过渡系统的大小。为了保证抽象的正确性，约简系统在某种意义上必须等价于原系统。这里我们要求两个系统都是弱双相似的，这意味着原始系统的每一步都可以通过约化系统的相应动作来模拟，反之亦然，其中τ-跃迁被忽略。定义2.5设（S，s0，L，→）是LTS且s，t∈S. 如果s→τt，我们写sεt，也就是说，如果有一个（可能是空的）从s开始的τ标记的跃迁序列，随时为我们提供帮助更进一步，对于eacha∈L，如果存在SJ，TJ∈S，则记为s∈αt，s <$εsJ→αtJ <$εt。 F或ea chla belα ∈L，当α=τ时，α∈L表示ε，而对于α否则。在两个LTSA =（S1，s1，L1→1）和B=（S2，s2，L1→2）的状态集上的二元关系R <$S1×S2是弱互模拟，如果当sRt和α∈L时，• 如果s→α1SJ，则存在tJ∈S2，使得t<$α<$2tJ和SJRtJ，且• 如果t→α2TJ，则存在SJ∈S1，such，使得s<$α<$1SJ和SJRtj.L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139143→→||||||--|||||两个状态s，t ∈ S是弱双相似的，记为s ∈ t，如果存在弱互模拟R使得sR t。初始状态分别为s1和s2的LTSA和B是弱双相似的，如果s1≠s2。我们注意到弱双相似性是一个等价关系[12]。3Erlang编程语言在本节中，我们将介绍前一个框架在Erlang编程语言中的应用，Erlang主要用于电信应用。3.1Erlang编程语言Erlang/OTP是一个提供开放分布式系统编程功能的编程平台：支持并发的Erlang语言，以及提供即用组件和服务的OTP（开放电信平台）中间件，例如，分布式数据库管理器，支持“热代码替换”，以及使用组件的设计指南。完整的描述见[1]。下 面 我们 考 虑 Erlang 编 程 语言 的 一 个核 心 片 段 ，它 支 持 在诸 如 原 子常 数（atoms）、整数、列表、元组和进程标识符（pid）等数据类型上运行的进程的动态网络的实现，通过称为邮箱的无界有序消息队列使用异步、按值调用通信。真正的Erlang有几个额外的功能，如模块，进程分布（到节点上），支持健壮编程和与非Erlang代码的互操作，例如， C或者Java。除了Erlang表达式e之外，我们还使用匹配子句cs、模式p和值v的语法类别进行操作。 Erlang表达式的抽象语法摘要如下：e：：= e1，e2e（e1，.，e n）CS结束的情况E p=e e1！e2接收CS结束OP（E1，...，e n）spawn（e1，e2）self（）X cs：：= p1e1;. ; p ne np：：= op（p1，.，p n） Xv：：= op（v1，.， v n）这里X的范围是Erlang变量，op的范围是一组原始常量和操作，包括元组e1，e2，列表前缀[e1e2]，空列表[]，整数，pid常量和原子。Erlang的函数式子语言相当标准：原子、整数、列表和元组都是值构造器; e1，e2表示顺序组合;函数调用用e（e1，...，e n）。csend的casee形式的表达式涉及匹配：e计算的值按顺序与模式pi匹配。如果成功，则继续执行ei，其中由pi绑定的变量相应地被实例化，否则引发运行时错误。对于赋值p=e也是如此，如果144L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139--关于我们---模块 柜启动（）->-export （[start/0]）。spawn =spawn（locker，[]），spawn（client，[]），spawn（client，[]）.locker（）->receiveclient（接收客户端）->request，Client->客户端！request，self（），客户！ok，接收接收ok->release，Client->% critical sectionlocker（）错误！release，self（），终端客户端端端Fig. 1. Erlang中的资源调用e的值与p不匹配，否则返回该值。涉及非功能行为的结构（即， （1）E1！e2表示输出操作，异步地将e2的值发送到由e1标识的进程，而接收csend检查本地进程的邮箱q，并检索（并删除）q中与cs中的任何模式匹配的第一个元素。 一旦找到这样一个元素v，则类似地继续进行评估 到CS的情况V结束;否则，该过程等待相应的消息到达。表达式spawn（e1，e2）动态地创建一个新进程，其中e1给出的函数被应用于列表e2给出的参数（并返回新进程的PID），self（）返回本地进程的PID作为一个介绍性的例子，我们考虑一个简短的Erlang程序，它实现了一个简单的资源锁，即，仲裁器，其在接收到来自客户端进程的对应请求时，准许对单个资源的访问。它在图1中给出。在[2]中给出了该算法的一个扩展版本任何Erlang程序都由一组模块组成。每个模块基本上都包含一个函数声明列表。在我们的例子中，系统被定义在一个模块中。它是使用start函数初始化的，根据导出声明，是唯一可以从储物柜模块外部访问的功能。通过调用spawn函数，它生成了三个新进程：一个locker和两个client。locker进程在非终止循环中运行locker函数。它使用receive构造来检查请求消息是否已经到达。 后者应该是一对由请求标记和客户端进程标识符（由变量Client匹配）组成的标记。然后，通过发送一个ok消息，客户端被授予访问资源的权限。最后，在接收到来自相应客户端的释放消息之后，锁柜返回到其初始状态。客户端进程展示了互补行为。通过发出请求，它要求访问资源。在这里，self内置函数返回客户端进程的进程标识符，然后由locker进程用作客户端的句柄。在收到ok消息后，它访问资源，并释放L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139145∪αα它之后。3.2Erlang的一种形式语义在本节中，我们将概述Erlang的形式语义。详情见[5，14]。Erlang运行时系统维护一组用户进程。任何这样的进程都由三个部分组成：一个必须被计算的Erlang表达式，一个唯一标识各个进程的进程标识符，它由系统内部确定，以及一个用于传入消息的邮箱，基本上是Erlang值的列表。此外，我们将把当前的评估环境归因于一个进程，该进程存储Erlang变量和分配给它们的值如前所述，我们将对规则中出现的重写逻辑变量使用某些标准表示，可能以索引或启动形式。 我们让e表示一个Erlang表达式，p一个模式，X一个Erlang变量，a一个原子，v一个值，f一个函数名，c一个子句。 此外，α表示一个转换标签，cs表示一个子句列表，i、j、k表示pids，q表示邮箱，ρ表示环境，s表示并发进程系统。因此，一个单一的过程是由一个术语的形式，|我|Q|ρ ρ3.2.1等式理论下一步是定义重写理论的方程组E。 我们只声明并行运算符是结合和交换的：E：={s1（s2s3）=（s1 s2）s3，s1s2= s2 s1}。3.2.2转变规则我们定义中最重要的部分是通过条件转移规则来形式化Erlang过程系统的操作行为。为了获得更清晰的结构，我们将R分解为两个不相交的子集：R：=RP RS。在这里，RP包含所谓的进程级规则，这些规则对单个进程进行操作，而RS，系统级规则的集合，处理并发进程系统。在下文中，我们从这两个类别中提出一些例子，再次参考[14]以获得完整的定义。流程级规则第一条规则描述了列表的递归求值。由于Erlang的最左-最内求值策略，我们必须从列表构造函数中的第一个表达式(list第一章第1章|我|Q|ρ ε → ε eJ1|我|QJ|pj[e1|e2]|我|Q|ρ→[e1J|e2]|我|QJ|pj146L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139αααατααττe|我|Q| ρ s → e| 我|Q| 帕里什一旦列表构造函数的第一个子表达式是不可约的（即，值），则求值继续进行第二子表达式：埃莱|我|Q|ρ ε → ε eJ|我|QJ|pj(list（二）[v]|e]|我|Q|ρ → [v|eJ]|我|QJ|pj接下来的规则将形式化排序构造的行为。求值从第一个子表达式开始，然后进行到第二个，忽略第一个的结果(seq第一章第1章|我|Q|ρ ε → ε eJ1|我|QJ|pj第1、第2页|我|Q|ρ ε → ε eJ1，e2|我|QJ|pj（seq2）波夫e|我|Q|ρ ε → ε ε e|我|Q|ρ ⟩以下规则处理模式匹配操作。在这里我们只是形式化的情况下建设。埃莱|我|Q|ρ ε → ε eJ|我|QJ|pj(case第一章 第e种情况，CS端|我|Q| cs端的ρ ε → ε情况eJ|我|QJ|pjmatch（v，cs，ρ）→τ（e，ρJ）(case（二）第五种情况关于CSEnd|我|Q|ρ ε → ε ε e|我|Q| ρJ ⟩这里match（v，cs，ρ）测试cs中的一个子句是否匹配值v， 如果成功，则返回实例化的右侧表达式和修改后的环境。接下来，我们考虑Erlang内置函数之一，它在语义的系统级别（产卵）产卵（a，v）|我|Q|ρ ⟩spawn（a，v，j）−→ j|我|Q|ρ ⟩这里j表示一个新的pid，它唯一标识新进程，并作为spawn调用的结果返回。 这可以通过引入系统状态中的最后，下面的规则处理Erlang的核心概念之一：异步发送消息。正如我们将看到的，消息将被附加到目标进程的邮箱中。请注意，进程也可以向自身发送消息系统级规则（发送）阿吉！v|我|Q|ρ ⟩msg（j，v）−→ v|我|Q|ρ⟩第一条规则只是表示，如果并发系统中的单个进程执行计算步骤，那么整个系统也执行计算埃莱|我|Q|ρ ε → ε eJ|我|QJ|pj（沉默）⟨τJ J J流程生成的形式化如下。从rule（spawn）可以看出，spawn内置函数带有两个参数：一个函数原子和一个列表L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139147JττTTΣΣ一111⟩−→ ⟨111111的论点。新进程将使用这些参数调用此函数，从空邮箱和空环境开始。（Spawn）埃莱|我|Q|ρ ⟩spawn（a，v，j）−→ e|我|Q|ρ⟩埃莱|我|Q |ρs → eJ|我|Q|（v）在任何情况下，|J |ε |ε ⟩接下来，我们指定如何将消息存储在接收进程的邮箱埃莱|我|Q|ρmsg（j，v）eJ|我|QJ|pj第1章|我|年q1|ρ1β2|J |Q2|ρ2s → eJ|我|QJ|日本语简体中文|J |q2·v |ρ2ε s需要更多的规则来完成重写理论的定义 对于Erlang。与初始表达式e0一起，它导出LTS（S，s0，L，→），其中s0是由s0=[ε e0]给出的初始状态|我0|ε|对于某个初始pid i0。4方程式抽象在下文中，我们描述如何使用等式抽象来减少转换系统的状态空间。这个想法是 一个例子是Erlang规范中的规则（seq2）在上一节中，它只是在序列中的第一个表达式被评估为正常形式时立即丢弃它。 另一个例子是调用通过用函数的函数体替换调用当然，也可以将这种抽象应用于原始的变迁系统，类似于通过去除ε-变迁将非确定性有限自动机转换为确定性有限自动机。 然而，这意味着我们必须计算 完整的LTS之前，这意味着峰值内存需求没有得到改善。在这里，我们遵循另一种方法，即修改重写逻辑规范，从而可以直接计算简化的LTS。 从技术上讲，这将通过将无条件τ-规则从转移规则集移动到方程理论来实现。这个简单的想法产生了以下特别的定义。让=（E，E，R，L）是LRT。改良的LRTJ=（Ej，EJ，RJ，L）通过将规则从R转换为E，如下所示：RJ=R1，l→τr∈R|l，r∈T P（X），EJ：=E，（l，r）|l→τr∈R，l，r∈T P（X），然而，这种简单的修改是不正确的，因为原始和修改后的LRT的诱导LTS通常是弱双相似的。 这是由于以下两个问题。非确定性：我们假设LRT T =（E，E，R，L），其中E= E，过渡规则为：R=，b→τc ，b→τd ，c→ad，.在改进的LRT T j中，b = E j c=EJ d和 c →d∈ RJ.因此存在（Com）148L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139一一T不τΣΣRE一个无穷序列的a-变迁的形式[b]EJ →TJ [b]EJ →TJ ... 在初始L RT，然而，每个计算都是终止的：[b]E→τT[c]E→aT[d]E和[b]E→τT[d]E。 这说明这两个跃迁系统不是弱双相似的。条件中的τ-规则：设=（E，E，R，L），其中E=，并具有以下过渡规则：.x1→τ y1x2→a2000年R=，h（x1，x2）→ah（y1，y2）、b→τc.d→ae则[h（b，d）]E→aT[h（c，e）]E，但[h（b，d）]J在Tj中没有a-后继.很明显，第一个问题是由无条件τ-跃迁和其他跃迁之间的可能选择引起的，不能用简单的构造来解决。因此，我们继续限制所考虑的LRT，假设所有无条件τ规则在以下意义上是确定性的定义4.1一个标记重写理论=（E，E，L，R）被称为受限的，如果它满足以下条件：• 如果l1→r1 ∈R，则不存在C∈R且w∈Pos（l~ 2）使得l1= El2|w和l2→αr2l→τr• 系统级上的所有转换规则都具有以下形式：ls→τr∈R，其中s∈TS（X），或l→als→a rsJ ∈R，其中s，sJ∈TS（X）.我们注意到，它是可判定的是否一个给定的LRT是限制或不，提供了方程理论是可判定的。第二个问题，条件中τ-规则的存在，可以通过改变修改的LRT的结构来解决。其思想如下：无论何时 一个条件可以通过应用一个无条件τ-规则来满足，我们添加一个新的规则，该规则是通过在适当的实例化下丢弃这个条件而获得的。这可以形式化如下。定义4.2设T =（E，E，R，L）是一个受限的标记重写理论。 其通过应用以下算法获得修正TJ =（E j，EJ，RJ，L）L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139149Σα1→dτRJ：=R;EJ：=E;对所有l1→τr1∈R，其中l1，r1∈TP（X），RJ：=RJ1，l1→τr1，;EJ：=EJ<${（l1，r1）};C→ d...Cαkd对于所有11k→kl2→αr2∈RJ， 1≤i≤k且σ∈Sub使得l1σ=Eciσ和r1σ=EdiσdoRJ：=RJ .... ci−1σαi−1i−1σ ci+1αi+1σ→d一期+1σ...Σ首尾相接l2σ→α r2σ显然，对于所有LRT，算法终止为无条件的R中的τ-规则是有限的。如果这个数用n表示，并且如果m表示R-规则中的最大条件数，则修改后的转移规则集RJ的大小是二次有界的：|RJ|≤ |R|-n+（|R|− n）mn ≤ m|R|二、注意，变换可能在RJ中创建新的无条件τ-规则，在这种情况下，它可以迭代地应用。这样就保证了整体正确性，因为正如我们将在第6节中看到的，修改后的重写理论的LTS是弱双相似的，并且因为弱双相似是等价的（因此是传递的）。5使用Erlang在研究隐藏无条件τ-规则的效果之前，我们必须证明Erlang的LRT是受限制的。但这是直接的，因为无条件τ-规则是确定性的，并且系统级上的所有规则都具有所需的形式。我们现在演示Erlang的修改后的LRT的构造，重点是第3节中开发的列表和顺序求值的规则：(list第一章第1章|我|Q|ρ ⟩ →J1|我|QJ|pj[e1|e2]|我|Q|ρ ⟩ →（seq2）[eJ1|e2]|我|QJ|pjτ波夫e|我|Q|ρ ε → ε ε e|我|Q|ρ ⟩然后，在定义式4.2中的构造将（seq2）从转移规则集合中删除，将其添加到方程理论中，并产生（列表1）的以下修改(listJ1）[（v，e1）|e2]|我|Q|ρ → [e1|e2]|我|Q|ρ ⟩αα150L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139ααα1→αi与1客户端2客户端3个客户原始LTS78个国家1014个州13182个州摘要LTS16个州64个国家256个状态表1原始与抽象的系统将这个修改过程迭代地应用于完整的Erlang规范，我们得到了一个修改的LRT，它诱导了抽象的LTS。在Maude [13]中调整我们的（核心）Erlang的原型实现，我们现在可以比较不同数量的客户端进程的原始和抽象LTS的状态空间大小。 相应的数字见表1。3我们看到，方程抽象将状态空间缩小了几个数量级，这意味着可以更有效地分析互斥、无死锁和饥饿自由等典型的验证问题。下面的部分表明这种方法是正确的：原始系统和抽象系统可以被证明是弱双相似的。这意味着，例如，对于不能区分弱双相似系统的逻辑，判定其模型检验问题，需要考虑抽象系统。6正确性证明我们现在可以证明由（限制）LRT诱导的LTS和由前者的修改诱导的LTS是弱双相似的。为此，我们首先证明了两个中间结果，它们只处理单个过程。第一个表示，原始系统中的每一个不是通过无条件τ-规则获得的转移也存在于抽象系统中。引理6.1设T =（E，E，R，L）是限制LRT，TJ =（E，EJ，RJ，L），Pα相应的修正LRT，s，t∈ T∈（X），α ∈ L。 如果[s] E→ T[t] E和st，则[s] EJ→ TJ[t] EJ。EJ\E证据我们证明了索赔的深度在原来的LRT T根据def的过渡归纳。2.4.n=0：清除，因为→T0=0n→ n+1：设[s] E→ Tn+1 [t] E且s i = EJ\Et。 根据定义2.4，存在c→d... Cαkd1 1k→kl→αr∈ R，w ∈ Pos（s）且σ ∈ Sub使得s|w= Elσ，t = Es[w <$rσ]，且[c i] ETn[d i] E对每一个1 ≤ i ≤ k。我们区分以下情况：(i) α = τ： 这里k ≥1，因为否则s =EJ\E t。 现在，分析[3]这些数字与[ 15 ]中得到的数字不同，因为后者没有考虑核心语言，而且它使用了ELAN重写工具。L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139151→→Tn+1[客α1Σα1ττ→τΣI ETnI EαΣ→ΣMm对于1≤i≤k，条件[c]αi[ d ]产生：• 若ci/=EJ\Edi，则通过归纳推理，[ci]E→TNJ[di]E。• 如果ci=EJ\Edi，则根据Def.4.2存在C∈Rj，其中C是通过丢弃ci→τdi得到的，其中lσαrσα因此是满意的。 T hus[s]E→TnJ+1[t]E。τ(ii) αi = τ：这里是sJt，因为否则存在 lJ→ rJ∈ R， w∈Pos（ s）和E\Eσ ∈ Sub使得s|W=ElJσ和t=Es[w←αrJσ].然而，这与Def的第一个限制相4.1. 故[s]E[t]E是归纳假设。Q下一个引理声称，修改后的LRT中的每一个变迁都对应于原始LRT中的一个变迁引理6.2设T =（Ej，E，R，L）是限制LRT，TJ =（Ej，EJ，RJ，L），则Pα α响应的修改的LRT，s，t∈ T∈（X），α ∈ L。 如果[s] EJ→ TJ[t] EJ，则[s] E→ TtE.证据我们再一次用归纳法证明了关于过渡深度的主张，现在是在改进的LRT中。n=0：透明αc→d... Cαkdn→n+1：设[s]EJ→TnJ+1[t]EJ.存在11k→l→αrK∈RJ，w∈αiPos（s）和σ∈Subsuch使得s|w=EJlσ，t=EJs[w←rσ]，且[ci]EJ→TnJ[di]EJ对于每个1 ≤i ≤k。我们区分以下情况：α1αkC→ d. cdα(i) 如果11k→kl→αr∈R，则通过归纳推理，[ci]E→iT[di]E对于每个1≤i≤k，因此[s]E→αTn+1个[t]E.(ii) 除此之外，如定义4.2所述，在改造后的轻轨列车结构中增加了过渡规则。相应地，存在m > k，c k+1，.，c m，d k+1，.，dm∈TP（X）且σ∈Sub使得αkC→ d. cd c→ d.c→ d1 1k→kk+1k+1∈R，lJ→αrJl=lJσ，r=rJσ，[c]αi[日]对于1≤i≤k，[cσ] →[d σ]为E E I ETni ETnjEk+ 1≤j ≤m。总之，这又意味着[s]E→Tn+1[t]EQ这两个结果现在使我们能够给出完整的互模拟证明，表明我们对修改后的LRT的构造产生了一个与原始系统弱互模拟的抽象系统。定理6.3设T =（E，E，R，L）是一个限制LRT，TJ=（E，EJ，RJ，L）是相应的修正LRT，s0∈ TS（X）是某个初始项.则导出的LTS（TS（X）/E，[s0] Ej，→ T，L）和（TS（X）/EJ，[s0] EJ，→ T，L）是弱双相似的.n152L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139Σ⇒Σα1→n∈R：如果sα⇒⇒ΣΣ→→ΣRΣΣΣΣΣΣαˆl→ǁ→αi证据 我们证明以下关系是弱互模拟：R：= {（[s] E，[sJ] EJ）|s = EJsJ}。为了这个目的，我们必须证明，这两个过渡系统弱相互模拟w.r.t. R.(i) （TS（X）/EJ，[s0]EJ，→TJ，L）模拟（TS（X）/E，[s0]E，→T，L）：令[s]E→αT[t]E。我们区分以下几种情况：• s∈TP：ifs/=EJ\E t，则[s]EJ→TJ[t]EαˆJ 引理6.1 因此， [s] EJT J[t]EJ.否则，α=τ，因此[s]EJ<$TJ[t]EJ。• s∈TS\TP：这里s可以表示为s=pps，其中p∈TP（X），ps∈T S（X）. 更上[s]E→αT[t]E意味着存在C→d... Cαkd1 1k→kl→αr∈R，w ∈ Pos（s）且σ ∈ Sub使得s|w= Elσ，t= Es [w ← rσ]和[c i σ] ETd i σ] E，对于每个1 ≤ i ≤ k。根据Def.4.1、可能有两种情况τr·l uτr uαˆEJ\Et，则[s]EJ→TJ[t]EJ 根据引理6.1，αˆ故[s] EJTJ[t] EJ。否则，[s] EJTJ[t] EJ，因为跃迁可以通过方程变换来模拟。l→arJ J·lu→ar<$uJ∈ R： 这里sj = EJ\E t和t=pps，否则τp=JPJ，则存在l→r ∈R，w∈Pos（p）和σ∈SubE\EJ J J使得p|w= Elσ和t = Ep [w<$r σ]，与定义4.1矛盾。ααˆ因此，根据引理6.1，[s]EJ →TJ [t]EJ，因此[s]EJ<$TJ[t]EJ。(ii) （TS（X）/E，[s0]Ei →T，L）模拟（TS（X）/EJ，[s0]EJ， →TJ，L）：Σ Σα令[s]EJ →TJ [t]EJ。我们再次区分两种情况：• s∈ T P：这里的跃迁可以分为以下三个部分。(a) 等式变换：s=EJ\EsJ(b) 实际跃迁：[sJ]EJ→TJ[tJ]EJJ(c) 等式变换：t=EJ\Et这些部分中的每一个可以在（TS（X）/E，[s0]E，T，L）中模拟如下。(a) 由于EJ和E在无条件τ-规则所加的方程中唯一不同，因此存在[t1]E， … ，[tn]E，其中[ti]E→τT[ti+1]E，对于1≤i≤n−1，[tJ]E→τ[t1]E，且[tn]E→τ[t]E。(b) 这里[sJ]EαT[tJ]E由引理6.2得出。(c) 如（a）总之，我们得出结论，[s]E <$α<$T[t]E。• s∈TS\TP：这里s和t可以表示为s=pps和t=qpsJ，保留部分。 相应地存在l→αlx→α r<$xJ∈R ，以及转型可以分为以下四个部分。(a) 等式变换：p=EJ\EpJα[αL.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139153αΣτ（b）自[pJ] →E\(b) 实际跃迁：[pJ<$ps]EJ→TJJ[qJpsJJ]EJ(c) 等式变换：q=EJ\Eq(d) 等式变换：psJJ=EJ\EpsJ同样，这些部分中的每一个可以在（TS（X）/E，[s0]E， →T，L）中模拟为：如下(a)由于EJ和E在无条件τ-规则所加的方程中唯一不同存在[p1ps] E，.，[pnps]E，其中[pips]E →T [pi+1ps]E，e very1≤i≤n−1），[pps]E→τ[p1ps]E，[pnps]E→τ[pJps]E。α(c) 就像在（a）T[qJ]Eby引理6.2，[pJ<$ps]E→αT[qJ<$p sJ J]E。(d) 通过应用等式变换，我们只能停留在同一等价类中。总之，我们再次得出结论，[s]E <$α<$T[t]E。Q7结论及相关工作在本文中，我们已经展示了如何方程抽象可以使用重写逻辑框架，以减少并发系统的状态空间。特别地，我们已经看到如何为给定的限制LRT构造一个新的LRT，其诱导的LTS与由原始LRT诱导的LTS弱双相似，避免构造（大）原始LTS。因此，我们的抽象可以用来获得有效的模型检测算法的逻辑，如CTLX不能区分弱双相似系统。我们已经证明了使用的建议的方法与并发函数式编程语言Erlang。 为 在储物柜的例子中，我们已经看到，方程抽象导致状态空间的显着本文中描述的工作建立在[15]中的结果之上，其中将无条件τ-转移到方程理论的想法已经被引入，再次在Erlang编程语言的上下文中，但没有给出正确性证明。事实上，正如第4节中的讨论所表明的，将无条件τ规则转化为方程的简单想法是行不通的;需要更精细的构造。另一个使用方程来定义状态空间上的抽象映射的出版物是[11]。 在这里，与我们的工作相反，只有w.r.t.才是正确的线性时间属性，使得所得到的抽象系统通常不是弱双相似的原始系统。此外，[4]研究了偏序约简技术在重写逻辑环境中的应用，再次采用了与我们不同的等价（口吃）概念引用[1] Armstrong，J.，S. Virding，M. Williams和C. Wikstr？om，“Concurre n t Programming inErlang ，”Prentice Hall International， 1996，第2版。154L.H. 哈茨，T.Noll/理论计算机科学电子笔记238（2009）139[2] 艺术，T。，C. Earle和J. Derrick，《Erlang code：a resource locker case study》，《FormalMethods184-203.[3] Emerson，E.，“Temporal and Modal Logics,” Handbook of Theoretical Computer Science 996-1072[4] Farzan ， A.和 J.Meseguer， State space reduction of rewrite theories using invisible transitions ，in：11th Int. 代数方法论和软件技术会议（AMAST '06 ） ， 计 算 机 科 学 讲 义 4019 （ 2006 ） ， 页 。142-157[5] 弗雷德隆德湖A.和H. Svensson，McErlang：分布式函数式编程语言的模型检查器，SIGPLAN Not。42（2007），pp.125-136[6] Leucker，M.和T.Noll，Specification Language Implementations的Rapid prototyping，1999年，第10届IEEE International Workshop on Rapid System Prototyping（RSP60比65[7] Leucker，M.和T.Noll，重写逻辑作为通用验证工具的框架，在：第三届重写逻辑及其应用国际研讨会论文集121-137[8] Mar t'oliet，N. 和j. Meseguer，Rewritingl ogic：Roadmapandbibli og raph y，TheoreticalComputerScience285（2002），pp. 121-154[9] Meseguer，J.，Rewriting as a unified model of concurrency，in：Proceedings Int. Conference onConcurrency Theory
我的内容管理
展开
