序列过程的合成性质

理论计算机科学电子笔记118（2005）111-128www.elsevier.com/locate/entcs序列过程的合成性质詹乃军LehrstuhlfuürPraktisscheInformatikIFacultürMmatikundInformatikMannheimUniversitüatD 7，27，68163 Mannheim，Deutschland电子邮件：{zhan}@ pi2.informatik.uni-mannheim.de摘要模块化方法是描述和验证复杂系统以避免组合爆炸的最有效方法之一。FLC（Fixpoint Logic withChop）是一种重要的模态逻辑，因为它具有表达性和逻辑特性，例如，严格来说，它比微演算更有表现力。本文研究FLC的组合性，即研究逻辑的连接词与程序的构造词之间的联系 为此，我们将FLC与其他参数设置为“+”（F L C +用于扩展），然后建立逻辑与带死锁的基本进程代数的对应关系，终止（缩写为BPAc）。最后，我们表明，作为对应的副产品，δcBPAδ到强（观测）互模拟的过程的特征公式可以直接从过程的语法构造。关键词：chop算子，模态逻辑，组合性，验证，互模拟，特征公式，进程代数1介绍人们越来越需要可靠的方法来设计正确的反应系统[9]，如计算机操作系统和空中交通控制系统。这些系统的特点是持续的，通常是非终止的和高度不确定的行为。这样的系统通常用于对“安全关键系统“进行建模航空交通控制系统、核反应控制系统等。由于这些系统的任何错误行为都可能带来灾难性的后果，1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.12.018112N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111对预期行为的尊重是不可避免的。有一个共同的协议，形式化的方法，如模态和时序逻辑[17，24]和进程代数[3，10，19]，是有效和可靠的方法来设计这些系统。由于大型系统的复杂性通常是不可控的，因此开发此类系统的方法必须是组合的（垂直或水平），以避免在指定和验证它们时出现组合爆炸，例如[10，19，3，2，16，4，5，15]。组合方法允许人们通过用定义的构造器组合现有系统来构建一个大系统，并将复杂系统的正确性问题简化为子系统的类似和更简单的正确性问题FLC [18]是µ-演算[12]的扩展，带有顺序合成运算符-“chop”（用“;“表示）。[18]指出FLC比μ-演算更严格地表达，因为[6，11]证明了只有[13，14]研究了FLC模型检查的问题。组合性在[8]中被描述为一个重要的要求，也应该被过程代数设置中使用的指定逻辑所满足，即任何程序构造函数cons对应于逻辑的运算符cons，使得(a) Pi|= φi，其中i = 1，.，n暗示cons（P1，...，Pn）|= cons（φ1，...，φn）;(b) cons（P1，.，Pn）|= cons（φ1，.，φn）是可以从P i推出的最强断言|= φi，其中i = 1，.， n.显然，FLC不满足上述条件，因为P满足φ，Q满足<$，但我们不能根据FLC中的φ和<$，得到任何在组合系统P+Q中成立的性质。为了保证特定逻辑满足上述条件，我们有两种选择：一种是证明对于进程代数中的每个构造函数，可以在逻辑中定义相应的连接符。据我们所知，到目前为止，在经典模态逻辑中是否可以定义一个合适的“+”仍然是一个悬而未决的问题;另一个是直接将一个连接符引入逻辑中，它与进程代数中的构造函数完全对应，例如，在[8，15]中，显式地引入了非确定性选择此外，进程代数的序列合成与FLC的“chop”算子之间的联系也值得研究本 文 首 先 用 一 个 非 确 定 性 算 子 “+” （ 由 FLC+ 表 示 ） 推 广 了 FLC.Intuitively，P|=φ+φ意味着P包含两个部分P1和P2，这两个部分非确定性地执行，使得P1|= φN. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111113|δδ^调整安装挡风玻璃得到汽车控制得到汽车调整控制安装挡风玻璃放车P2=0。然后我们证明了算子+，;和νX。在逻辑中涉及+、;和rec x在进程代数设置中，例如基本进程代数终止和死锁（BPA）简而言之）。 因此，我们可以声称逻辑是合成的。更重要的i) 这意味着进一步利用过程项的结构进行模型检验。ii) 它允许给出某些非决定性系统的精确和紧凑的规范。iii) 当系统行为的附加替代方案应该被承认时，修改系统的规范是非常容易的。iv) 它增强了模型检测中模块化的可能性，这对系统的重新设计是i) 这取决于是否有可能为FLC+设计一个语法导向的模型检查器。事实上，我们相信，这可以利用本文件中存在的FLC+和BPA之间的联系来完成。为了在此列表中显示ii)，iii）和iv），我们给出以下示例：考虑想要建立图1中所示的装配线的汽车工厂，放车Fig. 1.过程P我们用过程P来表示，对于一个生产步骤。如果有一辆汽车可供P使用，那么P要么得到汽车，调整电机，安装挡风玻璃，控制汽车，并将汽车放在传送带上，要么得到汽车，安装挡风玻璃，调整电机，控制汽车，并将其放回。P可以重新开始第一个选项可以指定为规格1=[get car];调整调整;安装挡风玻璃;控制;放车第二种情况描述为：114N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111^^^^^δδ规格2=[get car];安装挡风玻璃;调整挡风玻璃;控制挡风玻璃;放车挡风玻璃你真会开车。我们现在正在寻找一种规范，它只允许这样的系统，即既包含两种选择，又可以很容易地从规范1和规范2构造出来。显然，规范1和规范2是不合适的，而规范1和规范2允许只表现出其中一种行为的实现。规范1+规范2描述了我们所考虑的行为和一个重复执行此行为的系统P描述了规格= νX。（规范1+规范2）; X.这将表明，rec x。（P1+ P2）; x| =第4节示例4.9中的质量标准，其中P1= get car; adjust; mount windscreen; control; putcarP2= get car; mount windscreen; adjust; control;put car.现在让我们假设系统规范应该被修改以允许第三种替代行为规范3，那么这个规范可以简单地规格J= νX。（规格1+规格2 +规范3）; X.如果我们建立P3|= Spec 3那么我们立即得到，rec x.（P1+ P2+ P3）; x |=质量标准J。此外，如果我们必须将Spec 1修改为Spec J1，使得P1J|=规格J1，并获得rec x.（P1J+ P2+ P3）; x |= νX。（规格J1+规格2+规格3）; X.本文的其余部分组织如下：在第2节中简要回顾了一些基本概念;在第3节中定义了FLC +的合成和语法;在第4节中建立了FL C+的构造函数之间的联系。BPA表示FLC+的连接;在第5节中，给出子一个用于计算过程P∈BPA的计算器P的总体结构，该计算器将所有系统连接起来，我们证明了P的特征公式是P的组合性最后，在第6节中提供了一个简短的结论。2预赛设Act是一组有限的（原子）动作，由a，b，c，. . ，并且是由x，y，z，. .顺序过程术语是那些不涉及并行性和通信的术语，它们由以下语法生成E：：= δ|X|一|E1;E2|E1+E2| recx.E|rec x.EXN. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111115JSP∈ XδT P不一11一1一一21我们用Ps表示上述语言。直觉上，我们认为Ps的元素表示程序;δ表示不能执行任何动作并永远停留在那里的死锁进程;δ表示不能继续进行但立即终止的终止进程;其他构造函数可以是像往常一样构思。在存在顺序组合运算符“;”的情况下，设s是包含n的最小集合，并且在规则下是封闭的：• 如果T（E1）和T（E2），则T（E1;E2）和T（E1+E2）;以及• 如果T（E），则T（rec x.E）。约定：为了简单起见，作为良构条件，例如E=E1+E2，其中T（E1）和<$T（E2）或<$T（E1）和T（E2）是禁止的。一个变量x∈ X的出现在表达式Ei中被称为自由的，它不出现在形式为recx.E的任何子项中，否则称为有界的。我们将使用fn（E）来表示在E中有一些自由出现的所有变量，而bn（E）表示在E中有一些约束出现的所有约束变量。一个变量x在一个项Ei中被称为保护的，x的每次出现都在一个子项F中，其中F位于一个子表达式F; F使得<$T（F）。 如果所有变量都出现，则项E称为保护项其中，有看守。的所有封闭和保护项的集合本质上对应于基本进程代数（BPA），其中终止进程δ和死锁进程δ（用BPA δ表示）的范围为P，Q，.BPA是ACP的亚片段[3]。例2.1表达式a; x，a;（b + x），rec x. （a+b）;x;（y+z），δ，δ是有保护的，而x，a+x是无保护的。Ps的操作语义由以下推理规则给出：E[rec。xE/x]→aEJa→α1rec. E1→E1JE→EJE→EJ和（E）E1;E2→E1J;E2aNdE1→E1JE1;E2→E2JE1+E2→E1J和e2+E1→E1J定义2.2二元关系S×BPA称为强双辛，δ δ如果（P，Q）∈ S蕴涵一一一法RecSeq-11序列22116N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111δδ∈∼δєδδ将缩写为。j=1• （P）i• 当P→a∈Act时;以及• 当Qa∈Act.那么对于QJ， Q→a则对于PJ， P→aQJ和（PJ，QJ）∈ S，对任意PJ和（PJ，QJ）∈ S，给定两个过程P，Q∈BPA<$，我们称P和Q是强双相似的，记为P<$Q，如果对某个强互模拟S（P，Q）∈ S.我们可以将Ps上的定义推广为：设E1，E2∈ Ps，fn（E1）<$f n（E2）<${x1，.，xn}。 如果E1{P1/x1，.，Pn/xn}{P1/x1，.，Pn/xn}对于任何P1，... ，PnBPA，然后E1E2。[1]证明了以下关于BPA的证明系统是完备的1：A0E1 +E2=E2+E1A1（E1+E2）+E3=E1+（E2+E3）A2E+E= EA3（E1+E2）;E3=（E1;E3）+（E2;E3）A4（E1;E2）;E3=E1;（E2;E3）A5rec x.E =E{rec x.E/x}A6E +δ=EA7δ;E=δA8E;E=EA9E;E=E在[1]中，还证明了以下引理。引理2.3对于任何P∈BPA，P<$iaa;Qa，j或P<$δ，其中Qa，j∈ BPA <$. 注意，如果对于所有a∈Act，ia<1，则拉吉阿a;Qa，j记法：从现在开始，我们用A op B代表{E1op E2|E1∈s s sA和E2∈ B}，Aop E对于Aop{E}，其中E∈ P，A <$P，B <$P，并且op∈{+，;}.3带不确定算子“+”的FLCFLC是Marku的Mulller-Olm[18]的结果，它是现代微演算的一种新形式，可以表示非正则性质.因此，它比μ-演算更严格地表达，因为[6，11]证明了只有正则性质可以在μ-演算中定义在这里，我们用一个非确定性算子“+"来扩展FLC1.本文提出的BPA的证明体系与文献[1]中的证明体系略有不同。但[1]指出，该变体仍然是完整的。一一δa∈Actj=1a∈ActN. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111117√ⓍⓍδ →δ2δδδHHδ√δδδδ根据两个组件的组合属性，可以非确定性地执行因图利山口|= φ1+ φ2意味着P由P1和P2组成，它们是非确定性执行的，使得P1满足φ1，P2满足φ2。3.1语法和语义令X，Y，Z，. range over an infinitite set Var of variables，true andfalse是命题常量，而对于另一个特殊的命题常量，用于指示过程是否终止。FLC+的公式由以下规则生成φ：：=真|法阿尔塞|√ |term |X|〔一〕| |φ1∧ φ2|φ1∨ φ2|φ1; φ2|φ1+ φ2|µX.φ |νX φ其中X∈V ar，a ∈ Act。√在续集中，我们使用或为，或为。[a]表示“真”，“假”或“假”，得双曲正弦值.正如在模态μ-演算中，两个定点算子μX和νX绑定各自的变量X，我们将应用变量在公式中的自由和绑定出现的常用术语，封闭和开放公式等。我们将使用fn（φ）代表在φ中有一些自由出现的所有变量，而bf（φ）代表在φ中有一些绑定出现的所有变量。我们假设X在φ中被保护，如果X的每个出现都在前面有一个通过如果φ中的所有变量都是保护的，那么φ就被称为保护的。或p实施例3.1公式X; X，V X。（ab）; X;（Y + Z），假; X是被保护的，但是X，aX，μX。（X+Y）[a]不受保护。与[18]一样，公式被解释为单调谓词Transformer这是一个简单的映射f：2BPAcBPAc 这是单调的w.r.t. 的2 BPA上的包含排序c.我们使用MPT来代表所有这些单调的与BPA变压器等同。MPTT与包含排序定义为ffJif（A）fJ（A）for allA BPA形成完整的晶格。 我们用和表示连接和相遇运算符.根据Tarski-Knaster定理，单调函数的最小不动点和最大不动点：（2BPAc→2BPAc）→（2BPAc→2BPAc）存在. 该方法用于为多个FLC+的计算结果提供解释。true和false的含义以标准的方式解释，即分别由BPA解释。 的意义是映射任何一组进程不118N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111一一∈єC（A）={P∈BPA|T（P）}ρδ一δδδδρδδρδδ√єє到包含所有终止进程的BPA队列的子集所以δ过程P满足i ∈T（P）。 术语被解释为身份。 因为，δ在有δ存在时有不同的行为，它们应通过FLC+加以区分。因此，FLC+的[a]被解释为一个函数，该函数将任何进程集合映射到其中每个进程都不被终止并且必须包含该进程的每个a这与FLC中给出的[a]的含义因此，根据我们的解释，P| [a]仅当<$T（P）。 而对于任何P∈BPA，P总是满足[a]，δ在刚果解放阵线。所以，很容易证明，不满足a∈Act [a]; f alse，而a Act[a];f alse是δ的特征公式。变量的含义由环境ρ：var→（2BPAc→2BPAc）给出，该环境分配变量到集合到集合的单调函数 ρ [X~f]与ρ一致，除了将f与X相关联。定义3.2给定一个环境ρ，用Cρ（φ）表示的公式φ的意义归纳定义如下：Cρ（真）（A）= BPAδCρ（false）（A） =δCρ（term）（A）=ACρ（X）=ρ（X）C（[a]）（A） ={P∈BPA<$|<$T（P）<$$>PJ∈BPA<$. P→aPJ<$PJ∈A}C（A） ={P∈BPA<$|<$PJ∈BPA<$. P→aPJ<$PJ∈A}Cρ（φ1<$φ2）（A）=Cρ（φ1）（A）<$Cρ（φ2）（A）Cρ（φ1<$φ2）（A）=Cρ（φ1）（A）<$Cρ（φ2）（A）Cρ（φ1;φ2）=Cρ（φ1）·Cρ（φ2）Cρ（φ1+ φ2）（A）={P ∈ BPA δ |P1，P2∈ BPA δ.P <$P1+ P2<$P1∈ Cρ（φ1）（A）<$P2∈Cρ（φ2）（A）}Cρ（μX.φ）= H{f∈ MPT T|Cρ[X~ f]（φ）<$f}Cρ（νX.φ）= H{f∈ MPT T|Cρ[X~ f]（φ）<$f}其中A BPA，·代表函数上的复合运算符由于封闭公式φ的意义与任何环境无关我们有时把C（φ）写成Cρ（φ），其中ρ是任意的环境。我们也滥用φ（A）来代表C ρ（φ）（），如果ρ在上下文中是清楚的。满足给定闭公式φ的过程集是φ（BPAφ）。一个过程P被称为满足φ i <$P∈Cρ（φ）（BPA <$），对于某个环境ρ，记为P |= ρφ。 如果ρ从上下文中是清楚的，我们直接写P |= φ。N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111119δδφ表示Cρ（φ）（A）<$Cρ（φ）（A），对于任何A <$BPA <$和任何ρ。φ惠惠指（φ惠）（惠φ）。其他符号可以用标准的方式定义给定一个公式φ，φ末尾的子公式集，用ESub（φ）表示，是：{φ}，如果φ=p，term，X或λa;ESub（φ1）<$ESub（φ2）ifφ=φ1opφ2，其中op∈ {φ，φ，+};如果φ = φ1;φ2则如果τ/∈ESub（φ2）则ESub（φ2）elese（ESub（φ2）−{τ}）<$ESub（φ1）;ESub（φJ）if<$φ=σX。φJ。我们现在在哪只发生在φ的末尾，这意味着只能在ESub（φ）中作为一个φ的子公式约定：接下来，我们假设逻辑运算符之间的约束优先级3.2关于FLC+的几个定理在这一小节中，我们证明了FLC+的一些定理，这些定理将在后面的文章中使用。事实上，我们可以证明[18]中所示的FLC上的所有性质对于FLC+仍然成立，例如，FLC+严格来说比μ-演算更具表达性，FLC+对于有限状态过程是可判定的，对于上下文无关过程是不可判定的，等等。此外，我们还证明了FLC+具有树模型性质，即定理3.3给定P，Q∈BPA<$，且P<$Q，则对任意闭公式，FLC +的φ，P| = φ i Q| = φ。定义3.4我们定义FLC+的一个子类，用N表示，如下所示：φ：：= p|拉瓜|φ∧φ|φ+φ|a其中a∈Act，n∈FLC+。通过定义FLC +的语义，φ; trueφ; true意味着对于任何进程P和环境ρ，P|= ρφ蕴含P| = ρπ。为方便起见，我们将φ;真惠;真惠。下面的定理表明了FLC+的命题字母、连接词之间的关系。120N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111δE E EFδδδ12定理3.5N1 长期优惠P2φ +false惠falseP3p +p惠pP4aT2优惠[a]; true优惠alseS1 φ+优惠价+φS2（φ+φ）+普惠φ+（φ+φ）S3φ +φ参与φ如果φ∈ NSIφ+（）（φ+）（φ+）SDφ+（）惠（φ+）（φ+）SC（φ+）;惠（φ;）+（;）C1φ;→φC2 （φ;）;惠φ;（;）IC（φ）;惠（φ;）（;）DC（φ）;惠（φ;）<$（;）SD [a];φ1+[a];φ2Participate[a];（φ1<$φ2）下面的定理说“定理3.6（i）如果φ，则φ;;和;φ;（ii）如果φ1<$φ2且φ1<$$>2，则φ1+<$1 <$φ2+<$2。通过扩展[13]中给出的FLC基于tableau的模型检查器，使用“+"规则（+）（E，F）φ1+φ2E=E+E（E1，F）φ1（E2，F）φ2其中，1，2，BPA= 0，我们可以得到一个FLC+的模型检测器，其复杂度与[13]中提出的FLC的模型检测器的复杂度相同。4FLC+与BPA的对应关系在本节中，我们将讨论如何从顺序流程的组件中导出其复合属性4.1非决定论很明显，BPA的“+”和FLC +的“+”之间的连接表示如下：定理4.1（i）对任意P，Q ∈ BPA，若P |= φ和Q |= P + Q |=φ+φ;（ii）对于任何R ∈ BPA，如果R |= φ + φ，则存在P，Q ∈ BPA φ，使得δ δRP + Q，P| = φ和Q| = 0。N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111121|√P√||||⟨⟩|⟨ ⟩|⟨ ⟩ ⟨⟩√4.2顺序组合在这一小节中，我们证明了进程代数的序列合成可以用chop算子来刻画。通常，P=φ和Q=φ，但P;Q=φ;φ，因为φ可能只描述了P的部分执行。例如，设P=a;b，Q=c;d。 很 因此，我们要求;的第一个操作数的属性必须指定相应进程的完全执行，即P=φ;。这类似于Seq-2规则的前提，即只有在;的第一个段P完成执行之后，才能执行第二个段另一个问题是，通过定义s的语义，P.因此，在所得到的公式中应省略关于中间终端的性质。 否则，组合属性不拿着你的手 例如，l∈P=a;φ和Q=b;δ，φ=a; ，and= 我不想这样|=φ;且Q|=P;Q|=φ; SO，WE将用项代替φ中的发生，因为项是快点这是符合的，即，“”是一个中性元素的顺序组成此外，由于φ{term/m};P;Q的可实现性，作为φ的子公式，使得φ的子公式后面跟着;在用P1计算φ的意义时，在计算φ{tem/m}的平均值时，平面不是一个微不足道的角色。 };. E. G.ϵ|=;[a];ba nda;c|=a;c，but;（a;c）|=（term;[a];b）;（a;c）. 那么，这样的要求是合理的，因为定理3.5可以将所有公式等价地转化为这样的形式。一句话，我们有以下关于序列合成“;"的定理：TheoreM4. 2如果φ的端点仅作为一个子公式，则P|=φ;φ和Q| = n，则P; Q| = φ{term/};注4.3一般说来，定理4.2的逆命题是无效的，e. G.（a;b;c+a）（a）（b）（c）（d）|=a;（b;c;c），但我们不能得出结论，a; b; c + a |=a;和c; d |=b; c;c。4.3递归在本小节中，我们将研究如何将rec x与νX联系起来。因此，在本小节中，所有出现在公式中的不动点算子都将引用ν，如果没有另外说明的话。为此，我们首先定义了一种称为语法的关系。我们要求只能作为子公式出现在φ的末尾事实上122N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111tue（E）=^sPt^erm（E）=^E^φ（E）=^φ（E）^ ^您的位置：φ（E）=^φ（E）;φ（E）=^φ·φ（E）12 11^^ ^您的位置：√^^^ ^您的位置：X^（E）=^{x;E|E∈E}φ^过程和公式之间的确认，类型为Ps×FLC+›→{true，false}，表示为|= sc。定义4.4给定一个公式φ，我们将一个从2Ps到2Ps的映射与之联系起来，用φ表示，它由以下规则构造^（E）=^{E|E∈P s< $ T（E）}f^alse（E）=^^a|EJ∈E。E→aEJ}[a]（E）={E|T（E）E→aφ^φ^φ^EJ∈E}1+φ2（E）=^{E|E1，E2E=E1+E2<$E1∈φ^1（E）<$E2∈φ^2（E）}σ^X。φ（E）={（recx. E1）;E2|E1∈φ（{φ}）<$E2∈E}其中，E =S。|= sc（E，φ）= false。|= sc(E, φ) = false.在这里，我们表示|= sc（E，φ）=真|= scφ且|= sc（E，φ）= false by E| = scφ。非正式地，P| = scφ意味着P和φ具有类似的语法，例如rec x. [（a; x; x; b）+c]|= scνX。[（a; X; X;b）c]。下面的定理指出，|= sc本身也是合成的。定理4.5设φ1、φ2和φ的末尾只出现一个子公式。然后，i) 如果E1|= scφ1和E2|= scφ2则E1+ E2|= scφ1+ φ2;ii) 如果E1|= scφ1和E2|= scφ2则E1; E2|= scφ1{term/iii) 如果E| = scφ，则rec x.E| = scσX.φ{term/}。};φ2;例4.6设E1 =（a; x; x）+d，E2 = x;（b + c）; y，E3 = a; b; c，φ = a; X; X，φ= X; b; Y且φ =[a];b;c。很明显E1| = scφ，E2|= sc，E3|= sc，E1+ E3|= scφ +φ ， E3; （ E1+E3 ） |= scφ; （ φ + φ ） 和 rec x 。 接 收 器E3; （ E1+E3 ） |=scνX.νY。（φ;φ+φ），定义4.4。N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111123|||δ||下面的引理表明，用=替换=sc，过程和公式之间的关系通过替换而保持，即，Lemma4. 7Lettfn（E）<${x1， . . ，xn}，fn（n）<${X1， . . ，Xn}。IfE|=sc且Pi=φi;那么，哪里在φ i中也不发生，因为i∈ {1，.，n}也不E{P1/x1，.，Pn/Xn}|={φ1/X1，.， φn/Xn};定理4.8建立了=sc和=之间的联系，因此我们可以把rec x和νX联系起来。例如，在上面的例子中，我们得到rec x. 接收器E3;（E1+ E3）|= νX.νY。（φ;（φ + φ））。第四章. 8若P∈BPAφ，则φ仅在φ和P的端点处发生|=scφ，thenP|= φ;.为了演示如何应用FLC+的组合性来简化反应系统的验证，我们继续第1节中给出的汽车工厂的例子。例4.9在这个例子中，根据定义4.4，很容易证明P1|= SC规格1和P 2|= sc规范2。所以我们rec x.（P 1+ P 2）; x |= scνX。（规格1+规格2）;X定理4.5 此外，可以得出结论，rec x.（P 1+ P 2）; x |= νX。（规格1+规格2）;X定理4.8 也就是说，P|=质量标准5序列过程特征公式的构造给定过程上的等价或预序≤，过程P的特征公式为φP，使得给定过程Q，Q| = φP当且仅当Q≤P。特征公式可以用来将关于过程的等式推理与模态逻辑中的推理联系起来，因此允许在逻辑框架中进行关于过程的证明。 [7]建议通过定义一个从有限CCS项到模态逻辑公式的转换函数，导出有限CCS项到强互模拟和观测同余的 [23]建议 一种从有限状态过程的转移图中定义前序的特征公式的方法，并将其方法应用于有限状态CCS-强（弱）互模拟项。 [18]提出了一种方法，124N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111δ=^^^δ∈ Pєδ的公式，以及为。δ=^Φδa=^Φ−{a}X=X通过求解由进程语义（进程的重写系统）诱导的方程系统，可以将在这一节中，我们提出了一个算法来构建的特征公式，在BPA中，达到强互模拟直接从其语法的组合方式的基础上，上述结果。这是一种表示ata∈Act[a]的方法;false（Φδforst）是特征吧为方便起见，a∈Act−A[a];false从现在起将缩写为Φ−A定义5.1给定一个过程项E∈Ps，我们将它与一个由下列规则导出的公式联系起来，该公式记为εEΨє^E1;E2=E1+E2=^E1+E2};blog2√C.X.E=νX。{term/}关于EEE，我们有引理5.2对于任意的 Es，k只作为子公式出现在k E的末尾.引理5.3对任意E∈Ps，E| = sc E和E| = sc E;本节的其余部分致力于证明，对于每一个P∈BPA<$， <$P ;<$是P到<$的特征公式。下面的引理说BPA的证明系统（见第2节）在FLC+中，如果P被替换为CUP，则将有效;δ和=由惠。 也就是说，引理5.4A0E1+E2;惠E2+E1;A1E1（E1 + E2）+E3; E2（E2 +E3）; E2（E2）+E3; E3（E1; E3）+（E2; E3）; E3（E1; E3）;E4（E1; E2）; E3（E2; E3）; E4（E1; E3）; E5（E1; E2; E3）;E6（E2; E3）; E7（E3）; E7（E1; E2; E3）; E7（E3）; E7（E1;E2; E3）; E7（E3）; E7（E4）; E7（E1; E2; E3）; E7（E3）; E7（E7; E7）; E7（E7; E7）; E8（E7; E8）; E8（E8; E8）; E9（E9;E9）; E9（E9; E9）; E9E;优惠券E{recx. E/x};A6E+δ;惠E;A7δ;E;惠δ;惠δA8[医]甲磺酸钠The mixture was stirred atroomtemperaturefor10 minutes.N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111125δδ^ ^您的位置：^通过上述引理和BPA的证明系统是com的事实在[1]中，很容易证明以下定理：定理5.5（完备性）如果E1<$E2，则<$E1惠<$E2。下面的引理在定理5.7的证明中起着关键作用。引理5.6对于任何P∈BPA<$，如果<$T（P）且不存在PJ使得P→aPJδ然后是[a]; false。定理5.7对任意的P ∈ BPA <$，<$P;<$是P的特征公式。注5.8在定理5.7中，条件P被保护是必要的。否则，定理不再为真，因为引理5.6将不再有效没有条件。 或者在一个，VX。（X+（a <$$>[a]<$Φ−<${a}））isequivalentcx. （x+a），nevertheless，（vX. （X+（a< $$>[a]<$Φ− {a}）;不是car-rec x的特征公式（x + a），因为rec x. （x+b+a）满足公式也是，但是rec x。（x + b + a）/x. （x+a）。例5.9设P = a; δ，Q = b; δ。然后，P=（a[a] Φ −{a}）;，并且<$Q=（<$b <$ $>[b]<$Φ−{b}）;Φδ定义5.1很一个Q。 根据定义5.1，阿雷克X。（P;x;x;Q+P）;=^νX。（a[a]Φ−{a}）;X;X;（（b[b]Φ−{b}）;Φδ）;，+（a<$$>[a]<$ Φ−{a}）这就是rec x的特征公式。（a;x;x;b;δ+a;δ）。6相关工作和结论由于模块化方法在开发大型系统中起着关键作用，因此在这方面已经做了许多例如，[20]从逻辑的角度研究了这样的而[10，19，3]则是从代数的角度来研究这个问题的，即把系统的具体化和实现表示为一个过程，用过程上的几种等价来描述具体化和实现逻辑的优势在于抽象，但不容易实现。 与逻辑相比，实现进程代数甚至进程代数是很容易的126N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111|⟨⟩⟨ ⟩∧ ⟨⟩δδ||δ代数本身可以看作是一种编程语言，例如[10]，但它缺乏抽象性。虽然建立的等价性使进程代数本身可以用作一种规范语言，但它并不是[15]中所讨论的理想候选者。因此，开发大型系统的一个合适的方法是使用逻辑作为规范语言，使用进程代数作为建模语言。[4，5]研究了Choppy逻辑[22]的组合性，Choppy逻辑是经典命题时态逻辑[21]（简称PTL）通过引入Chop算子的扩展。[15]定义了一种具有组合性的模态过程逻辑。但逻辑只能表示过程的正则性质[18] 用chop算子（FLC）扩展了µ-演算，它可以定义非正则性质，因此比µ-演算更严格地表达。[13，14]讨论了FLC的模型检验问题。然而，FLC没有组合性，例如， Q| = νX。[a];b;X;X;c d（简称φ）且P = νX。[a];c;X;X;c d（简称φ），但很难找到一个基于φ和φ构造的公式，该公式满足P+Q。为了建立BPA与而FLC，我们引入了一个不确定的，最小运算符所以，FLC+具有组合性。例如，在上面的例子中，我们将看到P+Q|=φ+ φ。为了根据子系统的性质导出递归过程的不变性质，我们定义了一个名为“语法构造”的概念，表示为：|= sc，BPA和FLC+之间，并表明，|= sc本身是如果P=scφ，则P=φ，其中所有不动点算子在φ中出现的只指最大的一个。FLC+的组合性的一个副产品是我们提出了一个算法来直接构造BPA分解的与[18]不同，本文通过求解由进程语义导出的方程组（进程重写系统），导出了进程的特征公式。本文不考虑并行算子的组合性.|“.此外，如果我们重新解释模态[a]和[a]，可观察等价的特征公式也可以在逻辑中组合地构造确认特别感谢Mila Majster-Cederbaum教授的指导和与本文相关主题的许多富有成效的讨论。作者还感谢匿名的参考者对本文的有益评论。N. Zhan/Electronic Notes in Theoretical Computer Science 118（2005）111127引用[1] L. Aceto和M.轩尼诗终止、死锁和分歧。Journal of ACM，Vol. 39，No.1：147-187. 1992年1[2] L. Aceto和M.轩尼诗进程代数中的动作细化。信息与计算，103：204-269。一九九三年[3] J.A. 伯格斯特拉 和J.W.克洛普抽象通信过程代数。理论计算机科学，37：77-121。一九八五年[4] H.巴林杰河Kuiper，A.普努埃利现在你可以编写时态逻辑规范了。在Proc.16thSTOC，pp.51-63.一九八四年[5] H.巴林杰河Kuiper，A.普努埃利一种类似CSP语言的组合时态方法。 在IFIP会议上，抽象模型在信息处理中的作用。207-227. 1985.[6] E.A.爱默生和C. S.朱特拉树自动机，μ-演算和确定性。第33届IEEE Symp.在发现。的Comp.科学，一九九一年[7] S. Graf和J. Sifakis。CCS有限项上观测同余的模态特征。信息与控制，68：125-145。一九八六年[8] S. Graf和J. Sifakis。描述非确定性程序及其性质的一种逻辑。信息与控制，68：254-270。一九八六年[9] D. Harel和A.普努埃利关于反应系统的发展。在K.R. Apt，editor，Logics and Models ofConcurrent Systems，Volume 13 of NATO，ASI Series，pp. 447-498. Springer-Verlag，1985.[10] C.A.R. 霍尔通信顺序进程。普伦蒂斯-霍尔，1985年。[11] D. Janin和我瓦鲁凯维奇关于一元二阶逻辑的命题μ-演算的表达完备性。CONCUR'96，LNCS1119，第263 -277页。Springer-Verlag，1996.[12] D.浩善命题μ演算的结果。理论计算机科学，27：333- 354。一九八三年[13] M. Lange和C.斯特灵使用chop对固定点逻辑进行模型检验。FOSSACS 250-263. 2002年。[14] M.兰格不动点逻辑的局部模型检验博弈。CONCUR 240-254. 2002年。[15] K.G. Larsen和B.我是杰森模态过程逻辑。在LICS'88的proc中，第203 -210页。IEEE计算机科学学会，1988年。[16] M. Majster-Cederbaum和F.萨尔格面向反应系统的分层验证