进程代数：确定性过程的等价性及其重要属性

理论计算机科学电子笔记162（2006）305-309www.elsevier.com/locate/entcs由于外延决定论的一致性A.W. Roscoe罗斯科1，2牛津大学计算机实验室沃尔夫森大楼，帕克斯路Oxford OX1 3QD，英国摘要一个过程是广义确定的，如果在任何迹s之后，给定任何事件a，它在s之后肯定接受或肯定拒绝a（稳定地）。我们展示了几个进程代数是如何能够表达这个属性，以及他们如何同意确定性过程的等价性。进程P的许多重要属性，包括连续性，可以根据某些上下文C[P]的确定性来捕获。保留字：决定论，连续性，进程代数，CCS，CSP1引言那些习惯于操作性地思考过程的人的第一反应自然是试图以这种方式理解关于过程的问题。操作语义自然地解释了进程代数中的不确定性是如何产生的：要么是由于τ操作的可用性引起的不确定性，要么是由于操作上的模糊分支因此，很自然地得出决定论的操作特征，例如禁止τ作用和模糊分支，以及米尔纳过程代数学家对决定两个非确定过程何时等价的问题很熟悉：我们的问题之一是，有意义的同余的范围非常大。这篇简短的论文表明，我们可以同意其余的过程，即确定性过程，并从一种形式主义的结果和对另一种形式主义的已知定义中获得洞察力1本文报道的工作得到了美国ONR的资助2电子邮件：bill. comlab.ox.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.098306A.W. Roscoe/Electronic Notes in Theoretical Computer Science 162（2006）305CSP具有长时间（例如，[1]，[2]）提供了我们可以称之为确定性过程的扩展定义：一个无发散的过程，并且永远不会既有迹s， {a}，又有故障（s，{a}）。在与LTS交互的标准解释下，这精确地对应于这样的陈述，即在任何跟踪s之后，对于任何事件a，如果{a}被执行，则确定a将发生，或者确定它将被稳定地拒绝。 这是最自然的决定， 一个过程的失败-分歧表示。有几种算法可以决定一个有限状态过程是否是确定性的：参见[6]，[7]。失败-分歧模型[8]对于过程是否是确定性的问题是完全抽象的这种确定性的定义可以转移到任何具有基于LTS的语义的语言中，因为过程的失败和分歧集很容易从LTS中计算出来。特别是它对CCS有意义，或者更舒适的CCS，其中无保护的递归被禁止，或者（遵循Walker [11]）被标记为递归并被视为发散的。它也可以翻译成测试的语言[3]：一个过程P是确定的，当且仅当P可能不惠P必须不惠如果t的形式为sω，对于s是有限迹，ω是这是直截了当地验证，在LTS的，这两个定义是等效的。两者都支持将决定论非正式地描述为可靠可测试的属性：在不同的场合进行相同的测试将产生相同的结果。他们与米尔纳的弱决定性概念略有不同s sJ J即如果P=<$Q且P=<$Q，则Q和弱双相似但没有太大的不同：如果P是无发散的，那么这也是等价的。在这两个过程代数中，两个确定的/弱确定的过程是等价的/弱双相似的当且仅当它们具有相同的迹集。我们可以得出结论，在CSP和CCS中：• 广义确定性过程的集合（即确定性/无发散的弱确定性过程的集合）实际上是相同的。• 两个进程代数都能够识别它们，并且（也许模初始τ）它们具有相同的等式理论。在本文的其余部分，我们将利用CCS和CSP的这种2个安保[10] ，[6]用惰性抽象L H（P）的确定性（其中H的事件被隐藏，但P可以非确定性地而不是像传统隐藏那样急切地获得），确定了从H到L的可证明的信息流的缺乏（设置划分P描述LH（P）的一种自然方式是A.W. Roscoe/Electronic Notes in Theoretical Computer Science 162（2006）305307as（P<$ChaosH）\H，其中H混沌H=停止H？x：H→混沌H是H上最不确定的无发散过程。我们总是假设P在这一节中是无发散的。CSP中严格的发散处理会导致一个问题：如果H事件的无限序列发生而没有L事件，它会将CSP项的值从上到下抛出。CSP中对此的解决方案是假设不存在发散，例如通过使用稳定故障模型来计算上述值。有一个替代方案产生于过程代数的连续性。命题2.1懒惰抽象LH（P）是确定的当且仅当过程（PH ChaosH）\H（以CSP）是弱确定的。由于各种原因，在CCS中，混沌H不能说是最不确定的过程。这将是有趣的调查是否抽象定义（P混沌H）\H（无论是与上述或一些CSP等效，但H混沌H）的CCS不等价定义具有CCS式等价的性质这类似于CSP中的惰性抽象的其他用途（参见[6]的第12章）。3功能与功能S在[4]、[5]中，Milner引入了连续过程的概念：P使得如果P=<$Q1，t t− s s− t且P=<$Q2，则存在R，其中Q1=<$R且Q2=<$R，其中s-t是由s组成的迹，其中t的事件根据从开始的多重性被删除。例如a，b，c，c，b，a我们可以很清楚地将这一点扩展到包含两个R是推论很容易被看作是弱决定性的暗示。这意味• 两个连续过程弱双相似当且仅当它们有相同的迹。• 一个过程是连续的，当且仅当它是弱确定的，并且有一个连续的迹集（即一个有s（t-s）的迹集，如果它有s和t）。连续过程具有许多吸引人的特性。在[9]中，作者提出了它们是布尔容限领域的有用工具（研究何时我们可以通过检查它们的无布尔类似物来建立布尔系统的性质下面的命题就是从这里引出的。308A.W. Roscoe/Electronic Notes in Theoretical Computer Science 162（2006）305命题3.1过程P是连续的和无发散的，当且仅当过程C [P]是外延确定的，其中在P的每个独立事件上 放 置 一 个单位指向内的缓冲器。这个结果的“如果”部分首先表明P本身是确定性的它的迹集是连续的：任何失败都会在C[P]中产生一个外部可见的非确定性。CCS和CSP对于外延决定性过程的对应性很容易地证明上述情况在CCS中也成立。事实上，这个证明可以被修改以建立以下稍微更强的结果。命题3.2P是连续的当且仅当C [P]是弱决定的。在[9]中，作者对函数过程得出了类似的结果：每个输出流都是输入流的函数的前缀，当没有输出挂起时不能它表明，（模的要求，其结构的输入是连续的）一个过程是功能性的，当且仅当把一个无界的确定性缓冲器（这一次适当地定向）在每个输入和输出通道创建一个确定性的过程。 从输出决定论的角度来看，其中输出能力和各通道的输出值例如，具有两个通道的进程P是缓冲器（在通常的CSP意义上[6]，其意义广泛）当且仅当BT[P]=COPY且COPY>>P是输出确定性的。其中，COPY是一个单位缓冲器，BT[P]将P与将外部输入传输到P并将P的输出传输到环境的过程并行放置由于存在多路同步，这在CSP中很然而以下定义在CCS和CSP中都有效（直到语法翻译）BT[P] =P[左分词，右分词]TT=左？x→a！x→b？y→right！x→TQb？y→right！x→左？x→a！x→TBT[P] =COPY表明P计算的函数（通过输出确定性条件存在）是恒等函数。T中的第二个子句（在检查的上下文中）的作用是确保P不会在每个输入中输出多个项。这提供了对非限定性规范的非常限定性的检查，这在CSP和CCS中同样有效A.W. Roscoe/Electronic Notes in Theoretical Computer Science 162（2006）305309引用[1] 布鲁克斯南达科他州，C.A.R.霍尔和A.W. Roscoe，A theory of communicating sequential processes，Journal of the ACM31，3，560[2] Brookes，S. D.，和A.W.陈文，一种基于多线程的并行计算方法，北京大学计算机科学研究所，1998。[3] de Nicola，R.，和M. Hennessy，过程的测试等效性，TCS34，1，83[4] 米尔纳河，[5] 米尔纳河，“Communication and concurrency”, Prentice Hall,[6] Roscoe，A. W.，“并发的理论与实践”，Prentice Hall计算机科学系列，Prentice Hall出版社，伦敦，纽约（1998），565页。相关网站web.comlab.ox.ac.uk/oucl/publications/books/concurrency/。[7] A.W. Roscoe，Finitary refinement check for infinitary specifications，Proc CPA 2004。可获自web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/96.pdf.[8] A.W. Roscoe，Revivals，Stuckness and Responsiveness，未出版的手稿（2005年）web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/105.pdf网站。[9] A.W.罗斯科，《对宽容，未出版的手稿（2005年），web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/106.pdf网站。[10] A.W. Roscoe，J.C.P. Woodcock和L. Wulf，Non-interference through determinism，Journal ofComputer Security4，1，27[11] 陈文辉，陈文辉（1990），资讯与计算，第85卷，页202-241。