定时正则表达式的等价性及其关键词

理论计算机科学电子笔记106（2004）315-333www.elsevier.com/locate/entcs一类赋时正则表达式的等价性里卡多·普切拉康奈尔大学计算机科学系美国纽约州伊萨卡，邮编：14853mailto：riccardo@ cs.康奈尔。edu摘要定时正则表达式是捕获时间概念的正则表达式的扩展。粗略地说，定时正则表达式可用于表示事件的定时序列，并使用新的运算符来控制这些序列的持续时间。这些定时正则表达式对应于配备时钟的定时自动机的一种形式，这类自动机是由Alfred和Dill引入的。 我们开发了一个coalgebraic治疗这样的定时正则表达式，沿线的coalgebraic治疗的正则表达式的基础上确定性自动机。 这产生了一个共归纳证明原理，可以用来建立一类定时正则表达式的等价性。关键词：定时正则表达式，时间自动机，确定自动机，共归纳。1介绍时间自动机是由Alfred和Dill [1]提出的，它已经成为一种流行的实时系统行为建模和描述框架。在某种意义上，它们的自然性是由这样一个事实反映的，即某些类的时间自动机等价于用于推理实时系统的各种实时逻辑（参见Wilke [19]及其参考文献）。也许更重要的是，时间自动机是经典自动机的推广，这导致了经典自动机理论的著名结果可以扩展并适应时间自动机理论的可能性[17]。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.042316R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315与经典自动机理论类似，定时自动机的行为也可以使用正则表达式的扩展来表示，称为定时正则表达式。粗略地说，计时正则表达式记录了计时单词的集合，这些单词不仅记录了事件发生的顺序然而，虽然正则表达式准确地捕获了经典自动机识别的语言，但时间自动机的对应关系更为复杂。将正则表达式直接扩展为定时正则表达式（通过限制定时正则表达式所表达的定时单词的持续时间的运算符）并不能完全捕获定时自动机所识别的语言。关于时间正则表达式的“正确”扩展，可以完全匹配时间自动机的表达能力，仍然存在分歧本文主要研究时间正则表达式的性质。我们专注于一个没有争议的子类的定时正则表达式，即定时正则表达式与一个单一的操作符，以限制时间词的度，并调查的问题，确定当两个这样的定时正则表达式是等价的，也就是说，当他们表示相同的语言。这个问题是不平凡的，因为与正则表达式的情况相比[16，13]，没有已知的声音和完整的公理化定时正则表达式。我们的方法遵循Rutten [14]的方法，他发展了经典自动机的共代数理论。这种共代数处理的结果之一是共归纳，这是一种证明古典语言等价性的证明技术，可以提升为决定正则表达式等价性的过程。我们将Rutten的工作扩展到定时正则表达式的情况。更确切地说，我们给出了一个coalgebraic处理的时间自动机，推导出一个coinduction证明原则，并表明，这可以用来决定等价的一类定时正则表达式。本文的结构如下。在下一节中，我们将回顾我们使用的计时词和计时语言在第3节中，我们定义了定时正则表达式，这是正则表达式的扩展，它带有一个限制定时单词持续时间的运算符。 在第4节中，我们定义了一种可以接受时间语言的确定性时间自动机的形式，并在第5节中表明这些自动机形成了一个具有几乎最终由状态为时间语言的时间自动机组成的对象的范畴DTA。这就产生了时间语言平等的共归纳证明原则。在第6节中，我们使用这个共归纳证明原理来R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315317···推导出一个算法来建立定时正则表达式的等价性。我们在第7节结束。由于空间的原因，我们把结果的证明留到全文中。2时间词与时间语言古典语言理论[11]研究字母表上的单词。对这些词的一种解释是，它们表示连续发生的一系列“事件”。从这个角度来看，计时词（也称为时间事件序列）是一个不仅记录事件，而且还记录这些事件之间经过的时间的词，相对于某个时间单位。例如，ab·3·c表示事件a和b同时发生，然后是3个时间单位的延迟，然后是事件c。为了正式定义计时词，我们采用Asarin，Caspi和Maler的方法[3]。回想一下，在n上的经典词形成了由n生成的自由幺半群（n，n，n），其中n是n的元素的所有有限序列的集合concatenation（从现在开始，我们将把concatenation中的元素写成ab而不是a/b），而concatenation是空词。 为了定义时间词，我们取幺半群（，·，）与幺半群的组合，（R≥0，+，0）非负实数，用于表示时间。更精确地说，我们通过同余关系将时间词的幺半群T（）定义为R≥0（有连接·和空词）上的自由幺半群的商：σ1·σ2<$σ1σ2ifσ1，σ2∈R<$1·t2<$1+t2 ift1，t2∈R≥0<$1<$20分。直观地说，这些同余规则允许我们用一个单一的元素来替换（R≥0）中同一个等式中的相邻元素，并去掉虚单位元素.这种推导的结果是，每个计时词都可以写成规范形式，t1·a1·t2·a2···，也就是说，作为R≥0的元素的交替。事实上，我们通常只关心单词的最后一个元素（当在规范形式）是一个元素的。（直觉上，当时间延迟发生在单词的末尾时，我们会忘记它。）我们称这些词为正常计时词。如果σ=t1·a1···tn·an·tn+1是定时字，则t1·a1····tn·an是与σ对应的正常定时字。时间语言是一组时间词，正常时间语言是一组正常时间词。如果L是一种计时语言，那么由所有正常计时词318R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315{···|联系我们{···|联系我们∪T−→····对应L中的计时词的语言称为对应L的正常计时语言。例2.1定时语言t1一t2Bt3Ct2+ t310是所有定时字的集合，其中最多有10个单元分隔a和c事件的发生，中间有b事件。定时语言t1at2bt3ct1+ t210，t2+ t310是所有定时词的集合，其中事件a和b在开始的10个时间单位内发生，并且此外，事件A和C在彼此的10个时间单位内发生，其间有一个事件B。注2.2定时字符串的替代符号可以在文献中找到。[1]中，一个在R上的时间词是一对（σ，τ），其中σ是R上的一个词，τ是R≥0中的时间值的无限序列，假设是单调的和无界的。直觉上，如果σ的每个元素σi都被认为是一个事件，那么相应的τi表示oc的时间σi的电流应该清楚的是，这两种表示是等价的，在这个意义上，我们可以自由地在两者之间转换。我们使用的符号的优点是单词连接更容易定义，并且表现得更自然。这使得本文的理论更容易发展。Asarin、Caspi和Maler [2]使用了不同的符号他们定义一个信号在一个字符串的形式为一个t1. a tk，其中a ti是指1ki以表示发生并持续时间ti的事件ai。 在他们的代表-一个事件持续到下一个事件发生。如果我们用信号符号中事件的瞬时第一次发生来识别我们的事件，那么在这两个符号之间又有一个直接的对应关系。给定一个时间词σ∈ T（T），σ的持续时间，即在σ中花费的时间量，可以通过投影来定义。 函数λ：（）R≥0是通过将矩阵的元素映射到0而获得的，并且将结果视为幺半群的元素（R≥0，+，0）。 例如，λ（ab3c）= 030为00+ 3+ 0 = 3。两种语言的连接L1·L2是语言{σ1·σ2|σ1∈L1，σ2∈L2}.注意，L = L. L =L.我们把L与自身的n重级联记为Ln，即L·. ·L（n次）。像往常一样，L0={}。最后，我们写L∞n= 0Ln. 语言的一种新的运算就是求导，这是一个改编自[6]的概念。给定时间词σ，时间语言L的导数D σ由D σ（L）={σJ|σ·σJ∈L}。对于mDt·a（L），如果t∈R≥0，a∈n。R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315319∞∈⟨⟩3正则表达式赋时正则表达式可以用来表示某类语言，而不需要对单个时间进行显式约束。一个常见的符号从以下核心开始：e：：= 0 |1|一|e1e2|e1+ e2|e|⟨e⟩I其中a表示n的任意元素，I是形式为[l，u]、[l，u）、（l，u]或（l，u）（其中l，u∈R≥0且l≤u）或形式为[l，∞）或（l，）（其中lR≥0）的区间。正则表达式运算符保持其直观的解释：0是空正则表达式，1是表示空单词的正则表达式，a表示事件a∈ E，e1e2是e1和e2中事件的连接，e1+e2是e1和e 2中事件的析取，e E是e中事件的任意但有限次数的迭代。这些营办商并不限制活动的时间使用新构造捕获限制你好。直觉上，e表示由e指定的事件被限制在区间I中的持续时间内。例如，ab[0，10]c表示在10个时间单位内发生的事件a和b，后面是事件c。注3.1我们应该注意到，我们允许区间I上的界是实值的，而在文献中，它们是整数值的。允许实值边界的附加表达性将在本节后面定义一个有用的定时正则表达式导数概念时非常重要。与正则表达式类似，我们可以将每个定时正则表达式e与一个正常的定时语言[e]相关联，如下所示：[[0]]=[[1]]关于我们[[a]]={t·a|t∈ R≥0}[[e1e2]]=[[e1]]·[[e2]][[e1+e2]]=[[e1]][[e2]][[e]]=[[e]][[eI]]= [[e]]{σ|λ（σ）∈ I}。定义是标准的，除了与事件a相关的语言，它是表示a发生之前的任意时间延迟的语言;这捕获了事件先验没有时间限制的事实。320R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315{···|联系我们{···|联系我们例3.2回到上面的例子，与定时正则表达式ab[0，10]c相关联的定时语言是{t1·a·t2·b·t3·c |t1+ t2≤ 10}。要了解eI运算符，请比较以下语言：[[a[0，1）a[0，1）]]={t1·a·t2·a |t1<1，t2<1}[[<$aa<$[0，2）]]={t1·a·t2·a|t1+ t2<2}[[a[0，1）a[0，2）]]={t1·a·t2·a |t1<1，t1+ t2<2}[[aa[0，1）<$[0，2）]]={t1·a·t2·a |t2<1，t1+ t2<2}。特别要注意的是，所有这些语言都是不同的。 例如，[[aa[0，2）]包含单词0。5·a·1。2.一个既不在[a[0，1）a[0，1）]]中，也不在[aa[0，1）[0，2）]中的，以及一个字。2·a·0。5·a，不在[[a[0，1）a[0，2）]中。将这种情况与以下语言进行比较：[[aa[0，2）]]={t1·a·t2·a |t1+ t2<2}[[a[0，2） a[0，2） ]]={t1·a·t2·a|t1<2 ， t1+t2<2}[[a<$a<$[0，2）<$[0，2）]]={t1·a·t2·a |t2<2，t1+t2<2}。所有这些语言都是平等的。虽然我们上面给出的定时正则表达式的概念包含了许多形式的定时语言，但它们仍然受到相当的限制。例如，它们无法从例2.1中捕获语言t1a t2b t3c t1+t210，t2+t310。为什么这是一个问题？回想一下，在经典的语言理论中，正则表达式所能表达的语言与有限状态自动机所能识别的语言完全对应人们可能会问，时间正则表达式是否可以捕获由Alfrer和Dill定义的时间自动机识别的语言，这是首先引入时间正则表达式的动机。(We将在下一节中定义时间自动机，尽管目标略有不同。事实证明，答案是否定的：语言t1at2bt3ct1+ t210，t2 +t310使用相当简单的时间自动机是可识别的研究人员一直在努力捕捉时间自动机识别的语言。提出了两种办法。1第一个由Asarin，Caspi和Maler [2，3]描述，扩展了上面定义的带有交集运算符和重命名运算符的定时正则表达式他们证明了这些扩展的时间正则表达式准确地捕获了时间自动机识别的时间语言。[2]不幸的是，重命名操作员相当笨拙。Asarin和Dima [4]和Dima [9]描述的另一种方法避免了对1Bouyer和Petit [5]引入了另一种形式的定时正则表达式， 在精神上比这一节中的，非常接近时间自动机本身。2 Herrmann [10]首先认识到重命名实际上是建立结果所必需的。R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315321⟨ ⟩⎨或者是交集或者是重命名运算符，并且使用一族I运算符，每个运算符基本上对应于对定时字中的时间的不同约束。这种方法的困难在于，由于不同的正则表达式运算符不需要嵌套，因此很难建立定时正则表达式的格式良好性。尽管我们介绍的时间正则表达式的表达能力不足以捕获由Alfrer和Dill [1]的确定性自动机识别的所有语言，但我们将在本文的剩余部分关注这些核心时间正则在最后一节中，我们给出了时间语言的导数的定义。 我们现在介绍一个对应于在语言s上取导数Dt·a的句法运算，其中我们写Dt，a。这可以被定义为纯粹的策略，凯莉首先，对于区间I和t ∈ R≥0，定义I − t ={x |x + t ∈ I}<$R≥0。直观地说，I-t是Dt，a（0）=0Dt，a（1）=0Dt，a（a）=1Dt，a（b）=0Dt，a（e1e2） =Dt，a（e1）e2+Dt，a（e2）Dt，a（e1+e2）=Dt，a（e1） +Dt，a（e2）Dt，a（e）=Dt，a（e）eDt，a（eI）= D000元，否则这个定义依赖于一个语法上检查表达式是否可以表示空单词的操作。同样，这可以在定时正则表达式的结构上归纳定义：322R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315ϵˆ(ee)=⎧⎨1ifϵˆ(e1)=ϵˆ(e2)=1⎩⎩+e）=0if（e1）=（e2）=0中文（简体）2a，c1：=0，c2：=0b，c1>=1，c2：=0Fig. 1. 时间自动机（0）=0（1）（1）（1）（a）=01 20.00否则1例其他情况ϵˆ(e∗)=1ϵˆ(⟨e⟩I)=ϵˆ(e).很明显，（e）总是表达式0或1。 我们可以证实然而，这是一个定义时间语言的操作员。命题3.3对于所有的时间正则表达式e，t∈ R≥0，且a∈ R，我们有R（e）=1当且仅当R∈[[e]]，且d[[DR t，a（e）]]=Dt·a（[[e]]）。4确定性时间自动机时间自动机的概念是由Alfred和Dill [1]引入的，它扩展了经典自动机的概念。 与经典情况一样，时间自动机由状态和状态之间的转换组成。不同的是，时间自动机依赖于时钟来跟踪时间。时钟初始化为0，当自动机处于任何特定状态时，它们以相同的速率单调增加。 像往常一样，跃迁由字母表中的元素标记，但也可能受到时钟约束的保护。例如，我们可以指定只有当时钟c1的值在1和2之间时，才能发生从状态的转换。此外，在转换时，时钟可以被更新。拥有可以独立更新的多个时钟意味着它们可以用于测量不同转换之间的时间。S1S2R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315323≥∈∈×例4.1考虑图1中的自动机，有两个状态s1和s2。 如果我们从状态s1开始，时钟c1和c2初始化为0，那么自动机在状态s1中保持一段不确定的时间t1，使时钟c1和c2增加t1。 在a转换到状态s2之后，时钟c1和C2被重置为0。自动机在状态s2中保持一段不确定的时间t2，使时钟c1和c2增加t2。当时钟c1≥1时，自动机可以执行到状态s1的b转换，这将时钟c2重置为0.此过程可以执行任意次数。不难看出，这个自动机的状态s1 所是{t1·a·t2·b·. ·t2n−1·a·t2n·b|n∈ N，t2i≥ 1，i∈ [1，.，n]}。我们以一般的方式形式化了这种自动机，实际上，它比Alfrer和Dill[1]给出的定义更一般。如上一节所述，设m是一个有限的字母表。如果C是一组时钟，则C上的时钟赋值v对于C中的每个时钟，给出时钟的时间读数形式上，v是a从C到R≥0的函数，即v（c）0对所有c其中v（c）是时钟c的时间值。设V（C）为C上所有时钟赋值的集合。令0表示零赋值，即，对于所有C.如果v是一个时钟赋值，t是R≥0中的实数，则v+t是与v相似的赋值，只是t被加到所有分量上，即对于所有时钟c∈C，（v+t）（c）=v（c）+t。如果v是一个时钟赋值，则v[c→t]是时钟赋值vJ，它与v一样，只是vJ（c）=t。我们也记为v≥t，如果对所有c∈C，v（c）≥t。我们定义了一个确定性的时间自动机，它是一个元组M=（S，C，o，δ），其中S是一组状态，C是一组时钟，o是一个函数它指定一个状态是否接受（o（s）=1）或不接受（o（s）=0），δ是自动机的转移关系。对于一组状态S，令T（S，C）=S×V（C）是定时状态的集合。 因此，定时状态具有form（s，v），其中s是状态，v是C上的时钟估值。过渡关系δ使得对于所有输入符号a和所有定时状态（s，v），我们有δ（（s，v），a）ST（S，C）。直觉上，δ（（s，v），a）=（sJ，vJ）指示从定时状态（s，v），自动机可以进行移动a，导致新状态sJ和新时钟估值vJ。例4.2例4.1（和图1）的自动机可以在我们的框架中被捕获为自动机（S，C，o，δ），其中：• S={s1，s2，ssink}• C={c1，c2}•0（s1）= 10（s2）= 0324R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）3151⎧2⎩·····o（ssink）= 0• δ（（s，v），x）=δ（s2，0）ifx=asink（ssink，v）否则δ（（s，v），x）=n（s1，v[c2<$→0]），若x=b且v（c1）≥1（ssink，v）其他δ（（ssink，v），x）=（ssink，v）.“sink”状态的sink 在大多数自动机描述中是隐含的。注4.3如前所述，这些自动机比由Alberr和Dill [1]定义的时间自动机这是主要的分歧。Alberr和Dill将他们的自动机限制为有限的状态集，并为每个时间自动机指定一个起始状态。更重要的是，当我们就时钟赋值而言，不对转换δ施加任何限制，则需要由以下形式的约束的布尔组合来保护在时间自动机中的转换：x i∈I，其中I是由整数（例如[0，1]，[4，8]或（10，∞））限定的区间。为了能够在第5节中定义最终自动机，我们的表述需要具有这种一般性。最后，唯一允许的时钟更新是时钟重置：一组时钟可以在转换时重置，而其他时钟保持不变。我们将自动机M的每个定时状态（s，v）与该定时状态识别的正常定时语言LM（s，v）相关联我们按以下步骤进行一个定时字σ =t1a1... t na nt n+1由定时状态（s，v）识别，如果：(1) σ=t且o（s）= 1，或(2) 若σ = t·a·σJ，且δ（（s，v + t），a）=（SJ，VJ），其中σJ由（SJ，VJ）识别.设LM（s，v）是M在定时状态（s，v）下识别的正常定时字的集合。正如下面的命题所表明的那样，把自己限制在正常的计时词上是足够的。命题4.4当且仅当对应于σ的正常计时词在计时状态（s，v）被M识别时，计时词σ在计时状态（s，v）被M识别。两个时间自动机M=（S，C，o，δ）和MJ=（SJ，CJ，oJ，δJ）之间的互模拟是关系R<$T（S，C）×T（SJ，CJ），使得：(1) 对于所有的（s，v）R（sJ， vJ），我们有o（s）=o（sJ）;R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315325∼∼∈∈(2) 对所有的（s，v）R（SJ，VJ）和所有的t∈ R≥0，我们有（s，v+t）R（SJ， v+t）;(3) 对所有的（s，v）R（SJ，VJ）和所有的a ∈ N，我们有δ（（s，v），a）RδJ（（SJ，VJ），a）.M与其自身之间的互模拟称为M上的互模拟。两个时间状态（s，v）和（sJ，vJ）被称为是双相似的，用（s，v）（sJ，vJ）表示，如果存在互模拟R使得（s，v）R（sJ，vJ）。这个关系是所有互模拟的联合，因此是最大的互模拟。对我们感兴趣的性质是，双相似状态识别相同的语言。命题4.5如果s是M的一个态，且sJ是MJ的一个态，其中（s，v）≠（sJ，vJ），则LM（s，v）= LMJ（sJ，vJ）。5类别DTA在上一节中定义的时间自动机可以给出一个范畴结构。我们定义了确定性时间自动机的范畴DTA（在一个固定的时间上），通过把上面的确定性时间自动机作为对象 给定自动机M =（S，C，o，δ）和MJ=（SJ，CJ，oJ，δJ），态射f：M −→ MJ是一个函数f：T（S，C）−→T（SJ，CJ）使得：(1) 对所有（s，v）∈T（S，C），若f（s， v）=（SJ，VJ），则o（s）=OJ（SJ）;(2) 对所有（s，v）T（S，C）且t R≥0，若f（s，v）=（SJ，VJ），则f（s，v+t）=（SJ，VJ+t）;(3) 对所有的（s，v）∈ T（S，C）和a ∈ T，f（δ（（s，v），a））= δJ（f（s，v），a）.由于态射复合的定义符合预期，因此可以直接检查DTA是否确实是一个范畴。态射的一个重要性质是它们保留了由时间状态识别的语言。这直接由命题4.5和下面的结果得出。命题5.1设f：M −→ M J是一个态射。 则（s，v）<$f（s，v）。就我们的目的而言，DTA范畴的主要特征是它拥有一个几乎是但不完全是最终的对象。直觉上，所有时间语言的集合可以被赋予一个时间自动机结构。定义时间自动机L=（SL，CL，oL，δL）如下：•SL是所有时间语言的集合;• CL是具有单个时钟c的集合;• oL（L）= 1当且仅当n∈L;326R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315• δL（（L，v），a）=（Dv（c）·a（L），0）.R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315327LLL∼时钟c在每次转换时重置，我们使用该时钟来决定转换之间经过了多少时间。我们可以检验LL（K，0）=K，即L中的定时状态（K，0）所识别的定时语言就是K本身。更一般地，我们有LL（K，v）=Dv （ c ）（K）。给定任何时间自动机M，存在从M到的自然态射，该自然态射将M的每个时间状态映射到M中的该时间状态所识别的时间语言。对于任何确定性时间自动机M，定义态射f F：M−→ L，取f F（s，v）=（LM（s，v），0）。 虽然这态射fF不是M到的唯一态射，所有其他态射都是密切相关。命题5.2对任意态射g：M−→ L，如果g（s，v）=（K，vJ），则f F（s，v）=（DvJ（c）（K），0）.这种几乎无穷性导致了下面的语言平等的共归纳证明原则，以一种现在标准的方式[15]。定理5.3对于两个时间语言K和L，如果（K，v）<$（L，vJ），则Dv（c）（K）= DvJ（c）（L）。特别地，如果（K，0）（L，0），则K=L。换句话说，为了建立两种时间语言的平等，当被视为最终时间自动机的状态时，展示两种语言之间的互模拟就足够了。L.作为这一原则的应用，我们展示了如何使用它来建立第3节中的定时正则表达式所描述的语言的相等性。例如，考虑例3.2中的语言[aa[0，2）]]和[[aa[0，2）a[0，2）]]。下面的关系R很容易被看作是互模拟：(([[aa<$[0，2−t）]]，v），（[[(([[a<$[0，2−t）]]，v），（[（（[[0]]，v），（[[0]]，v））∈R.为了建立一个双模拟的HATR，我们可以使用第3节中定义的SYNTACTICDERIVED。例如，对于v（c）= 1，为了证明（（D1·a（[[aa[0，2）]]），0），（D1·a（[[aa[0，2）a[0，2）]]），0））∈R，我们可以检查我们有：328R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315D1·a（[[aa[0，2）]]）=[[D1，a（aa[0，2））]]=[[D 1，a（aa）[0，1）]]=[[D 1，a（a）a[0，1）]]=[[a[0，1）]]D1·a（[[a[0，2）a[0，2）]]）=[[D1，a（a[0，2）a[0，2））]]=[[D 1，a（a[0，2）a[0，1））]]=[[D 1，a（a）[0，1）a[0，1）]]=[[1[0，1）a[0，1）]]=[[a[0，1）]]。对于所有其他情况也是如此在下一节中，我们将展示当时间语言由特定类型的时间正则表达式描述时，如何6时间正则表达式的等价性证明定理5.3给出了一种证明技术，用于确定两种时间语言何时相等，即通过展示两种语言之间的互模拟在本节中，我们将展示这种证明技术可以用来证明特定类型的两个定时正则表达式是等价的，也就是说，它们表示相同的定时语言。此外，该技术是完整的，因为它可以建立任何两个等价的定时正则表达式的等价性从本质上讲，我们表明，给定任何两个等价的定时正则表达式，我们可以有效地构造一个有限的互模拟然后，和建设只需要简单的语法操作的定时正则表达式。显然，时间正则表达式的等价性包含了正则表达式本身的问题，因为每个正则表达式都是一个时间正则表达式。然而，在仅依赖于计时运算符的计时正则表达式之间存在重要的等价性。考虑例3.2中的例子。因为它们表示相同的语言，所以aa<$[0，2）和aa<$[0，2）a<$[0，2）是等价的，而两者都不等价于a主要步骤是构造互模拟的句法形式，它与时间正则表达式所表示的语言无关，而是与时间正则表达式本身有关。要做到这一点，我们需要一些定义。我们说两个R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315329⊆时间正则表达式e1和e2等于ACI属性，ACIe1=e2，如果e1和e2在语法上相等，直到结合性，交换-的幂等性和幂等性。也就是说，如果可以将以下三个重写规则应用于e1的子表达式以获得e2，则e1和e2等于ACI属性：e+（f+g）=（e+f）+g e+f=f+ee+e=e。给出了一个关系R与时间关系的表达式，从而导出了时间关系如果存在eJ1、eJ2，eA=CIeJ，eA=CIeJ，anddeJReJ.1122 1 2时间正则表达式e1和e2之间关于TR≥0的句法互模拟是时间正则表达式such的一个RR互模拟对的（1）e1R→e2;(2) ifeReJ，then（e）=（eJ）;(3) i f eReJ，则nf或所有t∈T且所有a∈T，Dt，a（e）RACIDt，a（eJ）。语法互模拟类似于互模拟，除了它是在时间正则表达式上定义的，而不是在时间语言上定义的，并且导数只需要关于R≥0的子集指定的时间。接下来的结果表明，任何两个等价的时间正则表达式（特定类型的）都是通过有限的语法互模拟来关联的，即，合成活性比模拟量R当这群人在R是有限的。 这是令人惊讶的是，因为我们可以先验地对任意正实数求导，这似乎表明我们需要无限多个在R中的元组，或对应于可能的派生。然而，这并不是我们所需要的当试图建立任何两个特定的定时正则表达式的等价性时，只考虑有限（尽管可能很大）数量的导数直观地说，对于某种定时正则表达式e，它可以查看关于有限时间增量集的导数我们的定理适用于时间正则表达式，其中每个子表达式都满足I是[a，∞）或[a，b），其中a，b∈Q≥0，也就是说，表达式中出现的每个区间都是有理有界的、左闭的和右开的。给定两个这种形式的定时正则表达式e1，e2，我们想确定是否[e1]]=[[e2]]。我们首先证明，为了建立这样一个等式，考察具有整数有界区间的表达式是足够的。直观地说，这是因为我们可以在定义函数330R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315Q（e）在定时正则表达式上，计算e中所有区间界限的公分母：让I（e）={I|是e的一个子表达式对于某个eJ}，并让Q（e）=（[p/q，∞）∈I（e）（q）（[p1/q1，p2/q2）∈I（e）q1q2）。Q（e）是自然数。给定一个自然数q，设e* q是时间正则表达式，其中e中的每个区间都乘以q：0*q= 01*q= 1a*q=a（e1e2）*q =（e1* q）（e2*q）（e1+e2）*q=（e1* q）+（e2* q）（e1）*q=（e* q）（e[a，∞））*q=e* q[qa，∞）（e[a，b））*q=e* q[qa，qb）命题6.1对于受上述限制的e1和e2定时正则表达式（e1和e2中的每个区间都是有理数有界的、左闭的和右开的），[[e1]]=[[e2]]当且仅当[[（ e1* Q（ e1））* Q（e2）]=[（e2* Q（e1））* Q（e2）]]。注意，（e1* Q（e1））* Q（e2）和（e2* Q（e1））* Q（e2）中的所有区间都是整数有界的。因此，对于具有整数界的定时正则表达式（并且每个区间都是左闭和右开的，如前所述），建立我们的结果是足够的这是本节的主要结果。首先，定义函数Θ（e）：R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315331∈∈Θ（0）= 1Θ（1）= 1Θ（a）= 1Θ（e1e2）= max（Θ（e1），Θ（e2））Θ（e1+e2）= max（Θ（e1），Θ（e2））θ（e2）= Θ（e）Θ（θeθ[a，∞））= max（Θ（e），a）Θ（θeθ[a，b））= max（Θ（e），b）定理6.2对于所有满足上述限制的时间正则表达式e1和e2（e1和e2中的每个区间都是整数有界的，左闭的，右开的），[[e1]]=[[e2]]当且仅当存在关于T（e1，e2）={0，1，2，. max（Θ（e1），Θ（e2））}在e1和e2之间。定理6.2的证明的从有限的句法互模拟出发，我们必须证明我们总是可以构造一个关于语言[e1]和[[e2]的完全互模拟。要做到这一点，我们需要以某种方式仅针对离散的导数集（即，针对T（e1，e2）中的任何时间）进行定义。如果R是一个有限系统，我们可以定义R基本如下：（L1，v）R（L2，v），如果存在TJ1，<时间d_r_g_ul表示e_J_1，e_J_2，可通过D_ t，a的重复应用获得，不T（e1，e2）满足Dtj（L1）=[[EJ1]]，Dtj（L2）=[EJ2]]和DEJ1Rej2. 因此，如果两种时间语言对应于R相关的时间正则表达式，则它们是R相关的，除非该时间正则表达式在每个单词的开头。证明的“仅当”方向更简单，并且通过构造适当的句法互模拟来进行。第一步是为每个定时正则表达式e1和e2构造一个有限状态具有状态定时正则表达式（直到ACI属性）的机器，并且其中转换s对应于D，以类似于Dt，a，对于t∈T（e1，e2）和a- 是的 这种有限状态机可以通过结构大肠粗略地说，机器通过取一个或多个导数来捕获可从e获得的定时正则表达式。对于e1和e2，给定这样的有限状态机M1和M2，结构如下。初始化eR以包含对（e1，e2），并迭代以下过程：对于R中的（e，eJ），以及通过从M1中的e和从M 2中的eJ进行所有转换而获得的对。 执行此迭代，直到没有新的对重新添加到R中。这是我们的终结，因为她的耳朵是无限的，332R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315⟨ ⟩状态对（e，eJ），其中e在M1中，eJ在M2中。在t[e1]]=[[e2]]的条件下，可以直接检查R是一个对称二进制。该过程可以容易地转化为用于判定两个时间驱动表达式是否相等的过程：c_n_struct_R_n，并且证明在R_n中的所有对（e，e_J）处，f_n（e）=f_n（e_J）。当且仅当此验证成功时，两个时间驱动程序的表达式才相等。有两个明显的未决问题仍有待解决。第一，定理6.2能推广到实有界区间吗？初步调查似乎表明情况确实如此，但细节仍有待研究。第二，定理6.2能否推广到其它类型的整数有界区间的时间正则表达式？定理6.2的证明的一个变化可以用来得到一个版本的定理，表达式e1和e2的区间有界，左开，右闭区间。这是否可以扩展到两种类型的音程混合的表达式，或者左开和右开音程的表达式还不清楚。7结论在本文中，我们已经开始了对确定性时间自动机的共归纳性质的研究，平行于Rutten [14]对经典自动机的工作。这让我们推导出一个时间语言的共归纳证明原理，它产生了一个算法来决定两个时间正则表达式（特定类型的）是否等价。 后者是令人惊讶的，因为先验地，人们需要展示的互模拟，以应用coinduction证明原则似乎是无限的。我们的工作适合Trakhtenbrot [17]提出的程序，将经典自动机理论和语言的结果提升到实时模型。我们将自己限制在研究定时正则表达式的无争议子类，该子类由使用e-I运算符扩展的正则表达式组成，该运算符限制对应于e.这种方法是否适用于第3节中描述的任何扩展形式的时间正则表达式，可以捕获由Alfrer和Dill的时间自动机识别的全部语言类，还有待观察。在时间进程代数的背景下，有相当多的工作研究时间进程的互模拟（例如，参见[18，12]）。将这项工作与本文件中的工作联系起来会很有意思。一个不同之处在于，定时过程通常不被认为是分布式的（即，·不分布在+上），而定时正则表达式是。Corradini等人的工作[8]可能与理解这种差异有关。从更广泛的角度来看，我们现在至少有三个结果的R. Pucella/Electronic Notes in Theoretical Computer Science 106（2004）315333将一种形式的正则表达式与一种形式的语言和确定性自动机联系起来，产生一种算法来建立表达式的等价性：经典正则表达式[14]，带有测试表达式的Kleene代数[7]，以及当前关于定时正则表达式的结果。我们留下一个悬而未决的问题，是否有一个一般的结果有关的正则表达式，语言和自动机，其中引用的结果可以被视为实例。致谢第6节的想法在很大程度上归功于与Hubie Chen的合作这项工作部分得到了NSF的资助CTC-0208535，ONR的资助N 00014 -02-1-0455，由ONR管理的国防部多学科大学研究计划（MURI）的资助N 00014 -01- 1-0795，以及AFOSR的资助F49620-02-1-0101。引用[1] 巴尔河和D.L. Dill，A theory of timed automata，Theoretical Computer Science 126（1994），pp.183-235[2] Asarin，E.，P. Caspi和O.Maler，A Kleene the