论述总结：介绍了逻辑过程演算（LPC），一种支持异构系统规范的形式主义，扩展了语法和配备了行为序

URL：http://www.elsevier.nl/locate/entcs/volume 68. html18页s逻辑过程演算1兰斯·克里夫兰2美国纽约州立大学石溪分校计算机科学系GeraldLüttgen3大学计算机科学系英国She Schooleld摘要本文介绍了逻辑过程演算（LPC），一种支持包含操作和声明子规范的异构系统规范的形式主义。在语法上，LPC扩展了Milner在语义上，LPC配备了一个行为前序，它概括了Hennessy从技术的角度来看，新演算的特点是包含（i）最小和最大固定点运算符和（ii）标记不一致规范的过程项上的不可实现性谓词。LPC的效用是通过一个例子来证明的，这个例子突出了异构系统规范的好处1介绍在过去的二十年里，已经引入了大量的方法来正式指定其中大部分可以根据它们是基于进程代数[3]还是基于时序逻辑[28]来分类。The process–algebraic paradigm is founded on notions of 底层语义通常在操作上给出，而细化关系被形式化为前序。相比之下1研究支助是根据美国航天局第1999/2000号合同提供的NAS 1CCR-9988489。第一作者还得到了AFOSR Grant F49620-95-1-0508，ARO Grant P-38682-MA和NSF Grants CCR-9996086和INT-9996095的支持2电子邮件：rance@cs.sunysb.edu。3电子邮件：g. jackettgen @ dcs.shef.ac.uk。2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。2其中实现以操作符号给出然后，人们通过确立一个系统是其形式逻辑意义上的具体化的一个模型来验证前一种范式的优势在于它支持compo- sitional推理，即，可以独立于其他部件来细化系统部件。后一种范式的好处源于它对抽象规范的支持，其中不相关的操作细节可以被忽略。当所考虑的系统是有限状态时，这两种方法都可以以模型检查的形式得到自动支持本文的目标是为异构规范开发一种组合理论，该理论统一集成了基于精化的规范因此，我们提出了一种新的逻辑过程演算（LPC），它将Mil- ner更准确地说，我们表明，逻辑析取在LTμ可以理解为内部选择，补充CCS中的外部选择运算符，和逻辑合取在LTμ同步并行组合，补充异步并行组合在CCS中。此外，LTµ配备了两个递归运算符，一个最小固定点运算符和一个最大固定点运算符，分别允许递归的因此，LT µ中最大不动点算子所描述的行为根据这一讨论，LPC通过用于析取、合取和最小不动点的运算符以及基本过程真和假来扩展CCS秒2）的情况。LPC的语义基于De Nicola和Hennessy的测试方法[12]。这一理论的特点是，一方面使用转换来模拟过程和测试，另一方面根据过程对测试的反应来区分过程因此，我们为LPC项配备了一个转换关系，定义了规范可能参与的我们还引入了一个新的unimplementabilitypredicate，其作用是识别不一致的规范，如false，不能实现。转换关系和不可实现性谓词都是通过结构操作规则定义的，即，以语法驱动的方式。然后，我们将[12]中必须测试的定义带到我们的设置中，并表明由此产生的行为前序（i）保守地扩展了CCS规范之间的传统必须前序，(ii)是LPC中所有算子的合成，以及（iii）自然编码CCS过程和LTµ公式之间的标准满意度关系（参见秒3）。因此，我们的框架可以被看作是将基于精化和基于逻辑的方法统一到系统规范，同时促进基于组件的推理。从技术上讲，这种表现力来自LPC中过程和逻辑运算符的逻辑一致性，3通过我们对不可实现性的处理（cf.秒4）.实际上，该理论允许系统建模者使用两个系统操作符（例如，并行组合）和逻辑构造器（例如，合取）。这为工程师提供了强大的工具，可以在不同的抽象级别上对系统组件进行建模，并对组件的执行行为施加声明性约束（参见秒5）。2逻辑过程演算本节正式介绍我们的逻辑过程演算LPC。我们提出了它的语法，通过操作规则和一个新的单一性谓词定义了它的语义，并为它配备了一个过程上的精化预序，这是从De Nicola和Hennessy [12]改编的的LPC。LPC的语法扩展了Milner它还包括一个通用过程true的过程常数，而false将是我们微积分中的一个派生过程项。形式上，设Λ是一个可数的动作或端口的集合，不包括区别的不可观察的内部动作τ。每a∈Λ，我们关联一个互补动作a。我们定义Λ：={a|a∈Λ}，取A表示集合Λ<$Λ。通过定义a：=a，补语被提升到A在CCS中，一个动作a与它的补语a通信，产生内部动作τ。我们让a，b，。。在A和α，β，. 在Aτ上：= A {τ}。LPC的语法定义如下：P：：=0|TT|X|W| α.P|P + P| PP|P|P|PP|P\L|P[f]|µ x.P|µkx. P|vx. P其中k ∈ N，x是取自某个非空变量集V的变量，w是A上的无限词，其包含 将在下一 节讨 论， 集 合L<$A是 限 制集，f： Aτ→ Aτ 是 有限个 re-labeling。 有限重标记满足性质f（τ）= τ，f（a）= f（a），并且|f（α）/ = α}|∞.|<∞. 我们定义L：={a |a ∈ L}，并使用自由变量和约束变量、开项和闭项、警戒性和contexts.对于定点项μx.P、μ k x.P和νx.P，我们要求直觉，μx.P代表P的无限解绕，而μkx.P编码由k限定的P的无限解绕。一个项被称为我们指的是封闭的，有保护的，最 后，我们用来表示句法相等。4.对无交替过程的限制是出于连续性的原因，这将在后面进行阐述。请注意，无选择过程仍然允许人们表达公平性约束，这将在第2节中演示。五、4−→|−→ ⟨ ⟩ ∈虽然LPC包含所有CCS过程是显而易见的，但它是否也编码了所有无交替线性时间微演算（LT微演算）公式[5]并不十分清楚5LTµ公式的语法定义如下：Φ：：=0|TT|ff|X| ⟨a⟩Φ|Φ ∨ Φ |Φ ∧ Φ |µx。Φ |vx. Φ在我们的设置中，LTµ公式将被解释为无限的动作序列，也会导致死锁。这就是为什么“死锁公式”0包含在LT µ中的原因在LPC中，对应于项µ x.. x，从下面的语义定义中可以清楚地看到，对于a ∈ A，下一个运算符'a'对应于前缀运算符' a。'.LPC的语义LPC过程P的操作语义是一个标记转移系统<$P，Aτ，−→，#，P<$，其中P是状态集，Aτ是字母表，−→ <$P × Aτ× P是转移关系，#<$P是我们下面讨论的不可实现谓词，P是起始状态。转换关系由表1中显示的结构操作规则定义。为方便起见，我们将P，α，Pj写成PαPJ. 注意，对于CCS操作符，语义与[26]中完全相同至于其他构造，tt可以不确定地参与任何动作转换，或决定死锁（参见。规则（True1）和（True2））。过程α.P可能参与行动α，然后表现得像P一样（参见规则（行为1）），同样，无限词aw描述的过程可能参与其初始行为a，然后表现得像w（参见规则（行为2））。包含进程w的原因是为了能够在我们的计算中对任意系统环境进行建模，包括那些表现出不规则行为的环境。求和运算符+表示不确定的外部选择，使得P+Q可以表现得像P或Q，这取决于P和Q最初进行的通信。被环境所接受（cf.规则（和1）和（和2））。类似地，编码分离或非确定性内部选择，即，流程P-REQ在内部确定是否执行P-，而或Q（cf.规则（Dis1）和（Dis2））。进程P Q代表进程P和Q的异步并行组合，根据交错语义，在互补动作上进行同步通信，导致内部动作τ（参见规则（第1款）类似地，PSQQ编码P和Q的联合或同步并行组合，在所有可见动作上同步，在τ上交错（参见规则（Con 1）限制运算符\L禁止执行L中的操作，因此，限制了操作的范围。ProcessP[f]是一个例子，其中操作根据重新标记f重命名。剩下的规则定义了最小和最大固定点运算符的语义最小不5 μ LT比线性时间时态逻辑更有表现力，因此对无交替公式的限制不会强加不适当的表现力限制。5−→0f（α）−真1−tt−τ→a。TTAct1−α。P−α→P表1操作语义a∈ ATrue2tt−τAct2−aw−a →wSum1P−α→PJP+Q−α→PJSum2Q−α→QJP+Q−α→QJDis1−P<$Q−τ →PP−α→PJDis2−P<$Q−τ →QQ−α→ QJPAR1CON1Par3P|Q −α→PJ|QP−τ →PJP<$Q−τ →PJ<$QP−a→ P JQ−a→QJP |Q −τ→ P J|QJP−α→PJPAR2CON2Con3P|Q −α→P|QJQ−τ →QJP<$Q−τ →P<$QJP−a→PJQ−a→QJP<$Q−a→PJ<$QJP−α→PJResP\L−α→PJ\Lα∈/L<$LRelP[f]−→PJ[f]MU1k∈Nμ 2P[µ k−1x.P/x]−α→PJk >0µx.P−τ →µk x.PP[vx]。P/x]−α→PJνx。P−α→PJµkx. P−α→PJ通常P可以被解绕，如过程μkx.P所编码的那样（参见规则（Mu1）和Nu6（Mu2））。这里，P[Q/x]代表过程P，其中变量x的所有自由发生都被Q取代。这种对μ的解释可以被看作是一种连续性的体现：μ是根据它的有限展开来解释的由于与交替的最小和最大不动点相关的连续性问题，在文献[33]中有很7∨∨∧中文（简体）本文只考虑最大不动点过程νx.P可以无限地展开它的规则（Nu））。请注意，在某些过程代数[17]中用于描述无限内部计算并且已经在CCS[26]中表示的纯发散过程可以在LPC中导出为ν x.<$. x。表2不可实现性谓词#(i) µ0x.P#(ii) （P−→和P<$Q −→） 意味着PQ#(iii) （Q−→和P<$Q −→）意味着 产品编号(iv) P#意味着·α.P#·P[f]#·P\L#·P+Q#·Q+P#·PQ#·QP#·P |Q #·Q|P编号• νx.P#·μx.P#·μk x.P#，对于所有k∈N(v) P#和Q#意味着P<$Q#(vi) P[µk−1x. P/x]#im pliesµkx. P#，对于所有k>0(vii) （k∈N.µ k x.P#）表示µx.P #时间逻辑，包括LTμ，能够指定不一致或矛盾，即，行为等同于false。从操作的角度来看，描述不一致性的流程是不可实现的，因此应该忽略通过不可实现状态的流程运行。然而，由于逻辑析取，可以参与这种运行的流程本身不一定是不可实现的注意逻辑析取P Q的不可实现性和非确定性选择P+Q之间的区别：后一个过程P+Q表示一个完全可操作的过程，如果P和Q都是可实现的。相反，如果P或Q可以实现，则P Q可以实现。这种直觉反映在我们的不可实现性预测的定义中，如表2所示，其中我们对P∈#写P#，其中P−→α表示<$PJ∈ P。<$α∈ AτP−→PJ。 特别是，一个矛盾是在合取过程中，如果合取过程不能进行，在任何过渡中，尽管它的一个论证过程可以（参见规则㈡和㈢）。 举个例子，考虑流程A。0b. 0，对于aB. 此外，本发明还规则（iv）的第一部分指出，P的不可实现性通过前缀向后传播。 请注意，LPC8αin ∈L区分了不可实现的不一致进程和可实现的死锁进程。例如，两个过程（a. 0|B.0）\{a，b}和a. 0美元b。0不能参与任何转换。然 而 ，（a. 0美元b。0）#while <$（（a. 0|B. 0）\{a，b}）#）。 所有其他的规则都是直接的，除了最小固定点过程，例如过程μ0x.P，它不能进一步展开它的主体P，因此被认为是不可实现的（参见。规则（i））。连同规则（vi）和（vii），这意味着过程μ x.. x，它可以参与有限但无限数量的τ实际上，我们将把这个过程标识为假，并用假来表示它。正是这个定义使我们能够区分进程0和进程0。LPC的语义不仅扩展了标准CCS语义，而且与LTµ公式的语义兼容;参见Thm。三点五然而，这个定理并不简单，它的证明需要我们为LPC建立一个丰富的语义理论。在此之前，我们先介绍一些符号。过程sP的一个点是跃迁s（Pi-→Pi+1）0≤i k，对某个k∈N<${ω}，使得P0<$P. 如果<$（Pi#），对于所有0 ≤i< k，且对于i= k，如果k∈N，则π称为可实现路径，或简称为路径。我们使用|π|k是π的长度。如果|π|我们说π是无限的，否则π是有限的。 此外，π称为极大，如果|π|<ω和P|π|−→。π的迹线（π）定义为w：=（αi）Iπ ∈ A∞：=AA，ω其中eIπ：={0≤i<|π| |αi/≡τ}. 在Iπ=π的情况下，我们将t和w=（）。此外，如果π是有限的，我们可以写为P=wP|π| 对于π。我们表示P的所有有限、极大和无限路径的集合，由λfinn（P），λmax（P），和ω（P）。我们也可以为P引入相应的语言：Lfinn （ P ）： ={trace （ π ） |π∈trace （ P ） }<$P L max（ P ） 的 一种 有 限 迹 语 言 ： ={ trace（π）|π∈ λ max（P）}<$P L ω（P）的一种极大迹语言：={ trace（π）|P的有限迹语言中的π∈ <$ω（P）}<$A∞为LPC开发的语义理论依赖于发散的概念，即，系统进行无限内部计算的能力。在本文中，我们采用了De Nicola和Hennessy [12]使用的传统发散概念;在文献[6，27，29]的其他地方可以找到更复杂的定义。 过程P是发散的，符号为P，如果ω（P）。例如，过程<$：=vx.<$. x是发散的。一个过程P称为Wv发散的，对于某些w ∈ A∞，符号为P <$w，如果<$P J∈ P <$v

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