运行时验证中的MEDL语言和DFA模拟的问题

理论计算机科学电子笔记113（2005）123-143www.elsevier.com/locate/entcs用于运行时验证的美国Sammapun Arvind Easwaran Insup LeeOleg Sokolsky奥列格·索科尔斯基1，2宾夕法尼亚大学计算机与信息科学系关闭PA，USA摘要在指定系统需求时，我们需要一种能够以最简单和最直观的形式表达需求的语言。虽然MaC系统提供了一种表达性语言，称为MEDL，但通常难以表达某些特性，如复杂事件的时间顺序、时序约束和安全属性中固有的事件频率。MEDL-RE扩展了MEDL语言，使其包含正则表达式，从而可以轻松地指定时序依赖性和时序约束。由于MaC系统同时生成事件，通过模拟DFA来监视正则表达式将导致潜在的问题。DFA模拟将涉及并发多路径模拟，并导致指数运行时间。为了廉价地处理并发事件，我们生成依赖图来识别可能的并发事件。此外，我们增加了原来的DFA与替代过渡，这将取代多路径模拟。关键词：验证，DFA模拟，DFA，MEDL。1介绍监控，检查和指导（MaC）框架[9，10，11]旨在确保实时系统的执行与运行时的要求一致。它提供了一种名为MEDL的语言，用于规范基于LTL的安全属性[13]。安全属性包括1本研究得到了NSF CCR-9988409、NSF CCR-0086147、NSF CCR-0209024和ARODAAD 19 -01-1-0473的部分支持。2电子邮件：{usa，arvinde，lee，sokolsky}@saul.cis.upenn.edu1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.030124联合Sammapun等人理论计算机科学电子笔记113（2005）123计算和定时要求。 安全属性定义为在事件、条件、辅助变量和辅助函数方面。事件是瞬时事件，如变量更新或方法调用的开始/结束。 条件是关于程序的命题，在一段时间内为真或为假。这些事件和条件也可以用第2节中描述的连接词组合。辅助变量是临时存储，例如，它允许我们计算事件发生的次数。辅助函数返回事件的值和时间戳。MEDL语言提供了一种优雅而直观的方式来指定计算需求。然而，它没有提供一种直观的方式来指定时序要求，例如具有复杂时序依赖性的事件的时间排序、时序约束或时间间隔中特定事件的计数。MEDL的扩展名为MEDL-RE [14]，增加了以正则表达式（RE）的形式在自定义事件集上指定事件顺序的能力，这为用户提供了更清晰，更少出错的规范。在本文中，我们提出了一个有效的模拟相应的DFA在运行时。通过观察目标系统中发生的一系列事件，MEDL-RE生成的DFA将事件序列与特定的正则表达式进行匹配。然而，由于复合事件可以同时触发，并且不能以任何方式进行时间排序，因此DFA必须识别这些事件的任何顺序。这意味着，如果正则表达式对同时发生的事件具有某种固有的顺序，则DFA必须接受这种顺序的所有不同排列。我们把这些排列称为线性化。为了建立这样的DFA，我们增加了原来的DFA与替代过渡，提供从一个线性化到另一个路径。然后，我们证明了原来的DFA和增广的DFA是等价的。只有那些其基础正则表达式在其相关集合中具有候选并发事件的DFA才候选并发事件可以通过构建和遍历第4节中描述的依赖图来静态检测。本文的结构如下。第2节简要介绍了MaC框架的概述第3节介绍了扩展MEDL-RE。第4节讨论依赖图的构造。第五节提出并证明了我们的增广DFA算法。第6节介绍相关工作。最后，第7节对本文进行了总结。联合Sammapun等人理论计算机科学电子笔记113（2005）123125Fig. 1. MaC架构2MaC概述2.1MaC架构MaC系统的开发是为了确保程序按照其形式要求正确运行。图1显示了MaC架构。该系统的工作原理如下。用户用形式语言指定目标程序的需求。给定一个目标程序和需求，MaC系统将一组探测器或过滤器插入目标程序。在运行时，探测目标程序的执行由MaC系统监视和检查事件识别器根据从过滤器接收的状态信息检测原始事件和条件。原始事件是值的改变（update（object））、进入方法（startM（method））和离开方法（endM（method））。基元条件是布尔变量或由基元类型化变量组成的布尔语句，目标程序。然后，这些事件和条件被发送到运行时检查器，该检查器确定当前执行历史是否满足需求规范。 执行历史记录是从事件识别器发送的事件序列中捕获的。如果运行时检查器检测到任何违规，它会通知用户并触发注入器采取引导脚本中指定的引导操作，并将目标程序引导回安全状态。2.2MaC语言MaC系统提供三种语言。需求规范或元事件定义语言（MEDL），基于代码对象名称监控脚本监控事件和条件指导脚本转向所需资源规范运行过滤器系统低级信息事件识别器事件和条件变化低空操舵转向动作调用注射器编译126联合Sammapun等人理论计算机科学电子笔记113（2005）123线性时序逻辑（LTL）[13]允许我们表达系统的安全属性的大子集，包括实时属性。监控脚本以原始事件定义语言（PEDL）表示，用于定义从过滤器发送到MaC系统的信息以及如何发送转换为MEDL中使用的事件和条件。使用转向操作定义语言（SADL）编写的转向脚本用于指定发生违规时要调用的操作。见[9，10]关于PEDL和SADL的详细信息。2.2.1事件和条件事件在系统执行期间瞬时发生，而条件表示在一段时间内保持的信息。例如，在传递控件的瞬间发生表示调用init方法的事件的值，而条件（角度30）只要可变角度不超过30°。事件和条件的语法如下所示。E* = e|启动（C）|结束（C）|E&&E|E||E|当CC * = c|定义（C）|[英、英]|！C|C&&C|C||C| CC事件和条件中使用的布尔连接词以通常的方式定义事件start（c）和end（c）分别在c变为true和false时触发。当e被触发且c为真时，c被触发时的事件e。当c被定义时，条件（c）被定义为真。条件[e1，e2）在事件e1和e2的发生之间为真，其中包括e1但不包括e2关于事件和条件的形式语义，参见[9，11]。2.2.2Meta事件定义语言MEDL包括从PEDL导入的事件和条件、复合事件和条件的定义、安全属性、辅助变量和辅助函数。安全属性可以表示为条件或称为警报的事件。在执行期间，安全属性条件必须始终为真，而警报必须永远不会发出。辅助变量可以用来定义事件和条件。例如，辅助变量辅助函数是time（e）和value（e），它们返回时间戳和事件e的值。3MEDL-RE的语义和语义本节描述了MEDL语言的扩展，通过将事件表示为常规表达式来包括事件排序联合Sammapun等人理论计算机科学电子笔记113（2005）123127RE={E}<$R1+R2=<$R1<$$>R2<$R1。R2=R1R2 R =R图二、一个函数函数R，它返回R的相关事件集在一个时间间隔内事件的频率3.1语法设为一组正则表达式名称，例如，R，R1，R2，等等。sMED L中的语句-RE，sMEDLbex是mMDL语句中的语句s，E是事件列表，r是正则表达式，C是中第2.2.1节。我们定义MEDL-RE扩展的语法如下。s：：=sMEDL现有MEDL语句| RER{E¯}=NewMEDL-REstatementr：：=E| R. R|R+R|正则表达式E：：= e|启动（C）|（C）现有活动|E&&E|E||E|当C|startRE（r）|成功（r）|fail（r） 正则表达式事件f：：=时间（E）|值（E）|occur（E，C）辅助函数MEDL-RE扩展包括正则表达式、事件startRE（r）、success（r）、fail（r）和辅助函数occurve（E，C）。正则表达式，范围在一组事件上，由事件（E），连接（r。r）、union（r + r）和Kleene star（r）。事件startRE（r）表示我们开始观察正则表达式。事件成功（r）表示我们已经找到了一个指定正则表达式的事件序列，事件失败（r）表示我们已经开始观察，但未能找到这样的序列。对于事件E和条件C，辅助函数occurrence（E，C）返回在C保持为真的时间间隔期间事件E3.2语义设图2中的R表示RER中指定的一组事件，在新的MEDL-RE状态中实现的客户最优化的空间设置显示在语法部分。 那么，R的相关事件集是：1995年。我们修改[9]中定义的模型M如下。模型M是元组（S，τ，L C，L E，o），其中S={s0，s1，. . }是状态的集合，τ是从S到时域的映射，LC是从S× C到{真，假，Λ}的全函数，其中C表示条件名称的集合，Λ表示未定义，并且LE是从S× E到值域的部分函数，其中E表示条件名称的集合。128联合Sammapun等人理论计算机科学电子笔记113（2005）123∗∧∨M{∈|∈}MMMMMMMMDa（a）=GDa（b）= ΛDa（Λ）= ΛDa（G）=ΛDa（R1+R 2）=Da（R 1）+Da（R 2）Da（R）=（Da（R））。 RDa（R 1. R2）=（Da（R1））. R 2，如果E（R）=假（Da（R1））。R2+Da（R 2）如果E（R）=真图三. 正则表达式R关于a（Da（R））的导数E（a）=假E（Λ）=假E（G）=TrueE（R1+R2）=E（R1） E（R2）E（R1. R2）= E（R1） E（R2）E（R）= True见图4。 一个函数E（R），它检验G是否∈R事件名称。对于所有ek，其中LE（si，ek）被定义，存在阶o（si，ek），使得在时间τ（si）处，每个出现ek的阶是不同的。阶o是一个全单射函数，它将ek和si映射到一个正整数的有序集合，并且对所有i和任意k，l都有o（si−1，ek） { aCountwxyz -> { wxyzCountaCount变量跟踪事件a发生的次数。当-everya出现时，我们递增它，当b出现时，我们重置它。当aCount变为3时，警报a3提醒用户。事件wxyz仅在c为真且y或z出现在w和x之间或z出现在x和y之间时触发。wxyzCount变量存储事件wxyz发生的次数。属性wxyz10在wxyzCount大于10时提醒用户。130联合Sammapun等人理论计算机科学电子笔记113（2005）123考虑当我们需要指定四个以上事件的顺序时，像wxyz这样的事件可能会变得非常复杂，因为需要考虑太多的情况。这表明使用现有的MEDL编写需求是容易出错的，并且难以理解。通过向语言，事件的顺序可以更直观地表达规范的以下片段显示了如何在扩展的MEDL-RE中指定示例要求。RE a3RE{b} = a.a.a>;RE wxyzRE {} = w.x.y.z>;报警a3 =成功（a3 RE）;财产wxyz10= occurred（fail（wxyzRE），c）<10;正则表达式a3RE和wxyzRE表示连续发生三次的事件a的顺序，以及事件w之后是事件x、y和z的顺序。 a3 RE中的相关集合{b}指示如果事件b发生在两个事件a之间，则该序列将无法匹配a3 RE。然而，如果事件x发生在两个事件a之间，则MEDL-RE将忽略事件x，并且不会使序列失败wxyzRE中的相关集合{} 的工作方式类似。警报a3在我们成功匹配REa3RE时提醒用户，而属性wxyz10在REwxyzRE失败超过十次时提醒用户。现在的要求要简单得多，也更容易理解比原来的MEDL。4执行监视的一个重要属性是它能够使用最少的系统资源尽可能高效、快速地监视目标系统。因此，使用确定性有限自动机（DFA）来监视RE优于非确定性有限自动机（NFA）。已经提出了几种现有的算法，以有效地构造和最小化从给定的RE的DFA我们选择Aho，Sethi和Ullman [2]的算法，因为它直接生成DFA而不生成NFA。Watson [15]的经验结果也表明这种DFA构造是有效的。DFA的模拟包括以下步骤。识别在其相关集合中具有当前事件的RE。 然后将当前事件与DFA当前状态的所有可能转换进行比较，并选择适当的转换。 如果当前事件启动DFA的模拟，则它将触发startRE事件。如果自动机移动到最终状态，成功事件在第5节规定的某些条件下触发。类似地，导致自动机卡住的事件触发一个失败事件。然而，在DFA模拟的问题时，有一个原始的事件或条件产生的由于没有固有的联合Sammapun等人理论计算机科学电子笔记113（2005）123131为了在这些同时发生的事件之间进行排序，DFA仿真必须同时评估这些事件的所有可能排列的多条路径。这在资源利用方面是昂贵的，并且对于某些应用，特别是在实时系统中，也可能是不可行的。4.1同时发生事件MaC语言由高级或复合事件和条件，以及第2.1节和第2.2节中描述的低级或原始事件和条件组成。当检测到基本事件或条件时，过滤器将它们按发生的顺序发送到事件识别器。这些基本事件和条件可以触发复合事件或更改条件的值。虽然原始事件和条件是有序的，但我们不能对由一个原始事件或条件触发的复合事件进行排序，因为所有复合事件都同时发生由于RE可以定义为可以单独和同时发生的复合事件，因此我们需要一种方法来识别可以同时发生的事件。如果两个事件可以同时发生，那么它们的顺序是无意义的，它们的串联可以在不改变意义的情况下进行排列。为了廉价地处理同时发生的事件，我们提出了以下步骤。在静态阶段，我们确定RE中使用的事件是否可以同时发生如果这样的事件存在，我们增加了原来的DFA与替代过渡。在运行时，我们尝试使用原始转换执行一个步骤。如果这是不可能的，我们尝试采取一个步骤，使用替代的过渡，只有当存在一组事件中的相关集合的这个RE，同时发生。4.2检测同时事件为了静态地检测可能的并发事件，我们使用第2节中描述的连接词从事件和条件的语法构建依赖图。依赖图G=（V，E）是一个有向图，其中顶点V是连接词、事件和条件，边E表示它们之间的依赖关系。 设e1，e2为事件或条件。 则（e1，e2）∈当且仅当e1用于合成e2。例 如 ，如果e3= e1||E2，则（E1，||），（e2，||），（||，e3）在E. 图图5示出了示例监控脚本，6显 示 了 相 应 的 依 赖 关 系 图 。 在 图 中 ， 有 两 个 原 始 事 件 update（A.x）、update（A.y）和两个原始条件A.c1、A.c2。它们都是图中底部的顶点六、由于事件update（A.x）和条件A.c1被用来构成连接词when，因此边（update（A.x），when）和（A.c1，when）在E中。由于事件e1是132联合Sammapun等人理论计算机科学电子笔记113（2005）123e2当e1e3当&&当更新（A.x）A.c1A.c2更新（A.y）e1 = update（A.x）when A.c1;e2 =当A.c1 A.c2时更新（A.x）; e3=当A.c2时更新（A.y）;RE测试{}= e1。e2. e3;图五. 监控脚本见图6。 依赖图由连接词when组成，边（when，e1）也在E中。的事件E2、E3的构造类似。我们表示事件e2依赖于事件e1当且仅当G中存在从事件e1到事件e2的路径。我们还表示，如果存在从图中的公共顶点到e1和e2中的每一个的路径，则它们可以同时发生。因此，可以从依赖图中的相同原语事件到达的一组事件可以同时发生。 例如，在图6中，事件e1、e2依赖于相同的原语事件更新（A.x），因此它们可以同时发生。 检测依赖，我们使用BFS以自底向上的方式遍历图。然而，依赖图的分析可能产生假阳性结果。这意味着从图中获得的同时事件可能永远不会在实际系统中发生。例如，考虑图6中的事件。基于依赖图，事件e1和e2可以同时发生因为两者都依赖于事件更新（A.x）。假设条件A.c1和A.c2是目标程序中的布尔变量，它们永远不会同时为真。因此，事件e1和e2不会同时发生。有两种特殊情况。第一种情况是当一个事件是由一个和连接词（e1e1）组成的。当且仅当它的两个参数e1和e2同时出现时，带有连接词的事件被因此，如果沿着路径存在连接符，则连接符的两个参数否则，带有连接符的事件将永远不会被触发，因此，联合Sammapun等人理论计算机科学电子笔记113（2005）123133排除了可能同时发生的事件。第二种情况是使用when连接词（ewhenc）组成事件，该连接词由事件侧e和条件侧c组成。当且仅当事件e在条件c为真时发生时，才会触发带有when假设我们正在检测的两个事件是e1和e2，e1由when连接词组成。如果e1和e2的公共顶点位于e1中的when连接词的事件侧，则e1和e2可以同时发生。如果它只存在于条件侧，那么e1和e2不能同时发生。例如，图6中的事件e2和e3不能同时发生。这是因为update（A.x）和update（A.y）不能同时发生，因为我们假设所有的原始事件总是有序的。然而，如果A.c1和A.c2同时为真，则事件e1和e2可以同时发生通过上述过程获得的一组可能的同时事件可以用于识别需要增强的RE。只有那些在其相关集合中有一个并发事件子集的正则表达式才需要扩充。5具有并发事件的DFA扩充与仿真算法基于第4节中提供的同时事件的信息，我们静态地将附加信息合并到DFA中。我们声称，这些额外的信息可以帮助在DFA的多个路径的同时模拟有效。提出以下算法以将此额外信息并入DFA中。假设DFA是使用第4节中描述的用于DFA生成和最小化的算法生成的最小DFA。我们称这个DFA为DFAorg，并将该算法生成的增强DFA称为DFAaug。我们在以下前提下构造DFAaug(i) 由事件识别器生成的同时事件的集合不构成同一事件的多次发生这个假设是有效的，因为MaC系统不记录任何给定时刻事件发生的次数它仅记录事件发生的存在或不存在。(ii) DFAorg由单个接受状态组成。由于我们只检测DFA组织接受的最短序列，因此可以从所有接受状态中删除所有传出转换。然后，最小化过程将这些状态合并为一个。134联合Sammapun等人理论计算机科学电子笔记113（2005）123∈设DFAorg=（Q，R，T，q0，qf），其中Q是有限状态集，R是R的相关事件集，如3.2节所述，T：Q×R→Q是部分转移函数，q0∈Q是起始状态，qf∈Q是单一接受状态。给定DFAorg，该算法构造DFAaug其中，Q、Q、T、q0和q f是从DFA org获得的，D：T → N nnn { 0 }是指示其与q f的最长距离的转换的距离注释，U：T→ N nn n {0}是将状态的每个转换映射到唯一自然数或零的唯一距离函数，ES：Q→ P（n n n）是状态的事件串注释，并且T alt：Q×N n n →Q是部分替代转换函数。 记T（q，e）= Λ i <$（q，e）/∈dom（T），记<$q，e，qJ <$∈T i <$T（q，e）= qJ.D、U、ES和Talt在以下章节中进一步详细描述。构造DFAaug的算法分为两个阶段：变迁和状态的标注以及交替变迁的生成5.1阶段1：转换和状态在这个阶段，我们用一个表示为D（t）的数值来注释DFAorg的每个转换t T，(i) 等于从接受状态Qf到转变T的距离。该距离等于使用该转换t从当前状态到达qf所要遍历的转换的数量。(ii) 表示所有这些距离的最大值。在此阶段，构成循环或自循环的转换将被忽略。该算法的距离生成阶段如图8所示。该注释可以通过使用从qf开始的BFS算法遍历DFA来完成。该距离信息D（t）将有助于在运行时对用于仿真的转变进行排序。我们将基于与转换相关联的距离值从当前状态遍历其中一个传出转换，即，首先降低距离值。这种选择背后的基本原理是，更接近接受状态的转换应该在更远离它的转换之前尝试。具有相同距离值的两个转变），我们基于相关集合中的对应事件的排序来挑选转变。在图8中，开始状态S具有两个输出转换，都编号为3。我们将根据事件e1和e2在相关集合中的顺序对这些转换进行排序。让这个唯一的转移顺序t称为U（t）。在此阶段，我们还使用附加信息注释DFAaug的每个状态，指示可能联合Sammapun等人理论计算机科学电子笔记113（2005）123135e2e4A B Ce1e5Se2e6De1Ee4Fe3见图7。 原始最小化DFA组织{e1}e2 /2e3e4 /1{e1e2e4，e1e2e3e4}e1 /3SA B{e1e2、e1e2e3}Ce5 /0e2 /3D{e2}e1 /2E{e2e1}e4 /1F{e2e1e4}e6 /0见图8。 DFAaug的距离D和事件字符串ES从起始状态Q0开始到达该状态。每个这样的输入序列被称为该状态的事件字符串。请注意，每个状态可以有多个事件字符串。 此注释步骤如下所示图8 .第八条。为每个状态q设置的事件字符串，称为ES（q），等于将其所有前驱状态的事件串集合与对应的转换串联。所有在事件e上具有自循环的状态在事件字符串被复制后，将事件e附加到它们的每个事件字符串。如图8所示，状态B在事件e3上具有自循环。 它的事件字符串集合由正常转换的事件字符串{e1e 2}和自循环的事件字符串{e1e 2e 3}给出。 在存在循环abca的情况下，则在复制事件串之后将abc附加到构成循环的状态的每个事件串。 请注意，事件串的确定仅在对于当前状态完全确定之后才进行到下一状态，即，当前状态的所有自循环必须在进行到下一状态之前被解决周期将是136联合Sammapun等人理论计算机科学电子笔记113（2005）12312345678910对于achstateq∈Q−{q0，qf}对于每个事件串es∈ES（q），对于每个事件e∈N，使得T（q，e）= Λ对于每个状态q1∈Q− {q 0}，使得max<$ei∈N，T（q1，ei）=Λ（U（T（q1，ei）））≥min<$ei∈N，T（q，ei）/=Λ（U（T（q，ei）））对于每个事件串es1∈ES（q 1），if（Hashed（es1）==Hashed（es））然后将T（q1，e）与Talt相加（如果T（q1，e））=Λ）else if（Hashed（es）==Hashed（Remove（e，es1）然后将q，e，q1加到Talt见图9。 生成交替转换Talt这里是个例外，因为我们无法识别循环，直到我们继续前进并返回到状态。即使在这种情况下，算法也将仅在已经确定了循环中的所有状态的所有事件串之后继续进行到循环之后的状态。5.2第二阶段：替代性转型的产生。在我们继续之前，我们需要定义术语线性化和线性化的等价性。线性化线性化是一组事件的总顺序。如果该集合由同时发生的事件组成，则该集合中这些同时发生的事件的排序是该集合的一个线性化 这些同时发生的事件的不同排列构成了不同的线性化这一套。等价性两个线性化是等价的，当且仅当它们是同一事件集的不同排列。在此阶段，我们将替代转换添加到DFA组织中的适当状态。交替转换将DFA从表示一个线性化的状态转换到表示某组同步事件的等效线性化的另一个状态。令Remove（e，es）是通过从事件串es中移除一次e的出现而获得的事件串。设Hashed（es）是与事件字符串es相关联的哈希值，其中es中的事件排序是不重要的。这意味着当且仅当两个事件字符串是等效线性化时，它们具有相同的哈希值比如说，Hashed（abc）=Hashed（cab）butHashed（aabc）Hashed（abc）。图9所示的算法比较两个状态的事件串，以查看它们是否是相同输入序列的不同线性化。 如果是这样，我们说这两个事件串是联合Sammapun等人理论计算机科学电子笔记113（2005）123137输入序列，我们可以添加从一个状态到另一个状态的替代转换，而不改变DFA的含义。因为我们总是从U（t）最小的状态q开始选择一个转移t，所以路径的顺序是唯一的。因此，我们需要添加仅从具有较低U（t）的状态到具有较高U（t）的状态的替代转换。这意味着，如果q和q1是状态，那么我们添加从q到q1的交替转换当且仅当在q1的所有跃迁t1中，U（t1）的最大值大于q的所有转换t中的U（t）的最小值（第4-5行）。当添加从q到q1的用事件e注释的替代转换时，我们确保q中的现有转换不具有用事件e注释的转换（第3行）。因此，所得到的有限自动机仍然是确定性的。该算法处理两种不同的情况。设es∈ES（q）和es1∈ES（q1）是两个事件串，使得q的U（t）小于q1.第一种情况是当两个状态q和q1的一些事件串具有不同但等价的线性化时。例如，es=abc和es1=bca。这里，算法在当前事件e上添加从状态q到由T（q1，e）表示的状态的替代转换（第7-8行）。 为每个事件e添加该转换，使得在这些事件中的任何事件上当前不存在从q这种情况如图所示10个。这里，q=F，q1=C，es=e 2e 1e 4，es1=e 1e 2e 4和e=e 5。 然后，该算法在e5到T（C，e5），这是接受状态qf。第二种情况是当Remove（e，es1）和es表示两个状态q和q1的等效线性化时。例如，如果es=ba，es1=aeb，并且当前事件是e，则从es1中删除e将返回一个等效于es的事件字符串。这里，算法在当前事件e上添加从q到q1的替代转换（第9-10行同样，仅为当前没有从q的转换的那些事件添加转换。这种情况如图11所示。这里，q=F，q1=C，es=e 2e 1e 4，es1=e 1e2e 3e 4和e=e 3。然后，算法在e3上添加一个到C的转换。完成此阶段后，我们可以从除D（t）值为1的状态之外的所有状态中删除事件串信息。 我们把这些状态称为倒数第二状态。它们的事件字符串将用于验证输入序列的可接受性。这个过程将在下一节中解释。5.3DFA模拟在运行时，只要没有同时发生的事件，我们就在没有替代转换的情况下模拟DFAaug。第一次出现时同时发生的事件，我们激活了所有的替代转换。从当前状态开始，我们选择最接近接受状态的路径138联合Sammapun等人理论计算机科学电子笔记113（2005）123{e1}e2 /2e3e4 /1{e1e2e4，e1e2e3e4}e1 /3SAB{e1e2、e1e2e3}e3Ce5 /0e5e2 /3D{e2}e1 /2E{e2e1}e4 /1F{e2e1e4}e6 /0见图10。 图9中算法的情况1{e1}e2 /2e3e4 /1{e1e2e4，e1e2e3e4}e1 /3SA B{e1e2、e1e2e3}e3e3Ce5 /0e5e2 /3D{e2}e1 /2E{e2e1}e4 /1F{e2e1e4}e6 /0图十一岁图2中的算法的情况29也就是说，U（t）最小的路径接下来，我们通常考虑替代转换和U（t）来模拟DFAaug因为同时发生的事件也可以单独发生，DFAaug接受的一些线性化可能不被DFAorg接受。当DFAaug达到接受状态时，我们通过比较输入序列和倒数第二个状态中的事件串进行验证，该倒数第二个状态在输入序列中的最后一个事件上具有原始转换到接受状态。因为DFA组织是最小的，只有一个这样的倒数第二个状态存在。如果它们匹配，DFAaug接受该输入序列。否则，DFAaug拒收。为了能够进行验证，我们需要保留从开始状态开始看到的所有事件的历史记录。历史记录还保存有关哪些事件同时发生以及哪些事件单独发生的信息。我们通过将输入序列存储为同时集的数组来实现。为了处理Kleene星，我们有一个标记来指示是否每个状态都被访问过。联合Sammapun等人理论计算机科学电子笔记113（2005）123139--1i = 0，j = 02对于每个ei∈ESelast3如果ei∈hj4然后把ei从hj5其他6然后将此输入字符串7如果hj为空8则j=j+19接受此输入字符串（如果尚未拒绝）见图12。 验证算法然后，我们只保留将模拟从一个状态带到另一个未访问状态的事件。这样，产生的历史字符串将类似于事件字符串的计算方式，并简化了我们的验证算法。让H=输入序列的历史。e最后=输入序列中的最后一个事件。ESelast=与倒数第二个状态相关联的一组事件字符串，在DFAorg中，elast状态转换为接受状态。ei=事件串中的一组事件，其中i是事件串中的位置hj=一组同时发生的事件hj∈H，其中hj发生在hj+1之前。图12中的验证算法是直接的。对于每个ei∈ESelast(line 2），我们检查ei是否出现在当前的同时集合中（第3行）。 如果不是，则拒绝输入字符串（第6行）。当当前集合被完全解析而没有被拒绝时，我们移动到下一个集合（第7-8行）。如果我们最 后 到达终点 如果没有被拒绝，我们接受输入序列（第9行）。例如，让输入序列在DFA被接受为{e1e 2，e 4，e 5}，其中事件e1和e2同时发生。由于序列中的最后一个事件，即，elast=e 5，我们有ESelast={e 1e 2e 4，e 1e 2e 3e 4}。 现在，由于ESe中的事件字符串{e1 e2 e4}最后匹配对于记录的输入序列e1，e2， e4，DFAaug将接受该输入序列。5.4算法分析该增强算法在每个阶段具有以下运行时间。 对于阶段1，我们运行BFS两次，因此运行时间为O（s + t），其中s = |Q|是状态数，t =|dom（T）|是转换的次数。对于阶段2，运行时间为O（s2·e·es2），其中e = |Σ|是140联合Sammapun等人理论计算机科学电子笔记113（2005）123Σ||i=1相关集合中事件的数量，es=q∈QES（q）是正则表达式中可能的事件串的数量，（最坏情况分析）。这然后构成扩充DFA的编译时间代价。图13中的表格比较了该算法与动态模拟所有可能路径的简单算法的运行时间。由于可以有O（2n）这样的路径，其中n是输入字符串的长度，动态模拟方法可以施加O（2n）的额外运行时间。在我们的算法中，O（n）添加到运行时间是为了当DFAaug接受时验证输入序列。时间复杂度为O（n2）。我们只添加从低编号到高编号的因此，时间复杂度为O（n）。因此，我们的算法显然是首选简单的算法。算法运行时间空间所有路径使用替代转换进行增强O（2n）O（n）0O（n2）图十三.两种算法5.5DFAorg和DFAaug在本节中，我们提供了DFAorg和DFAaug等价的证明定理5.1 DFA aug接受当且仅当DFA org接受。证据第1部分：如果DFA org接受，DFA aug接受。这个陈述可以重述为，如果DFAorg接受输入序列的某种线性化，那么DFAaug接受其所有等效线性化。我们将一条道路和一组道路定义如下。DFAorg中的路径是从起始状态q0到接受状态qf的任何路径。每一条这样的路径都由算法唯一排序。路径集是DFAorg中从q0到qf的所有可能路径的枚举。通过对算法的描述，每一个交替变迁都是从集合中的一条路到另一条路的变迁，而且变迁总是从较低的U（t）到较高的U（t）。假设a是当前正在考虑的事件。设q1和q2为所考虑的两个状态。设es1和es2分别是与q1和q2相假设当前状态为q1，因此，es1是迄今为止看到的一种输入线性化。该算法具有以下备选方案。(i) 事件串es2是迄今为止所见的输入的不同等效线性化（Hashed（es1）=Hashed（es2））。然后，算法添加联合Sammapun等人理论计算机科学电子笔记113（2005）123141在A上从Q1到状态Q3的可选转换使得在A上存在从Q2到Q3的转换，即，T（q2，a）=q3.因此，这种交替的过渡从一个线性化到另一个线性化采取一个步骤。（Hashed（concat（es1，a））=Hashed（concat（es2，a）。(ii) 从 es2中 移 除 a 是 迄 今 为 止 所 见 的 输 入 的 不 同 等 效 线 性 化 。（Hashed（es1）=Hashed（Remove（a，es2）。然后，该算法在a上增加了一个从q1到q2的交替过渡.因此，这种可替换的过渡再次采取从一个线性化到另一个线性化的步骤（Hashed（concat（es1，a））=Hashed（es2））。现在我们证明了对于每一对等价线性化都存在这样的交替跃迁设状态q1、q2、q3、q4分别属于路径p1、p2、p3、p4，并设这些路径的顺序为p1p2p3p4。<<<那么状态的顺序是q1q2q3q4。<<<如果与这些状态中的每一个相关联的事件串之一是不同的等效线性化，排序如上所述，则可以看出，该算法以该顺序对每对状态（Q1，Q2）、（Q1，Q3）、（Q1，Q4）、（Q2，Q3）、（Q2，