理论计算机科学电子札记138（2005）87-99www.elsevier.com/locate/entcs时间转移系统奥尔加·格林奇坦1本特·琼森2马丁·卢伊克3乌普萨拉大学IT系瑞典乌普萨拉摘要我们扩展Angluin更具体地说，我们描述了一个过程，用于推断系统，可以通过事件记录自动机描述，通过询问一系列成员查询（系统是否接受给定的定时词？）和等价查询（假设的描述是否等价于正确的描述？）。在推断的描述中，状态由符号序列连同定时信息来标识。 成员查询的数量在区域图中是多项式的，并且在自动机的最大常数中学习。保留字： 模型推理，模型学习，时间系统1引言过去几十年的研究已经开发出强大的技术，用于在特定情况下使用反应系统模型，自动验证（例如，[9]）、测试用例生成（例如，[12，25]）、实施（例如，[17]），以及电信、嵌入式控制和相关应用领域中的反应系统通常，假设这些模型是在系统开发的规范和设计阶段先验然而，在实践中，通常没有正式的规范，或者随着系统的发展而过时。然后，我们必须推断出一个模型，1电子邮件：Olga. it.uu.se2 电子邮件：Bengt. it.uu.se3 电子邮件：Martin. it.uu.se本文作者由欧洲研究培训网络“游戏”支持。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.06288O. Grinchtein等人理论计算机科学电子笔记138（2005）87描述现有系统或实现的行为在软件验证中，正在开发用于通过对源代码的静态分析来生成软件模块的抽象模型的技术（例如，[10、20]）。但是，外围硬件组件、库模块或第三方软件系统不允许进行静态分析。在实践中，必须通过观察它们的外部行为来分析这样的系统事实上，通过分析外部可观察的行为来构建模型的技术（黑盒技术）可以在许多情况下使用。• 创建硬件组件、库模块的模型，这些组件是较大系统的一部分，例如，必须进行正式的验证或分析。• 对于回归测试，可以使用已实现系统的早期版本的模型来创建良好的测试套件和测试Oracle，以测试后续版本。这已经得到证明，例如，Hungaret al. [16、21]）。• 黑盒技术，如自适应模型检查[15]，已经被用来检查正确性属性，即使在源代码或正式模型不可用时。• 静态分析源代码的工具在很大程度上依赖于所使用的实现语言。黑盒技术更容易适应不同语言编写的模块。从系统行为的观察中推断模型可以看作是一个学习问题。 对于有限状态反应系统，它意味着从一组有限的查询的答案中构造一个（确定性的）有限自动机，每个查询都询问某个词是否被自动机接受。有几种技术（例如，[13，22，24，5]），其中使用基本上相同的基本原理;它们在如何选择成员资格查询以及如何从答案中构造自动机方面有所这些技术保证了如果获得“足够”的信息，将构造出正确的自动机为了检查这一点，Angluin和其他人还允许等价查询，询问是否假设自动机接受正确的语言;这样的查询要么回答是，要么回答假设和正确语言不一致的反例在[14]中，我们将Angluin等人的学习算法扩展到定时系统的设置我们研究了事件记录自动机（ERA）的一个子类这些是时间自动机[2]，对于每个动作a，使用一个时钟记录最后一次出现的时间。事件记录自动机可以被确定，并且具有很强的表达能力来建模许多有趣的定时系统;例如，它们与定时转换系统一样强大[18，3]，定时系统的另一个流行模型。O. Grinchtein等人理论计算机科学电子笔记138（2005）8789然而，对于[14]中提出的方法，我们进一步限制了事件记录自动机是事件确定性的，因为每个状态在每个动作中最多有一个传出转换（即，通过去除时钟约束获得的自动机是确定性的）。在这种限制下，动作发生的时间约束只取决于过去的动作序列，而不取决于它们的相对时间。所选择的方法是基于这样一种思想，即重用学习规则系统的技术，而不是直接学习定时系统。因此，我们建立了一个表征的时间语言接受DERA的正规词语言。这样一种规则的词语言可以被理解为时间语言的一种符号表征.由于它是一种正则语言，因此可以使用Angluin算法等方法为了实现这一点，我们描述了符号词和定时词是如何相关的，更重要的是，如何通过定时词的几个查询来学习符号词在本文中，我们将我们以前的结果推广到事件记录自动机（ERA）的全类。虽然我们重用[14]中开发的繁荣计划，但细节不同。我们制定了一个（符号）的语言的电子逆向拍卖的语言正规语言的特征此外，我们还证明了每个符号词都可以由一个计时词来识别。因此，Angluin算法中的介绍了学习确定性事件记录自动机的算法LSDERA. LSDERA学习一个所谓的简单确定性事件记录自动机。我们证明了每一个确定性的事件记录自动元都可以转化为一个唯一的简单自动元，它至多具有一个指数上更多的位置。我们的转换是基于用于获得所谓的区域图的想法。我们表明，LSDERA的成员查询的数量是多项式的最大常数出现在警卫的大小和简单的确定性事件记录自动机的位置的数量n等价查询的数量最多为n。除了[14]，我们不知道任何其他关于学习时间系统或时间语言的工作然而，有几篇论文关注的是寻找适合作为学习基础的时间语言有几个作品定义了时间自动机的可确定类（例如，[3，26]）和时间语言的右同余（例如，[23，19，27]），以测试和验证为动机。本文件的结构如下。在下一节的讨论之后，我们将在第3节中定义事件记录自动机（DERA），以及我们学习ERA及其时间约束的技术。第5节给出了一个简短的例子。90O. Grinchtein等人理论计算机科学电子笔记138（2005）872个房间我们把非负实数集写成R≥0，自然数集写成N设是一个有限大小的字母表，|Σ|.一个时间词在上是一个有限序列wt=（a1，t1）（a2，t2）. （an，tn）的符号ai∈ {\displaystyle a i}与非负实数ti配对，使得序列t1t2...时间戳的t n是非递减的。我们用λ表示空词。一个时间语言是一组时间词的集合。一个事件记录自动机对于每个符号a∈ A都包含一个时钟xa，称为a的事件记录时钟。直观地说，xa记录了自符号a最后一次出现以来所经过的时间。 如果a之前没有出现，则时钟x a的值是unfined，用表示。对于集合{xa|a∈ <$}的事件记录时钟。一个时钟赋值γ是一个从C到R≥0<${}的映射。 时钟约束是一个原子约束的合取，形式为x= n，x<$n或x−y<$n，其中x，y∈C<$，<<$∈ {，≤，>，≥}，n∈N。我们用γ| =表示时钟估值γ满足时钟约束;然后我们使用仅满足时钟约束x=的约定。一个时钟约束是K有界的，如果它不包含大于K的常数.有时，在方便的情况下，我们识别所有大于K的值，并将它们表示为∞。一个时钟约束可以确定一个|Σ |n维多面体[[n]] n（R≥0）|Σ|即实数向量满足约束条件的数。 时钟保护是一种时钟约束，合取只有x=n或xn =n（对于x∈Cn，n ∈ {<，≤，>，≥}）的形式，即，时钟之间的比较是不允许的。时钟保护的集合由G表示。一个时钟警卫g识别一个|Σ|- 维超立方体[[g]]<$（R≥0）|Σ|. 一个简单的时钟保护是一个时钟约束，它的合取只有x= k，x =n，n x n+ 1或x > K（对于x∈C）的形式。 一区域约束是形式为x∈C<$c（x）<$x，y∈C<$的时钟约束 d（x，y）其中c（x）具有x=n，n × n+1或x> K的形式，并且d（x，y）具有形式x−y=n或n x−y n+1。时钟约束可以使用差分边界矩阵（DBM，[11]）有效且唯一地表示。此外，DBM允许对时钟约束进行高效操作，如交集，检查相等性等。时钟控制字wc是序列wc=（a1，γ1）（a2，γ2）. （an，γn）的sym-ai∈，与事件时钟赋值配对。每个定时字wt=（a1，t1）（a2，t2）. （an，tn）可以自然地变换为时钟字CW（wt）=（a1，γ1）（a2，γ2）. （an，γn）其中对于每个i，1≤i≤n，• γi（xa）= γ i如果aja对于1≤j i，• γi（xa）=ti−tj如果存在aj，其中1≤j i且aj=a，使得aka对于j k i.O. Grinchtein等人理论计算机科学电子笔记138（2005）8791保护字wg是序列wg=（a1，g1）（a2，g2）. （an，gn）的符号ai∈ n，与时钟保护配对。我们要求每个gi只能引用定义的时钟，即，时钟xa使得a在a1a2. ai−1。请注意，我们将空合取符与真合取符标识为真。 对于时钟字wc=（α1，γ1）（α2，γ2）. （an，γn）我们用wc|= wg表示γi|= gifor1≤i≤n。 对于计时词wt，我们使用wt|= wg表示CW（wt）|= wg. ↑是条件将每个时钟y替换为y-d。一个保护字wg=（a1，g1）（a2，g2）. （an，gn）称为a1a2..一个n，一个1，一个2 An被称为W g下的单词。以类似的方式来定义作为计时词wt基础的词w对于一个保护字wg，我们引入wg的最强后置条件，记为sp（wg），作为对由 在符号的任何随后出现时，后置条件计算是时间自动机符号验证工具的核心[8，6]，可以归纳如下：• sp（λ）=true，• 如果g中引用的所有时钟都由wg定义，则sp（wg（a，g））=（（sp（wg）g）[xa<$→0]）↑，否则sp（wg（a，g））=假，其中，对于时钟约束θ和时钟x，• 条件x=0<$<$x.<$，• ↑是条件在字母表Γ上的一个确定性有限自动机（DFA）A= L × Γ，L，l0，Lf，δn由状态L，初始状态l0，一个接受状态集Lf<$L和一个部分转移函数δ：L×Γ→L组成. 在这个词上打一个Aw=aa.. . aisafinite序列el→a1 l→a2·· ·−a→nlofstat esl∈L1 2n0 1n i使得l0是初始状态，δ（li−1，ai）定义为1≤i≤n，其中δ（li−1，ai）=li.在这种情况下，我们写δ（l0，w）=ln，从而以自然的方式扩展了δ语言L（A）包括所有的词一个一个二...在其上存在接受游程的n，其中游程是接受i，δ（l0，w）∈Lf.3事件记录自动机定义3.1事件记录自动机（ERA）D= A，L，l0，Lf，δf由有限输入字母表A，有限位置集L，初始位置l0∈L，接受位置集Lf，转移函数δ组成：92O. Grinchtein等人理论计算机科学电子笔记138（2005）87JL× N ×G→L，这是一个部分函数，对于每个位置，输入符号和保护潜在地规定了一个目标位置。我们称ERA时间确定的i ∈ δ（l，a，g1）= l1和δ（l，a，g2）= l2隐含s[g1] ]n[[g2]]=l2Thus，当一个位置可能有不同的后继者时，这些后继者可以通过守卫来区分.定理3.2（[3]）每一个ERA都可以转化为一个等价的时间确定ERA.因此，下面我们将集中讨论时间确定性电子逆向拍卖，简称TDERA。为了定义TDERA接受的语言，我们首先将其理解为DFA。给定一个TDERAD= r，L，l0，Lf，δj，我们定义dfa（D）为DFAAD=r，L，l0，Lf，δJ在字母表Γ =×G上，其中δJ：L×Γ→L定义为δJ（l，（a，g））=δ（l，a，g）当且仅当δ（l，a，g）被定义，否则δJ（l，（a，g））是未定义的。注意，D和dfa（D）具有相同数量的位置/状态。此外，请注意，这种从TDERA到TDERA的映射G×G上的DFA是单射的，这意味着对于G×G上的每个DFAA，都有一个唯一的（直到同构）ERA，记为tdera（A），使得dfa（tdera（A））同构于A。被TDERA D接受的语言L（D）被定义为定时词w t的集合，使得wt|= wg对于某个保护字wg∈ L（dfa（D））. 我们称两个TDERAD1和D2等价于i <$L（D1）=L（D2），并将其表示为D1<$tD2，或仅为D1<$D2。 一个TDERA是K-有界的，如果它的所有守卫是K-有界的定义3.3一个TDERAD是简单的，如果对于所有的保护字wg（a，g）∈ L（dfa（D）），我们有g是简单的并且gsp（wg）是可满足的。我们注意到，TDERA是否简单仅取决于L（dfa（D））。这一定义的结果如下。引理3.4如果wg（a，g）∈ L（dfa（D）），其中D是一个简单的TDERA，则存在一个时间字wt（a，t）∈ L（D）使得wt（a，t）|= wg（a，g）.证据这个主张很容易从简单的定义中得出。Q每个TDERA都可以使用区域图构造[1]转换为简单的等价TDERA。引理3.5对于每个TDERA，存在简单的等价TDERA。证据 设T_（DERA）D= k_（？），L，l_0，L_f，δ_（？）是K-有界的.我们定义一个基于所谓区域的等效简单TDERADJ= j fj，L，l0，L，δO. Grinchtein等人理论计算机科学电子笔记138（2005）8793自动机D.我们绘制了结构草图，细节可以在[1，7]中找到。DJ的位置集合包括对（l，n），其中l∈L，n是aK-有界区域约束。然而，（l，n）有一个稍微不同的解释，比在区域图构造中的站。它应该被理解为D在位置l，并且时间开始于由m给出的某个点。换句话说，我们想到的是"“而不是"”。为了将区域图变成自动机，我们必须添加一个转换函数和最终状态。直观地，我们通过一个动作a和一个简单的保护g从（l，n）前进到（lJ，nJ），如果D可以通过a从l前进到lJ，关于D中的某个约束g。此时，J是通过用g约束↑并重置a的时钟而获得的区域。 换句话说，对于每个符号a和简单保护g，让δJ（（l，n），a，g）定义为（lJ，nJ），如果存在一名警卫定义了包含g的g，且对于whichδ（l，a，gδ），定义了d，且dislJ，且dJ=（否则，它是不确定的。最后设（δ（l，a，g），n（J））∈LFJi ∈δ（l，a，g）∈Lf.这是例行表明，从初始位置（l0，真）可达的自动机的一部分是简单的。Q简单TDERA的重要性质是等价与对应DFA上的等价一致。定义3.6我们称两个简单的TDERA为D1和 D2dfa等价，记为 D1dfaD2，i dfa（D1）和dfa（D2）接受相同的语言（在DFA的意义上）。引理3.7对于两个简单的TDERAD1和D2，我们有D 1类 D2iD 1iD 2证据 从右到左的方向紧随其后，因为L（Di）由L（dfa（Di））定义。为了证明另一个方向，假设D1/dfaD2。 则存在一个最短的wg使得wg∈ L（dfa（D1）），但wgL（dfa（D2））（或相反）。 根据引理3.4，这意味着有一个时间词wt使得wt∈ L（D1）但wt/∈ L（D2），即，D1/D2。Q我们现在可以证明简单TDERA的中心性质定理3.8对于每个TDERA，存在唯一等价的极小单TDERA（直到同构）。证据通过引理3.5，每个TDERAD可以被转换成简单的等效TDERADJ。 设Amin是唯一的极小DFA，它等价于dfa（DJ）（直到同构）.因为（如后所述）94O. Grinchtein等人理论计算机科学电子笔记138（2005）87定义3.3）TDERA是否简单仅取决于L（dfa（D）），我们有Dmin=tdera（Amin）是简单的。通过引理3.7，Dmin是唯一的最小简单TDERA（直到同构），使得Dmin≠DJ，即，使得D最小等于D。Q4学习事件记录自动机学习DFAAngluin在这个算法中，一个所谓的学习者，最初对A一无所知，试图通过向一个知道A的老师提问来学习L（A）。有两种查询：• 成员查询包括询问字符串w∈Γ是否在L（A）中• 等价查询包括询问假设的DFAH是否正确，即，L（H）=L（A）。如果H是正确的，老师将回答是，否则提供一个反例w，或者在L（A）\ L（H）中，或者在L（H）\L（A）中。学习器维护前缀的前缀闭合集合U_f，其是用于识别状态的可识别数据，以及子集的子集闭合集合V_f，其用于区分这些状态。在算法期间，当需要时，增加集合U和V学习器对（U<$UΓ）V中的所有单词进行成员查询，并将结果组织到表T中，该表T映射每个u∈（U<$UΓ）到映射T（u）：V<$→ {接受，不接受}.在[4]中，每个函数T（u）被称为一行。 当T是闭的（意味着对于每个u ∈ U，a∈ Γ，存在uJ∈U使得T（ua）= T（uJ））并且是相容的（意味着T（u）= T（uJ）暗示T（ua）=T（uJa））时，则学习者构造假设的DFA H= l（u）r，L，l0，δl，其中L ={T（u）|u∈U}是不同行的集合，l0是行T（λ），δ由δ（T（u），a）= T（ua）定义，并在等价查询中提交H。 如果答案是肯定的，那么学习过程...dure完成，否则返回的反例用于扩展U和V，并执行后续的成员资格查询，直到到达新的假设DFA等。对于Angluin 粗略的想法是，对于表T中的每个条目都需要查询，O（knm）是行数，n是列数O. Grinchtein等人理论计算机科学电子笔记138（2005）8795a [xa=]a [xa= 0]0 1 2a [xa≥1]a [xa=0]Fig. 1. 自动机A1学习TDERA给定一个被TDERAD接受的时间语言，我们可以不失一般性地假设D是由于定理3.8而存在的唯一的最小和简单的语言。则D由它的符号语言A=dfa（D）唯一确定，这是一个正则（词）语言。因此，我们可以使用Angluin算法学习A然而，L（A）是一种简单的保护词之上的语言，但在时间设置中的教师应该处理时间词而不是保护词。因此，让我们通过助理来扩展Angluin算法中的学习者此外，它还必须回答等价查询，咨询计时教师。对于一个简单的保护字w =（a1，g1）. （an，gn）每个扩展w的简单守卫g与作用量a一起定义一个区域。因此，如果w是可接受的，则在该区域中的单个点中检查a就足够了，该区域定义为：g和w的后置条件。换句话说，它可以检查一个任意的定时字，|= w来检查w是否是符号语言。一个区域可以拥有的后继区域数为O（|Σ |K）。算法的复杂度为O（|Σ |2n2mK）。5示例让我们通过展示如何学习图1中描述的自动机A1的语言来解释该算法。最初，该算法询问λ和（a，xa= λ）的成员资格查询。这产生了表0（a）中所示的初始观测表T1。4它是一致的但不是封闭的，因为row（（a，xa=n））不同于row（λ）。按照Angluin然后，学习者构建一个如图2所示的假设TDERA A2，并在等价查询中提交A2。假设返回反例（a，xa= 0）（a，xa= 0）（a，xa它被A1接受，但被0表示不接受，1表示接受。96O. Grinchtein等人理论计算机科学电子笔记138（2005）87a [xa=1] a[xa=1]01（一）T1λλ1a（xa=0）0表1（b）第（1）款T2λλ（a，xa =0）10（a，xa =0）（a，xa = 0）1（a，xa =n）（a， 0xa 1）0（a，xa =0）（a，xa = 1）1（a，xa =0）（a，xa> 1）1a [0
1]a [xa=0]图二. AtomatonA2a [01]a [xa=]a [xa>1]a [0 1）10（a，xa =0）（a， xa = 0）（a，0 xa 1）00（a，xa =0）（a，xa = 1）00（a，xa =0）（a，xa> 1）00（a，xa =0）（a， xa = 0）（a，xa = 0）00（a，xa =0）（a，xa = 0）（a，0 xa 1）00（a，xa =0）（a， xa = 0）（a，xa = 1）00（a，xa =0）（a， xa = 0）（a，xa> 1）00（a，xa =0）（a， xa = 0）（a，xa = 0）（a，xa = 0）（a，xa = 0）00（a，xa =0）（a， xa = 0）（a，xa = 0）（a，0 xa 1）00（a，xa =0）（a， xa = 0）（a，xa = 0）（a，xa = 1）00（a，xa =0）（a， xa = 0）（a，xa = 0）（a，xa> 1）00表2wg=（a，xa= 0）（a，xa= 0）我们的学习算法的复杂性是多项式的区域图的大小。一般来说，这可能比表示相同语言的最小确定性ERA自动机大指数。建立时间系统学习问题的下界是一个有趣的问题引用[1] R.好吧时间自动机在Proc.11th International Computer Aided Verification Conference，卷1633的Lecture Notes in Computer Science，第8-22页。Springer-Verlag，1999.[2] R. Alzheimer和D.迪尔时间自动机理论。理论计算机科学，126：183-235，1994。[3] R.巴尔湖Fix和T.亨辛格事件时钟自动机：一类可确定的时间自动机。理论计算机科学，211：253[4] D.安格鲁从查询和反例中学习正则集。信息与计算，75：8798O. Grinchtein等人理论计算机科学电子笔记138（2005）87[5] J. L. Balc'azar，J. 迪亚斯河。 去吧。Algorithmsforlearningfiteautomatafrommueries： A unifiedview.在算法，语言和复杂性的进展，第53-72页。Kluwer，1997年。[6] J. Bengtsson，K. G. Larsen，F. Larsson，P. Pettersson，and W. 逸 UPPAAL：用于实时系统自动验证的工具套件。In R. T.A. A. Henzinger和E. D. Sontag编辑，混合系统III，计算机科学讲义第1066卷，第232-243页。Springer-Verlag，1996.[7] P. Bouyer不可驯服的时间自动机。In H. Alt和M. Habib，editors，Symp.计算机科学的理论方面，计算机科学讲义第2607卷，第620- 631页。Springer Verlag，2003年。[8] M.博兹加角道斯岛Maler，A. Olivero，S. Tripakis和S.尤文Kronos：实时系统的模型检查工具。以 . J.Hu 和 M. Y. Vardi ， 编 辑 ， Proc.10th International Conference on Computer AidedVerification，Vancouver，Canada，Volume 1427 ofLecture Notes in Computer Science，pages546-550. Springer-Verlag，1998.[9] E. Clarke，O.Grumberg和D.佩尔德。模型检查。MIT Press，Dec.1999年[10] J. 科贝特，M。Dwyer，J.Hatelaisi，S.劳巴赫角Pasareanu，Robby，and H.郑班德拉：从Java源代码中提取有限状态模型。第22届软件工程国际会议，2000年6月。[11] D.迪尔有限状态并发系统的时间假设和验证。在J.Sifakis，编辑，自动验证方法的状态系统，第407卷的讲义在计算机科学。Springer Verlag，1989年。[12] J. - C. Fer n and ez，C. Jard，T. 杰罗和C。 Viho。一种用于验证技术协议的测试套件的改进方法。计算机程序设计科学，29，1997。[13] E. M.黄金 语言识别在极限。 信息与控制，10：447[14] O.格林希坦湾Jonsson和M.洛克尔事件记录自动机的学习。在FORMATS和FTRTFT联合会议的会议记录中，计算机科学讲座笔记，9月11日。2004. 出现[15] A. Groce，D. Peled和M. 扬纳卡基斯 自适应模型检测 在J. - P. Katoen和P. Stevens，编辑，Proc. TACASSpringer Verlag，2002年。[16] A. Hagerer，H.洪加尔岛Niese和B. Ste daughen.用适度规则外推法生成模型。在R.- D.Kutsche和H. Weber编辑，Proc. FASE'02，第5届软件工程基本方法国际会议，计算机科学讲义第2306卷，第80-95页。Springer Verlag，2002年。[17] D.哈雷尔Lahover，A. Naamad，A. Pnueli，M.波利蒂河Sherman，A. Shtull-Trauring和M.Trakhtenbrot STATEMATE：一个用于开发复杂反应系统的工作环境IEEE软件工程学报，16（4）：403[18] T. Henzinger，Z. Manna和A.普努埃利时间转移系统的时间证明方法。信息与计算，112：173[19] T. Henzinger，J.-F. Raskin和P. -Y. 朔本斯常规实时语言。在K. Larsen，S. Skuym和G. Winskel，编辑，Proc. ICALPSpringer Verlag，1998年。[20] G. 霍尔茨曼 使用SPIN对ANSI-C代码进行逻辑验证。在K。 Havelund，J.Penix和W.Visser ， editors ， SPIN Model Checking and Software Verification ： Proc.7thInt. SPINWorkshop，Volume 1885 ofLecture Notes in Computer Science，pages 131施普林格出版社O. Grinchtein等人理论计算机科学电子笔记138（2005）8799[21] H. 洪加尔岛Niese和B.Ste daughen. 自动机学习中的特定领域优化在2003年第十五届国际电脑辅助验证[22] M. Kearns和U.瓦齐拉尼计算学习理论导论。MIT Press，1994.[23] O. Maler和A.普努埃利关于可识别的时间语言。FOSSACS 04，软 件 科 学 和 计 算 结 构 基 础 会 议 ， 计 算 机 科 学 讲 义 。 Springer-Verlag ， 2004. 可 从www.example.com获得http://www-verimag.imag.fr/PEOPLE/Oded.Maler/。[24] R. Rivest和R.夏皮尔使用归巢序列的有限自动机的推理。信息与计算，103：299[25] M. Schmitt，M.Ebner和J.格拉博夫斯基使用autolink和testcomposer生成测试在Proc. SDL论坛协会关于SDL和MSC-SAM'2000的第二次讲习班，2000年6月。[26] J. Springintveld和F. 凡德拉格最小化 定时 自动机在 B. Jonsson和J. Parrow，编辑，Proc. FTRTFTSpringer Verlag，1996年。[27] T.威尔基 在强大的可判定逻辑和时间自动机中的时间状态序列。在H. Langmaack，W. P. de Roever，and J. Vytopil，editors，Proc. FTRTFTSpringer Verlag，1994年。
我的内容管理
展开
