LTS自动分析的并行进程网络验证中的组合状态空间约简和解开行动

理论计算机科学电子笔记175（2007）27-46www.elsevier.com/locate/entcs使用的组合状态空间约简解开行动王旭Marta Kwiatkowska1伯明翰大学计算机科学学院Edgbaston，BirminghamB15 2TT，UK摘要我们提出了一种组合技术，用于并行进程网络的有效验证。它是基于一个自动分析的LTS的个别进程（使用基于故障的等价保留分歧），确定他们的一套不纠结的行动是合成的，也就是说，在未纠缠的动作上的同步不会破坏它们的“冲突自由”。对于网络的进程，使用全球解开行动来自当地的，有效的减少算法已经设计了大量的小进程并行运行的系统关键词：解纠缠作用，连续自由，偏序约简，过程代数，组合性，决定论，和部分连续。1引言非正式地说，一个未纠缠的行动2是一个因果关系和冲突的离散事件系统中的特殊行动[23]。在系统的任何状态下，动作（如果被启用）不应通过与系统的其余部分的任何冲突而纠缠在一起，并且其对系统动力学的唯一贡献是因果关系。因此，如果未观察到解开的动作（由于隐藏或其他操作），则其发生变得与时间无关3。这使我们有机会通过只考虑其发生时间的一种可能性解纠缠动作的概念与真正的并发语义[23]、偏序约简[12，21]和Petri网展开[10]中的类似思想密切相关。由于我们的工作将在进程代数的框架中进行（相比之下，到基于状态的形式主义或Petri网），并集中于状态空间缩减，1{X.Wang，M.Z.Kwiatkowska}@ cs.bham.ac.uk[2]我们在这里倾向于使用“行动”一词而不是“事件”，以便区分行动和它们的发生。但在本文的其余部分，它们可以互换使用3需要某种类型的进展/最大化假设来保证动作最终会发生。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.05228X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）27与我们最接近的工作是Groote，van de Pol和Blom [8，7，2，3]的τ2动机这项工作的动机是我们使用进程代数（例如CSP和FDR2 [6]）来验证异步电路[22]的经验，其中门级电路中的高并发性会导致严重的状态爆炸问题。一个著名的例子是树仲裁器[5]。树仲裁器由仲裁器单元树组成。每个仲裁器单元充当其子仲裁器的双向仲裁器，同时充当客户端之一的父节点。以这种方式，树仲裁器通过双向仲裁单元的层次结构来树型仲裁器的状态空间随着树的增大呈指数增长，并且由于其固有的冲突性，不容易进行约简仲裁。在此之前，Petri网展开技术[10]和偏序约简增强的BDD方法[1]已被应用于它，但成功有限。在本文中，我们将提出解开行动作为一个可行的解决方案，以验证这一点 类似的系统。..图1. 仲裁器树，以及仲裁器单元的原始LTS和简化LTS不纠缠是一个简单的想法。我们将把理论论证推迟到后面的章节。对于仲裁单元的例子，不难看出只有两个动作在冲突中纠缠，即1+和 2+。这些纠缠的动作与所谓的输出选择信号转换一致[4]。有了这些信息，通过在状态空间的探索中优先考虑未纠缠的动作（类似于FDR2中的追逐缩减），可以直接给出状态空间缩减算法。也就是说，在深度优先搜索中，给定一个具有非空的未纠缠传出转换集合的状态，我们使用某种策略从集合中挑选并优先考虑一个进行探索;来自同一状态的所有其他转换，未纠缠或纠缠，将在探索中完全忽略。如果一个国家没有R1+R2+R1+R+a+XA1+A2+r1-r2-r-r-a-a-a2-a1-R1+R2+R2+R1+R+R+R2+R1+a+R+a+A1+r2+r1+a+A2+XR2+R1+r1-A1+ A2+r2-R2+R1+r-a1-r1-r2-r-a2-R2+R1+a-r-r-a-a-a-R2+R1+a2-a1-R a阿布塞尔..r1 a1 r2 a2.X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）2729联系我们如果没有混乱的转换，则需要探索从该状态的所有转换。 它并不难应用该算法来手动减少仲裁器单元的LTS。图1给出了基于一种可能的优先级策略的缩减状态空间。然而，只有当我们将仲裁单元视为一个封闭系统并且所有未纠缠的动作对于检查的属性都不可观察时，上述简化才是正确的。与环境同步可能会引入新的冲突，从而破坏动作的连贯性。以前的τ-连通性研究通过只考虑τ作用[7，2，3]或局部可见全局不可见来解决这些问题（lvgi）行动4 不同步[11]。其次，考虑环境因素的无纠缠性分析是困难的，因为分析必须避免显式地在全局状态空间上工作，这在我们的上下文中是难以解决的在τ-连续约化中，所提出的解决方案是使用全局状态空间的符号表示（所谓的线性过程）上的定理证明[3]，或者使用我们所采用的组合性[11然而，由于所涉及的动作必须是无同步的，因此它们的组合性不适用于树仲裁器，树仲裁器的lvgi动作，例如r、a、r1等，需要进一步同步。在本文中，我们提出了一个并发系统的组合技术，这样的untangledness分析是在一个局部的水平。组合性定理自动地从局部信息计算全局无纠缠性信息。利用所得到的结果，状态空间约简可以直接应用于全局系统。论文的结构。 在介绍了基本符号（第3节）和并发系统（第4节）之后，第5节提出了两个关于具有lvgi作用的LTS的重要（部分）确定性概念，一个比另一个更强。前者在lvgi作用上是合成的，没有同步势，并引入了一个简单而有效的on-the-dummy还原过程（第6节）。后者消除了同步限制，并成为所有lvgi动作的合成，从而实现合成约简（第7节）。初步的实验结果，并在第8节中总结的文件3基本符号LTS（Labelled Transition System）是一个元组（A， S， T， s0），由一个被称为字母表的可见事件的（有限或可数无限）集合A、一个状态的（有限或无限）集合S、一个转移关系T：S×（A<${τ}）ParticipS和初始状态s0∈S组成。（事件、序列和迹）设e是可见事件，a是τ或可见事件，Δ是A的子集。 Δτ和Aτ表示Δτ和τ。 k和l是事件的有限序列（包括空序列）5。 t和u是有限的[4]形式上，给定一个进程网络，lvgi动作是在单个进程上可见的动作，但最终在进程组合期间被隐藏，因此在全局网络级别上不可见。5有时，a和e也被用作单例序列或迹。30X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）27−≤| |=∈K一不Kτee=迹，即非τ事件的有限序列。k、l、t和u是无限变体，而k、l、t和u可以表示无限和无限。（序列操作）并置用于序列连接，例如k=l。 k 给出序列k的长度（对于无穷大，ω）。 head和tail（一元前缀运算符）被定义为正常。是一个二元整数运算符，根据多重性从一个序列中从左到右删除另一个序列中的所有成员例如e1e2e2e3e1e2−e3e2e2=e1e1e2和e1e2−e2e3=e1。（前序、投影和包容）是（有限）上的前缀顺序 或无限）序列。[001 pdf1st-31 files]计算一个有限的（有限的）前缀集合，或in finite有限sequence序列. k∈TΔ从k ∈ Δ中移除所有不在Δ中的向量。两者都可以被举起在序列集上运行。 我们有一个条件，即kia∈Aτ·kT{a}≤lT{a};条件kilTA包含kTA。更进一步，我们定义了以下符号：定义3.1[路径和箭头符号]给定LTS，（A， S， T， s0）：• 一条 有限的路径是一系列交替的状态和事件，s0a1s1a2... 一个NSN（∈PATH ^ S ×（Aτ ×S）），其中（s i−1，a i，s i）∈T，对所有1 ≤i≤ n。s0a1s1a2. （PATH标记序列。K^S×（Aτ （1）是一条无限长的路，1a2...... 是其• S−→K有一条从s到SJ的k-标号有限路。• s−→i → k有一条从s开始的k-labelled无限长路径。• k在s处被启用，即， s−→，i ≠t这里存在一个状态s Jsuch，sJ。•−→s Jitheexists areablesattasJ，我们假设SJ是由a引起的• s=sJis−→sJandkTA=t;s=tis−→和kTA=t;s=t我在那里存在一个状态sJsuch，sJ。状态s是死锁的，即死锁（s），i_s没有任何传出转换。一个状态s是发散的，即发散的（s），如果LTS中有一条从s开始的无限τ-路径。不定义3.2[Traces]给定LTS，有限迹FT的集合是{t|s0=0不，故《无量寿经》云： | s0 =0}，则死锁跟踪集LT不是{t |s·deadlock（s）{s0 =s}，并且发散迹线DT的集合为{t|s·dive rgent（s）定义3.3[归一化] LTS，LTSN，在所有τ-跃迁中归一化areself-loops，即S−→sjs=s J，并且不存在m双周期跃迁，即s−→sjs−→sJsJ=sJJ。K一K路径的标记顺序是a1a2.. an（即n=0时为n同样地，X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）2731−→Je−→Je\\SBDτ一^ee4并发系统LTS中的基本进程可以使用并行和隐藏运算符组合起来，形成一个并发系统[15]。SCS：：= LTS|SCSSCSJ|SCS\Δ |SCS [R1−1]定义4.1[平行]给定LTS1和LTS2，LTS1<$LTS2给出另一个LTS，（A， S， T，s0），其中A=A1<$A2，S=S1×S2，s0=（s0，s0），T是最小1 2满足以下规则的关系：一s1s1一a∈/A2一s2s2一a∈/A1s1−→s1Js2−→s2J（s1，s2）−→（s1J，s2）（s1，s2）−→（s1，s2J）（s1，s2）−→（s1J，s2J）定义4.2[隐藏]给定LTS，LTS Δ给出一个新的LTS，（AJ，S，TJ，s0），其中，AJ=AΔ，并且TJ=TJ[τ/Δ]，即，在T中的每次出现时，用τ代替每个Δ事件。定义4.3 [重命名]给定LTS，LTS [R]，其中R：AParticipateAJand dom R ranR={}，给出一个新的LTS，（AJ，S，TJ，s0），其中AJ=（A\dom R）ran R，and TJ={（s ，a ，sJ ）|（a∈/domR<$（s ，a ， SJ ）∈T）<$（<$e·（e ，a ）∈R<$（s，e，SJ）∈T）}.该定义允许m到n重命名。通常只需要特殊情况：1比1（R1−1）、1比m（R1−m）和m比1（Rm−1）。4.1语义在经典CSP [15]中，稳定故障和故障/分歧是CSP中使用的主要语义模型。它们都是有限的跟踪模型。然而，有一个新开发的无限迹CSP模型[16]，该模型保留了CSP过程中的所有发散迹给定LTS，（A，S，T，s0），状态s是稳定的，即. e. stable e（s），i<$（s−→）. 一些-次，我们也使用stable e（s，Δ）来表示εa∈Δ·<$（s−→）。 Givenasetof有限序列，lmt（）输出一组无限序列，每个序列都是属于该集合的递增（即预定序）有限序列链的极限定义IB=IT成本（DT）。（稳定故障和行为）稳定迹线ST的集合是{t|伊普斯·stable e（s）{0=0}。 s个表故障的集合SF是{（t，Δ）|s·stable（s）s0=<$ts<$<$e∈Δ· <$（s−→）}。B_e的类型为BEHV（A）=^A_e（A_e·{τ ω}）Aω。具有一个或多个BH的结构是{k|k<$∈FT<$k<$∈IT<$（k<$=tτ ω<$t∈DT）}。定义4.4[SBD等式]LTSS=BDLTSJi <$SBD（LTS） =SBD（LTSJ），LTSSB=DFLTSJi <$SBDF（LTS）=SBDF（LTSJ），其中SBD（LTS）=（FT， DT， IB）和SBDF（LTS）=（SF， DT， IB）。32X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）27∪定理4.5（最弱同余[20，13]）W.r.t.并行、隐藏和重命名操作符如上文6所定义，SB=DF是在LTS上保存LT和DT信息的最弱的一致性。定义4.6[U-确定性]给定一个LTS，它是U-确定性的（即不稳定确定性7）i <$ST<$DT={}且te∈FT<$（t，{e}）∈/SF。命题4.7给定U-确定性LTS和LTSJ，LTSSB=DFLTSJiLTSS=BDLTSJ 。给 定 U- 决 定 性 LT S ， 存 在 一 个 正 规 的 L TSN 使 得LTSSB=DFLTSN。证据根据U决定论定义和FT= STDT. 基于SBD（LTS），由于IB=lmt（FT），可以构造归一化的LTS。Q命题4.8U-确定性LTS在平行合成下是封闭的证据 规范化这些LTS并使用并行运算符的转换规则。很容易看出，结果也是正常的Q5解缠动作分析给定一个由τ动作、lvgi动作和全局可见动作组成的LTS，其状态空间遍历算法的最重要组成部分可能是，在具有多个传出转换的状态下，如何选择下一个要继续的分支。这个决定可以分为两部分。一种是我们称之为可见的选择，它决定了全球行为中的下一个可见行动。另一种被称为无形的选择;它们决定遵循哪个特定的下一个分支，以实现可见选择的目标τ和lvgi转换，以及模糊的转换，产生了看不见的选择。通常，可见的选择与不可见的选择交织在一起。但在一定条件下，它们可以相互分离或分离，即它们相互“独立”。也就是说，无论采取什么样的无形选择，它都不会影响已决定的有形选择的实现。对于不考虑二义性跃迁的情况，这是τ-惰性[8]。这种见解导致了许多过程代数框架中的状态空间缩减算法[14，11，2，6]。该算法简单地对不可见的选择进行任意决策，并在状态空间遍历中完全忽略其他选择。它也构成了我们在第6节中的约简算法的基础。 我们把这样的系统称为可分离系统。6最弱同余结果可以推广到其他CSP算子[15]，因为SBDF也是这些CSP算子的同余[16]。[7]正如罗斯科[ 19 ]所建议的，U决定论与经典的CSP决定论（排除了分歧）相反，并不完全符合决定论的操作直觉。例如，它不具有τ-惰性[8]。在这个意义上，空A i集上的可积性（第5节）更接近于运算直觉。X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）2733∈一我e我我我我{}我我5.1拆卸性LTS被视为行为的接受者。我们假设Av和Ai分别是全局可见动作的集合和lvgi动作的集合。当被喂食一个globalbeh aviour（即，kBEHV（Av）），则接受者将控制LTS中的不可见选择并尝试接受或拒绝该行为。接受者决定无形选择的不同方式因此，一个策略可以被看作是原始LTS的展开，然后是解决其中所有不可见选择的约简，例如图1中的约简LTS是原始LTS的策略。对于同样的行为，接受者可能既有接受它的策略，也有拒绝它的策略给定LTS，形式上是一个策略，stg：PATH×BEHV（Av）→（Aτ×S）{stop， reject}是满足以下规则的最小（子集顺序）部分函数：(i) {s0}×BEHV（Av）额定电流stg(ii) （s0a1.. . sn，ekn）∈domstgstg（s0a1.. . sn，ek）∈{（a，s）|sn −→sa∈Aτ{e}}{reject| <$sn−→稳定e（sn，Aτ）}(iii) （s0a1. sn，n）∈dom stgstg（s0a1. sn，n）∈ {（a，s）|n−→{停|stable（s n，Aτ）}S 拉瓜 ∈Aτ}(iv) （s0a1. sn，τω） ∈dom stgstg（s0a1. sn，τω） {（a，s）|n−→Aτ}{拒绝|stable（s n，Aτ）}S a∈(v) stg（s0a1.. . sn，k）=（a，s）（s0a1.. . snas，k<$−（aTAv））∈domstg最初，接受者准备好接受任何行为（规则1）。一旦被馈送，接受器就开始执行以逐步消耗序列（规则5）。执行状态（即函数的输入）由历史（LTS中的有限路径，其标记序列在投影到Av上之后给出了表示消耗部分的馈送行为的前缀）和行为的子集（表示剩余部分）组成。函数的最小性意味着stg上只定义了可达状态。给定一个可到达的状态和一个挂起的动作，即在顶部 在当前的summix中，接受者可以自由地做出任何看不见的选择来在LTS中过境，例如，（a，s），只要跃迁与e（可见选择）一致，即a Aτ e（规则2）。当执行到达一个无法做出一致的不可见选择的状态时，接受者将停止（如果消费完成）或拒绝（如果消费未完成）。 给定一个viourk和一个strategystg，如果接受者的执行以stop或reject结束，则它产生一个有限路径;否则执行产生一个无限路径。接受条件：Wesaystg是k的一种加速策略，在LTSi上，执行不以reject结束，并产生一条路径，其标签序列跟踪包含k。 另外，stg是一种针对k-εL-TS的再激励策略.然而，这些策略不能正确处理分歧。例如，如果LTS的初始状态有一个τ循环，LTS对任何非平凡的Av行为都有一个简单的拒绝策略（即无限地遵循τ循环）。这对于像标准化LTS这样的系统是一一34X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）27我我我我∪\我联系我们（因此，在战略上要有额外的要求定义5.1[公平性]策略stg是一个公平的策略，它（无限）执行不会导致一个状态，在此之后，尽管一个动作e等待被消费（比照规则2），它不再进行Av跃迁，且作用量a∈Aτ<${e}总是已启用（即在LTS上）但从未使用。上述定义是一种最大化和弱公平性要求的行动，在偏序语义。但是，它并不适用于所有行动。只有挂起的e和Aτ操作将被保证进行。e的进步将能够引导战略走出不进步的循环。Aτ行动的进展可以指导策略摆脱Aτ任何成员的无限延迟。这是这是合成的必要条件定义5.2[可能必须接受]如果存在接受策略，LTS可能接受行为。它必须接受一个行为，如果不存在一个公平的拒绝策略。不难看出，可能被接受的行为的集合恰好是BH（LTS Ai），因此暗示了SBD等价。定义5.3 [可分离性]给定LTS和A iA v= A，A i可从LTS分离（或LTS可在Ai上分离）i <$LTSm ay-acceptk<$i <$LTSmust-acceptk<$，对于所有k<$∈BEHV（Av）。可分离性有许多好的性质，其中一些将在第6节中显示，其中将给出基于可分离性的约简算法。在这里我们将只提到U-决定论和组合性的一种受限形式命题5.4Δ可从LTS分离意味着LTSΔ是U-确定的，但反之则不然。证据违反U-决定论定义中的任何一个条件都意味着BH（LTS\Δ）中行为的公平拒绝策略。 由于反例：S =（e→Div Q eJ→Stop），其中Δ ={e}，因此相反的情况不成立。Q然而，重要的是要注意，Δ上的可分离LTS并不意味着LTSΔ是可分离的。隐藏消除了Δ成员之间的区别;因此，对策略的进度要求更少，行为的公平拒绝变得更容易。实际上，在第6节的简化算法使用了独特性信息之前，不应对LTS应用隐藏可分离性是在无同步的lvgi动作上合成的（参见Theo-rem7.1 for its form）8.这部分是由于Aτ的进度要求行动例如，R=e→R在{e}上是可分离的，并且RJ=eJ→eJJ→Stop在{eJ}上是可分离的（即，即使没有任何进展要求）。但是，如果没有对{eJ}的进度要求，RRJ在{e， eJ}上是不可分离的。8由于篇幅所限，省略了定理及其证明\X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）2735--我我我我的v另一方面，合成性不适用于具有同步潜力的lvgi行为。非正式地说，这是由于可扩展性允许在Ai动作内的冲突（极端情况是在一个动作内的“自动冲突”）。 它 只是这些冲突的解决并没有排除与Av部分的因果关系依赖，这使得这些冲突与Av部分的冲突是可分离的。一旦存在同步，冲突就可以在进程之间传播并创建可能不可分离的新冲突以下两个过程给出了示例：P=e→e→eJ→停止Qe→eJ→停止Q=e→eJ→停止在A i=e的情况下，P和Q都是可分离的，尽管P包含一个自动连接，在这个意义上，一个分支需要两个e动作来启用eJ，而另一个只需要一个。然而，两者的平行组合是不可分离的，因为一个分支将导致eJ的出现，而另一个则不会。因此，为了使组合性充分发挥作用，必须完全排除Ai行动上的冲突。这就给了我们一个无纠缠行为的概念。5.2不纠缠在lvgi动作同步的情况下，不缠结应对类型敏感以及驱动因果关系所花费的lvgi行动的数量给定LTSN9和Ai≠Av=A，策略stg：PATH×BEHV→S）{stop， reject}是满足以下条件的最小偏函数(i) {s0}×BEHV无规stg（Aτ×(ii) （s0a1.. . sn，ekn）∈domstgstg（s0a1.. . sn，ek）∈{（a，s）|n −→eS a∈Aτ{head（ekT）}}{reject| <$sn−→}(iii) （s0a1. sn，n）∈dom stgstg（s0a1. sn，n）∈ {（a，s）|n−→{停|stable（s n，Aτ）}S 拉瓜 ∈Aτ}(iv) （s0a1. sn，τω） ∈dom stgstg（s0a1. sn，τω） {（a，s）|n−→Aτ}{拒绝|stable（s n）}(v) stg（s0a1.. . sn，k）=（a，s）（s0a1.. . snas，k<$−（aTA））∈domstgS a∈与前一个一样，接受者控制Ai动作的顺序和发生 因此，规则3以及规则2和规则4中不涉及拒绝的部分保持不变。 与前一个不同的是，A i的行为在美联储的行为中变得可见（规则1和5），而接受者更敏感（规则2和4中涉及拒绝的部分）。例如，一旦发生了正确类型和数量的动作（即从馈送行为中删除），则将在当前suprix（即未决e）之上启用新动作。e不能被任何其他A动作延迟;如果它没有在LTS上同时启用，它可能会导致立即发出拒绝（9基于非标准化LTS的定义也是可能的。但它使陈述复杂化，并且本文不需要一一一36X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）27∪拒绝规则2的部分）。它给了接受者更多的拒绝行为的自由（例如，上面P过程的Pj行为将导致拒绝）。验收条件保持不变，但对Ai可见性的调整接受条件：stg是k的一个ccepting策略，在LTS上，执行不以reject结束，并产生一条路径，其标签序列跟踪包含k。 另外，stg是k-均值L-均值S的一个拒绝策略.同样，公平性可以被简化，因为美联储的行为（Ai可见）现在可以引导自己。定义5.5[公平性]策略stg是一个公平的策略，它（无限）执行不会导致一个状态，在该状态之后，挂起的动作e总是被启用（即在LTSN上），但从未被执行。此外，如果我们区分有限拒绝策略（即不包含fed行为的跟踪的有限执行）和有限拒绝策略（即以reject结尾的有限执行），很明显只需要有限拒绝策略命题5.6（有限拒绝）如果一个行为有一个无限公平的拒绝策略，那么它也有一个有限的证据 当最终未决e未启用时，在其中一个状态下发出拒绝。Q可以接受和必须接受可以像上一节一样定义。然而，BH（LTSN）只是可能被接受的行为的一个子集，并且无纠缠的定义必须相应地改变定义5.7[解纠缠]给定LTSN（且Ai= Δ），Δ解纠缠于LTSN（或LTSN不纠缠于Δ）i <$LTS必须接受k<$，对于所有k<$∈BH。给定Δ，其无纠缠性决策问题可以通过使用附录A中的稳定故障模型的CSP细化检查来解决。这是由于有限拒绝属性。支票的LHS（即规范）是一个固定过程，而RHS是由另一个固定过程协调的LTSN的两个副本这种形式的精化问题在NLOGSPACE中命题5.8解纠缠的作用集在子集包含和并集下是封闭的。证据子集化：对一个行为的任何拒绝策略都将随着Ai的增加而保持不变。联合：假设w.l.o.g. A i，AJi和A v划分A.如果A iAJi是纠缠的，则存在满足c0的（t，u）或满足c0J（c.f. 附录A中的提案A.2和A.5如果A i和AJi都被解开，则A i或AJi中的任何动作都可以自由地向前移动或插入到t或t J中的另一个位置，在那里它也被启用（参见图10）。提案A.3）。例如，如果e = head uj e∈ A i，则e（t J−e）必须在FT（c1 on A i）中;如果e = head uJe ∈ A v，则e在t J中，并且可以逐步移动到头部（c2 on A i和AJi），从而得到e（t J− e）。 e（t J− e）∈ FT和e（tJ−e）∈DT（c0J）。因此，可以逐步将t（和tJ）转换为以ue为前缀的形式（并转换为uJ∈ DT）。矛盾QX. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）2737∈我（Maximal untangled set）给定Δ，通过对Δ的每个单例子集进行CSP检查并取成功子集的并集，可以找到它的最大未纠缠动作子集定理5.9 LTS N中的解纠缠Δ也是可分离的（反之亦然）。证据假设可接受性不为真，并且可以接受但不必须接受的B是K。 有两种情况：一种是有限的拒绝策略，或无限公平拒绝策略。k∈BH（LTS\Δ）意味着有克杰BH（LTSN）表示Avb由ykJ等于k所隐含。 由于无纠缠性的接受者在拒绝时有更大的自由度，而且无纠缠性的公平性严格弱于可 纠缠性的公平性，因此B策略可以直接作为k ∈ j的公平性拒绝策略.相反的情况并不成立，因为有反例，比如最后的过程P第5.1节。Q注意，无纠缠性、可分解性、U-决定性等形成了部分决定性属性的层次结构（参见附录C中的图2）。一个有趣的讨论 经典进程代数中的各种确定性和连续性概念可以在[18]中找到，其中may-testing和must-testing也用于验证确定性。 在我们的上下文中，一致性与A上的无纠缠性相同（即，全字母表）。未纠缠的动作是合成的;全局未纠缠的动作可以从局部动作计算出来。 组合性定理将在第7节中给出，其中还提出了一种由其实现的新的组分还原技术。新技术将全局解纠缠信息馈送到一个专门设计的称为Chase+的在线约简过程，该过程通过利用可解性来减少状态空间（参见定理5.9）。6约简算法新算法是FDR 2 [6]中chase函数的扩展，并且与基于τ-惰性的约简算法[2，11，14]也有相似这个想法是基于这样一个事实，即在一个可分离的系统中，一个行为被它的LTS接受，如果它被LTS的公平策略接受因此，LTS可以通过删除其中的所有其他策略来减少因此，约简算法最重要的组成部分是找到一个合适的公平策略。（循环策略）假设A τ中的动作被安排在具有默认起始位置的（有向）循环中，并且next（c，Δ）是一个函数，给定当前动作c和候选动作集合Δ，该函数输出在循环中最接近的c之后的候选。 (Note当c=0时，假定默认起始位置。）有限状态LTS上的公平策略的一个子类，称为循环策略，使用循环策略来实现公平性。形式上，它们是满足5.1节中相同条件的最小偏函数38X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）27我e我我ee一我e我我我我我我MCC{}我我^}我但将第2改为以下第10条：2aJ。 （s0a1.. . ansn，ekn）∈domstgn< $fairl o o p（s0a1.. . ansn）stg（s0a1.. . ansn，ek）∈aτa{（a，s）|sn−→sa=next（anTAτ，{a：Ai|sn−→}）}{（e，s）|sn−→s可稳定e（sn，Aτ）} <${reject| <$sn−→稳定的（sn， Aτ）}2bJ。 （s0a1.. . ansn，ekn）∈domstgnfairl o o p（s0a1.. . ansn）stg（s0a1.. . sn，ek）∈{（e，s）|sn−→s} <${（a，s）| <$sn−→<$sn−→s<$a∈Aτ}{reject| <$sn−→稳定e（sn，Aτ）}其中公平循环（s0a1. s n）是真的，i ∈ s0a1.. s n是一条Aτ-路，比如s ia i+1. s n，包含一个公平的 Aτ-环，但s ia i+1. sn-1没有。 一个 公平的 Aτ环是我Aτ循环至少经历了一轮循环。直觉上，这意味着策略将优先考虑Aτ我过渡作为只要历史上的Aτ跃迁还没有形成一个公平的Aτ环我我一旦一个被形成（并且正好在这一刻），即将到来的e过渡将是优先级（在e上实现弱公平性）。此后，Aτ跃迁继续优先。命题6.1给定LTS和Ai，循环策略是公平策略。在LTS上应用循环策略stg给出了减少的LTS。与[2，3]类似，可以证明存在一个让...，我... 是LTS中A τ跃迁的反射性、对称性和传递性闭包所诱导的等价性。每个成员Si是一个等价类。将S i上 的stg入口点的 集 合 定 义 为ENT（S i）={s：S i|s = s0（stg（s0a1.. . sn，k∈（n）=（e，s）∈Av）}，并且S i上的第g^个出口点的集合为EXT（Si）={sn：Si|（（s0a1... . ansn，ekn）∈domstgnfairl o o p（s0a1.. . ansn））stable（s n，Aτ）. stg退出点的集合恰好是规则2bJ被激活或达到Aτ稳定性的那些状态。命题6.2给定LTS上的可分离A i和循环策略stg，如果stg的任何执行在任何时间进入Si ∈ MCC并打算离开（即具有待定e），则退出点（∈ EXT（Si））由其入口点（∈ENT（Si））唯一确定。证据 NEXT对如何输入入口点不敏感。 因此，同一点上的所有条目导致LTS中的相同路径，因此激活了相同的点或达到了相同的Aτ稳定点。Q（代表函数）设ENT和EXT是所有Si∈ MCC的入口点和出口点集合的并集。因此，存在一个代表性函数exit：ENT→EXT，将每个入口点映射到其出口点。出口点可以[10]严格地说，本节隐含地假设了LTS的规范化这改善了演示文稿，但在技术上并不需要。eX. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）2739我我\\完全代表了它的所有入口点。如果退出点是Aτ-稳定的，则代表上的传出变迁集恰好是该点上的传出变迁集。否则，在代表上的传出跃迁的集合恰好是与τ自环组合的Av传出跃迁的集合定义6.3[归约函数]给定可从LTS分离的Ai，函数chase+（LTS， Ai）输出另一LTS，（Av， EXT， TJ，exit（s0）），其中TJ={（s，e，sJ）：EXT×A v×EXT|s i：S·s −→EXT稳定（s，Aτ）}。s i<$sJ=exit（s i）}<${（s，τ，s）|s ∈因此，我们可以采用类似于[2]中的方案来实现chase+，作为一个集成在精化或模型检查中的on-the-physical过程。还要注意，循环策略是局部策略。也就是说，定义只取决于未决的行动和历史的顶部元素，退出点可以通过简单地遵循策略来计算。因此，退出函数不必明确地构建。它使Chase+Reduction过程的实现更简单、更有效。定理6.4（保持）Δ可从有限态分离LTS意味着chas e+（LTS，Δ）是正规的并且chase+（LTS，Δ）SB=DFLTS\Δ.证据 标准化遵循Chase+的定义。Preservation：chase+（LTS，Δ）包含单一策略（由于标准化）。该策略正是原始循环策略的加速（即去除中间τ链）（除了当没有挂起时的执行状态 即死锁或发散，由于可并行性，可以安全地忽略）。因此，chase+（LTS，Δ）和LTS具有相同的一组可能被接受的行为，这意味着chas e+（LTS，Δ）S=BDLTSΔ。因为b是U-决定性的，所以它们是SBDF-等效。Q7成分还原为了使本文的归约技术有效地工作，最好以LTSNΔ的形式表示所有过程（包括U-非确定性过程），而不是直接表示为非归一化LTS。我们的哲学是，如果一个人对细节有足够的好奇心，那么LTS中所有未考虑的选择，即那些由于τ-跃迁或模糊跃迁而产生的选择，都可以通过引入一些额外的lvgi作用来解释。这不会导致任何表现力的损失，例如w.r.t. SBDF模型。此外，这些lvgi选择在验证过程中需要保持不变，除非它们是可分离的，在这种情况下，它们可以在还原后隐藏和删除。一个过程的网络通常表示为SC[−L−T−S−→N]，其中SC是一个“过程”cess上下文”。（关于上下文符号和相关转换的详细信息见附录B。）复合性定理的形式如下：e40X. Wang，M.Kwiatkowska/Electronic Notes in Theoretical Computer Science 175（2007）271212∈{}∈1联系我们2定理7.1（组合性）11LTSN关于LTSN理清行动集合U1和U2（分别）意味着U在LTSN <$LTSN中解纠缠，其中U=（A1<$A2）\（（A1\U1）<$（A2\U2））。证据归一化LTS的并行组合给出了新的归一化LTS。 给定一个（全局）b∈k∈BH（LTSN<$LTSN），k∈TAj是L T S j的一个（局部）b∈ a对于所有j1， 2 . U的定义 确保任何未纠缠的动作全球层面也解开了所有参与行动的本地LTS。因此，如果k的（全局）策略可以导致具有最优kj的执行，则接下来kJTAj将给出LTSj上的kTAj的（局部）策略。假设对于一个全局behaviourk，存在一个有限的弹出策略，它会导致一个具有行为t（在拒绝之前）的执行。 如果拒绝是由于tTA j之后e上的规则2，其中eA j和e在迹tTAj之后的LTSj上未被启用，则给出有限拒绝策略f或kTAj。如果k是不同的，并且拒绝是由于规则4，则预测的l ocalbeh a viour是一个不同的痕迹，这是一个很好的例子。 Thus（kjTAj）τ ω是LTSj的发散行为。 在t T A j之后，给出了（kjTAj）τ ω 的 有 限 拒 绝 策 略。 因此，两个局部LTS上的非纠缠性是不成立的。Q因此，我们的约简工作如下：(i) SC[−L−T−S−→N]c可以被变换为（N[−L−T−S−→JN]）\Δ。(ii) 在每个LTSJN上，找到Δ的最大未纠缠子集，比如U。(iii) 用定理7.1计算从−→U的全局纠缠作用量U。(iv) 在全局系统上应用chase+，我们得到最终的简化系统：chas e+（[−L−T−S−→JN]，U）