（计算机应用技术专业论文）基于时间自动机若干新模型的研究.pdf

基手瓣瓣耱祝蓉千薪模鼙瓣鞯窍 采缍军 摘要 时阙鑫动橇薮广泛箱子实露系统验诬蠢模黧梭溺。方露毒凌了馁多箨法 和工具；另一方面有不少基于时间自动机的坷i 同模型被提出，以适应不同类型 的系统验证。信号自动机与时间树自动机是两个新提出的模型。 嚣誊鞫褥鑫动凝璜谂还穰不完善，疆翦主要怒基于嚣誊阕秘蠡秘税谖鬟静语言 类及相必性质的研究。本文提出了一个时问树自动机识别语言的一个条件，并 证明了结论的正确性。如果一个语言不能满足该条件，它定不能被时间树自 动瓿援潮。这为证秘个其体语言不麓被跨凌瓣蠡动謇毛识溺疑供了愚路。 信号自动机为灏实时系统建立了比普通时间自动机更邂合的模型。本文 通过对信号自动机与时问自动机的模型对比与深入分丰斥，证明了两种模粼触行 为等徐关系，著撬窭了互模掇算法，这样信号熬磅辊验证涟戆被妇终为时澜自 动机验诞问题。如果把这样的互模拟算法与时间自动机验证辣法组合在一超， 就可以褥到信号自动机。验证算法，以便在此基础上开发出信号自动机验融工具。 在蘩霾工程中，形式纯方法竣瘸子预溺入工基因鼹络控麓生物基因麓络麓 行为结果。这种预测已经在生物医药研制与开发领域发挥了很大作用。目前已 有的基于有限状态自幼机的方法的局限是不能描述系统时间约束。本文提如了 基予对滴蠡囊瓠匏基鞭秘络逻辑模囊，敬诗舞拜季闻约束下控裁罄霞丽络的行为。 关键词：时问自动机时闻树自动枫信号自动枫基因网络 离散多圣乏双向穰按说裂语言 基于时问自动机若十新模型的研究朱维军 a b s t r a c t t i m e da u t o m a t ai si nt h ea p p l i c a t i o no fr e a l - t i m es y s t e ma n dm o d e lc h e c k i n g i t a p p e a r sm a n ya l g o r i t h m sa n dt o o l si np r a c t i c eo fv e r i f i c a t i o n o nt h eo t h e rh a n d ， v a r i o u sm o d e l sb a s e do nt i m e da u t o m a t ah a sb e e ns u g g e s t e ds u c ha st i m e dt r e e a u t o m a t aa n ds i g n a la u t o m a t a t h et h e o r yo ft i m e dt r e ea u t o m a t ai sf a rf r o mp e r f e c tn o w t h ec l a s s e so f l a n g u a g e sa n dt h e i rr e l a t i o n s h i ph a v e b e e n d i s c u s s e d t h ep a p e rp r o p o s e s a c o n d i t i o no ft i m e dt r e ea u t o m a t ar e c o g n i z i n gl a n g u a g e w ep r o v et h ec o r r e c t n e s so f o u rc o n c l u s i o n i fal a n g u a g ec a nn o ts a t i s f yt h ec o n d i t i o n ，i tm u s t n tb ea c c e p t e db y at i m e dt r e ea u t o m a t a i ti sap o t e n t i a lw a yt o a p p r o v i n gal a n g u a g eb e i n gan o n t i m e dt r e er e g u l a rl a n g u a g e s i g n a la u t o m a t ai sam o d e lr a t h e rf i tt h a nt i m e da u t o m a t af o rac l a s so fr e a l t i m e s y s t e m b u tn o w , i ti sn oa l g o r i t h ma v a i l a b l e t h i sp a p e rp r o v et h er e l a t i o n s h i po f b e h a v i o r e q u i v a l e n c eb e t w e e nt i m e da u t o m a t aa n ds i g n a la u t o m a t a ，t h e nw e p r o p o s e dab i s i m u l a t i o na l g o r i t h mu n d e rd i s c r e t es t e p s o ，t h eq u e s t i o no fs y s t e m v e r i f i c a t i o nb a s e do ns i g n a la u t o m a t ai sd e d u c e dt ot h es a m eq u e s t i o nb a s e do n t i m e da u t o m a t a t h e r ea r em a n ym u c hs o f t w a r ea n dt o o l sf o rt h el a r e ns o ，i th a s o p e r a b i l i t yo f s o l v i n gt h ef o r m e n i nt h ee n g i n e e r i n go fg e n en e t w o r k ，f o r m a lm e t h o di su s e df o rf o r e c a s tt h e b e h a v i o ro fc o n t r o l l i n gb i o l o g i cg e n en e t w o r kb ya r t i f i c i a lg e n en e t w o r k t h em o d e l b a s e do nf m i t es t a t ea u t o m a t ah a sf l a w ss u c ha sp o o ra b i l i t yo fd e s c r i b i n gt i m e c o n s t r a i n t i nt h i sp a p e r , w es u g g e s t sam o d e lo fg e n en e t w o r kb a s e do nt i m e d a u t o m a t a ，t h e nw eg i v e saw a yf o rc o m p u t i n gt h ep a t h w a yo f n e t w o r k k e yw o r d s ：t i m e da u t o m a t a ；t i m e dt r e ea u t o m a t a ；s i g n a la u t o m a t a ；g e n en e t w o r k r e c o g n i z i n gl a n g u a g e ；b i s i m u l a t i o nu n d e rd i s c r e t es t e p ； i l i 篁z 璺量竺譬s 郑重声明 本人的学位论文怒在导师指导下独立撰写并完成的，学位论文没有剽窃、抄 袭等违反学术道德。学术规范的侵权行为，否则，本人愿意承担由此产生的一切 法律责任和法律螽巢，特赶郑重声明。 学位途文佟者( 签名) ： 基于时删自动机若干新模型的研究 朱维车 引言 为了适应实时系统的验证需要，r a l u r 等人提出了时间自动机( t i r e e d a u t o m a t a t a ) “1 理论。直到今天，这一理论为模型检测和实时系统验证以及自 动验证工具的开发提供了重要的基础。 1 、研究背景与研究现状 时间自动机理论提出十年来，有大量研究人员的研究工作集中在这一领域 “+ ”。“。1 。“”7 “，主要表现在以下几个方面： ( 1 ) 讨论各种接受条件下时间自动机的识别能力与性质，涉及到强接受条 件，弱接受条件，b u c h i 、m u l l e r 等各种接受条件以及时间正则表达式，时间正 则语言与时间自动机的关系等等 1 - 2 , 1 6 , 2 7 , 4 2 , 6 6 】。 ( 2 ) 对基于时间自动机实时验证和模型检测的理论研究即r ”瑚f 4 5 “5 0 ，6 0 。6 3 6 8 - 7 0 1 ，3 9 i 状 6 9 、【7 0 总结了这方面的研究成果。 ( 3 ) 引入新的时钟约束和时钟操作。例如对角线时钟约束，时钟赋值等操 作。在这些新的条件下，时间自动机具有不同的性质【6 3 2 , 5 7 1 。 ( 4 ) 提出各种扩展的时间自动机模型7 1 1 1 5 。1 7 。1 9 2 8 3 0 。3 1 + 3 3 3 4 3 73 9 - 4 1 - 4 3 ， 4 4 5 9 6 训。d a n g 等人讨论了离散时间自动机；b e a u q u i e r 提出了概率时间自动机 ( p r o b a b i l i s t i ct i m e da u t o m a t a ) 雎j ；m a t e u s 等人提出了随机时间自动机( r a n d o m t i m e da u t o m a t a ) 9 。时间自动机与其它类型的自动机结合产生了新的自动机类型， 比如时间i o 自动机1 0 1 、时间树自动机1 1 1 。 ( 5 ) 开发出了基于时间自动机理论的验证工具。近年来，时问自动机在系 统验证领域取得了一系列的成功应用旧1 3 ，2 9 6 2 6 4 ，6 5 1 。目前已经开发的主要验证 工具有：c o s p a n l l2 1 ，u p p a a l 6 ，k r o n o s 2 9 6 2 , 6 5 】等等。 ( 6 ) 对时间自动机的语义解释【1 心h4 0 堋1 7 1 。这方面既有代数学基础研究， 也有双向模拟的研究。目前时间自动机比较流行的语义有时间事件和信号。 s a l v a t o r e 等人于2 0 0 3 年提出了一种新的模型时间国一树自动 j k ( t i m e d m t r e ea u t o m a t a ，t t a ) 1 h “圳。这种自动机可以被看作把时间自动机从国一 序列上扩展到了国一树上，也可以看作把0 9 一树上的自动机扩展到了时间自动机 “。s a l v a t o r e 等人的目标是引入一个新的形式化工具规范实时系统，并提供一 套健壮的理论来研究系统合成验证相关判定问题。一般来说，分支时间模型适合 基于时间自动机若干新模型的研究 朱维军 非确定性推理，它对并发程序的模型非常有用( 原子处理的非确定性重叠) 。并 且，它允许路径表达，这一点在系统合成中非常有用。“3 s a l v a t o r e 证明了简单时问计算树逻辑( s t c t i ，) 的满足性问题可以归约为 时间树自动机的判定空语言问题“，也证明了对于一个s t c t l 公式，存在一个时 间树自动机，接受该s t c t l 公式的模型”“。我们知道，t c t l 和s t c t l 可以用来 规范实时系统的待验证性质，以便检测时间自动机规范的系统行为是否满足该性 质。这样，时间树自动机作为一个形式化工具，如上所述，它和s t c t l 具有某种 意义上的等价关系，也就为规范系统性质提供了。种基于行为的选择。 时间树自动机也被用来解决时间自动机的控制合成问题“。 在普通的时间自动机模型中，所有的状态转换都是瞬时完成的，时间在状态 中流逝，在状态转换中，输入事件和时钟约束必须在转换的瞬间被满足或有效。 但是，在工业界，广泛存在着这样的实时系统，它的状态瞬时存在，时间在转换 过程中流逝，而且在转换过程中，输入事件和时钟约束必须时刻有效。也就是蜕， 输入事件维持段时间，并且时间约束一直被满足，状态才能完成转换。显然， 这样的系统存在大量的原型。在2 0 0 4 年，j e r o m e 等人提出了一种基于“分裂信 号”( s p l i t a b l es i g n a l ) 的信号自动机( s i g n a la u t o m a t a ，s a ) “，为上述 系统建立了形式化模型。他们提出了信号自动机模型后，又证明了信号自动机与 信号正则表达式的等价关系1 。 在看起来不相关的另一个学科，有一些工作将使时间自动机找到了新的应 用。研究生物细胞行为的一个基础问题是理解生物活动怎样被基因和蛋白质之间 的相互联系所控制。这样的相互联系可以由基因网络的形式来表述。一个基因网 络由一组相互作用的基因组成，它们之间的作用控制蛋白质的合成。近来，研究 人员通过设计和构造合成基因网络来理解自然生物环境中基因网络的作用”“。 这些网络通过工程化的操作来影响与基因网络交互的生物系统。这些研究的目的 是开发人工基因网络来操作并控制自然生物系统的行为“。这样的控制生物系 统的方法将在很多领域的实际应用中提供广谱的可能性“，例如生物医药。在 人工基因网络的工程中，形式模型非常有用，它使设计者在真实建立网络以前， 就可以分析、预测网络行为，判断是否能满足设计者的需求，以决定实际构建刚 2 基于时间自动机若干新模型的研究 朱维军 络的取舍，减少不必要的巨额投资。目前建立的自动机模型主要是细胞自动机 7 z 7 8 1 。2 0 0 4 年，p e t e r 提出了一一种基于有限状态自动机的基因网络模型i ，它可 以计算基因网络的行为路径，通过这种方法预测基因网络行为。 2 、研究内容和研究意义 对于时间树自动机，已经得到有关它及接受的语言类的一系列结论，但关于 一个语言不是时间树正则语言的证明，目前还没有比较好的方法。例如，我们已 经知道时间树正则语言在补运算下不封闭( 见本文第二章) ，也就是说，一个时 间树正则语言的补不一定是时间树正则语言。但是，给定一个具体的时间树正则 语言，我们怎样知道它的补是否可以被个时间树自动机识别，如果不能，怎样 证明? 对于时间自动机，p i l l i p e 提出它识别语言的一个条件。“，并用该条件定 理证明一个具体的语言不能被时间自动机识别。在这里，本文提出一个类似的条 件，它是时间树自动机识别语言的条件。我们证明了结论的正确性，我们的目标 是提供一种方法，它可以用来证明一个具体语言不能被时间树自动机识别。 对于信号自动机，如上节所述，它虽然为一类实时系统建立了更加适合的模 型，但是用于实际的系统验证和模型检测，还不可能，因为没有验证算法可用。 而时间自动机模型已经有不少成熟的验证工具。我们考虑把信号自动机验证问题 归约为时间自动机验证问题。本文的研究为这个归约做了关键性的一步：证明了 两种自动机模型在行为上的等价性，在此基础上，本文给出了互模拟算法。如果 把互模拟算法和已有的时间自动机验证算法结合起来，就得到了信号自动机的验 证算法，基于信号自动机的验证就具有了可操作性。 基于有限状态自动机的基因网络模型的局限是不能描述基因与蛋白质之间、 基因之间的时间约束关系。本文提出了基于时间自动机的基因网络模型，以描述 它们的时间约束，我们的结论是该模型可以计算它们在时间约束下的行为路径， 以分析、预测基因网络的逻辑行为。我们的目标是为基因工程设计人员提供一种 形式化工具，可算法化地判断他们的设计是否满足一些需求和性质。 3 、本文结构 本文的研究工作分为三个部分：提出时问树自动机识别语言的一个条件：证 明信号自动机与时间自动机在系统行为上的等价性，并给出它们的互模拟算法； 提出基于时问自动机的基因网络逻辑模型。 基予对瓣鑫麓祝若卡薪搂望熬磷究 朱缝军 下面的内容是这样组织的：第一章介绍时间自动机的基础性概念和主要理 论。第二肇奔绍薅闼撼蠡动褪模型，舞：提出它识别语言敕一个条俘。第三鼙分鲻 信号自动机模型，并诞明它与时间囱动机的行为等价性，给出它们之间的互模拟 算法。笫四章介绍熬于时间自动机的验证理论与工具，介绍了一个验证：卜具 k r o n o s ，莠给出了一令基于k r o n o s 貔验证实铡对e s 融e 黪议进行验涯。第 五章介绍基于有限状态自动机的基闲网络模型，并针对其不足，提出了一种基于 时间自动机的基因网络模型。第六窜提出我们下一步工作的方向。 4 纂予时间自动执着予新模型的研究朱维军 第一章时间自动机 本章我们介绍时间自动机的基础概念和主要理论。 1 1 时间语富 为了引入时间自动机，我们首先介缁些基本定义。 # 负实数簇r + 被选镦时间域。 定义1 1 一个时间序列f = q 吃是个无穷序列，熬有时间值0 科目j - t i 0 ， 。鼓满足下面的约束： 擎璃毪：f 严捂擎 | 鼍递增，氇藏麓 显露嚣有j l ，t f 定义1 2 运行在字母表妻瓣嚣闻字是一今二j 三缀( 孑，；) ，其中；= q 疗。是字 母表上的无穷字，一t 是时间序列。 定义l 3 一个上的对阕谗言是一个上的对阁字组戏躲集合 在时间字中，如果吒被解释为一个鬻件的发生，则t 就代表呱发生的时间。 这里，单调性保证时间向前推进，而进展性保证不允许无穷多的事件发生在一个 有限兹嚣藤歉瘫。 例1 1 设字母袋= ，b ，意义一个时间语言厶，它由这样的时间字组成： 时间单元为5 6 以后，没有任秘事孛 b 发生，这榉的语言 厶= 晒；舯( ( t 5 6 ) 斗( 吼= 口) 语言理论中的运算如交、并、补等也可用于时间语言上，并且，我们定义一 释裁豹搡 睾黪兔 薅润运棼，宅丢弃了鞠应符号戆瓣润毽，考虑辩瓣字f ；j 在 它的第一个成份上的投影： 定义1 4 对一个上的时间语言l 来说，它的非时问诺言： u n t i m e = 胤孑，； e 上 例1 2 对于例】1 ，l i 的非时间语言是： 三2 = u n t i m 8 ( 弓) = 孑| i i ，够，j i ，哦= ，t - 4 基于时间自动机若一f 瓤模型的研究 i 2 时间约束和时钟髁释 为了形式地定义时间自动机，我们需要指出时钟约求的形式。个原子约束 院较薅锌僮积辩闻鬻量。丽辩镑终束跫骚子约束静联合。 定义1 5 对时钟集x ，由时钟约束j 组成的集合西( x ) 可定义如下： 艿掣盖e 卜鬣| x q r v ( x ) 卜q 2 ) 对所有x ，y x 且v ( x ) c ，j l v ( y ) 蔓e ，少( v ( x ) ) 蔓步( y ) ) 当且仅当 ( v 并) ) 蔓少( v 力) 3 ) 对所有x x 且v ( x ) q ，f r ( v ( x ) ) = o 当且仅当步( v x ) ) = 0 矗上斡一个辩锌区域怒等价关系兰定义下兹露镑辩释等价类。我销雳 v 夜 示v 所属于的时钟区域，每个区域可以被它所满足的时钟约束集合唯标识。例 如，考虑有两个时钟的时钟解释v ，v ( x ) = 0 5 ，v ( y ) = o 7 ， v 中每个对钟解释满 足约束( o x y t ) ，我翻可敬愆 o x y l 】采表示该区城。 例1 4 考虑一个时间转换液，它有两个时钟x ，y ，c 。= 2 ，c ，= l ，时钟区域如图1 3 掰示。我们注意到只有有限个时钟区域，也注意到对a 上的一个时镑约束6 ，如 鬃v 兰v ，那么v 满足艿，当显仅当v 满髓艿，一个时钟区域满足荸，当篮仅当 该区域内每个时钟解释满足艿。 6 个点城t ( 0 ，1 ) 】、【( 1 ，1 ) 】、f ( 1 ，0 ) 】，( ，0 ) 】、【( 2 ，1 ) l 、f ( 2 ，o ) 】， 1 4 个开放线域： o 靠1 ，) 一o 】、 o x 1 ，f ：1 】、f 1 嘲2 ，j v = o 、【1 z 2 ，尸1 】、 【o y 1 ，x _ 0 】、 o y 2 ，y = - o ，l v l ，z 固】、陟 ，f 臻 1 ，x = 2 】 8 个开放蛾；【o x 9 ”【o 秒x 1 】、 1 x 妒1 2 】、【1 铲1 x 2 ，0 9 1 】p 2 ，妒l 】、 o x 球【l l 。g 区域自动视r ( a ) 图1 4 一个时间自动机及其相廒的区域自动机 对予一个对隧爨凌提a ，它豹区域鑫动槐可竣弱_ 寒识剐萁j 时越语言 u n t f m e ( l ( a ) ) t 2 基乎时间自动机若r 新模型的研究朱维馨 定理1 1 3 “1 给定一个t b a ：“= f ，s ，岛c ，e ，1 ，存在一个舢接受 u n i m e ( l ( a ) ) 定理1 1 3 也可等价绝稻舅一种方式来描述： 如果一个时间语言l 煺时间正则语言，则u n t i m e ( l ) 是脚一正则语言 l 。7 带自动撬 区域自动机中区域数日和时钟数有指数关系，而且和时钟约柬中大量的常 滢成正比，为减少区域数目，带自动机被提出 考虑一个时闻转换表a = ( ，s ，s o c ，嚣) ，一令露镑露楚一个或燹多的对镑嚣 域的并 形式地讲，一个时钟带集合由下丽嬲语法产生； 艿：= x c 睁。l e 0 ，乏= 艿 然0 ，刘( s ，s ，鼻i 最) 和( 善，葶，拶，五，磊) 为 e 中的边。 定理1 1 5 “”给定辩阅自动枕a ，它的正觌形式识剐的疆言为l ( 矗) 。 1 6 纂于时间自动机若干新模型的研究 来缎颦 我们假设a 是正规时间自动机，硝是它的一次运行， 硝= 巫型q 奶亟灿q 2 ，其中吼s ，( g 叫，q 。哦，点丑) e 为一条转换。 我们可敬对鼹径疗定义螺魔的藿g ( 1 r ) ： 1 ) 路径中每一一个顶点q 对应阁中一个顶点f ，f n 2 ) 若： z c ，矗g 詹，i c ，_ ，n , i d t ，则存在一条软讶兰啼f ，酱x ，其中t 楚一令一菠 值一树，f 鼹个时间脚一树。 非形式地讲，一赋值脚一树可以做为自动机的输入树，输入树中靛每个结点 楚一个输入符号，每个输入符号都对应予一个输入时刻( 或者对应于裙对其父结 点的相对时间) ，这样输入树和时间树就组成一个二：元组，表示一个基于无穷树 的对阕字( 区别予基于无穷序捌愆对闼字) ，并且这嵇对闯字组成的集合就是对 闻树语言( 区别于对闯语畜) ，我们可以定义一个时闻树自动机来识剐、接受时 间树语言( 区别于时间自动机接受时间语言) 。 这里，灸籁单起见，我 | 、j 搜翔“对润辫”表示“黪越一赋蘧国一糖”；使用 “时间树语富”表示“时间x 一赋值国一树语言”；使用“时间树自动机”表示“时 阍一赋值珊一树自动机。” 宠义2 1 5 设c 是一个时钟集，时钟约策集西( c ) 包耩 x y + c ，x y + c ，x c ，x c ，其中vx ，y c ，月c q 若矗，最，岛垂( c ；，燹j 一5 辔( c ) ，磊 岛0 ( c ) 基于时间自动帆若h * 模型的研究 粜雏辩 定义2 1 6 一个时钟解释是个映射v ：c 呻r 如果v 是个时钟解释，丑是清0 时钟集，d 是个实数，则防_ o ( v + d ) 表示对每一个时钟x 矗，v ( x ) 等0 ，对每个时钟x c ，x 硅无v ( x ) v 十d 。 我们给出时间树转换农的形式定义： 定义2 。1 7 一令秘定型时期挺转换表是一令五元组么= ( ，s ，磊，a ，c ) ，其中： 是有穷字母表 s 是有穷状态集 s s 楚镑戆袄态祭 c 是有穷时钟集 是u ( s x e x s 2 。m ( c ) ) 的有限子集 定义2 。1 8 一个时闯树转换表是确定稳，如果| 睁1 ，虽对任意转换规则 ( 钆莎，墨， ，五，巧) 和( j ，盯，毹，文，爿，五，毋) a ，巧和j 。不能同时满足 ( 5 艿= f a l s e 辩任意v 筠成立) 。 一个时间树转换表( ，s ，s o ，a ，c ) 把时间树中每一个结点w e 如删( r ) 和一个 囊s 集中的状态s 、一个时钟鼷释v 组成麓二元缓对慰起寒，著虽遴过转换规则 ( s ，s i ，s k ，五，磊，艿) a ，或者通过时闯流逝，这个二二元组的德发生改变。 定义2 1 9 设爿= ( ，s ，s o ，a ，c ) 是一个时阃树转换表，( r ，f ) 是一个时间树，a 在 ，f ) 上静一个运行是一个二元缝( bv ) ，英中： r ：d o m ( t 、一s v ：a o m ( o - 砖 r ( s ) 童s 。且v ( s ) = ，其中对穰崽x c ，v 。( x ) = 0 vw d o m ( t ) ，k = d e g ( w ) ，如果v ( w ) 十r ( w ) 满足5 ，有 ( r ( 宵) ，t ( w ) ，r ( w 1 ) ，r ( w k ) ，墨，磊，艿) 虽v ( w i ) = 磊一0 ( v ( w ) + f ( w ) ) ，i 毯n ，k 。 非形式地讲，自动机处于状态r ( w ) = s ，并在s 中时间流逊，当时间流逊为 f ( w ) = f 薅，羧入字耱t ( 妨= 玎，爱对蘩慕渍是薅镑终寐万，黉| j 鑫魂橇避入获态 2 l 基予时间自动机若干新模型的研究 朱绦攀 ( ，唯) = ( r ( w 1 ) ，r ( w k ) ) ，相应清0 时钟集为( ，五) 。显然，确定型转换 表在每个时间树 i 至多只有”一个运行。 粪议予露澜鸯动税或无穷褥鸯动瓿，麴上接受条传，我瘸藏蠢转按表褥至l 囊 幼机。 定义2 。2 0 一个非确定的b u c h i 时间树囱动机是一个六元组 a = ( ，s ，s 。，c ，f ) 其中( x ，s ，s 。，c ) 是一个菲确定时闯 树转换表。f c s 是接受状态集。一个时间树( t ，f ) 被一个g u c h i 时间树自动 爹 a 接受，当量仅当存在a 凌( t ，f ) 主黥一令运嚣r ，傻褥对r 中每一令鹣经 硝，i n ( r i 丌) n f 审 定义2 2 1 一个语言被b u c h i 时间树自动机a 接受，阁l ( a ) 表示，被定义为l ( a ) = ( t ，g - ) l ( t ，f ) 被盘接受； 懋义2 2 2 一个非确定m u l l e r 时间树自动机是一个六元组，a = ( ，s ，s 。， c ，f ) 萁中( 美，s ，& ，e ) 是一个j 确定对间树转换表， t 篓2 。是接受状 态集族。一个时间树( t ，f ) 被一个m u l l e r 时间树自动机a 接受，当且仅当存 在a 在( t ，r ) 上的一个媳行r ，使得对i n ( r | 石) f 对r 上任意玎均成立。 定义2 。2 3 一个语言被m u l l e r 辩阕树彝动掇a 接受，攒l ( 矗) 表示，定义为l ( a ) = f ( t ，r ) i ( t ，f ) 被a 接受 这样，我们得到时间树自动机的四种范型：非确定型b u c h i 时间树自动机 ( t b t a ) ， # 确定型m u l l e r 辩霾薅是动枫( t m t a ) ，确定篓b u c h i 时越瓣鑫动辊 ( d t b t a ) ，确定型m u l l e r 时间树自动机( d t m t a ) ，圈种范型的自动机识别的语 爵类也可以分别用t b t a ，t m t a ，d t b t a ，d t m t a 来表示。 2 。3 时阉褥自动规戆嚣域梅造 和时间自幼机的区域问题构造一样，时间树自动枫的区域构造也使用同样的 蹶域等价关系。( 见第一章。) 一个簿镑区域是跨锌鳃释懿等徐类，对于一个簿镑送域o f ，球鹣时藩螽继g t 魁这样的：对所有v 口，存在一个n 6 m ，使得v + r l 曩群 定义2 。2 4 设舾( ，s ，s 。，c ) 是个时间树转换表，相应的区域自动枫 鐾乎时阐自动机若干辫模型的研究朱维举 r ( a ) 是一个转换表： 状态集r ( s ) = ( s ，搿) ；s e s ，l 搿是a 的一个时钟区域) 齐始羧态集r ( ) = ( s o ，) s 。爨禹，显露搿。杰簇有x e ，v ( x ) = 一条转换规则具有形式。 如a ) ，o - ，( s t ，嘎) ，( & ，嚷) e r ( a ) ，当且仅当( ，1 7 ， ，与，丑，回， 糕掰具有时间后继t 2 ，d 满足每，对所有i ( 1 ，- - m ) k ，口。= 五一o 】盘t 。 区域自动机是时间树自动机接受语言的非时间语言的树自动机的转换表。“” 瓮蓬2 。1 “。懿柒t 是一个时闽褥语言( t m t a 或t b t a ) ，郑么u n t i m e ( 善) 是令 树语言( m t a 戏b t a ) 定理2 。2 “设t 是一个树语言，那么 ( t ，f ) | t e t ( d ) t b t a ，当毽缓当