有限观测模型与CSP的优先级测试

可在www.sciencedirect.com在线获取理论计算机科学电子笔记325（2016）237-252www.elsevier.com/locate/entcs通过优先级David Mestel1 A.W. 罗斯科2号牛津大学计算机科学系摘要Hoare在本文中，我们研究了有限观测模型，其中至少有六个已被确定为CSP，即迹，失败，复活，接受，拒绝测试和有限线性观测[11]。我们将演示如何使用最近引入的优先操作符（[12]，第20章）将这些模型中的细化问题转换为跟踪细化（语言包含）测试。 此外，我们能够将其推广到任何（理性的）有限观测模型除了理论上的兴趣之外，这也具有实际意义，因为最先进的精化检查工具FDR3 [4]目前只支持两个这样的模型。关键词：CSP，指称语义，优先级1引言许多不同形式的进程演算已经被开发用于并行程序的建模，包括Hoare与后两者不同，CSP在本文中，我们研究CSP的有限线性时间观测模型;也就是说，所有考虑的观测都可以由实验者在有限时间内确定的模型，实验者可以看到过程通信的可见事件以及它可以在任何稳定状态下运行的事件集虽然实验者可以任意频繁地运行该过程，但他或她只能记录单个有限执行的结果因此，记录的每个行为都可以从一个有限的事件序列以及在该跟踪期间和之后立即接受的稳定状态的事件集合中推断出来。1电子邮件：david. cs.ox.ac.uk2电子邮件：bill. cs.ox.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2016.09.0411571-0661/© 2016作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。238D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237至少有六个这样的模型已经被考虑用于CSP，但目前的状态是，技术改进检查工具FDR 3 [4]目前只支持两种，即跟踪和故障（它还支持故障-发散模型，这不是有限的观测）。我们提出了一个构造，它产生一个上下文C，使得故障模型中的精化问题对应于应用C的跟踪精化问题。我们能够推广这一点，以表明（定理5.4）不仅对已经研究过的六个模型，而且对任何合理的有限观测模型（这里“合理”意味着模型可以被有限存储器计算机识别，在某种意义上，我们将使其精确），类似的我们首先简要介绍了CSP语言。接下来，我们给出一个非正式的描述我们的结构的失败模型。为了证明这个结果的充分普遍性，我们首先给出有限观测模型和合理性概念的形式定义。然后我们描述我们的一般结构。最后，我们讨论性能和优化问题。2CSP语言我们提供了语言的简要概述，主要取自[11];鼓励读者查阅[12]以获得更全面的处理。在整个过程中，通信被认为是一个有限的非空通信集合，它是可见的，并且只有在观察环境允许的情况下才能通过握手通信发生。每一个过程的动作都是从τ{τ}开始的，其中τ是不可见的内部动作，不能被环境阻止。 注意，CSP的通常处理允许通过包括另一个不可预防的事件C来表示终止的顺序组合;这给每个模型增加了轻微的复杂性，为了简单起见，我们省略了它。它可以被加回去，而不会对本文的结果产生任何重大影响CSP的恒定过程是• STOP，它什么也不做，这是死锁的一种表示。• div（仅）执行内部τ作用的无限序列--发散或活锁的表示。• 混沌可以做任何事情，除了发散。prefixing操作员介绍通信：• a → P在行为像P之前传递事件a。在一对进程之间有两种形式的二元选择：• PH Q让进程决定行为像 P还是像 Q：这是不确定的或内部选择。• P QQ表示环境在P和Q的初始事件之间的选择。如果选择的事件是明确的，那么它的行为就继续像选择的事件一样;如果它是两者的初始事件，那么随后的行为就是不确定的。D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237239ǁ∈在P和Q中出现τ并不能解决选择问题（与CCS+）. 这是外部选择。在我们的核心语言中，我们只有一个并行运算符，因为CSP的所有常用运算符都可以用它来定义，如第2章等所讨论（12）。• P Q并行运行P和Q，允许它们中的每一个执行任何动作。XX中的动作必须在X和X之间同步，两个.有两个操作符可以更改进程通信的性质• P\X，对于X，通过将所有P的X -动作转化为τ s来隐藏X。• P [[R]将重命名关系R×应用于P：如果（a，b）∈ R且P可以执行a，则P [[R]]可以执行b。R的域必须包括P使用的所有可见事件。由关系{（a，b）}重命名表示为[a/b]]。还有另一个操作符允许一个过程跟随另一个过程：• P ΘA Q的行为类似于P，直到集合A中的事件发生，此时P关闭，Q启动。这是throw操作符。最后的CSP结构是递归：它可以是单递归或互递归（包括无限参数空间上的互递归），可以由方程组定义，或者（在单递归的情况下）通过符号μ p.P线性定义，对于一个可能包含自由进程标识符p的项P。递归可以在操作上解释为具有对应于单个解旋的τ动作。在外延上，我们将P视为外延空间上的函数，并将μ p.P解释为该函数的最小不动点我们还利用交织算子|||，它允许进程独立地执行操作，等效于CPU，而进程RUNX，∅也可以表示集合X的每个元素，定义为yRUNX=QxXx→运行X。2.1优先优先级运算符在[12]的第20章中详细讨论。 它允许 我们可以指定可见事件集合的排序，并防止低优先级事件在高优先级事件或τ可用时发生在[12]中描述的在FDR3 [4]中实现的操作符由三个参数化：过程P，事件集上的偏序≤，以及子集当τ可用时可能发生的事件的X次方。我们要求X的所有元素都是关于≤的极大值。 书写集合的首字母缩写（P）{τ}通过增加y≤τy∈τ\X，将≤推广到τ{τ}上的偏序，我们定义了优先级排序240D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237如下所示一P−→PJ<$$>ba. a≤b<$b∈/initials（P）prioritise（P，≤，X）−a→ prioritise（P J，≤，X）（a ∈ {τ}）.请注意，优先级并不是最精确的模型FL之外的指称模型的组成部分，因此我们认为它是CSP的可选添加，而不是它的组成部分;当我们在下文中提到特定类型的观察作为CSP的有效模型时，我们指的是没有优先级的CSP3示例：故障模型我们首先使用故障模型来证明我们的构造：我们将产生一个上下文C，使得对于任何过程P，Q，我们有Q在故障模型中定义P，当且仅当C[Q]在迹模型中定义C[P]3.1跟踪和故障模型迹模型T在自动机理论中很常见，它用一组（有限的）事件串来表示一个过程。每一个过程（对于固定的字母表）都与的子集相关联，是上的有限词的集合故障模型F还记录在跟踪s之后进程能够稳定地拒绝的事件的集合X（即，进程能够在跟踪s之后处于故障状态）。其中没有τ事件是可能的，并且其中初始事件的集合不满足X）。因此，一个过程与一个子集的×（P（）{·}），其中• 表示没有记录的拒绝集。[3]请注意，记录·并不意味着没有拒绝观察，只是我们没有观察到稳定性。对拒绝的观察意味着在当前迹之后过程可以是稳定的，而·则不是。在任何模型M中，如果与Q相关联的集合是与P相对应的集合的子集，则我们说QM-限定P，并写作P±MQ。3.2故障模型的模型转换结构如下：引理3.1对于每个有限字母表，存在一个上下文C（在扩展字母表上），使得对于任何过程P和Q，我们有P ±FQ当且仅当C [P] ±TC [Q]。证据步骤1：我们使用优先级来产生一个进程（在扩展的字母表上），当且仅当原始进程P能够稳定地拒绝x时，该进程可以传递事件x j。这是通过将字母表扩展到J（其中J包含中每个事件的相应引发事件），并根据[3]这等价于标准表示，其中一个过程由一个子集合和一个子集合表示：迹分量正好是{s：（s，·）∈ P}。D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237241偏序，其使每个x优先于对应的xJ。回想一下，优先级运算符的定义意味着这也会导致τ在被引发的事件上被提升。我们还必须引入一个事件戳来表示稳定性，而不需要任何拒绝。这是必要的，以便能够记录空的拒绝集。设偏序≤1定义为xJ<1x<$x∈ <$，且上下文C1定义为C1[P]=prritise（P|||RUN不超过100%{sta b}，≤1，n）。这个过程对于P的每个状态都有一个状态J，其中J有与相同的未引发事件（和相应的转换）。此外，当xj稳定时，xj可以传递XJ，并且可以拒绝X，并且当xj稳定时，可以刺入步骤2：我们现在回想一下，故障模型的定义只允许在跟踪结束时记录拒绝集，而对拒绝集之后发生的事情我们通过使用调节器过程来防止引发事件（或刺）被未准备好的事件跟随。让UNSTABLE=Qx∈Nx→UNSTABLEQQx∈{stab}x→ST ABLESTABLE=Qx∈{stab}x→ST ABLEE，定义C，C[P] =C1[P]Σ∪ Σ∗∪{stab}不稳定C[P]的迹包括：首先，P的迹s;其次，如果P在s之后可以处于稳定状态，则对于某个这样的状态σ0，任何由可以在σ0中拒绝的事件形成的串，连同stab。这个引理清楚地跟随着。Q很明显，任何这样的上下文都必须涉及一个在迹上不是压缩的算子，否则我们将有P±TQ蕴涵C[P]±TC[Q]，这等价于P±FQ，而这对于一般的P和Q是不正确的（例如考虑P=a→STOP，Q=（a→STOP）HSTOP）。因此，只有像我们这样涉及优先权的背景才能实现这一点。4语义模型为了将这种构造推广到任意的有限观察语义模型，我们不仅必须给出特定模型的形式定义，而且必须给出有限观察模型的概念本身的形式定义242D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）2374.1有限观测值我们只考虑由有限线性观测产生的模型。直观地说，我们假设我们能够观察到进程执行有限数量的可见动作，并且当进程在动作之前是稳定的（无法执行τ）时，我们能够观察到它愿意执行的接受动作集请注意，我们无法完全观察到不稳定性：我们从一个处于不稳定状态的行为中所能记录到的最多是我们没有观察到稳定性。因此，在任何我们可以观察到稳定性的背景下，我们也可以通过简单地不看而无法观察到它。我们将模型定义在有限个字母表上，并将每个有限个字母表上的任意顺序按字母顺序排列。最精确的有限观测模型是考虑所有有限线性观测的模型，记为FL：定义4.1字母表上的有限线性观测集是FL：={A0，a1，A1，.，A n−1，a n，A n：n∈N，a i ∈，A i或A i=·}，其中a i被解释为通信事件的序列，而A i表示稳定的可接受集，或者在·未能观察到稳定性的情况让对应于一个过程P的这类观测值的集合记为FL（P）。（有时候我们会把字母F去掉，只写FL（P））。更正式地说，FL（P）可以归纳地定义;例如FL（PQQ）：={α，β：α∈ FL（P），β∈ FL（Q）}（其中X=·，对于任何集合X）。更多详情请参见[12观察FL有一个对应于扩张的自然偏序（其中α·β和αA都被αAβ扩张，对于任何集合A和任何α和β）。注意，对于任何过程P，我们有FL（P）关于这个偏序是向下闭的。4.2有限观测模型我们精确地考虑了从FL的观察中导出的模型，这些模型在CSP语法上是组合的（而不是优先级），并且它们尊重字母表的扩展定义4.2有限观测前模型M由一组观测的每一个（有限）al-phabet n，obs n（M），以及一个关系Mn，FLn×obs n（M）组成。过程P在M中的表示记为M（P），并由下式给出：M<$（P）：= M<$（FL<$（P））={y∈ obs <$（M）：<$x∈ FL<$（P）.（x，y）∈ M<$}.对于字母表上的过程P和Q，如果我们有M<$（Q）<$M<$（P），那么我们说QM-对P进行修正，记为P±MQ。D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237243.Σ我ΣΣΣΣ(As在我们有时候会掉下那个“”之前）。请注意，这个定义不如我们将前模型定义为P（FL）上的任何等价关系那样普遍。例如，具有相同基数的等价关联集没有对应的预模型。定义4.2与[12]中的定义一致在不失一般性的情况下，M不标识obs（M）的任何元素;也就是说，只有当x=y时，我们才有M−1（x）=M−1（y）（否则通过这种等价而商关系）。在这个假设下，M在obs（M）上导出一个偏序：定义4.3由M_∞在obs_∞（M）上诱导的偏序由下式给出：x≤y当且仅当对所有b∈ M−1（y），存在a∈ M−1（x）且a≤ b。观察到对于任何过程P，从这个定义可以得出M（P）关于这个偏序是向下闭的（因为FL（P）是向下闭的）。定义4.4一个预模型M是合成的，如果对于所有的CSP算子，比如说元数k，以及对于所有的过程P1，...，Pk和Q1，…，Q k使得对于所有i，M（Pi）= M（Q i），我们有M.（Pi）i=1. k = M。（Qi）i=1. k.这意味着，通过沿着M向前推进而在obs（M）中的过程上定义的算子是良好定义的：对于任何集合X1，...，X k个对应于CSP过程的图像的随机数（M），取过程P1，.，P k使得Xi= M（Pi），且令（Xi）i=1. k= M（Pi）i=1. K.定义4.4说，这个结果不依赖于Pi的选择。请注意，没有必要要求定义4.4的等同物来重新定义。在模型的定义中，由于以下引理，最小不动点递归是自动良好定义的（并将[12]中给出的一些参数形式化）：引理4.5设M是合成前模型。 设C1，C2是CSP上下文，使得对于任何进程P，我们有M（C1 [P]）= M（C2 [P]）。 设C1和C2（在子集序下看作P（FL）上的函数）的最小不动点分别为P1和P2。则M（P1）= M（P2）.证据 利用CSP上下文诱导Scott连续函数的事实，P（FL）（见[6]，第2.8.2节），Kleene不动点定理给出Pi=∞n=0Cn（n）. 现在，任何x ∈ M（P1）都在取到某个有限个N的并集中，并且由于有限并集对应于内部选择，而子图对应于过程div，因此我们有C1和C2的直到N的并集在M下通过组合性而一致。因此x∈ M（P2），所以M（P1）<$M（P2）. 类似地，M（P2）<$M（P1）。Q定义4.6一个前模型M是可拓的，如果对于所有字母表<$1 <$$> 2，我们有obs <$1（M）<$obs <$2（M），并且M<$2 同意M1 在FL（101）×obs101（M）上。244D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237定义4.7前模型是一个模型，如果它是组成和伸展的。在这种情况下，我们现在描述五个主要的比FL粗糙的有限观测模型：痕迹，失败，复活，接受和拒绝测试。4.2.1Traces模型粗略模型只测量过程的痕迹;也就是说，它能够接受的事件这对应于被视为非确定性有限自动机（NFA）的过程的语言定义4.8迹线模型T由下式给出：obs（T）=，T=trace其中trace是与观察相关的等价关系A0，A1，A1，...，a n，An n把字符串a1...一个;4.2.2失败痕迹模型给我们提供了一个过程可以做什么的信息，但是在某种意义上，它并没有告诉我们它需要做什么。特别是，进程STOP跟踪-细化任何其他进程。为了指定活性属性，我们可以结合一些关于允许进程拒绝的事件的信息，从失败模型开始。直观地说，它捕获跟踪s，以及允许进程在s之后稳定拒绝的事件集。定义4.9故障模型F由下式给出：obs（F）=×（P（）{·}），F=fail，其中，故障与观测值A0，...，a n，An n映射到所有对（a1. a n，X），对于所有如果An·，则X=An，否则X=A n。4.2.3复兴下一个粗模型，首先在[11]中介绍，是复兴模型。直观地说，这捕获了跟踪s，以及在s之后可以被稳定拒绝的集合X，以及然后可以被接受的事件a（如果有的话）定义4.10恢复模型R由下式给出：obs（R）=×（P（）{·}）×（{·}），R=rev），其中，rev将观测值ΔA0，a1，.， a n−1，A n−1，a n，A nto(i) 三重数（a1. a n−1，X，a n），对于所有X\A n−1，如果An−1其他人士• 对于X= ·(ii) 三重数（a1. a n，X，·），对于所有X，如果A n/=·，则an =\ A n，否则X=·。有限线性观测与所有三元组相关，三元组包括：它的初始迹;可能被观测到的稳定拒绝，或者·如果原始观测没有观测到稳定性;以及可选地（上面的第（i）部分）可以接受的单个进一步事件。D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）2372454.2.4承兑到目前为止所考虑的所有模型都只涉及拒绝集，这些拒绝集在子集下是封闭的。下一个模型，接受（也称为定义4.11验收模型A由下式给出：obs（A）=×（P（）{·}），A=acc，其中，acc_n与观测值ΔA0，a1，.相关， a n，A n与对（a1. a n，A n）。4.2.5拒绝测试我们认为最后的模型是拒绝测试，首先在[9]中介绍这通过考虑事件的整个历史和稳定的拒绝集来改进F和R。 它与A无法比较，因为它没有捕获精确的接受集。定义4.12拒绝测试模型RT由下式给出：obs_n（RT）={nX0，a1，X1，.， a n，X n<$：n ∈ N，a i∈ N，Xi<$N或X i=·} RT<$= RT <$，其中，rt= 0与观测值ΔA0，...，a n，A n从0到0，...，a n，X n n≠，对于所有X i≠如果Ai·，则Ai，否则对于Xi=·。4.3理性模型稍后我们将只考虑模型M，对于模型M，FL-观测值和M-观测值之间的对应关系可由有限存储器计算机判定。我们将把这个概念解释为说关系M对应于某个有限状态自动机所接受的语言。为了做到这一点，我们必须首先决定如何将FL中的元素转换为语言中的单词。 我们这样做以明显的方式（使用新变量来表示Ai的原因将在第5节中变得明显）。定 义 4.13 FL 的 规 范编 码是 在字 母表 ： = JJSym 上，其 中 eeJJ： ={aJJ ： a∈} 和Sym={，，'，'，·}。[4]它是由定义4.1中的表示给出的，其中集合Ai是通过按字母顺序列出与Ai的成员相对应的元素来表示我们将这种编码表示为φ：FL→FL。我们现在定义一个模型是理性的（从自动机理论中借用一个术语），如果它的定义关系可以被某种非确定性有限自动机识别（当适当编码时）。定义4.14一个模型M是理性的，如果对于每个字母表θ，有一些有限的字母表Θ和一个映射θθ：obsθ（M）→θ，使得有一个（不确定性）[4]请注意，这个有点令人不满意的符号表示一组四个元素：尖括号和逗号和符号·。246D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237有限自动机A识别{（φ（x），φ（y））：（x，y）∈M}，并且使得φ是相对于θ上的前缀偏序和由M在obs（M）上诱导的偏序的序相关的（即，只有当x≤y时，φ（x）≤φ（y自动机“识别”一个关系意味着什么定义4.15对于字母A和T，一个关系R×T被自动机A识别，当：(i) A的事件集是左的。是的，T，然后(ii) 对于任何s∈T∈ R，t∈T∈ R，我们有sRt当且仅当存在某种交织左.s和右.t被A接受。注意，定义4.15意义上的可识别性很容易证明等价于例如在[16]中给出的有限状态转换器的可识别性的常见概念还要注意FL本身（将FL视为对角关系）是平凡有理的。引理4.16模型T、F、R、A和RT是有理数的。证据 通过检查定义4.8- 4.12。我们取Θ =<$$><$J<$$>Sym，其中<$JJ和接受集的表达式与FL的规范编码相同，拒绝集以对应的方式表示在<$J：={aJ：a∈<$}上。Q请注意，并非所有关系都是有理的。例如，将每个有限线性观测映射到其长度的“计数关系”显然是不合理的。我们不知道作为一个有限的观测模型的额外约束是否必然意味着合理性;然而，没有非理性的模型是已知的。因此，我们提出以下猜想：猜想4.17（有限观测模型的合理性）设M是有限观测模型。M是理性的。5模型转换我们现在来到本文的主要内容：我们证明了“模型转换”的结果，表明存在上下文允许我们在不同的语义模型和基本的痕迹模型之间传递。主要结果是定理5.4，它表明这对任何理性模型都是可能5.1FL的模型转换我们首先证明最精细模型FL的结果。我 们 证明了存在一个上下文C FL使得对于任何过程P，P的有限线性观测对应于C FL（P）的迹。引理5.1（FL的模型移位）对于每个字母表T，存在字母表T上的上下文CFL：=jjj{done}，以及顺序映射D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237247π：FL→T（关于FL上的扩张偏序和T上的前 缀 偏 序）使得对于π 上 的 任何p，我们有T（CFL[P]）=π（π（FL（P）（其中π（X）是集合X的前缀闭包）。证据我们将使用无素字母表<$i来表示来自原始轨迹的通信事件，使用双素字母表<$JJ来表示稳定的接受。在一个中间步骤中，将使用J来表示拒绝，并使用done来区分（表示空的接受集）和·（表示未能观察到任何东西）。第一步：我们首先生成一个能够传递事件xJi的进程，而原来的进程可以稳定地拒绝相应的x i。定义偏序≤1=xJ<1x：x∈，当相应的事件可能发生时，它可以防止拒绝事件。让上下文C1由下式给出：C1 [X]=优先级（X|||RUN≤1，≤2）。请注意，第三个参数防止引发的事件在不稳定状态下发生。步骤2：我们现在类似地引入接受事件，它可以在稳定状态下发生，而相应的拒绝类似地定义偏序≤2=xJJ<2xJ：x∈，当相应的拒绝是可能的时，它阻止了接受事件。让上下文C2定义为：C2 [X]=优先级（C1 [X] |||RUN≤2，≤1）。步骤3：我们现在确保从跟踪推断的接受集是被检查的进程接受的完整集这是最直接地通过采用调节器过程来完成的，该过程可以接受未引发的事件，也可以接受第一个拒绝或接受事件，然后依次拒绝或接受每个事件。在后一种情况下，它会传递一个done事件，并返回到其原始状态。done事件是必要的，以区分终端，它可以在最后一个事件之后有一个done，和终端·，它不能（观察到不能发生在结尾之外最后，我们隐藏拒绝事件。令a和z分别表示按字母顺序排列的第一个和最后一个事件，令succx表示x的按字母顺序排列的后继事件。定义流程UNSTABLE=Qx∈Nx→UNSTABLEQaJ→STABLE（a）QaJJ→STABLE（a）STABLE（x）=xJ→STABLE（succx）QxJJ→STABLE（succx）（x/=z）稳定（z）=完成→不稳定，248D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237.C C并让FL[X]=2[X]Σ∪ Σ∗∪ Σ∗∗不稳定第4步：我们现在通过如下归纳定义函数π来完成证明：π（s）=π（s）π（sx）=π（s）xπ（s）={x1， . ，xk} n）=π（s）nnxJ1J. . . xJkJdone，其中不失一般性地，X1按字母顺序列出很明显，这是命令相关的，通过上述满足的结构，T（CFL[P]）=pre f（π（FL（P）。Q这个结果允许我们将FL-细化的问题转化为CFL下的迹细化问题，如下所示：推论5.2对于引理5.1中的CFLP±FLQ，如果CFL [P] ±TCFL [Q]，则为0。是的。当然，如果FL（Q）<$FL（P），则T（CFL[Q]）=pref（π（FL（Q）<$pre f（π（FL（P）=T（CFL[P]），因此CFL[P]±TCFL[Q]。相反地，假设存在x∈ FL（Q）\ FL（P）。然后，由于FL（P）是下闭的，我们对所有y∈ FL（P）有x、y。由于π是阶自反的，对所有y∈ FL（P），我们相应地有π（x）<$π（y）.因此π（x）∈/pre f （π（FL（P），所以pre f （π（FL（Q）<$pre f（π（FL（P）。Q5.2理性观测模型的模型转换我们现在基本上有了证明主要定理所需的一切。我们记录了一个民间结果，任何NFA都可以作为CSP进程实现（直到前缀闭包，因为跟踪集是前缀闭包的，但正则语言不是）：引理5.3（NFA的实现）设A=（Q，Q，δ，q0，F）是（非确定性）有限自动机。则存在一个CSP过程PA，使得<$（L（A））=<$（T（PA））。证据 微不足道的建筑。 参见[10]的第7章。Q定理5.4（有理模型的模型转移）对于每个有理模型M，re存在一个上下文CM，使得对于任何概率P，我们有T（CM[P]）=T（M（P））.证据设A是识别（φ×φ）（M）的自动机（如定义4.14所示），设PA是引理5.3中的相应过程。我们首先应用引理5.1来产生一个过程，其迹对应于原始过程的有限线性观测，以左为前缀：D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237249..根据引理5.1的上下文，并让上下文C1定义为：C1[X]=CFL[X][[left. x/x]]。我们现在与PA并行合成，以产生一个过程，其迹对应于原始过程的M-观测C2定义为：C2[X] =C1[X]{|左|}PA\{|左|}[[x/right.x]]。那么C2[X]的迹线就是X对应的观测值在x下的像的预取。Q通过与推论5.2相同的论证，我们有推论5.5对于任意有理模型M，设CM如定理5所示。四、 则对于任意的过程P和Q，我们有P±MQ当且仅当CM[P]±TCM[Q]。6执行我们通过实现具有Corol- lary5.5属性的上下文来演示该技术;源代码可以在[1]中找到为了效率起见，我们直接工作，而不是使用定理5.4的一般方法。上下文C1引入拒绝事件和插入事件，其仅在相应的正常事件可以被拒绝时才可以发生。这实现了拒绝测试模型，而只允许正常事件可选地跟随一些拒绝（和stab）的上下文CF实现了失败模型。然而，在大多数事件在大多数时间被拒绝的典型情况下，这在大字母表上是次优的。FDR3上下文C那么问题就来了：如何检查规范的接受是实现的接受的子集，尽管跟踪细化以另一种方式检查包含？答案是使用优先级来防止stab事件在接受仍然可用时发生，以便CFImpl然后，我们通过与RUN并行组合所有接受事件来形成CFSpec类似的结构，稍微不同的限制，允许的事件序列产生有效的过程中的复苏和拒绝测试模型。对于接受模型，我们只想检查实现的接受集是否包含250D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237| |||适用于规范和实现;有限线性观测的工作原理类似于拒绝测试所取代的失败6.1测试我们通过构建过程来测试这种实现，这些过程首先分别由失败、恢复、拒绝测试和接受模型来区分（后两者也由有限线性观测模型来区分）。表1显示了这些过程以及区分它们和不区分它们的模型（回忆一下模型的精度等级：T ≤ F ≤ R ≤{A，RT }≤FL）。使用上述实现在FDR3中运行这些检查时，可获得正确的结果质量标准执行通过失败a→diva→停止不F（（a→div）Qdiv）HSTOP a→divF（a→div）H（divΔ（a→STOP））a→STOPR，A（a→停止）H（b→停止）（a→停止）Q（b→停止）R，RTRRT，FL，FL表1检验模型精度高低的判别水平Δ是中断操作符;详见[12]。6.2性能我们通过运行[5]的表1中涉及细化检查（与死锁或发散自由断言相反）的示例来评估模拟的性能 本文所述的方法）。表2中示出了针对上述原始和修改的上下文两者的结果;还示出了FL检查的性能正如可以看到的，性能有些差，但不是灾难性的。然而，请注意，这些过程涉及相当小的字母表;对于较大的字母表，性能预计会更差内置FCFCF'FL输入文件|S||Δ|T（s）|S||Δ|T（s）|S||Δ|T（s）|S||Δ|T（s）inv21M220M2321M220M7821M220M12521M220M145国家和平与安全委员会6.9M121M226.3M114M734.1M72M555.4M97M92SWP24M57M1630M123M6143M76M10742M93M131表2实验结果比较我们的建设与FDR3的内置故障细化检查的性能。S是状态的数量，Δ是转换的数量，T是时间（以秒为单位），M表示百万。6.3示例：连接检测我们说明了更丰富的语义模型的有用性，而不仅仅是痕迹和失败，通过一个样本应用程序的复兴模型。假设我们有一个过程P，它由两个子过程Q和R的并行组合组成。的问题D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237251模型能够检测P何时可以拒绝其共享字母表的所有事件，或者在它们在整个字母表上同步的情况下死锁。然而，它无法区分这两种可能的原因：可能是其中一个合成器能够拒绝整个共享字母表，或者可能是每个接收来自共享字母表的一些事件，但是Q和R的接收是不相交的。我们把后一种情况称为“冲突”。没有冲突（以及类似的情况）是证明并行运行的进程网络无死锁的许多有用方法的核心[14]。复活模型可用于检测冲突。 对于过程P = Q XYR，我们引入一个新事件a来表示来自共享字母表的类属事件，并形成过程PJ=QJX YR RJ，其中QJ=Q[[{（x，x），（x，a） ：x∈X}]]，XJ= X <${a}，对于RJ和Y J 也 是 类 似 的。P的连接现在对应于revivals（s，X<$Y，a），其中s是不包含a的迹。7结论定理5.4的结果表明，所有有限观测（理性）模型的可表达性在某种意义上都可以用使用优先算子的迹模型来模拟这提供了一种实用的方法来测试FDR不直接支持的模型上的精化。虽然任何这样的模型都可以直接在程序本身中实现，但我们已经证明了这是不必要的。这也进一步证明了优先级运算符的强大功能和实用性（另请参阅第二位作者之前关于优先级CSP的表达能力[13]和“慢抽象”[ 15 ]的注意，这种类型的结构可以更普遍地使用。 首先，这个构造似乎可以扩展到非有限模型;例如，将失败-发散检验减少到迹-发散，或将无限迹-失败-发散减少到无限迹-发散。其次，构造不使用模型是组合的要求。这意味着它将适用于任何合理的可观察对象集，例如[3]中提出的单例故障语义。这里描述的技术也可以用于支持FDR3 [2]中定时CSP的定时故障模型。从理论的观点来看，对理性模型的限制是相当不令人满意的，尽管它可能没有什么实际意义，因为所有已知的模型（以及可能提出的所有模型）显然都是理性的。然而，猜想4.17仍然很有趣，因为在任何一个方向上的分辨率无疑都会使我们深入了解[ 11 ]中提出的位于R之上的模型的“云”的结构确认作者感谢Tom Gibson-Robinson对FDR 3的有益讨论和实践帮助这项工作得到了DARPA的部分赞助252D. Mestel，A.W.Roscoe/Electronic Notes in Theoretical Computer Science 325（2016）237协议编号FA 8750 -12-2-0247。引用[1] www.cs.ox.ac.uk/people/david.mestel/model-shifting.csp网站。[2] 菲利普·阿姆斯特朗，G a vin L owe，J oéelOuaknine和A.W. Rosc oe.Modelche ckingtimedCS P. 在安德烈Voronkov和玛格丽塔Korovina，编辑，霍华德-60。霍华德·巴林杰60岁生日庆典，第13-33页。EasyChair，2014.[3] 克里斯蒂·博尔顿和吉姆·戴维斯。一种用于顺序进程通信的单例故障语义Formal Aspects of Computing，18（2）：181[4] Thomas Gibson-Robinson，Philip Armstrong，Alexandre Boulgakov，and A.W.罗斯科FDR 3-CSP的现代细化检查器。系统构造和分析的工具和算法，第187-201页。Springer，2014.[5] Thomas Gibson-Robinson ， Henri Hansen ， A.W. 罗 斯 科 和 王 旭 。 CSP 的 实 用 偏 序 NASAFormalMethods，第188-203页。施普林格，2015年。[6] C.A.R.霍尔通信顺序进程。普伦蒂斯-霍尔公司，上鞍河，新泽西州，美国，1985年。[7] R.米尔纳通信系统的微积分。Springer-Verlag New York，Inc.美国新泽西州锡考克斯，1982年。[8] 罗宾·米尔纳，约阿希姆·帕罗，大卫·沃克。移动过程的演算，即。信息与计算，100（1）：1[9] 伊恩·菲利普斯。拒绝测试。Theoretical Computer Science，50（3）：241[10] A. W.罗斯科并发的理论与实践。普伦蒂斯霍尔PTR，上鞍河，新泽西州，美国，1997。[11] A.W. 罗斯科CSP模型的复兴、稳定性和层次结构The Journal of Logic and Algebraic Programming，78（3）：163[12] A.W.罗斯科了解并发系统。计算机科学中的文本。Springer，2010.[13] A.W.罗斯科CSP优先级的表现力。在2015年MFPS会议记录中，2015年。[14] A.W.罗斯科和纳伊姆·达蒂追求死锁的自由。信息与计算，75（3）：289[15] A.W.罗斯科和菲利帕·霍普克罗夫特。通过优先级缓慢抽象。Zhiming Liu，Jim Woodcock，and HuibiaoZhu，editors，Theories of Programming and Formal Methods，pages 326-345. Springer-Verlag，柏林，海德堡，2013年。[16] J·沙利特形式语言与自动机理论第二教程。剑桥大学出版社，2009年。