CSP的余代数导论：通信序列过程和部分自动机的密切关系

URL：http://www.elsevier.nl/locate/entcs/volume 19. html20页sCSP的余代数导论乌韦沃尔特1FBInformatikTechnischeUniversitaütBerlinD-10587 Berlin，Germany摘要本文给出了对HOARE在[3]中引入的通信序列过程概念进行共代数分析的第一步。我们使CSP和部分自动机之间的密切关系变得明显，即，特殊余代数因此，事实证明，[3]只处理非常特殊的自动机，即最终自动机，即，自动机，其中状态和过程的概念之间的差异，分别消失。共代数的方法将使我们能够开发一个适当的模型理论的过程演算。作为这个方向的第一步，我们首先概述了过程上的操作如何以兼容的方式推广到自动机上的构造。其次，提出了一种求解递推过程方程的新方法。最后，我们讨论了CSP中的不确定性可以不能基于通常在共代数文献[5]中考虑的非确定性过渡系统建模。1介绍对于那些通常从事模型理论或形式规范语义学研究的人来说，要接近进程演算和进程代数领域往往变得非常困难有些过程没有任何物理基础。机器、代理、进程和状态等概念之间没有区别 只有语法而没有语义。进程和进程表达式之间没有区别。等本文旨在提出一些克服这些困难的措施我们展示了通信顺序过程的概念[3]和部分自动机的概念之间的强关系。允许将这两个概念带入共同视角的关键概念是余代数的概念[5]。事实证明，CSP被粘在非常特殊的余代数上，即最终1非常感谢霍斯特·雷切尔如何在1987年就开始向我们解释我是野笃也。1999年由ElsevierScienceB. V. 操作访问和C CB Y-NC-ND许可证。2无输出的部分自动机然而，共代数的观点提供了一个机会，在未来发展一个适当的模型理论的过程演算。这篇论文是为两种读者写的读者熟悉所提出的coalge-推理，例如，在[5]中，可以阅读该论文，作为CSP基本概念和思想的介绍从技术上讲，关于余代数的理论不会有什么新的东西熟悉CSP或其他过程演算的读者为了使这类读者相信抽象范畴论的实际意义，我们详细分析了最终部分自动机的范畴论定点构造作者完全相信余代数理论将是实现[4]所提倡的计算科学理论统一的重要环节本文的结构如下。在第2节中，我们根据[3]引入了确定性过程的概念，并试图表明与确定性部分自动机概念的密切关系。因此，事实证明过程与部分自动机的curried版本有关，如[8]所研究的，因此过程的共代数处理似乎是很自然的。第3节探讨了[8]中的见解，即（部分）自动机在其curried版本中应被视为特殊的余代数。我们展示了最终余代数的一般范畴论固定点构造如何适用于确定性部分自动机，并且这些一般构造提供了一个合理的确定性过程模型，该模型与Hoare模型同构。第4节表明，过程的相互作用在[3]中以共代数的方式描述此外，我们表明，进程的相互作用可以推广到部分自动机的同步，部分自动机的同步是兼容的进程的相互我们用部分自动机中状态测试的定义来结束这一节在第5节中，我们概述了[3]中的关键见解，即确定性过程可以通过迹完全描述，如何出现在共代数方法中本文没有时间和空间对文[3]中的不确定过程的处理作全面的分析因此，在最后一节中，我们将只提出一些关于非确定性过程和自动机的基本观察和想法，为进一步的研究提供指导。2确定性过程和自动机幸运的是，与过程的其他表述相反，[3]具有数学上的严格性，可以立即开始对所提出的过程概念进行更面向语义的分析首先，霍尔假设3⊆∅对于任何进程P，该进程可能参与的事件的固定集合A。A称为P的字母表，也记为αP。具有字母A的过程实际上从未参与A的任何事件，称为STOPA。其次，HOARE为进程提供了一个清晰的符号。 过程它首先参与事件a∈A=αP，然后完全像过程P表示为（a→P） 其中α（a→P）= αP（Prefixing）。省略括号是允许的，因为→是右结合的。以这种方式，可以通过以下过程表达式来描述在破碎之前成功地为两个顾客提供巧克力的简单自动售货机VMA（coin→choc→coin→choc→STOPαVMA）其中αV MA={coin，choc}。最初参与不同事件a1，...，an∈A，然后，在这些可选的第一事件a i发生之后，其行为完全与过程P i表示为（a1→P1| ··· |a n→P n）（选择）其中我们假设αP1=. = α Pn= A，并定义A也是（a1→P1）的alpha-bet| ··· |a n→Pn）。注意，由过程表达式（a1→P1）表示的过程| ··· |a n→Pn）是确定的，只要过程P1，. ，Pn是确定性的，因为事件a1，. ，n必须是不同的。一台机器VMB在破碎之前供应巧克力或给被破碎者，现在可以用过程表达式来（coin →（choc → STOP αVMB|其中αV MB ={coin，choc，tof}。第三，HOARE指出，每个具有字母表的确定性过程PA可以被认为是具有域B A的函数F，定义了对于B中的每一个a，如果第一个事件是a，则确定性过程F（a）定义了过程P的未来行为。这意味着每个确定性过程P∈DPA可以唯一地由部分函数F：A→DPA描述，其中dom（F）=B，其中DPA代表字母表为A的所有确定性过程的集合从全局考虑，HOARE假设，以这种方式，存在一个双射映射下一个A：DPA→[A→ DPA]其中[A→DPA]表示从A到DPA的所有部分函数的集合。停止A，例如，是由条件dom（nextA（STOPA））=唯一确定的进程 运行A，即， 在任何时候都可以参与A的任何事件的确定性过程，可以唯一地由条件dom（nextA（RUNA））=A和nextA（RUNA）（a）=RUNA来描述，对于所有a∈A。4一M ×→∅考虑到自动机的思想，我们立即看到，所有字母表为A的确定性过程的集合可以被看作是没有输出的无限确定性部分自动机的状态集合传统上[1]，没有输出的确定性部分自动机被定义为三元组其中I是输入符号的集合，S是状态的集合，并且d：S是一个部分状态转移函数。然而，众所周知，对于任何这样的部分函数，都有一个等效的curried版本，即，全函数λ（d）：S→[I→S]，其中i∈dom（λ（d）（s））i <$（s，i）∈dom（d），对所有s∈S，i∈I，且对所有i∈dom（λ（d）（s）），λ（d）（s）（i）=d（s，i这样，一个自动机M可以等价地用三元组（I，S，λ（d））的d的curried版本来描述，如[8]中所指出的。霍尔的确定性过程的概念真的可以用部分自动机（A，DPA，下一个A）来反映，现在将通过考虑[3]中确定性过程的数学模型来其中，A被定义为A的任意前缀闭子集P，即，任何（非空）子集P∈A，满足两个条件：（s，t ∈A），和（s，t∈A）：s，t∈P，其中，s，t∈P表示空迹（有限序列），s，t表示迹的连接以这种方式，进程STOPA由集合{STOP}建模，而RUNA由A本身给出。下一个A（P）的域在[3]中表示为P0，并定义为dom（下一个A（P））={a |a<$∈P}。 对于任意a ∈ P0= dom（next A（P）），next A（P）（a）在[3]中表示为P（a），并定义为next A（P）（a）={t |a从现在开始，让DPA是A的所有前缀闭子集的集合，部分自动机HMA=（A，DPA，下一个A）将被称为霍尔模型，字母A的确定性过程。注意，下一个A确实是双射的，因为我们可以将下一个− 1（F）= {}{a t}的前缀闭集赋给任何部分函数F：A→DP A|a ∈ dom（F）<$t ∈ F（a）}.在认识到部分自动机可以作为开发过程演算的适当模型理论的起点之后，可 能会对过程表 达式的含义进行反思，例如，V MB =（coin→（choc→STOP A|tof→STOP A）），其中A ={coin，choc，tof}。首先，如[3]中所建议的，它可以被解释为迹的预闭集PVMB={pixel，pixelcoin，pixelcoin，pixelcoin，choc，pixelcoin，tof}的“用户友好的”语法符号，即，表示DPA的元素PVMB（也比较下一节）。然而，其次，我们可以将V MB视为有限部分自动机MVMB=（A，S，tVMB）的语法表示，其中S ={1，2，3}并且tVMB：S→[A→S] 由 dom （ tVMB（1））={coin}，dom（tVMB（2））={choc，tof}，dom（tVMB（3））=，并且tVMB（1）（coin）= 2，tVMB（2）（choc）=tVMB（2）（tof）=3. 该部分自动机可以被描述如下（比较图1中的第1.2节）。[3]关于过程的图形表示法）r，~，~，，coinr，，~，~，choc，rz，~，~，1 2TOF 3¸5HMS→→--为了将过程表达式E转换为部分自动机ME，我们可以使用E的子表达式来表示ME的状态，例如， （硬币→（巧克力→停止A|tof→STOP A））而不是1，（choc→STOP A|tof→STOP A）而不是2，STOP A而不是3.注意，这个想法是识别从2开始请进一步注意，这个想法将使我们更接近[6]中用于推理过程的标记迁移系统在下一节中，我们将看到，确定性过程的霍尔模型A可以被表征为具有字母表（输入符号集）A的所有确定性部分自动机范畴中的最终对象。这意味着，对于任何确定性部分自动机M=（A，S，t：S→[A→S] ） 唯 一 的 自 动 机 态 射 τM ： M → HMA ， 即 ， 一 个 全 映 射 τM ：S→DPA，使得对于所有s∈S和a∈A，τM（t（s）（a））=nextA（τM（s））（a），其中等式的左侧定义为，如果，只有当右手被定义。注意，这个条件等价于自动机态射的未修饰版本的传统条件。St[A→S]τM，τMS×AτM ×idAλ− 1（t）τMJnextA[A→JJλ− 1（nextA）J的dpaDPA×ADPA在我们的示例中， ：{1，2，3}→DPA将1映射到PVMB，将2映射到P VMB。{，，}，3到{}。注意，过程表达式的两种解释是兼容的，因为过程表达式E到确定性部分自动机ME的转换隐含地指出了ME中的初始状态，即对应于整个表达式E的状态，并且该状态将通过τME映射到通过过程表达式E的“过程解释”获得的过程PE表情对于我们的示例，例如，τMVMB（1）=PVMB。使用prefixing和choice，我们只能构建定义确定性过程的过程表达式为了能够在语法上描述有限过程，HOARE引入了递归。设X是一个过程变量，F（X）是一个过程表达式，它是通过使用来自A是一个固定的集合。[3]中的思想是，F（X）定义一个映射[F]]：DPADPA，使得递归过程方程X=F（X）可以作为确定性过程的语法描述，如果恰好有一个固定点（F）。HOARE证明，只要F（X）是有保护的，即，作为只要在F（X）中至少出现一次唯一固定点称为μX：A.F（X）。字母A=coin，choc，tof的机器V MC，例如，可以用递归方程来描述，X =（硬币→（巧克力→X|tof→ X））其中，对应的唯一固定点由A的所有迹给出，6M {}M → HM→11→J，X，，chocr，，~1，在每个奇数位置有硬币，在每个偶数位置有CHOC或TOF然而，将过程表达式转换为上述的确定性部分自动机，提供了一种将过程唯一地分配给递归方程X=F（X）的新方法：我们可以构造一个有限的部分自动机MX=F（X）=（A，S，t），其中X∈S，使得X的像w.r.t.独特的自动机态射 τMX=F（X） ：X=F（X）A可以看作由方程X=F（X）描述的确定性过程对于我们的示例V MC对应的部分自动机=（A，S，t），其中S=X， 1可以描述如下TOF对于保护表达式τMX=F（X）（X），根据[3]等于[[ F]的唯一不动点，希望在下一节中变得清楚。注意，怎么-然而，与[3]相反，我们将为方程X=X分配一个唯一的过程，即STOPA，即，Id：DPA的“最小固定点”DP A.最后，我们要提到的是，进程RUN A= A可以用一个“单态”部分自动机（A，S，t）来表示，其中S = { X }，dom（t（X））= A，t（X）：A → S是从A到{ X }的唯一全函数。3最终余代数对于函子T：SET→SET，T-余代数是由集合S，余代数的载体和映射t：S→T（S）组成的对（S，t）。 两个T-余代数（S1，t1）和（S2，t2）之间的T-同态f：（S1，t1）→（S2，t2）由一个映射f：S1→S2构成，它与运算t1;T（f）=f;t2交换.St1T（S）FJT2T（f）JS2T（S2）要将这个定义应用于确定性部分自动机，我们只需检查赋值S<$→[A→S] 是 否 扩 展 到 函 子 A→ ：SET→SET。为此，我们将映射A→（f）：[A→（f）]赋给任何映射f：S1→S2S1]−→[A→ S2]withA→（f）（g）=defg;f对于所有函数sg∈[A→ S1]。很容易检验这是否真的定义了一个函子A→：SET→SET。本文证明了“A→ -余代数”与“A → -确定型部分自动机”的概念因为函子A→：SET SET是ωop-连续的[7]，即，保留ωop链的极限，我们可以幸运地使用范畴论版本的最小固定点构造[9]来构造最终的A→-7......，π，→关于我们联系我们→、2、、、3余代数：ωop-链的极限（L，（πi：L→Ai）i∈）f0f1f2A0，，A1，，A2，，A3，，···在SET中，可以用所有的无穷序列来规范地描述：a0，a1，a2，. . 证明了对所有i∈，fi（ai+1）=ai. 映射πi：L→Ai分别对应a1，a1，a2， . . . 除此之外，还存在πi=πi+1;fi，对所有i∈。我...···π0π1，，π2，3，J，Z，......A0，，A1，，zA_，，zA_，，·· ·现在将由下式给出预期的最终A→-余代数的载波N FA：下列ωop-链的极限（NFA，（πi：NFA→Ai（1））i∈！A→（！）2A2（！）31，，A→（1），，A→（1），→，A→（1），，·· ·通过连续地将函子A→应用于从A→（1）到单例集1 =的唯一映射最后一个是SET类的对象。要看到N FA是我们已经熟悉的东西，我们首先要知道，考虑A的元素→(1)，可以称为嵌套函数深度小于或等于i。 对于A= 硬币，巧克力，例如，A→（1）= [A1]有四个函数作为元素，通过用它的图表示函数，我们得到A→（1）={，{（coin，）}，{（choc，）}，{（coin，），（choc，）}}。图形表示可以如下所Ⓢ ⓈⓈ别，巧克力硬币choc硬币......JJJvzA2（1）=[A→[A→1]]has（4+1）2=25elementsas，e. G. ，，{（coin，）}，{（coin，），（choc，）}，{（coin，{（choc，）}）}，andd{（coin，{（coin，），（choc，）}），（choc，）}wecanebenefiteddbyy但是，巧克力但是，巧克力硬币J硬币 J， z硬币 J硬币 J， zⓈ Ⓢ ⓈⓈ你，chocJ硬币，乔克J， z∗ ∗ ∗现在，很明显，通过前缀和选择构建的过程表达式可以作为有限深度嵌套函数的图形的适当标记因此，STOPA代表完全未定义的图形、、f0f1F28硬币我的天ⓈⓈⓈ→函数和变量X表示“未知”函数的图形。在这种情况下，存在元素g1={（coin，n）}和g2={（coin，{（coin，n），（choc，n）}），A 2（1）的（choc，n）}，例如，correspondtotheproporcessexpressions（coin→STOP A）和（→→（coin→X1|choc→X2）|choc→STOP A），相应地-活泼地 考虑到图像表现，我们还可以考虑A的元素(1) 作为深度小于或等于我[6]。→！：A→（1）→1将A→（1）=[A→1]中的每一个函数映射到递归A→（！）为;！ ：[A→ [A→1]]→[A→1]将每个g∈[A→[A→1]]映射到g;！ [1][2][3][4][5][6] =dom（g）和（g;！）（a）=！（g（a））=对所有人都适用a∈dom（g;！）. 一般来说，Ai（！）：Ai+1（1）→Ai（1）只是削减（可能空）（i→ → →i+ 1）其中1）一个树的第二层，深度小于等于（在深度i处已经发生切割的信息通过在相应的记录中写入“n”来宣布。对于我们的示例，具有A→（！）（）=，A→（！）（g1）=（coin，），且A→（！）（g2）=（coin，），（choc，），即， 我们有下面的树Ⓢ ⓈⓈ Ⓢ你好，巧克力巧克力硬币硬币硬币......硬币......JJJ zJvz硬币巧克力......JzN F A的元素通过构造成有限序列g1，g2，g3，. . ⟩的嵌套函数s（同步树），使得Ai（！）（gi+1）=gi，即，→gi等于gj直到深度i如果i j. 以这种方式，看起来，，g，g2，g，.是一个可能无限过程的近似（比较[3]中第96页的L3定律）。 g1，g2，g3， . . .对于somei∈，ε表示一个有限过程sifgi=gi+1，对于alli≤j，thusgi=gj。注意，这使得egi=gi+1，其中e不在gi的图中，即，在相应的进程表达式中没有变量。A→：SET→SET的ωop连续性需要（A→（N FA），（A→（πi）：A→（NFA）→Ai+1（1））i∈）是ωop-chain的一个极限A→（！）2A2（！）3A3（！）4A→（1），，A→（1），→，A→（1），→，A→（1），·· ·由于只有一个从A→（N FA）= [A→N FA]到1的映射，我们平凡地有A→（π0）;！- -从而得到原ωop链[A→ N FA]···ss，，！ S s，A，→，（π2）S→（π0）A→（π，1）......ssssJ， z、Ⓢ9→→，z_1，，c，sA→（1），，A2（1），A3（1），A4（1），，···！A→（！）→A2（！）→A3（！）→10、→我OA→123我→这两个图的极限性质确保存在唯一映射uA：N FA→[A→N FA]，(1)uA;A→（πi）=πi+1对所有i∈，并且此外，确保该映射是双射的，即，SET中的同构。NFuA[A→NF]A，π 、一oooA（π）ooo···Ai （1）、、一zi+1 ，so（1）第一章···i（！）A→（1），，i+1（！）→确定性过程的预定的余代数模型现在由A→-余代数CMA=（N FA，uA）提供注3.1注意，范畴论的定点构造提供了过程的一种也就是说，一个进程P被序列g1，g2，g3，. . 它的有限近似的一种形式，其中gi请记住，g i中的一个开分支是用而不是用表示的。不需要所使用的过程的在[3]中，即，为了定义过程的偏序，因此有限过程可以作为无限过程的有限近似。为了证明余代数模型和霍尔模型是同构的，我们必须分析映射uA：NFA→[A→N FA]如何工作。 设序列P=g1，g2，g3，. . 白藜芦醇NFA. Pw. r. t的形象。uA必须是部分函数uA（P）：A→N FA，因此我们首先必须求uA（P）的定义域 为此，我们必须牢记，部分函数gi+1∈Ai+1（1）=[A→Ai（1）]，i∈H有相同的定义域因为，gi+1=Ai+1（！）（gi+2）=A→（Ai（！））（gi+2）=gi+2;Ai（！）→ → →Ai→（！）对所有i∈ uA的定义域等于这个P的复合物gi+1的共同点是通过等式1施加力d，对所有i∈（2）gi+1=πi+1（P）=A→（πi）（uA（P））=uA（P）;πi并且t husdo m（uA（P））=do m（uA（P）;πi）=do m（gi+1）sinceπi是总和.接下来，我们必须对任何a∈dom（uA（P））定义一个序列uA（P）（a）=你好，你好，你好。. n∈ N F A. 然而，等式2告诉ga=πi（uA（P）（a））=gi+1（a）我们已经完成了。定理3.2Hoare模型HMA=（DP A，next A）与余代数模型CMA=（N FA，u A）是同构的A→-余代数，即 存在一个双射映射apr A：DPA→ N FA，使得下图i+，1→11一{∈|||联系我们∈HMCMM →→→→NFA]通勤的dpa下一个A[A→DP]近似AJNFA;近似AuA [A→J证明大纲：根据[3]，任何迹P ∈ DPA的预定闭集都可以由无穷序列P0，P1，P2，.唯一地描述。. 有界迹的Prefix闭集的一个子集，其中Pn=defSPSn，即，Pn包含从P开始的长度不超过n的所有迹。Prefix封闭性确保了这些序列是P0，P1，P2，. . n与嵌套函数序列n，g1，g2，g3，.. . n∈N FA. 的将P转化为一个近似的序列，g1，g2，g3，.. . 嵌套的函数与下一个A和uA兼容，可以使用上述结果和[3]中的结果直接检查✷注3.3注意，精确的前缀封闭性保证了P可以用一个近似序列P0，P1，P2，.. . 证明了有限过程解的唯一性，并证明了这种近似是[3]中证明有保护递归过程方程解的唯一性的基础余代数模型CMA=（N FA，uA）通过构造而最终归属于A→-余代数范畴[9].因为HMA同构于CMA，我们有推论3.4CMA=（N F A，u A）和HMA=（DP A，next A）是最终A→-余代数。为了证明第2节中的主张，即我们求解递归方程X=F（X）的新方法，它基于A或A的无穷性，与[3]中的不动点构造密切相关，我们必须更接近CMA的无穷性的证明。让=（S，t：S[AS]）是任意的A→-余代数。我们感兴趣的是，确定从状态S开始的过程。也就是说，我们必须一步一步地分析从s可以到达哪些状态哪些过渡。状态转移函数t：S→[A→S]的展开给出以下交换图A→（t）2A2（t）3SA→（S）A（S）→A（S）· ··！SA→（！S）JJ→A2（！S）2 J→A3（！S）3 J1，，！A→（1），， A→（1），，2A→（1），，···A→（！）A→（！）其中最左边的矩形是可交换的，因为只有一个从S到1的映射，所有其他矩形都是第一个的逐步图像12→我我1塔夫脱山X→→→你好一期+112一期+1→我→12我→我t：S→A→（S）告诉任何状态s∈S，哪些状态可以从这是一个过渡的一步。A我→（t）：Ai→（S）→Ai+1（S）描述了如何长度为i的任意转换序列，即，序列不考虑考虑到t所做的限制，可以在下一步中根据t继续从状态s∈S开始，我们以这样的方式得到一个无限序列展开M（s）= defs，t s，t s，.. . 带ts=defAi （t）（ts）∈Ai+1（S）对于所有i∈，即， 其中ts=t（s）∈A→（S），ts=A→（t）（t（s））∈A2（S），S1 2 →.. . ，其中ti表示M中长度至多为i从s开始。 此外，ts告诉哪些状态是由长度正好是i。其间访问的国家在ts中被遗忘。对于自动售货机VMC和（初始）状态X，我们可以描绘，例如，展开VMC（X）的前三个元素如下J，XⓈ硬币，r，~，~J，Ⓢ硬币J、、、、chocJ，......J，X，z最后，我们考虑将展开M（s）抽象为一个过程。的映射！S：S→1将所有的状态都标识为Ai（！S）：Ai（S）→Ai（1）仅仅忘记长度为i的序列到达哪些状态的信息，并且仅仅保持长度为i的序列可以继续的信息我们现在得到，对于任何s∈S，procM（s）= define，g s，g s，.. . 其中gs=defAi（！S）（t s），对于所有i≥ 1。procVMC（X）的前三个元素，例如，是∗ Ⓢ硬币JⓈ硬币 J、，，tofchocJ vz∗上述图的交换性和ts和si+1 ，分别，对所有i∈gs=Ai（！S）（ts）=Ai（！）（Ai+1（！S） （Ai（t）（ts）=AiG13（！）（Ai+1（！（ts））i→=Aii→i（！）（gs）→ →i+1→i+1因此，procM（s）实际上成为一个过程，即，N FA的元素。这意味着我们已经通过procM（s）构造了从状态s∈S开始的过程。全局地，这提供了映射过程M：S→N FA。这个映射构成一个A→-同态过程M：M→ CMA，并且这个A→ -同态过程M：M →CMA14ǁǁCMSYN → CMNFA]同态是唯一的，可以根据NFA的极限构造和函子A→：SET→SET的ωop连续性，直接证明.4交互和并发首先，HOARE讨论了具有相同字母表αP=αQ的过程P和Q的相互作用。他定义了一个过程P Q，其中α（P Q）=αP=αQ，它的行为类似于由P和Q组成的系统在锁步同步中相互作用，即，任何事件的发生都需要同时执行所涉及的两个过程为了模拟这种相互作用，我们必须定义一个映射：N FA×NFA→N FA。在上一节中，我们已经看到A=（N FA，uA）是最终的A→-余代数，即，最后的部分自动机与字母A。这提供了一种规范的方法来定义从任意集合S到NFA的映射[5]。我们只需要构造一个A→-余代数M=（S，t），它的载体是S. 然后，通过CMA的无穷性，存在唯一的A→-同态过程M：M →CMA. 唯一的问题将是以这样一种方式设计M，即底层映射过程M：S→N FA成为预期的映射过程。为了定义过程的相互作用，我们构造了一个A→-余代数SYNA=（N FA×N FA，synA：N FA×N FA−→[A→N FA×N FA]）它可以被认为是通过使部分自动机CMA与自身同步而获得的自动机：对于任何一对过程（P，Q）∈NFA×NFA，我们定义：dom（synA（P，Q））=defdom（uA（P））dom（uA（Q）），对于所有a∈dom（synA（P，Q）），我们设置syn A（P，Q）（a）= def（u A（P）（a），u A（Q）（a））。由于第3节的最终A→-同态过程SYNA：AA使得下面的图是可交换的N FA ×NFA合成A [A→NF×N FA]进程SYN AJNFA;procSYN AuA[A→J也就是说，对于每一对（P，Q）∈N FA×N FA，uA（procSYNA（P，Q））=synA（P，Q）;procSYNA是必需的。对于任何事件z∈dom（synA（P，Q）），这意味着u A（procSYNA（P，Q））（z）= procSYNA（u A（P）（z），u A（Q）（z））.使用[3]中的符号，最后一个条件变成方程（P<$Q）（z）=P（z）<$Q（z），因此很明显，过程SYNA的余代数定义：N FA×N FA→N FA等价于[3]中第67页第4定律中对相互作用算符N的要求：N FA×N FA→N FA。一15∩∈由于procSYNA是由上述条件唯一定义的，我们可以确定procSYNA确实是预期的交互操作符。使用共归纳证明技术[5]，我们现在可以证明其他相互作用定律，在[3]中。其次，HOARE描述了进程P和Q与不同的字母αP/=αQ。只有那些同时处于α-赌注，即，在交叉点αP αQ，需要同步。然而，P字母表中的事件而不是Q字母表中的事件可能在P参与它们时独立于Q发生类似地，Q可以单独参与在Q的字母表中而不是P的字母表中的事件。这样，进程P<$Q的字母表将是组成进程字母表的并集αP<$αQ注意，在[6]中使用超行程是另一个技术来固定不同集合A和B中的哪些事件必须同步。现在给出两个字母A和B。预期映射的余代数定义可以从[3]第71页的CMA和CMB的同步提供了部分同步。自动机SYNA，B=（N FA×N FB，synA，B：N FA×N FB−→[A<$B→ N FA×N FB]）用字母A<$B表示如下：对任意一对过程（P，Q）∈N FA×N FB我们定义dom（synA，B（P，Q））=defdom（uA（P））\Bdom（uA（P））dom（uB（Q））dom（uB（Q））\A对于任何cdom（synA，B（P，Q）），我们设置n（uA（P）（c），Q），c∈dom（uA（P））\BsynA，B（P，Q）（c）=def<$（uA（P）（c），uB（Q）（c）），c∈dom（uA（P））<$dom（uB（Q））（P，uA）（Q）（c）），c∈dom（uB（Q））\A最终的（A<$B）→-同态过程SYNA，B：SYNA，B→ CMA<$B提供了预期的并发相互作用算子<$：N F A× N F B→N F A<$B。注意，显然SYNA，A=SYNA。并发相互作用算子的共代数定义表明，同步可以直接推广到任意部分自动机。定义4.1对于任何部分自动机 M1=（ S1， t1： S1→[A→S1]）和 M2=（ S2， t1：S2→[B→S2]），我们定义相应的同步自动机SYNM1，M2=（S1×S2，synM1，M2：S1×S2−→[A<$B→ S1×S2]）如下：对于任何（s1，s2）∈S1×S2，我们定义dom（synM1，M2（s1，s2））=defdom（t1（s1））\Bdom（t1（s1））dom（t2（s2））dom（t2（s2））\A16choc--12222J，X，，choc，r，~1，J，Y，，bisr，a~，~，，对于任意c∈dom（synM1，M2（s1，s2）），我们设n（t1（s1）（c），s2），c∈dom（t1（s1））\BsynM1，M2（s1，s2）（c）=defm（t1（s1）（c），t2（s2）（c））， c∈dom（t1（s1））<$dom（t2（s2））（s，t（s）（c）），c∈dom（t（s））\A作为示例，我们将来自第2节的自动售货机VMC与字母表A={coin，choc，tof}同步，并且将客户与字母表B={coin，choc，tof}同步。由递归方程Y =（coin→（tof→Y））描述的{ coin，tof，bis}|bis→Y））。顾客付了一枚硬币后，决定要一块饼干还是一块饼干。相应的部分自动机可以描述为：托夫托夫两个自动机的同步给出了（X，Y），，choc （1， Y）双......硬币TOF，，双（X，a），，z（1，a）也就是说，在客户能够支付硬币之后，他可以决定向被许可人支付硬币，并且机器可以同时向被许可人交付硬币如果他决定要饼干，机器稍后会提供巧克力。或者，甚至值得，机器可能决定给他一块巧克力，他必须把这解释为他自己的决定，让饼干有第二次机会得到一块巧克力。请注意，通过简单地将客户的字母表更改为B=coin，tof，bis，choc，我们将获得具有死锁的同步自动机（X，Y），，双硬币（X，a）TOF（1，Y），，双z（1，a）现在证明，进程的并发交互作用精确地描述了同步自动机SYN M1，M2中 的进 程是如何通过合成单个自动机M1和M2的进程而获得的。也就是说，自动机的同步与亲-cesses中所述，，17定理4.2对任意部分自动机M1=（S1，t1：S1→[A→S1]），18M → → ∈××2=（S2，t1：S2[BS2]），并且任何一对状态（s1，s2）S1S2，我们有procSYNM 1，M 2（s1，s2）=procM1（s1）procM2（s2）证明：由 于 n：NFA ×NFB → NFA <$B是由最终的（A <$B）→-同态过 程 SYNA ， B ： SYN A ， B→ CMA<$B给出的，因 此证 明 了 映射 过 程 M1 ×procM2：S1× S2→ NFA × NFB构成一个（A <$B）→-同态过程M1×procM2：SYNM1，M2→ SYN A，B.S1×S2顺式M1、M 2 [AB→S1×S2]procM 1×procM 2JsynA，B;procM 1×procM 2JN FA×N FB[A→N FA×N FB]必要的平等 进程SYNM 1、M 2 = procM1procM2; procSYNA，B则由最终同态的唯一性确保。我们必须证明，对于任何对（s1，s2）∈S1×S2，等式(3)synA，B（procM1×procM2（s1，s2））=synM1，M2（s1，s2）;procM1×procM2保持。 自进程M1起 ：M1→ CMA是A→-同态，我们有S1∈S1相等(4)uA（procM1（s1））=t1（s1）;procM1由于过程M2：M2→ CMB是一个B→-同态，我们有对s2∈S2(5)u B（procM2（s2））= t2（s2）; procM2.根据等式4和等式5，映射procM1，procM2的全体，以及SYNM1，M2和SYNA，B的定义，我们可以首先证明等式3中两个函数的域是相等的：dom（synA，B（procM1×procM2（s1，s2）=dom（synA，B（procM1（s1），procM2（s2）=dom（uA（procM1（s1）\Bdom（uA（procM1（s1）dom（uB（procM2（s2）dom（uB（procM2（s2）\A=dom（t1（s1）;procM1）\Bdom（t1（s1）;procM1）dom（t2（s2）;procM2）dom（t2（s2）;procM2）\A=dom（t1（s1））\Bdom（t1（s1））dom（t2（s2））dom（t2（s2））\A=dom（synM1，M2（s1，s2））=dom（synM1，M2（s1，s2）;procM1×procM2）其次，我们证明了等式3对所有c∈dom（t1（s1））\B=dom（uA（procM1（s1）\B.根据synA、B的定义，等式4和synM1、M2的定义，我们得到synA，B（procM1×procM2（s1，s2））（c）19=synA，B（procM1（s1），procM2（s2））（c）=（uA（procM1（s1））（c），procM2（s2））20=（procM1（t1（s1）（c）），procM2（s2））=procM1×procM2（synM1，M2（s1，s2）（c））=（synM1，M2（s1，s2）;procM1×procM2）（c）其他情况可以用类似的方法来证明。✷此外，部分自动机的一般同步可以用来定义部分自动机中状态的测试也就是说，测试一个进程是否可以在某个状态下成功运行（比较[2]）。我们考虑一个部分自动机M=（S，t：S→[A→S]）.则一个进程P∈N FA可以在状态s∈S开始成功运行，如果procSYNCM A，M（P，s）=P。5跟踪和运行假设给定一组事件A然后，所有有限迹和无限迹的集合A∞可以构成A→-余代数TRA=（A∞，popA：A∞→[A→A∞]）。我们设置pop A（pop）=def f，对于空迹，设为pop A（pop A）= deff，对于非空迹，设为tr= popa0，a1，a2，. . 我们定义dom（popA（tr））=def{a0}和popA（tr）（a0）=defA1，A2，.. . - 是的最后的A→-同态过程TRA：TRA→ CMA将变换任何迹a0，a1，a2，.. . 插入序列⟨∗,{(a0,∗)},{(a0,{(a1,∗)})},{(a0,{(a1,{(a2,∗)} )})},.. . 嵌套函数的集合，可以被看作是前缀序列a0，a1，a2，.. . - 是的显然，映射过程TRA：A∞→N FA是内射的，因此TRA可以看作CMA的一个子余代数[7].现在，我们可以测试部分自动机中的任何状态，如果跟踪可以从这个状态开始连续运行。 也就是说，对于任何具有字母A的部分自动机M =（S，t），M与T RA的同步将成为线性自动机，因此A→-同态过程SYNTRA，M：SYNTRA，M−→ CMA可以分解为A→-同态检验M：SYNTRA，M−→ T RA接着是A→-嵌入过程TRA：TRA→ CMA。对于最终部分自动机CMA，这些测试在以下意义上是穷举的。命题5.1假设给定一组事件A。对于任何进程，P，Q∈N FA，下列断言是等价的：(i) P=Q(ii) testCMA（tr，P）= testCMA（tr，Q）for all traces tr ∈ A∞.(iii) 对于所有迹tr∈