元件连接器的符号模型检测 - Sascha Klüppelholz、Christel Baier - 德国德累斯顿工业大学

理论计算机科学电子笔记175（2007）19-37www.elsevier.com/locate/entcs元件连接器的符号模型检测Sascha Klüppelholz，Christel Baier德国德累斯顿工业大学理论信息学院{klueppel，baier}@ tcs.inf.tu-dresden.de摘要本文报告的基础和实验结果与模型检查器的组件连接器建模的网络的通道在演算Reo。具体化形式主义是一种分支时间逻辑，它允许推理网络中的协调原则和数据流。底层的模型检测算法依赖于标准的基于自动机的方法的变体和类CTL逻辑的模型检测。该实现使用了一个符号表示的网络和启用的I/O操作的二进制决策图的手段。它已被应用到一对夫妇的例子，说明我们的模型检查器的效率关键词：约束自动机，模型检测，分支时间逻辑，数据流，二元决策图1介绍在过去的15年里，许多语言和协调模型已经被定义，它们提供了用于将组件插入在一起的粘合代码的形式化描述在本文中，我们解决了外生协调语言Reo [2]的后一个方面。在Reo中，粘合代码由通道网络提供，通道网络通过一系列操作获得，这些操作创建通道实例并将它们链接到（网络）节点中Reo网络的语义以不同但一致的方式提供[2]通过声明是否以及哪些数据项可以在节点上写入或读取的接受和输出谓词，形式化了网络配置下I/O操作的启用和在[6]中，使用标记转换系统的变体（称为约束自动机）提出了一种操作语义，该语义指定了Reo网络中的逐步行为和可能的数据流，并与[5]的定时数据流语义一致1作者得到DFG-NWO-项目SYANCO和VOSS II的支持1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.00320S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）虽然Reo是一种优雅的形式主义，可以用简单的组合操作符合成组件连接器，但具有许多通道的Reo网络往往很难理解。因此，分析Reo网络指定的协调机制的工具支持基于约束自动机语义验证Reo网络的算法已经在[6]中提出，用于检查（bi）模拟和语言等价性，并在[3，10]中提出了时间逻辑规范。我们在这里遵循后一种方法，并处理[3]中引入的定时数据流逻辑（TDSL）的分支时间，时间抽象变体，用于推理线性时间设置中Reo网络忽略一些小的差异，我们的逻辑，称为分支时间流逻辑（BTSL），包含在[10]中考虑的逻辑中，其中主要关注动态重构的处理，而不是模型检查。BTSL将标准的CTL运算符[11，12]与一种特殊的路径模态<$α<$及其对偶[α]，允许通过正则表达式α来推理在网络节点处可观察的数据流。例如，假设C是通过输出端口Request和输入端口Grant链接到Reo网络的组件，在输出端口Request中，C发送请求以获得对某些资源的访问，在输入端口Grant中，C可以接收授权。然后，BTSL公式[true陈述C的每个请求最终将被批准并且所需资源将可用于C的可能性。本文的目的是报告一个BTSL模型检查器的实现。输入是一个Reo网络和一个BTSL公式Φ，必须对该网络进行BTSL模型检查过程依赖于用于模型检查类CTL逻辑的已知方法和用于线性时间逻辑的基于自动机的一个粗略的草图模型检查的BTSL类逻辑已经在[10]中给出的，其遵循标准CTL模型检查方法[14，12]并使用对TDSL模型检查问题的简化。然而，[10]中没有提供关于有效实施的事实上，对于BTSL，对实时逻辑TDSL的模型检查问题的简化是不必要的，因为更简单的技术是可行的。 正如我们将在本文中展示的那样，治疗的方式α和[α]，甚至减少到普通的CTL，可能此外，我们通过处理无限次和有限次运行，与以前的约束自动机方法不同后者对于处理Reo网络中可能出现的死锁配置至关重要。我们的模型检查器处理一个象征性的方法，约束自动机的一个Reo网络表示的二元决策图（BDD）。第一步是为网络生成约束自动机的BDD表示。这是通过模仿Reo的操作符以合成的方式来完成的，以通过借助于BDD上的相应操作符添加通道和加入节点来合成网络。然后，第二步是使用用于操纵BDD的适当操作来执行BTSL模型检查。为此，我们应用最先进的技术，结合符号CTL模型检查，S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）21符号化处理的α-和[α]-模态。文件的组织。第二节简要介绍了协调语言Reo和约束自动机作为Reo网络的操作模型在第三节中，我们解释了逻辑BTSL的语法和语义。第4节总结了BTSL模型检测算法的主要步骤，并报告了我们的符号实现。实验结果见第5节。第六节是论文的总结。2Reo与约束自动机在本节中，我们总结了协调语言Reo及其操作约束自动机语义的主要概念。更多的细节可以在[2，6]中找到。Reo是一种外生的协调语言，它基于基于通道的演算，其中复杂的组件连接器被组织在通道网络中，并以组合方式构建。Reo网络为连接到网络的组件的协调和交互提供了粘合代码。Reo依赖于一个非常自由的通道概念，并支持任何类型的点对点通信。Reo网络中使用的通道的要求在源端，数据项进入通道（通过执行相应的写操作），而在宿端从通道接收数据同步FIFO1同步沟道排水上图显示了我们的示例中将使用的三种简单通道类型的图形表示同步和FIFO通道有一个源端和一个接收端。在同步通道中，写和读操作必须同时执行。中间的图片显示了一个FIFO通道，其中有一个缓冲器单元，简单地称为FIFO 1通道，其中缓冲器最初是空的。只要缓冲器为空，就可以在源端写入数据项。的写入D的后果是D将被存储在缓冲器中。水槽端的读数是如果缓冲器被填充，则启用，在这种情况下，从缓冲器中取出数据项在Reo中设计复杂协调原则的一个非常有用的通道是同步引流。它有两个源端（但没有汇端）。数据项必须同时在两端写入，并且两端都被销毁。Reo网络的节点代表通道末端的集合。它们通过Reo的连接运算符产生是源节点）、汇点结束（则A是汇点节点），或者A是否将汇点和源端（则A是混合节点）。源节点和汇聚节点表示组件可能连接到网络的输入和输出端口混合节点22S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）用作路由器，其中数据项可以通过网络传输。并发I/O操作。为了论文的简单性，我们在这里假设一个固定的有限且非空的数据集Data，可以从通道中写入或取出数据项。如果N是一组网络节点，则在某个时刻的可观测数据流可以通过并发I/O操作来描述。这意味着一对（N，δ）其中N是非空节点集（即，N 直观的并发I/O操作（N，δ）的含义是节点A∈N同步它们的I/O操作使得δ（A）是在节点A处观察到的数据项。更准确地说，每个源节点A∈N在所有信道上写入数据项δ（A），其中源端在A上，而每个汇聚节点A∈N从其中一个信道获取数据项δ（A），其中汇聚端在A上。混合节点A∈N从其中一个通道读取δ（A），其接收端在A上，同时在所有通道写入δ（A），其源端在A上。在执行并发I/O操作（N，δ）的时刻，在其他节点B∈ N\N处没有数据流。已经引入了约束自动机来为Reo网络提供组合的操作语义[6]。Reo网络的自动机的状态表示配置FIFO通道的缓冲器的内容），而转换对启用的并发I/O操作进行建模。在[6]过渡中，N，dc具有形式q−→p，其中q和p分别是起始状态和目标状态，N是同时执行I/O操作的节点集合，dc是数据约束，即，在节点A∈N处写入或读取的数据项的布尔条件。根据我们的基于BDD的实现（参见第4节），我们进一步向符号表示和处理转换迈进了一步Gq−→p，其中g是nI/Oconstraint，即，一个条件是，如果I/O-操作将被执行和数据项。此外，我们从[6]出发，放弃了所有运行必须无限的要求。我们还处理finite run，这是讨论死锁配置所必需的I/O约束。 我们使用并发I/O操作集合的符号表示，通过节点A ∈N上的布尔条件和在节点A上写入或读取的数据项dA。形式上，N的I/O约束是由文字A（其中A∈ N）和原子公式“（d A 1，..，dAk）∈R“，其中k ≥ 1，A 1，...，Ak是成对不同的节点，并且R是Datak。在整个论文中，我们将使用直观的符号，如2f or“d A ∈ { 0 }“or r“d A d B“f o r“（d A，d B）∈ {（δ A，δ B）∈ Data|δAδB}“，以及为所有I/O约束的集合编写IOCI/O约束以预期的方式在并发I/O操作（N，δ）上被解释（N，δ）|=A i <$A∈N且（N，δ）|=（dA1，...，dAk）∈R i {A1，.，Ak}Nδ（A1），.，δ（Ak））∈R.命题逻辑运算符有其标准的语义。我们写[|G|]N对于并发I/O操作集合（N，δ），其中N≠ N且（N，δ）|= g.注意，I/O约束的语义取决于底层节点集N。例如，[|dA=dB|[N={（N，δ）|{A，B}NN，δ（A）=δ（B）}且[|真正|[N={（N，δ）|N N，δ：N →数据}。两 个I/O约束g1和g2是N等价的，记为g1<$Ng2，i <$[|G1|]N =[|G2|]N的。 如果节点集在上下文中是清楚的，我们简单地写[|G|”“言必行，行必果。S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）23NNs srcsnkI/O约束的等价性定义2.1约束自动机（CA）是一个元组A=（Q，N，−→，Q0，AP，L），其中Q是状态的集合，N是节点的集合，不相交地划分为N=NsrcSNK混合 ，Q0<$Q是初始状态的集合，−→ <$Q×IOC×Q转移关系，AP是原子命题的有限集合，L：Q→2AP是标号函数。Nsrc（Nsnk，Nmix）中的节点称为源节点（分别为汇聚节点和混合节点）。转换（q，g，p）的实例是元组（q，N，δ，p），其中（N，δ）∈[|G|]N的。在整个论文中，我们只考虑有限约束自动机，即，我们要求N，Q和−→是有限的。Qg N，δ在等式中，对于一个transitionn（q，g，p）和q−−→p，我们使用一个新的符号sq−→p。p为例。图1示出了具有源节点A和宿节点B的同步信道、具有源节点A和宿节点B以及数据域Data={0，1}的FIFO 1信道以及具有源节点A和B的同步漏极的约束自动机。在所有三种情况下，节点集是N={A，B}。用于同步通道的自动机中的I/O约束对于FIFO通道，可以使用带有明显标记功能的原子命题空和满dA=dBQ同步信道FIFO1信道dA=0Bq（0）dB=0AdA=1BA组B组同步漏极dB=1Aq（1）Fig. 1. CA用于同步通道、FIFO 1通道和同步漏极G对于q，I/O约束条件i oc（q，p）={g|q−→p}表示周必须同步以进行移动的节点处的I/O操作的条件从q到p的一步。 因此，如果P<$Q，则ioc（q，P）=p∈Pioc（q，p）成立对于在q中启用的所有并发I/O操作的集合，并导致一个con，在P中的图形化。对于P=Q，我们得到布尔特征ioc（q）=ioc（q，Q）对于q中所有启用的并发I/O操作的集合。如果ioc（q）<$A∈Ns，则称状态q为终端其中N = N <$N。该条件意味着在q中的所有启用的并发I/O操作中，至少一个的sink或source节点。如果连接到这些节点的组件不愿意提供相应的写或读操作，则这些I/O操作可能被拒绝因此，数据流可能会在终端状态停止约束自动机的直观操作行为可以通过其运行形式化。约束自动机中的序列被定义为有限序列或无限序列Q24S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）√.连续的转换实例。在有限次运行的情况下，我们允许它们以一个特殊的伪转换结束，标签为“”，表示数据流的结束，假设最后一个状态是终端。 也就是说，有限游程的形式为N1，δ1Nk，δkN1，δ1Nk，δk（1）q0−−−−→.. . −→qkor（2）q0−→.. . −→qk−−→qkNi，δi其中qi−1−→ qi是转换实例（i = 1，. ，k）和qk是终端，以-transition结束的有限次运行长度|θ| ∈IN<${ω}被定义为θ中所采用的转换实例的数量（可能包括伪转换，标签为"最大游程意味着无限游程或有限游程运行，以标记为“”的伪转换结束。我们把集合写成（q），对于从q开始的所有游程，以及对于从q开始的所有最大游程，Maximum（q）。如果θ=q0N1，δ1−→q1N2，δ2−→q2N3，δ3−→.. . 这是一个无限的或有限的，但不是-最大游程则为（N1，δ1）（N2，δ2）（N3，δ3）. 通过采取亲，对并发I/O操作序列的映射称为θ的I/O流。N1，δ1Nk，δk对于有限emaximaluns，sayθ=q0−→. 。 . −→qk−−→qk，I/O流θ的值是（N1，δk）. （Nk，δk）。3分支时间流逻辑在本节中，我们将介绍一个分支时间时序逻辑，用于推理约束自动机的控制和数据流。该逻辑称为分支时间流逻辑（BTSL），结合了CTL [11，12]，PDL [15]和定时数据流逻辑（TDSL）[3，9，4]的功能。在CTL中，公式可以通过原子的方式引用组件连接器的配置（约束自动机的状态）。命题ap ∈ AP，可以使用路径量化器和。路径属性为由标准直到操作员或PDL/TSDL类模态指定，其中α是一个正则表达式，指定节点上的I/O操作序列分支时间流逻辑（BTSL）。 BTSL签名是一个元组（AP，N），由原子命题的有限非空集合AP和有限非空节点集合N组成。BTSL的语法有三个层次：状态公式（用大写希腊字母Φ、表示）、运行公式（用小写希腊字母-ter表示）和常规I/O流表达式（用字母α表示）。BTSL的抽象语法由以下文法给出，其中ap∈AP且g∈IOC：.....Φ：=真。 AP. Φ1Φ2. 是的 好吧 ∀ϕΦ：= Φ 1。 U Φ 2。. 你好Φ。..α：= g。别说了ααα。α1;α2. α1和α2。α1∩α2状态公式和直到运算符U的直观含义与CTL中的相同。在类似PDL的公式中，正则I/O流表达式α指定了一个集合有限的I/O流，即，并发I/O操作的有限序列，可能以符号“”结尾。直觉上，如果最大游程开始，有一个有限的前缀，其中数据流匹配α指定的条件。可以导出其他运算符，例如， QΦ=真UΦ（最终），S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）25√∗√--<$<$Q <$Φ和<$QΦ =<$$> Q <$Φ（总是）。PDL类模态的对偶形式是由αΦ和αΦ得到的。直觉上，[α]Φ对于最大游程成立，如果它的所有有限个前缀θ，其中诱导的I/O流属于α给出的语言，结束于Φ成立的状态。LTL/CTL类逻辑的下一步运算符是·的一个特殊例子，由Φ=trueΦ产生。正则数据表达式α的语义由语言LN（α）2IOS提供，其中IOS表示所有有限I/O流的集合，即，并发I/O操作的有限序列，可能以表示没有进一步数据流的特殊符号结束。我们将LN（g）定义为所有并发I/O操作（N，δ）的集合，将其视为长度为1的字（I/O流），例如故（N，δ）∈[|G|]N的。语言LN（stop）是单例集{n}。经营者在常规I/O流表达式的语法中，意思是，即，代表交集，（可以在常规I/O流表达式的语法中删除互补和交集，而不会降低逻辑的表达能力。我们将它们包含在语法中，因为没有<$α或α1<$α2的封闭正则表达式。）;和的意义与标准的连接和Kleene闭包一致，除了对k的特殊处理。如果L1，L2等于2IOS，则L1，L2由σ1∈L1和σ2∈L2中元素的逐点拼接σ1;σ2其中σ1;σ2=σ1，如果σ1以。然后Kleene闭包以标准的方式定义为L=Ln，其中L0=ε（由空I/O流组成的语言），L1=L和Ln+1=L; Ln。签名（AP，N）上的BTSL公式被解释为具有节点集N和原子命题集AP的约束自动机。 对于A=（Q，N，−→，Q0，AP，L），满足关系|BTSL状态公式的= A以标准方式定义：Q|=AtrueQ|=Aapap∈ L（q）Q|=A<$Φ拉克|=AΦQ|=AΦ1Φ2q |=AΦ1和q |=AΦ2Q|=A存在一个游程θ∈Maxim（q）s. t。 θ |=Aq|对于所有运行θ∈Maxim（q）：θ|=A路径公式的含义如下。 如果θ是最大游程，则θ |=A<$α<$Φ i <$存在θ的有限个prefix θJ使得p|对于θ j的最后一个状态p，θ j的I/O流属于LN（α）。until运算符的语义与CTL中的相同。如果θ是A中的极大游程，则满足关系θ|BTSL运行公式的=A（·）定义如下。N1，δ1N2，δ2N3，δ3如果θ=q0−→q1−→q2−→. . isin finitethenθ |=AαΦj≥0 s.t. QJ|=AΦ和（N1，δ1）. （Nj，δj）∈LN（α）26S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）DDN1，δ1Nk，δk如果θ=q0−→.. . −−−−−→qk−−→qkisfinite，则θ|=A<$α<$Φ <$<$0≤ j ≤ k s.t. QJ|=AΦ和（N1，δ1）. （Nj，δj）∈ LN（α）或qk|=AΦ和（N1，δ1）. （Nk，δk）∈ LN（α）对于θ是无穷大游程或无穷大游程，状态序列为q0q1q2.。. ：θ|=AΦ1U Φ2 <|θ|S.T. QJ|=AΦ2φ 0≤ i A<$B <$是真的，对于FIFO 1通道成立，说明在A和B处不可能同时进行数据流。对于图2左侧的网络（的约束自动机），BTSL公式<$Q <$$><$A<$B<$true，<$[true<$;A]<$$>B<$true，<$[ true<$;B]<$$>A <$true和A=ddB=dd保持。（图中的d表示上部在初始配置中，缓冲器填充有数据项d。前三个公式表明A和B处的数据流是交替的，而后一个公式断言只有在A或B处观察到的数据项d是可能的。AAB BC图二. 两个Reo网络虽然左边的网络没有终端状态，因此数据流总是无限的，但右边网络中的源节点C可以写入上面的缓冲器，这产生了两个缓冲器都被填充并且数据流停止的配置。因此，右边的网络满足公式（B;A）（C;stop）true，[true;B]Atrue和[true;C]both_bu ers_full，其中，_buffer_full是一个具有明显语义的原子命题。图3示出了用于定序器的网络，该定序器由4个FIFO 1通道和几个同步通道以及允许AiS. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）27复合CABTSL模型检查BTSL公式组件接口回答+见证/反例REOA3A2A1A0图三.定序器B的顺序为A0A1A2A3A0A1A2A3。. . 该属性可以通过以下方式形式化：公式<$（true;Ai;Aj）<$true，其中0≤iα<$Φtheree istsarunq=q0−→.. . −→qkinA使得N1，δ1（N1，δ1）. （Nk，δk）∈LN（α）且qk|=A。Nk，δkLe t z0−→.. . −→zk是一个n接受runinZforr（N1，δ1）.. . （Nk，δk），即，zk∈ZF和z0∈Z0。然后，N1，δ1Nk，δk（q0，z0）−→.. . −→（qk，zk）是A× Z中的一次运行。 因此，（q，z0）|=A×Z<$Q（sat（sat）最终）。假设（q，z0）|=A×Z<$Q（sat（n）final）其中z0∈Z0。然后，存在一个运行N1，δ1Nk，δk（q0，z0）−→.. . −→（qk，zk）在A×Z中，q=q0且（qk，zk）|=A×Zsat（Z）最终，即，QK|=A且zk∈ZF.因此，在本发明中，N1，δ1Nk，δkz0−→.. . −→zk是（N1，δ1）的可接受游程. （Nk，δk）在A. 这产生（N1，δ1）. （Nk，δk）∈LN（α）. 自qk|=A，N1，δ1Nk，δkq=q0−→.. . −→qk是A中的一个游程，其中，(b) 设A是确定的，z0是Z的初始状态。如果q|=A<$[α]Φ，则存在形式为N1，δ1Nk，δ2N3，δ3q=q0−→q1−→q2−→.. .N1，δ1Nk，δks ucht hatθ|=[α] L et usconside raprefixq=q0−→.. . −→qkofθ，让N1，δ1Nk，δkz0−→.. . −→zk30S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）J是（N1，δ1）的唯一游程. （Nk，δk）在A.则zk∈ZF蕴涵qk|=A。因此，θ可以提升到A×Z中的最大游程，其中Q（sat（θ）最后）成立。这产生（q，z0）|=A×Z<$Q（sat（sat）最终）。假设（q，z0）|=A×Z<$Q（sat（sat）最终），令θJ=（q，z）N1，δ1N2，δ2（q，z）...00−−−−−→11−−−−−→是A×Z中的极大游程，其中q=q0，θJ|=A×ZQ（sat（sat）最终）。将θJ投影到A-分量上，得到A中从q开始的最大游程θ。我们现在证明θ|=A[α] 让N1，δ1Nk，δkq=q0−→.. . −→qk是θ的前缀。那么，zN1，δ1−→.. .Nk，δk--（N1，δ1）. （Nk，δk）在Z.由于θJ|=Q（sat（sat）final），我们有：zk∈ZFimplies qk|=A。这就产生了索赔。Q然而，通过应用算法1可以避免Z的确定（这可能导致指数爆破）。算法1Sat（α [α] δ）的计算构造α的NFAZ，并构造乘积A× Z;V：={（q，z）∈Q×Z|q∈Sa t（ε）<$z∈/ZF};重复VJ：=V;N，δR：={（q，z）|转换实例qqJ<$zN，δzJs. t. （qJ，zJ）∈/V};V：=（V\R）<${（q，z）∈V|Quntil（V=V）;−→A终端机Z<$}−→Zreturn {q ∈ Q|（q，z0）∈ V，对所有z0∈ Z0}命题4.2算法1计算状态集q ∈ Q，其中q |=A[α]。证据设V是重复循环终止时属于V的状态（q，z）的集合。 F（q，z），其中tV0={（q，z）|q∈Sa t（ε）<$z∈/ZF}，W0=Q×Z\V0，设Wi是第i次迭代中从V中去掉的状态集. 然后，V=i≥0其中Vi+1=Vi\Wi+1，n是迭代次数S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）31−−−→此外，我们有：(i) 对于所有的（q，z）∈V，其中q是非终结的，存在一个转移实例N，δq−−→qJ，使得（qJ，zJ）∈V，对所有zN，δN1，δ1zJ。Nk，δk(ii) forall（q，z）∈Wiandforallunsq=q0−→.. . −→qmofthm≥iN1，δ1Nk，δk在A中存在游程z=z0−→. . −→zkofthk≤min{i，m}s ucht hat（qk，zk）∈/V0，即，qk|=Aandzk∈ZF.现在让我们假设q0是包含在算法1返回的集合中的状态。则对Z中的所有初始状态z0，（q0，z0）∈V.我们依次应用（i）获得A中的最大游程N1，δ1N2，δ2使得对于所有运行θ=q0−→q1−→.. .N1，δ1N2，δ2z0−→z1−→.. .在Z中，对于相同的I/O流，对于所有索引i，我们有（qi，zi）∈V。自V至V0我们得到θ |=A[α]，因此，q0|=A[α]。我们现在考虑一个状态q0∈Q，使得q0|=A[α]。让N1，δ1N2，δ2θ=q0−→q1−→.. .是A中的极大游程，使得θ |=A[α] W.l.o.g. 在所有的r_s_θ_J∈M_xR_un_s（q_0）下，θ具有最小长度，其中e_θ_J|=A[α]。 如果对于某个z 0 ∈ Z 0，假设（q0，z0）∈Wi，我们假设t（q0，z0）∈/V，则|θ|（ii）存在k ≤ i和一个游程N1，δ1Nk，δkz0−→.. . −→zkiinZs ucht hat（qk，zk）∈/V0.因此，zk∈ZF和qk|=A。但是，（N1，δ1）. （Nk，δk）∈LN（α）和θ|=A[α] 矛盾 这产生（q0，z0）∈对所有z0∈Z0.因此，q0在算法1返回的状态集中。Q计算满足集的算法的复杂性，[1][2][3][4][5][6][7][8][ 9]因此，BTSL模型检测的总体时间复杂度是A的大小和输入公式Φ的长度的多项式，假设Φ中的正则I/O流表达式是普通正则的表达式，即，不要使用互补或交运算符，因为它们可能导致从α构造Z时的指数爆破。符号实现。我们现在用二元决策图（BDD）总结我们的符号BTSL模型检查器的主要特征，参见例如[8，17，16，19]。BDD是用于切换功能的数据结构F：Eval（x1，.，xn）→{0，1}哪里 x1，.，xn 是 布尔 变量和Eval（x1，. ，Xn）表示针对X1，. ，xn. 代表一个骗子-通过BDD，我们固定状态的二进制编码，即， 我们通过单射函数bin将Q嵌入{0，1 }n：Q → {0，1}n，其中n =[log |Q||，选择布尔状态变量q1，... ，q n，然后用对q1，. ，q n由bin（q）给出。同样，我们可以32S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）¯¯通过比特元组对数据项进行编码 为了简单起见，我们在这里假设布尔数据域Data={0，1}，并将符号dA和节点A∈ N视为布尔变量。接下来，令N={A1，.，Ak}并且di=dAi，i=1，.，k. 我们写A和d为变量元组（A1，.，Ak）和（d1，.，dk）。转换关系−→可用其特征函数来确定，并可看作是一个函数TA：Eval（q<$，A<$，d<$，q<$J）→{0，1}，其中变量q<$=（q1， . . ，qn）表示该起始时间，q<$J=（qJ1， . . ，qJn）目标状态，其中A和d用于表示并发I/O操作。例如，过渡具有源节点A并且汇聚节点B和同步漏极由下式给出：Tsync_channel（q1，A，B，dA，dB，qJ1）=q1<$A<$B<$（dAParticipidB）<$qJ1Tsync_drain（q1，A，B，dA，dB，q1J）=q1<$A<$B<$qJ1对于FIFO 1通道，我们必须编码三种状态，比如bin（q）=00，bin（q（1））=11并且bin（q（0））=10，并且然后可以通过下式表示自动机：（q2BAqJ1qJ2）Reo网络的转移关系的BDD表示可以以组合的方式构造，通过模仿Reo我们将简要地考虑连接操作符，它允许将两个节点折叠成一个节点。通过对节点进行适当的重命名，Reo给定约束自动机的节点（见[6]）。如果A1和A2是约束au-tomata分别具有节点集N1和N2，则乘积A1×A2中的并发I/O操作由以下同步规则和两个交错规则获得的转移实例给出g1g2q1−−→A1p1，q2−−→A2p2（q，q）g1g2（p，p）1G1q1−−→A1p1（q，q）g1N22−→A1×A21 2G2q2−−→A2p2g2N112−→A1×A2（p1，q2）（q1，q2）−−→A1×A2（q1，p2）其中<$Ni是A∈Ni<$A的缩写。 这些规则可以通过一个象征性的通过TA1×A2=（TA1<$TA2）<$（TA1<$$> N2<$idA2）<$（TA2<$$> N1<$idA1），其中idA=q∈Q（qParticipqJ）且Q在A的状态空间中。除了转移关系外，我们还需要标记函数的BDD-表示。 这可以通过表示Sat（ap）={q∈Q|ap∈L（q）}通过一个BDD对诱导函数ap：Eval（q<$）→{0，1}.Φ的子公式φ的满足集Sat（φ）的BDD-表示S. 克吕佩尔霍尔茨角Baier/Electronic Notes in Theoretical Computer Science 175（2007）33J通过用布尔算子对BTSL模型检测算法进行符号化改造，并应用相应的BDD综合算法，得到了BDD综合算法.算法2中示出了算法1的符号重构，其中假设已经构造了用于Sat（k）的BDDf和用于终端状态集合的BDD表示终端我们使用变量元组q<$=（q1， . . ，qn）来表示A中的状态s，并且z =（z1， . . ，zm）的情况下，对Z. Q × Z的子集合V由qān和z中的可变值编码。 记法V（q<$J，<$zJ）意味着V的变量被重命名为它们的primed副本。 集合Z0、ZF和ZZZ 由 具 有 可 变 s<$z的BDDs表示。Sat（λ [α]θ）的λ [α]θ的对称性表示的Algorithm2计算构造A的NFA Z，并生成Z的转移关系和集合Z0，ZF和Zn的BDD-表示TZ;V：=f<$ZF;重复VJ= Vj。R：=q。ΣTAzJ. （TZ<$V（q<$J，<$zJ））;V：=（V<$$>R）<$（V<$端子<$Z<$）until（V=V）;returnz. （Z0V）（*symbolicrepresentationnf[α]forrSat（[α]）*）5实例和结果我们将BTSL模型检查器应用于几个示例。我们将在这里报告两个案例研究。所有结果都是在Pentium IV，1.8GHz，1.5GB RAM，Mandriva Linux和内核2.6.12上实现的。该工具是用C++编写的，使用GCC4.0.3编译，并使用JINC [18]作为二元决策图的库例5.1 [用餐哲学家]第一个例子描