Maude LTL模型：并发系统动态显式状态模型检查及其性能和应用领域扩展

理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html26页Maude LTL模型StevenEkera，Jos'eMeseguerb，andAmbarish Sridharanarayananba计算机科学实验室，SRI International，Menlo Park，CA 94025。b伊利诺伊大学厄巴纳-香槟分校计算机科学系，厄巴纳IL 61801。摘要Maude LTL模型检查器支持并发系统的动态显式状态模型检查，表示为重写理论，其性能与当前的此类工具（如SPIN）相当。 这极大地扩展了适用于模型检测分析的应用范围。 除了现有工具支持的传统领域（如硬件和通信协议）外，许多新的应用领域（如重写细胞生物学的逻辑模型或下一代反射分布式系统）都可以很容易地使用我们的工具进行指定和模型检查。关键词：模型检测，并发系统，Maude1介绍模型检查器通常支持两个不同级别的规范：（1）系统规范级别，其中要分析的并发系统被形式化;（2）属性规范级别，其中要进行模型检查的属性（例如，时态逻辑公式）被指定。在他们优秀的模型检查书[2]的结论中，Clarke，Grumberg和Peled指出，“的。. . 当前系统的一个明显问题是如何使规范语言更有表现力和更易于使用。虽然他们似乎主要考虑的是属性规范级别（2），但我们认为大大提高系统规范语言的表达能力同样重要问题是，许多潜在的应用领域-超越传统的，如硬件和通信协议-可以很难表达在当前的模型检测系统规范语言。例如，PROMELA [10]-SPIN的系统规范语言-被设计和优化，目的是有效地模型检查分布式算法规范。这是完全合理的，但203年7月，出版《ElsevierScienceB》。 诉在CC BY-NC-ND许可下开放访问。162EKER、MESEGUER和 SRIDHARANARAYANAN163其代价是限制了可以自然规范的系统的种类特别是：（1）进程不能嵌套，在这个意义上，包含在其他子进程，子子进程，等等;（2）通信被认为是通过FIFO通道发生的;（3）有一个有限的数据类型供应，所有其他数据必须编码。 嵌套过程或“对象”是指定细胞生物学的重写逻辑模型的自然方式，该模型将细胞状态表达为膜、细胞质和细胞核中蛋白质复合物的嵌套汤[7，6]，也是反射分布式系统，该系统涉及元对象的任意嵌套，控制它们下面的其他对象组-所谓的分布式对象反射的“俄罗斯娃娃”模型[16]。在诸如PROMELA之类的语言中很难实现这样的嵌套过程。相比之下，刚才提到的所有应用程序都可以在Maude中轻松指定（参见[7，6，16]）。 由于LTL模型检查器的唯一要求是可达状态的有限性，因此假设成立，这样的应用程序和任何其他可表达为重写理论的应用程序可以由Maude的LTL检查器进行模型检查，而无需任何修改（参见[6]，resp. [24]，Maude模型检测应用于细胞生物学，分别。主动网络）。此外，Maude LTL检查器可以模拟检查系统，其状态涉及无限基数数据类型的数据，例如数字，列表或任意大小的多集;事实上，在任何代数数据类型中。唯一的假设是，从给定的初始状态可达的状态集是有限的。这种有限可达性条件可以下降的情况下，半判定搜索的反例的无限状态系统的安全性在Maude支持的搜索命令（这种能力是不讨论本文，由于空间的限制）。目前有意识地努力扩展SAL [22]等语言中并发系统规范的表达能力，该语言明确地解除了有限状态限制并支持无限状态系统的规范，然后可以将其抽象为有限状态系统以用于模型检查目的，PVS定理证明器验证抽象的正确性。Maude的表达性目标与SAL的类似，但有两个重要的区别：（1）Maude是可执行的，而SAL通常不是;以及（2）SAL被设计为支持固定（尽管可能是参数）数量的通信对象之间的固定同步和/或异步通信拓扑;而Maude允许高度动态和可能嵌套的反射通信体系结构的规范。总之，这项工作的主要贡献是将一种非常有表现力的可执行系统规范语言，即Maude [3]，与显式状态动态线性时态逻辑（LTL）模型检查器相结合，其时间和空间性能可与当前高性能模型检查器（如SPIN [1]）相媲美。重写逻辑作为一个语义框架的巨大的通用性和灵活性[15，19]当然是Maude的表现力的原因。系统说明书EKER、MESEGUER和 SRIDHARANARAYANAN164RRR∈R−→ P→/E，状态，即所有对的集合（[州/东部考虑到最新的研究进展，优化dBuuchi自动机结构和显式状态模型检测算法，在不牺牲性能的情况下，达到了最高水平。本文的结构如下。在第2节中解释了任意重写理论的线性时态逻辑的语义。LTL模型检查器的功能在第3节中描述，可满足性和重言式检查器在第4节中描述。然后在第5节中描述算法和实现。与SPIN的性能比较在第6节中给出。结论见第7节。2重写理论R的LTL性质重写理论R =（E，E，R）的初始模型TR在固定一个区别排序状态的情况下，具有一个底层Kripke结构，该结构由扩展其单步顺序重写的全二元关系给出.由于T/E有一个代数的-代数结构，所以对于这样的Kripke结构，有一个非常有表现力的状态谓词的一阶语言。然后，我们可以以标准的方式关联到线性时序逻辑的底层Kripke结构和状态谓词语言，即重写理论的LTL性质的语言. 我们将在下面的内容中使所有这些精确化，首先是Kripke结构和LTL的一些集合A上的二元关系R<$A×A称为全当且仅当对于每个a∈A至少有一个aJ∈A使得（a，aJ）∈R。如果R不是全的，则可以通过定义R · = R <${（a，a）∈ A2|/aJ∈A（a，aJ）∈R}.定义. Kripke结构是三元组A=（A，→A，L），使得A是一个集合，称为状态集合，A是A上的一个完全二元关系，称为转移关系，L：A（AP）是一个函数，称为标记函数，将AP中在状态a中成立的那些原子命题的集合L（a）与每个状态a A相关联。设=（t，E，R）是重写理论[17]，其中（t，E）是其基础的隶属方程理论[18]，并且设状态是在T中的排序，使得对于每个[t]∈T/E，状态，如果[α]：[t]−→[tJ]是在TR中的重写证明，则[tJ]∈T/E，状态。 然后我们可以将R与Kripke结构K（R，State）=（T/E，State，→·，LR），其中→R是一步顺序R。TRt]，[tJ]）∈T2上的重写关系使得存在一步顺序重写证明（参见[17]）[α]：[t]→[tJ]在TR中，其关联的总关系→·为每个死锁状态添加自循环，也就是说，对于每个[t]∈T/E，状态R无法再被改写标签函数LR的形式为LR：T/E，State−→ P（SPred0（，State）），其中SPred0（NSL，State）是一阶公式P的集合，称为状态谓词，在一阶语言中具有等式1FOL（NSL），具有单个固定的1这种语言当然是多种类型的;此外，我们允许使用排序变量。EKER、MESEGUER和 SRIDHARANARAYANAN165作为满足相应排序谓词的kinded变量的缩写EKER、MESEGUER和 SRIDHARANARAYANAN166RRR|∈−→PA→AA|∈K R|{}联系我们sort State的自由变量x，即fvars（P）={x}。然后，函数LR将每个状态[t]∈ T/E，State映射到在[t]中成立的状态谓词的集合，即LR（[t]）={P∈SPred0（E，State）|T/E|= FOLP（x→t）}。 注意，刚刚给出的LR（[t]）的定义并不依赖于代表t在[t]中。给定原子谓词的集合AP，AP上的线性时态逻辑公式的语言LTL（AP）可以以通常的方式被定义为集合AP上的（未排序的）自由代数TLTL（AP），其用于具有常数T（真），T（假），一元运算符<$（否定），T（下一个），Q（最终）和Q（此后）的签名LTL，并且具有二元运算符<$（合取），<$（析取），→（隐含）、参与（等价）、U（直到）和R（释放）。模型LTL（AP）是Kripke结构=（A，A，L），具有AP作为它们的原子命题，即具有L：A（AP）。由于LTL公式是在无限计算路径上直接普遍量化的，因此满足关系A，a|在Kripke结构A，它的一个状态a，和公式LTL（AP）之间成立当且仅当对于所有的无限计算路径π，从状态a开始，满足关系a，π=LTLπ成立（例如参见[2]，其中黑体大写字母用于所有时间运算符）。特别地，给定重写理论R =（T，E，R），其中排序State满足上述假设，state [t] ∈ T TT/E，State，以及LTL公式LTL（SPred0（状态）），满意度关系，（，State），[t] 表示重写理论和初始状态[t]满足LTL性质[t]。当不可能出现混淆时，我们可以隐式地保留对状态排序的选择，并通过，[t]=LTL来简化上述满足关系。这给出了重写理论所满足的LTL属性的精确语义。我们当然对证明这些性质的演绎技术感兴趣，并且只要可能，在模型检查决策过程中，以确定在给定的初始状态[t]下LTL性质的满足值得指出的是，SPred0（Numbers，State）是一组相当通用的无参数状态谓词。 通过放松fvars（P）= X 到较弱的要求Xfvars（P）. 也就是说，对于P SPred（P，State），我们将fvars（P）x中的变量称为其参数。然 后 ， 我 们 可 以 定 义 一 个 更一般的 时态逻辑 LTL（SPred （STATE ，State）），其中状态谓词可以具有参数和满足关系R，a|= LTL，其中a是公式中所有变量（包括其参数）在T/E中的赋值。这超出了[2]中所处理的严格的“命题”语义，但推广是没有问题的。即使当（E，E）是汇合的和终止的，状态谓词P LTL（SPred（E，State））的满足一般也可能是不可判定的。这对于演绎使用是可以接受的，但对于模型检查则不行如第3节进一步解释的，Maude LTLEKER、MESEGUER和 SRIDHARANARAYANAN167RR{∈|R→}模型检查器允许定义非常一般的属性是通过允许在SPred（STATE，State）中的可判定参数状态谓词的丰富子类中的状态谓词定义3Maude LTL模型Maude 2.0支持对有限重写理论R=（E，E，R）的初始状态[t]进行动态LTL模型检查，例如排序状态，使得集合[u][1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19重写 理 论 应 该 满 足 已 经 提 到 的 要 求 ， 即 所 有 这 样 的 可 达 状 态 [u] 也 有sortState。此外，方程理论（E，E）应该是融合的和终止的（也许模一些公理，如结合性，交换性或恒等式），规则R应该相对于方程E是连贯的[25]。注意，许多感兴趣的重写理论可能有无限多个状态，但从任何给定的初始状态可到达的状态可能仍然是有限的。满足上述假设的重写理论可以在Maude中由系统模块来指定，比如M。然后，给定一个初始状态，比如说初始化状态M，我们可以从这个初始状态开始，通过执行以下操作来模型检查• 定义一个新的模块，比如说MODELK-M，它包括模块M和预定义的模块MODEL-MODELKER作为子模块（如果我们希望，例如为了引入辅助数据类型和功能，我们也可以包括其它子模块• 给出一个子排序声明，子排序状态M<状态。 其中State是模块MODEL-MODELKER中的关键排序之一（如果StateM=State，则可以省略此声明）;• 通过常数和排序Prop的运算符来定义我们希望使用的状态谓词的语法，排序公式的子排序（即，LTL公式）;我们可以将无参数状态谓词定义为Prop排序的常数，并通过从其参数的排序到Prop排序的运算符来定义参数化• 通过涉及算子的方程定义状态谓词的语义操作_|=_：状态属性->结果[特殊. ]中。在模型制造器中。排序结果是布尔值的超排序。我们定义每个状态谓词的语义，比如一个参数化的状态谓词p，通过给出一组（可能是条件的）方程的形式：ceq exp1| = p（u11，...，un1）= true ifC1....CEQ Expk| = p（u1k，.，unk）= true ifCk.其中：EKER、MESEGUER和 SRIDHARANARAYANAN168·≤≤·≤≤·≤≤expi，1我k，是排序状态M的模式，也就是说，项，可能-bly与变量，并只涉及建设者，使他们的任何情况下，由简化的基础条款不能进一步简化;项P（U11，...，uni），1 i k同样是类Prop的模式;每个条件Ci，1i k是等式和条件的结合;这样的条件可能涉及辅助函数，或者从辅助模块导入，或者由我们的模块KK-M中的附加方程定义。一旦定义了每个状态谓词的语义，我们就准备好了，给定一个初始状态init，对任何涉及这些谓词的LTL公式（比如form）这样的LTL公式是Sort公式中的基项2;我们通过给出Maude命令来实现，减少初始化|=形式。如前所述，假设可达状态的集合是有限的。然后会发生两件事：如果属性形式成立，那么我们得到结果为真;如果opcounterExample：transitionList transitionList-> Result [ctor].这是因为，如果有限Kripke结构不满足LTL公式，则总是可以找到一个反例，用于具有由循环跟随的过渡路径的形式的LTL公式。上面构造函数的第一个参数是通向循环的路径，第二个参数是循环本身。每个转换都表示为一对，由状态和规则标签组成注意，我们已经定义了状态预测的语法和语义，使得它们的状态参数是隐式的。例如，具有S1，. . . ，Sm被定义为通过操作员，op p：S1. Sm-> Prop.而不是由操作员op p：状态S1. Sm-> Prop.注意，第一语法中的语义等式ceq exp1| = p（u11，...，un1）= true ifC1....CEQ Expk| = p（u1k，.，unk）= true ifCk.完全符合方程，ceq p（exp1，u11，.，un1）= true ifC1....ceq p（expk，u1k，.，unk）= true ifCk.2如上所述，我们允许定义参数化状态谓词;然而，在提供给模型检查器的任何LTL公式，例如参数化状态谓词，必须通过它们的每个参数的适当的基本项来实例化EKER、MESEGUER和 SRIDHARANARAYANAN169R在第二种语法中。这一观察有助于阐明关于如何在LTL模型检查器中指定状态谓词的另一个非常方便的特性，即仅必须指定肯定情况;也就是说，如果表达式为exp的状态谓词基础表达式|= p（w1，.，wk）（等价于p（exp，w1，...，第二种语法中的wk）不能简化为true，则假定为false3上述定义状态谓词的方法有多普遍设=（E，E，R）是一个重写理论，表示为模M，并且满足本节前面已经提到的所有假设设p由上述k个方程在其显式状态公式中定义，其中第i个方程涉及变量集Xi，并假设条件中可能需要的所有辅助函数已经在M中定义。然后，状态谓词p产生了一阶语言FOL（n）的定义扩展，将以下析取公式与p相关联，该析取公式对于Tn，E中的任何基实例都是可判定的：p（x，y1，. . . ，yn）= true当且仅当（（x =exp1）y1= u11）。. . y n= un1. . . （（. . y n= unk模型检查器fmod LTL是排序道具公式。子分类Prop<公式。* 原始LTL算子ops True False：->公式[ctor]。op ~_：公式->公式[ctor prec 53]。op_/\_：公式公式->公式[comm ctorgather（E e）prec55]。op_\/_：公式公式->公式[comm ctorgather（Ee）prec 59].op0_：公式->公式[ctor prec 53]。op_U_：公式公式->公式[ctor prec 65]。op_R_：公式公式->公式[ctor prec 65]。* 定义的LTL运算符op _->_：公式公式->公式[gather（e E）prec 61]。op_->_：公式公式->公式[prec 61]。op<>_：公式->公式[prec 53]。op[]_：公式->公式[prec 53]。3然而，允许用户给出表单的定义ceq exp |= p（u1，.，un）= bexp如果C.bexp是一个任意的布尔表达式;C也可以是空的，所以一个无条件的等式（Eq）就足够了。EKER、MESEGUER和 SRIDHARANARAYANAN170op _W_：公式公式->公式[prec 65]。* 弱直到op_|->_：公式公式->公式[prec 65]。*leads-tovars f g：公式。方程式f-> g =~ f1/g。方程式f<-> g =（f-> g）/l（g ->f）。eq<>f = True Uf。eq [] f= False Rf。等式fW g =（fU g）\/[] f.方程式f|-> g =[]（f->（<>g））。* negative normal form eq~True = False。eq ~ False =True。方程f = f.方 程 f/g= f/g 。 eq~（f/g）= ~ f/~ g。eq ~ O f= O ~ f.eq~（f U g）=（~ f）R（~ g）.eq~ （ f R g ） = （ ~f ） U（~g）. endfm这个模块中的方程做两件事：（1）它们用基本运算符True、False、negation、conjunction、disjunction、next、O、until、U和release、R来表示所有定义的LTL运算符;（2）它们将仅使用这些基本运算符的LTL公式转换为负范式中的等价公式，也就是说，否定被一直向下推到状态谓词中。我们说明了使用Maude模型检查器与Dekker算法，最早的正确解决方案之一的该算法假设进程在共享内存机器上并发执行，并通过共享变量相互通信有两个进程，p1和p2。进程1将布尔变量c1设置为1，以指示它希望进入其临界区。进程p2执行相同变量C2。如果一个进程在将其变量设置为1后发现其竞争对手的变量为0，则它立即进入临界区在平局的情况下（两个变量都设置为1），使用在{1，2}中取值的变量turn来打破平局。进程1的代码如下，重复c1：= 1;当c2 = 1时，如果turn=2，则c1：= 0;当turn= 2时跳过od; c1：=1EKER、MESEGUER和 SRIDHARANARAYANAN171Fi临界值;turn：= 2;c1：= 0;永远记得其中用于临界部分和用于程序的剩余部分的代码片段分别被抽象为常数CRIT和REM。我们假设暴击是终止性的，但对快速眼动却没有这样的假设。在附录A的Maude规范中，这是通过声明子排序和常量来实现的，子排序LoopingUserStatement UserStatement程序。opcrit：-> UserStatement。oprem：-> LoopingUserStatement.并且通过语义规则，其中不在LoopingUserStatement中的UserStatement总是终止，但是LoopingUserStatement可以不终止。 进程2的代码是完全对称的。支持上述特性的简单并行语言的语义的Maude规范在附录A中给出这两个过程在模块DEKKER中定义，该模块导入定义并行语言语义的模块PARALLEL为了指定Dekker算法的相关属性DEKKER公司的Moderis公司。inc MODEL-标记器。incLTL-SIMPLIFIER.*可选子排序MachineState Prop.var M：内存。vars R：Program.var S：汤。vars I J：Pid.eq {[I，crit; R] |S，M，J}|= enterCrit（I）=true。eq {[I，rem; R] |S，M，J}|= in-rem（I）= true。等式{S，M，J}|= exec（J）=true。恩德姆然后我们可以验证是否满足互斥性质减少在：初始|= []~（enterCrit（1）/\enterCrit（2））。Modelautomaton：属性自动机有两个状态。ModelToolkerSymbol：检查了263个系统状态。重写：1156 in40 ms cpu（40 ms real）（28900重写/秒）EKER、MESEGUER和 SRIDHARANARAYANAN172∈一|结果Bool：true无限执行往往意味着无限进入临界区的强活性性质Maude LTL模型检查器返回一个反例。减少在：初始|= []<> exec（1）-> []<> enterCrit（1）.Modelautomaton：属性自动机有三个状态。ModelToolkerSymbol：检查了16个系统状态。重写：148 in 0 ms cpu（0 ms real）（~ rewrites/second）结果ModelCheckResult：反例（{{[1，repeat而“turn = 2 do skip od ;”c1：= 1 fiod;.由于rem可能不会终止，如果p1和p2都无限频繁地执行，那么两者都无限频繁地进入其临界区的较弱活性性质也失败了。减少在：初始|= []<> exec（1）/\[]<> exec（2）->[]<> enterCrit（1）/\[]<> enterCrit（2）.Modelautomaton：属性自动机有7个状态。ModelBikerSymbol：检查了236个系统状态。rewrites：1463 in 60ms cpu（60msreal）（24383rewrites/second）resultModelCheckResult：counterexample（{{[1，repeatwhile'c2 = 1 do if 'turn = 2 then 'c1：= 0 ;while 'turn = 2 do skip od ; 'c1：= 1fiod;.但更微妙的弱活性性质是，如果p1和p2都无限频繁地执行，那么如果p1无限频繁地超出其rem部分，那么p1无限频繁地进入其临界部分。当然，对称性陈述对p2也成立。减少在：初始|= []<> exec（1）/\[]<> exec（2）->[]<>~ in-rem（1）-> []<> enterCrit（1）.Modelautomaton：属性自动机有5个状态。ModelToolkerSymbol：检查了263个系统状态。rewrites：1661in70ms cpu（70ms real）（23728rewrites/second）结果Bool：true上面的Dekker算法例子说明了在Maude中对任何编程语言中的任何程序（或程序的抽象，具有许多可达状态）进行模型检查的一般能力：我们只需要在Maude中定义语言4满意度求解器与重言式公式A∈LTL（AP）是可满足的，当且仅当存在Kripke结构A=（A，→A，L），其中L：A−→ P（AP），状态a∈A，以及从a开始的计算路径π，使得，a，π= LTL π. 公式的可满足性LTL（AP）是一个可判定的属性。在Maude中，可满足性决策过程由预定义的功能模块SAT-SOLVER支持。一EKER、MESEGUER和 SRIDHARANARAYANAN173¬一A → −→ P∈可以在扩展SAT-SOLVER的模块中定义所需的原子谓词，例如，fmod测试是incSAT-SOLVER.ops a b c d e p q r：-> Prop.endfm然后，用户可以通过应用操作符来决定涉及这些原子命题的LTL公式的可满足性，op satSolve：Formula -> [SatSolveResult] [special. ] 的一种对给定的公式求值。然后，如果不存在模型，则SatSolveResult排序的结果解为假，或者满足公式的有限模型。这样的模型由一对状态的有限路径来描述：一条初始路径通向一个循环。每个状态都由原子命题或否定的原子命题的合取来描述，合取中没有提到的命题是例如，我们可以评估，Maude> red satSolve（a/\（O b）/\（O O（（~c）/\ []（c\/（Oc））。在测试中减少：satSolve（O O（~ c/\[]（c\/Oc））/\（a/\O b））。重写：2in 0 mscpu（0 msreal）（~重写/秒）result SatSolveResult：model（a; b，（~ c）;c）这由四状态模型满足，其中a保持在第一状态，b保持在第二状态，c不保持在第三状态而是保持在第四状态，并且第四状态返回到第三状态。我们称A ∈ LTL（AP）为重言式当且仅当A，a，π|对于每个Kripke结构，=（A，A，L），其中L：A（AP），每个状态A，以及从A开始。 因此，很容易得出结论，这是一个同义反复，当且仅当这是无法满足的。因此，模块SAT-SOLVER也可以用作重言式检查器。这是通过在SAT-SOLVER中使用以下运算符和方程来实现的：optautCheck：公式->[TautCheckResult]。op $invert：SatSolveResult ->TautCheckResult。var F：公式。 vars LC：FormulaList.eqtautCheck（F）=$invert（satSolve（~ F））。eq $invert（false）=true。eq$invert（model（L，C））= counterexample（L，C）.因此，如果公式是互变函数，则tautCheck函数返回true，或者返回不满足公式的有限模型例如，我们可以评估：Maude> red tautCheck（（p U r）/\（q U r）<->（（p/\q）Ur））。在TEST中减少：tautCheck（（p U r）/\（q Ur）<-> p/\q U r）。重写：31in 0 mscpu（0 msreal）（~重写/秒）结果Bool：trueEKER、MESEGUER和 SRIDHARANARAYANAN174≡K RR¬¬Ⓧ重言式检查器还给出了语义LTL相等的判定过程。设可数集X={x1，. . .，xn，. . . }，语义LTL相等关系LTL是由下式定义的LTL（X）上的二元关系，LTL优惠券参与者是同义反复。关键的观察结果（在附录B中证明）是替换-闭的替换LTL-同余，因此（参见，例如，[4]Thm. 1.1.2）在等式推导下闭合。 也就是说，定义ELTL ={=|，[1]我们有一个简单的例子，那就是：我们有一个简单的例子，那就是：我们有一个简单的例子，那就是：ELTLµ = ν惠µLTL ν。5模型检测算法及其实现动态LTL模型检查包括两个主要步骤[11]。首先，我们构造了一个与反例逻辑公式的否定相关联的Bu？hi自动机，它识别反例的语言其次，我们利用与重写理论相关的Kripke结构（，State），懒洋洋地构造了Bu？hi自动机的同步过程，寻找从初始状态可达5.1BuchiAutomatonConstructionGivenanLTLformulaφ我们希望构造一个接受满足φ的ω-词的语言的Bu？chi自动机。第一阶段是将φ置于负正规形式，如第3节所述，可能简化公式以产生更小的自动机。在Maude中通过包含可选模块LTL-SIMPLIFIER完成LTL简化。这种简化必然是启发式的;一般的想法是减少时态运算符的数量，并将命题运算符推入时态运算符中。Pennsylvania命题子公式可以通过命题技术来处理，并且不需要产生额外的自动机状态。在文献中有几种简化方案我们使用的主要技术是Etessami和Holzmann [8]的方法，在算子的情况下进行了微小的改进。该方法是基于语法分类的LTL公式的子集作为纯偶然性公式或纯普遍性公式，并执行重写，只适用于属于适当的子集的公式。我们引入第三组LTL公式（纯公式），这是其他两组的交集。这些概念，连同它们的语法基础，可以通过引入额外的排序来表示公式True和False，而相当整齐地映射到Maude类型系统的顺序排序片段fmod LTL-SIMPLIFIER是incLTL。排序TrueFormula FalseFormula PureFormula PE-Formula PU-Formula。EKER、MESEGUER和 SRIDHARANARAYANAN175子排序TrueFormula FalseFormula TrueFormula [同上]。“伪”：“伪”：“伪”。op_/\_：PE-公式PE-公式-> PE-公式[同上]。op_/\_：PU-公式PU-公式-> PU-公式[同上]。op_/\_：PureFormula PureFormula -> PureFormula [同上]。op_\/_：PE-公式PE-公式-> PE-公式[同上]。op_\/_：PU-公式PU-公式-> PU-公式[同上]。op_\/_：PureFormula PureFormula -> PureFormula [同上]。opO_：PE-公式-> PE-公式[同上]。op O_：PU-公式-> PU-公式[同上]。操作O_：PureFormula -> PureFormula [同上]。op _U_：PE-公式PE-公式-> PE-公式[同上]。op_U_：PU-公式PU-公式-> PU-公式[同上]。op _U_：PureFormula PureFormula -> PureFormula [同上]。op_U_：TrueFormula公式-> PE公式[同上]。op _U_：TrueFormula PU-Formula -> PureFormula [同上]。op _R_：PE-公式PE-公式-> PE-公式[同上]。op _R_：PU-公式PU-公式-> PU-公式[同上]。op _R_：PureFormula PureFormula -> PureFormula [同上]。op_R_：FalseFormula公式-> PU公式[同上]。op_R_：假公式PE-公式->纯公式[同上]。使用原始论文中的规则编号，简化规则可以表示为Maude方程：vars p q r s：公式。var pe：PE-公式。var pu：PU公式。var pr：PureFormula.* 规则1、2和3;各有其对偶。 eq（p Ur）/\（q U r）=（p/\q）U r。eq（p R r）\/（q R r）=（p\/q）Rr。e q （p U q）\/（p U r）= p U（q\/r）。e q （p R q）/\（p Rr）= p R（q/\r）。e q True U（pU q）= True U q。eq假R（p R q）=假R q。* 第四条和第五条做了大部分工作。等 式 p U pe = pe。方程式p R pu = pu。**等式0 pr=pr。为了进一步简化，我们还包括了不包含在Etessami和Holzman方法中的Somenzi和Bloem [23]的重写规则EKER、MESEGUER和 SRIDHARANARAYANAN176这些包括涉及辅助二元关系≤的条件规则。* 四对双胞胎。等式O p/\O q = O（p/\q）。等式O p\/O q= O（p\/q）。因此，时间复杂度为O（p U q）。等式O p R O q = O（p Rq）。因此，O（n）= O（n）。eqFalse R O p = O（False Rp）。eq（FalseR（True Up））\/（False R（True Uq）） =假R（真U（p\/q））。eq（TrueU（False Rp））/\（True U（False Rq）） =真U（假R（p/\q））。*<= 公式关系op _<=_：公式公式->布尔值[prec 75]。等式p< = p = true。eq False<= p=true。等式p <= True= true。ceq p< =（q/\r）= trueif（p< = q）/\（p< =r）. 如果p = q，则ceq p< =（qI/r）=真<。ceq（p/\q）<= r = trueif p< = r.ceq（p\/q）<=r= true if（p <=r）/\（q <=r）.ceq p< =（q U r）= trueifp< = r.c e q （p R q）<= r = trueifq<= r.ceq（p U q）<= r = trueif（p< = r）/\（q< = r）.ceq p <=（q R r）= true if（p <= q）/I（p <=r）.ceq（p U q）<=（r U s）= trueif（p< = r）/\（q< =s）. c e q （p R q）<=（r R s）= trueif（p< =r）/\（q <= s）.* 条件规则取决于<=关系ceq p/| q = p ifp <= q。如果p = q，则ceqp |/q =

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