61网址：http://www.elsevier.nl/locate/entcs/volume67.html15页树自动机层次结构的低层判定LaBRI波尔多大学DomaineUniversitaire，b^atimentA30，351coursdelaLibration33405 Talence Cedex法国igw@labri.fr摘要本文研究了nite对象上nite自动机的指标层次这个层次结构完全对应于最小和最大的交替层次结构μ演算中的xpoints它也与一元二阶逻辑中的数量层次有关开放的问题是找到一个过程，给定一个规则的树语言决定其在索引层次结构中的级别在这里，决策程序的层次结构的低级别。结果表明，这些程序具有最佳的复杂性。关键词：nite自动机，quanti er hierarchy，μ演算，XPoint1引言在并发系统验证理论中，运行于夜间的有限状态自动机是一个基本模型。这个模型明显地提出的一个复杂性度量是状态的数量，但是更微妙的标准是指自动机的行为，并且根据对经常发生的事件的正约束和负约束来指定。正、负条件的嵌套深度反映在自动机索引的概念中。有趣的是，指数的层次结构在一元二阶逻辑的微积分和量化层次结构中的最小和最大定点的交替层次结构中有一个对应部分。Wagner [19]早在1977年就用nite的话建立了确定性自动机的指标层次的严格性一个类似的非确定性自动机的体系结构很容易崩溃到B u的水平chi自动机。 这就是说，非确定性可以帮助减少由自动机的索引所反映的接受条件的复杂性。的2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。62在nite树上的自动机的情况是不同的。 这种自动机的力量自Rabin的开创性论文[15]以来就得到了认可。1986年证明了nite树上的确定性和非确定性自动机的严格性[9]。大约在同一时间，Muller和Schupp引入了交替树自动机[8]。层次问题的演算（或等价的交替自动机上的树的任意分支）解决了十年后，由布拉德费尔德[4]。然后，它被重新定义为二叉树的情况[5]。同时Arnold [1]基于对角论证和Banach空间给出了这个结果的一个非常漂亮的证明x点定理一旦解决了层次结构问题，下一个挑战可能是提供用于确定给定可识别语言的层次结构中的级别的算法。对于字自动机，文[20]和[11]分别给出了计算Muller自动机指标和奇偶条件的[1]对于树自动机，我们所知不多。Urbanski[18]表明，如果确定性Rabin树自动机等价于非确定性Bu，则它是可判定C你好1。 一种稍微不同的方法[12]给出了该问题的PTIME算法。Otto [13]证明了如果一个微积分公式等价于一个公式，xpoints. 这个问题就像问一个给定的交替自动机等价于一个非常有限形状的弱自动机本文给出了上述结果的统一表示，以及关于非确定交替自动机层次最低层的一些新结果。 我们将展示如何决定一个非确定性（或交替）自动机识别（0; 0）或（1; 1）级语言。我们还提供了最佳的复杂性界限的问题。Buchi自动机对应于指标层次中的水平el（0;1）。对于非确定性自动机，如何确定其（0 ; 1）水平，目前尚不清楚. 对于确定性树自动机，如何确定更高的索引级别也是未知的在本文中，我们考虑二叉树。扩展到任意度的树似乎是可能的，但超出了这篇短文的范围在下一节中，我们将介绍单词和树上的自动机。我们也-索引层次结构。在第3节中，我们给出了一个程序的概述，确定确定性字自动机的索引层次结构中的语言的水平。 然后我们就变成了不确定的树自动机。第4节中我们显示了一个EXPTIME下界的复杂性，决定一个级别的树上的不确定自动机的索引层次结构中的语言。在下一节中，我们将给出一个EXPTIME算法，用于判断交替自动机给出的语言是否在层次结构的（0;0）层上。利用对偶性，我们还得到了（1; 1）层的一个算法.在此之后，我们简要地描述了确定性自动机给出的语言是否在（0; 1）层上的过程。1 [11]中推论15所述结果的另一个证明后来出现在[6]中。63我我01n！101N2预赛自动机在夜间的话。一个在晚上的话超过一个 夜间字母表是一个函数u：N ！.通过！ 我们把所有的集合都用nite字表 示 。一个不确定的奇偶自动机！是一个tuple：A=hQ;;qI; Q！ P（Q）;：Q！Ni其中，Q是具有初始状态qI的状态的集合，Q是转换函数，并且：Q！N是秩函数。一个确定性奇偶自动机是一个非确定性自动机，使得对于每一个（q;a）2 Q，一个自动机A在一个单词u2上 运 行 ！ 可以作为一个在夜间世界秩序2Q！对每个m 2 N，有（m+1）2<$（（m）;u（m））。 这是一个很好的机会！1（（n））是even n;换句话说，nitely经常重复的最小秩是偶数。A所识别的语言L（A）是由下列单词组成的！存在一个接受运行。语言L！是可识别的，如果它是由一个非确定性奇偶自动机识别。自动机在nite树在一个alphabet上的一个全二叉树是一个函数t：f0;1g ！ . 我们为所有标记树的集合编写Trees（）。我们把w扩展为0的单词写为w0，同样地，对于w1也是如此。 我们可以把w 0看作w的左子，把w1看作w的右子。F或M2N我们写tjM 对于一个nite树，这是一个限制t的节点的深度最多为M。Trees（）上的非确定性奇偶自动机是一个元组：A=hQ;;qI; Q！ P（QQ）;：Q！Ni其中，与自动机在词上的唯一区别在于转换函数的类型。A在树t2Trees（）上的游程本身是Q {值树r：f0;1g ！ Q使得r（“）=q，并且对于eachw2f0;1g，w有ve（r（w）;a;r（w0）;r（w1））2π，其中vert（w）=a. r中的一条路径是一条连通的，如果沿着该路径出现的最小秩是偶数。更正式地说，对于路径P=pp： 2f0;1g！，这意味着limi nf（r（pp ： p））是偶数。如果一个运行的所有路径都是接受的，则该运行是接受的。树语言L（A）由A识别的Trees（）中的那些树组成，它们允许接受游程。我们称一个树语言L T正则的，如果它是由一个不确定的奇偶校验树自动机。交替自动机利用奇偶对策是最容易定义交替自动机的方法。我们先来简单介绍一下这类博弈648一个二元博弈G=hV;V0;V1; EVV;：V！ f0; ：dgi是顶点集V的划分为（V0;V1）的二部标号图. 设E（v; v 0）成立，则v 0是v的后继顶点.我们不要求V是nite，但我们要求分配给顶点的秩集是夜间，即，的范围是夜。一个来自一些vertexv02V0的剧本如下所示：第一个player0co 的值，则player1选择后继v2 在nitum中，除非其中一个参与者不能移动，否则v 1的值，依此类推。如果一个玩家不能移动他输了。如果序列（v 0）;（v1）;：满足部分条件，则夜间游戏的结果是夜间路径v 0 ; v1;v2; ：该路径对于玩家 0获胜。 V1的顶点的平面也是类似地定义的，但这次是参与人1开始。参与人0的策略是一个函数，它分配给每个顶点序列v 以V0的顶点结束asuccessorvertex （ v ） 2V1. 一 个 策 略 是 无 记 忆的i （ v ） = （ w ）wheneverv 和w 在同一个顶点结束。一个策略是赢的，它保证参与人0在任何时候遵循该策略都能赢。同样我们也为1号博弈者设计了一个策略交替树自动机是一个元组：A = hQ;Q9; Q;;q0;：Q！P（Qf0;1;“g）;i关于非确定自动机有两种不同之处。 首先，状态集合Q被划分为存在状态Q9和泛状态Q8。 其次，过渡函数具有不同的类型。 执行顶点v中的过渡（q 0; d）2 Q f0; 1;“g意味着到顶点vd 并将状态改变为q0。所以，如果d=“，则自动机停留在v中，如果d= 0，则它移动到v的左子。这个想法是，如果自动机处于存在状态q，并且在标记为a的顶点中，那么它将从n（q;a）中选择一个它将要执行的转换。 如果q是单向的，那么选择是由对手做出的，这相当于说自动机必须执行所有从q（q;a）开始的转换。用博弈形式化交替自动机A的运行和接受的概念是最简单的。给定一棵树t，我们定义接受博弈GA;t：集合V0 平面0的顶点数是f0;1 g Q9，集合V1 平面1的顶点数为f0;1 g Q8，从ea chvertex（v;q）和（q0;d）2<$（q;t（v））有到（vd;q0）的边。验收条件由下式给出 （v; q）=（q）我们说A接受一棵树ti参与人0在博弈G中有获胜策略A;t。A所识别的语言是A所接受的树的集合词上的交替自动机的定义类似，但由于每个位置只有一个后继者，因此转换函数的类型为：：Q！P（Qf0;“ g）。65Mostowski指数的层次结构。自 动 机 A 的 Mostowski 指 数 ， 其 接 受 条 件 由 给 出 是 对 （ min（（Q））;max（（Q）。我们可以不失一般性地假设min（（Q））2f0; 1g。（否则，我们可以按比例缩小秩（q）：=（q）2。因此，对于任何类型的自动机，Mostowski指数都会产生图1所示的层次结构对于非确定性（1; 1）自动机，有必要假设存在一个特殊的状态>，从该状态中接受每棵树。 对于具有其他索引的自动机，这个假设是不需要的，因为所有树的语言都可以被（0; 0）自动机接受。对于（1; 1）交替自动机也不需要这个假设，因为所有树的语言都是从一个通用状态接受的，对于这个通用状态，转移函数给出了空的移动集合（1;2k+ 1）（0;2k）（1;3）（0;2）（1; 2）（0; 1）（1; 1）（0; 0）Fig. 1. Mostowski指数索引为（0;1）的自动机传统上称为Buchi自动机，并由A=h;Q;qI; Fi表示，其中F是秩为0的状态集（称为计数状态s）。请注意，Bu如果某个接受状态经常发生，则自动机是接受的。如果在每一层都有一个自动机不能被任何较低层的自动机模拟，则层次结构是严格的。正如在引言中提到的，层次结构对于单词上的确定性自动机[19]和nite树中的所有类型的自动机都是严格的。 相比之下，对于非确定性词自动机，层次结构折叠到（0; 1）级水平el（Buchi自动机）[1 4]，并且对于交替自动机，e ven到水平（0; 1）和（1; 2）的交叉点[2]。66nnn1n1公式中只有和是 - 关闭公式。用于nn与μ演算的在索引层次结构和-演算中的层次结构之间有着非常密切的联系。在后者中，我们通过计算最小、和最大、x点运算符之间的交替次数来衡量公式的复杂性。所以这组公式只有，2 1我们请读者参考[10，3]的层次结构的正式定义。由微积分公式定义的语言是一组树，其中公式在根中成立。我们有[3]：定理2.1二叉树语言可以由一个一式 资讯科技是索引为（1; n）的交替自动机的语言。类似地对于（0;n）1）自动机。在本文中，我们也感兴趣的非确定性树自动机的指标。这些是不同于上述定理中所提到的交替自动机的指数。对于我们在这里考虑的小水平，两者是相同的[2]。定理2.2对于任何索引（0;0），（1;1）和（0;1）：如果树语言被具有这些索引之一的交替自动机识别，那么它被具有相同索引的非确定自动机该定理对指数（1; 2）或任何更大的指数都不成立定理2.1给出了x点公式与非对称公式之间的一种联系.我们也将对模态逻辑的公式感兴趣，即，没有x点的公式这些对应于严格的树自动机。严格树自动机（英语：Strict tree automaton）是一种状态具有偏序的树自动机，并且使得从状态q到严格小于q的状态的所有可能的转换。以下简单的事实使一个理想的连接。事实2.3二叉树语言可以由模态公式定义，i它是某种严格自动机的语言。3决定词正如我们上面提到的，词上的Mostowski层次结构只适用于确定性自动机。在本节中，我们简要总结了[11]的结果，展示了如何计算给定语言的确定性索引。为了看到层次结构的严格性的例子，考虑对于每个n2N，字母表n=f1;：; n g。然后我们定义语言：M=fw2！：lim infw（n）是偶数你好！1N=fw2！：lim infw（n）是奇数你好！1所以，Mn由单词组成，其中最小的n经常出现在67是偶数，对于N n中的字，这个数是奇数。很容易看出，Mn可以由（1; n）确定自动机识别，Nn可以由（0;n1）确定自动机识别.证明这些语言没有更简单的自动机，从下面给出的更一般的引理得出 它显示了一个连接之间的Mostowski指数的！-word语言和识别该语言的确定性奇偶自动机的形状粗略地说，它说，在一个自动机识别一个“硬”语言的图中，必须有一个子图，称为“权力”，“见证”这种硬度。定义3.1设A= h; Q; q0;i是一个关于词的确定性奇偶自动机. A的图是以Q为顶点集，从q到q0加上边 当hq;a;q0i2时，对于某个字母a。图中的路是顶点v1;：;vj的序列，使得对于每个i= 1;：;j 1，图中存在从vi到vi+1图的极大强连通分支是图的顶点的极大子集，使得对于子集中的每两个顶点v1，v2，存在从v1到v2和从v2到v1的路。对于一个整数k，A中的一个k-环是A的图中的一条路径v1;：;vj，其中v1=vj，j> 1且k= minf（vi）：i=1;：;jg.注意k-循环必须至少通过一条边.给 定 整 数 m 和 n ， 状 态 q2 Q 是 A 中 的 m-n- 幂 ， 如 果 对 于 每 个k2fm， ：;n g，在A的graph中，r e是包含q的k-1个环.Mnqm+1图二、m-n-ower定义3.2我们说语言L！如果存在确定的Mostowski自动机A，使得L=L（A），并且A有m-n- owerq，其中q不是A中的无用状态（即q发生在A的某个接受游程中）.上述定义的微妙之处在于，它讨论了语言的确定性自动机的存在。直觉上，我们对语言的最小自动机感兴趣，但对于nite words上的自动机，最小性的概念并不很方便。特别是有几个不同的最小确定性自动机识别它们的语言。68L（A）树木树木L>i引理3.3（花引理）对于每个n 2 N和L！：（1）若L是（1;n +1）-不可行的，则L对某个i容许一个2 i-（2 i + n）-幂;（2）若L是（0; n）-不可行的，则L对某个i容许一个（2 i + 1）-（2 i +1 + n）-幂。先验地，我们不知道如何找到一个具有幂的确定性自动机。幸运的是，事实证明，将任何确定性自动机用于语言并以某种方式对其进行规范化就足够了。由此产生的自动机保证具有与语言所需的索引一样大的功率。这个归一化过程可以在二次时间内完成[11]。推论3.4建立具有Mostowski条件的确定性自动机A所接受的语言的索引的问题可以在时间O（jAj2）内解决。4不确定树自动机在本节中，我们将证明非确定性树自动机的层次问题是EXPTIME困难的。定理4.1对任意i 2 N.决定一个给定的非决定自动机A是否接受一个（1;i）语言的问题是EXPTIME困难的。对于（0; i）类也是如此。证据我们将简化树语言的普适性问题：给定一个非确定自动机A，决定L（A）是否接受每一棵树（即L（A）=Trees）。这个问题即使对于nite树上的自动机也是EXPTIME困难的[17]。修复语言L>i不属于层次结构的（1; i）层。这种语言的存在就像夜间的等级制度一样。对于一个给定的自动机A，构造一个自动机B，它接受一棵树，如果：左子树被A接受，右子树是任意的，或者左子树是任意的，右子树在L>i中。这在图3中示意性地示出注意B的行为我们称L（B）在（1; i）层i上L（A）=树.图三.语言L（B）如果L（A）=树那么L（B）= Trees，所以L（B）是（1; i）语言，因为它是（1; 1）语言。如果L（A）6=树木然后我们证明了L（B）不可能是（1; i）语言。假设L（B）是由一个（1; i）自动机C识别的。69我我一在62 L（A）处取一棵树。如果一个树从L（B）有t作为左子树，那么它必须有一个树从L>i在右子树。设S t是C的状态集，它从其中接受t。设Sr是可能的右状态的集合，左状态是S，即， S =fq：9（q; q）2<$（qC;a）g;这里qC是T RRa2;ql2StlrIIC的初始状态令C（Sr）表示自动机C，其中来自Sr是初始状态。直接由定义我们得到L（C（Sr））= L>i。但这是不可能的，因为C（Sr）是（1; i）自动机，而L>i不是（1; i）语言。25严格树自动机在本节中，我们将给出严格自动机的可判定性结果。 这是（0; 0）和（1; 1）级别的子级别。实际上这正是两个层次的交叉点。 对这个层次的兴趣主要是因为与模态逻辑的联系。从事实2.3我们知道，这个层次等价于模态逻辑中的可定义性。我们在下面需要的主要概念是关于给定自动机的树的类型定义5.1修复自动机A。树t的类型是从其接受t的状态的集合：类型A（t）= fq2Q：t2L（A（q））g。当自动机从上下文中清楚时，我们将省略下标我们将使用类型（A）来表示所有类型A的集合。回想一下，tjM表示t对深度至多为M的节点的限制。引理5.2对每个正则语言L：L可由严格自动机i识别re是有界M使得对每个t2L和每个t0，如果tj M=t0j M则t02L.证据 假设L被严格自动机A识别。这样的自动机可以在最多等于其大小的深度处查看树的节点。所以自动机的大小给出了M的上界。相反，假设L有一个界M。有许多树的深度为M。所以我们可以列举出所有深度为M的树，它们是L中树的前点。然后我们构造一个严格的自动机来识别所有这些前缀。2为了检验给定自动机A=hQA;A;qA; FAi是否等于严格自动机，我们在字母表B=f 0; 1g上的nite词上构造自动机BAB=hP（QA）;B;fqAg; FBi其中：（S;（a;l））=ffq：99（q; q）2*A（q;a）g：2Ty pes（A）g;和lq2S qr2lr（a; r）字母。F B=fS：L（A（S））6=;^L（A（S））6=树g70vvvw i lvuvvW1KW因此，当我们不接受来自S的状态时， S（a;l））描述了一种情况，S位于树的一个节点中，并计划只检查左子树，而假设右子树具有某种类型。对于右边的每个可能类型，转移函数给出了所有状态的集合，我们可以从这些状态中接受左边的子树，并从S中的某个状态中接受整个树。接受集F的元素是一组状态，A可以接受其中的某棵树，但不能接受其中的所有树。引理5.3 L（A）不能被严格自动机iBA识别，它接受任意长的词。证据 对于从右到左的方向，我们需要为每个界M找到两棵树t和t0，使得tjM=t0jM，但t2L（A）和t062L（A）. 考虑一个w命令w=w0; ：;wM 2L（BA）。让rw =rw（0）rw（1）：rw（M+1）e是B A在w上的可接受游程。对于w的每个子集xv，我们构造树tv而t0使得测试V被接受从r（M+1jv j）中的某个状态，并且t0不被从r（M +1j v j）。如果v =“是空的子集x，那么对于tv，我们取一棵树，国家在rw（M+1）和t0我们拿了一棵不被任何州接受的树rw（M+1）.辅助位置v=wiu，其中wi =（ai;di）. 考虑当di =l，另一种情况是对称的。 让本人bey pesuch chthatrw（i+1）=fql：9q2r（i）：9q02：（q;q0）2<$（q;a）g. 树T是一棵树，其根标记为ai，tu为左子树，类型i的树为右子树子树树T0定义类似，但不包括0作为左子树。通过对v的长度的归纳，我们可以证明， 被一些人状态在r（M+1j vj）中，并且t0不从r（M+1j v j）中的n y状态被接受。或者所需的t和t0，然后我们可以taketandt0。对于从左到右的方向，我们需要证明，如果L（A）不能被严格自动机识别，那么BA接受任意长的单词。给定M2N，我们将构造一个长度为M的词，该词可被BA识别.从引理5.2我们知道L（A）没有界。让我们以树木为例，t2L（A）和t062L（A），则tjM=t0jM。让s; ：; s作为序列在所有的节点上的L VELM在T。 我们可以把t0看作是通过把一些子树代入其中的一些节点而得到的。我们构造一个树序列如下：t0是t，ti+1是从ti通过在s i中代入在s i中计算的t0r 0的子树而获得的。由建筑tk=t0.因此，必须有一个索引i，使得ti 2 L（A）和 ti+1 62 L（A）。所以节点si中的子树的改变阻止了ti被接受。71B一我们用ti和ti+1来构造一个被BA接受的词。设u0;：：;uM是从根到si的路径。单词w0;：; wM由wj=（aj;dj）定义，其中aj是节点uj的标签，dj是到si的路径上的子的方向。可以通过归纳法证明，有一个关于w的BA的游程，它只通过接受态。2引理5.4自动机BA接受任意长的字i它接受长度>2jAj的字。证据自动机B A具有这样的性质，即它不接受来自不在F中的状态的任何东西。如果BA接受长度>2jAj的路径，则在BA的图中存在停留在从F开始的状态中的循环。这个循环可以用来产生BA接受的任意长字。2推论5.5判定一个给定的变换自动机的语言是否可由模态自动机定义的问题是EXPTIME-完全的。6（0;0）和（1;1）情况在本节中，我们将讨论层次结构的最低级别。我们表明，在这些水平的成员决定的问题是EXPTIME完全的。引理6.1如果L是（1;1）语言，则对于每个t2L，存在有界Ms. t。对于每一个tret0，其中tjM=t0jM，我们有t02L证据取一个（1; 1）自动机为L。如果这个自动机接受t，那么它只看t的nite部分。2注6.2另一个方向的含义也成立。 也就是说，如果L是正则的，并且L中的每棵树都有界，那么L是一个（1;1）语言。这是从下面的结果得出的。回想一下，类型（A）代表自动机A的类型集合。直接从定义可以得出，根的儿子的类型与根中的标签一起确定根的类型。我们写（0; 1）！这意味着如果节点被标记为B并且节点的左子和右子分别具有类型0和1，则节点具有类型。设STypes（A）是A的一组类型。 我们将使用L（S）来表示树的集合具有S中的一个类型。假设L（S）是一个（0; 0）语言。我们将描述L（S）的（0; 0）自动机的直接构造考虑自动机CS=hTypes（A）;;S;c;ci，其中c指定0到eaCh状态，并且EaC由y定义：（0;1）2c（;a） i（0;1）！观察这个自动机有一组初始状态。引理6.3如果L（S）是（0;0）语言，则L（S）=L（CS）。72Si iSSS1K证据包容是容易的。有一棵树t2L（S），只需将它的类型赋给每一个节点. 这次作业是一次C S作业. 根据定义，每一次运行的CS都是可接受的。如果包含或其他包含，则一致地假设存在树t2L（CS）nL（S）。 则t2L（CS）\L（S），其中L（S）是L（S）的补数t. 假设L（S）是一种（1; 1）语言，那么根据引理6.1，树t有一个界M. 进行接受运行r：f0;1g！C（A）的类型。 让我们;：; s是从t开始深度为M+1的所有节点设t0是一棵树，其中我们在每个节点s中替换为r（s）类型的树由C的定义可知，t0在S中有一种类型.因此t02L（S）。这是一个矛盾，因为tjM=t0jM和t2L（S）.定理6.4判定交替树自动机是否接受（0; 0）语言是EXPTIME完全问题。 对于（1; 1）语言也是如此。证据 从定理4.1可以得出下限。因此，它仍然显示上限。给定一个自动机A，设S Types（A）是包含初始状态的类型。因此，L（A）=L（S）。 构建CS就足够了 则c he ck是否L（A）=L（CS）。 根据引理6.3，等式y成立，iL（A）是（0; 0）语言。由L（ CS）的定义可知，L（A）L（ CS）始终成立.因此，如果L（CS）L（A），则仍需证明。 F或这是一个证明L（CS）\L（A）=;其中A是接受L（A）的补的自动机。由于A是一个大小为n的交替自动机，我们可以构造一个大小为O（n！）时间复杂度O（n）自动机C的大小为O（2n），接受条件为平凡（每次运行都是接受的）。 所以L（C）\L（A）=;可以在2O（nlogn）时间内完成。（1; 1）水平的情况遵循对偶性。（1; 1）语言的补语是（0; 0）语言。因此，给定一个自动机A，我们可以构造一个交替自动机A，用于检查它是否识别（0; 0）语言。A的构造可以在线性时间内完成。 27（0;1）例已知如何确定（0;1）水平（Buchile vel）仅用于确定树语言。对于这样的语言，定理4.1的下界并不成立实际上，正如我们将在这里看到的，我们可以在PTIME中决定给定的确定性自动机的语言是否在（0; 1）级别上（假设我们知道给定自动机的所有状态都是生产性的）。我们从一个非常有用的表征确定性树语言的路径在树上。树中的标记路径t：fl;rg！是整数序列0p11p22：，因此i2，pi2f0;1g，且t（p1：pi）=i（因此特别是t（“）=0）。请注意，标记路径是字母表f0;1g上的一个无尾字[We令Paths（t）表示t中所有标记路径的集合，并且，对于树语言L，73t2L0BPaths（L）= S Paths（t）。 对于单词语言K（f0; 1g[）！我们之内树语言：8 K = ft 2 T ：Paths（t）KG命题7.1下列条件对于树语言L T是等价的。(i) L是确定性可识别的。(ii) L是可识别的，并且L = 8（Paths（L））。(iii) L =8K，对于一些可识别的语言K，在nite单词中。把一个自动机A的图用nite的话来表示。我们说A的一个状态是正确可达的，如果它在一个以字母from结尾的单词上是可达的，. 我们说A允许分裂2 如果对于某个可正确到达的状态Q，0w1v有两个循环：q0 +q1+q0 q0 +q2+q0，其中w和v是一些字在（f0;1g），这样的最高排名出现在这些循环是不同的奇偶校验，和较小的两个是偶数。例如：设=fa;b g，设L是所有的nite词的集合，形式0p11p22p3：：：，i2和 pi2 f 0; 1 g，其中b很少出现。语言L可以通过具有秩（q）=（qa）= 1和（qb）= 0的状态q（初始）、qa和qb的确定性自动机来识别跃迁qqa，q！q b和q a;q b0;1！ Q. 这个机器人有一个分裂，州QA.拉宾[16]表明，树的集合，其所有路径都在L之外，即，在每条路径上，b只偶尔出现，不能被aBu识别c是自动机。这一事实可以概括如下。引理7.2路径（L）的确定性词自动机允许分裂i8 路径（L）不能由B生成自动机。因此，要决定确定性树自动机A是否接受BuC语言我们可以如下进行。首先，我们将A转换为路径（L（A））的确定性奇偶字自动机。构造是容易的，并且不增加自动机的状态的数量，但是它需要知道A的哪些状态是生产性的。一旦构造了路径（L（A））的自动机，我们通过简单地将秩增加1来获得路径（L（A））的确定性自动机。现在，很容易在多项式时间内检测到一个词自动机是否有分裂。这给出了：定理7.3如果一个确定性可识别的树语言（由一个没有不可导状态的确定性奇偶自动机表示）可以由一个Buchi自动机让我们注意到，检查自动机的状态是否是生产性的，确定性自动机和非确定性自动机一样困难。对于具有部分条件的自动机，已知该问题是NP\co-NP问题[7]。2 这个概念类似于[18]中使用的小工具。一748结论我们已经考虑了二叉树上自动机的索引层次结构的最低层。目前，对于确定性自动机，我们可以决定所有的水平，直到（0;1）。 F或不确定的交替自动机，我们可以决定（0;0）水平，（1;1）水平，和两个Wo的交集。对于任意度的树，给出这些结果也是很有趣的.对于严格的自动机，或等价于（0;0）和（1;1）水平的交，这是由Otto [13]完成的。我们猜想，这里给出的证明的一个修改应给出（0;0）和（1;1）水平的结果。引用[1] Arnold ， A.， μ 演 算 交 替 深 度 层 次 结 构 对 二 叉 树 是 严 格 的 ， RAIRO（Theoretical Informatics and Applications33（1999），pp.329{ 339.[2] 阿诺德，A. 和D. 杨文，张晓刚，等.一元线性可确定树集的点特征的确定.Nivat 和 A. Podelski ， editors ， Tree Automata and Languages ， Elsevier ，1992 pp. 159{188.[3] 阿诺德，A.和D. Niwiski，\μ演算的基础，”逻辑研究146，北荷兰，2001年。[4] 布拉德·菲尔德，J.，模态μ演算交替层次结构是严格的，理论计算机科学195（1997），pp。133{153.[5] 布 拉 德 · 菲 尔 德 ， J. ， 不 动 点 交 替 ： 算 术 、 转 换 系 统 和 二 叉 树 ，RAIRO{TheoreticalInformaticsandApplications33 （ 1999 ） ，pp.341{356.[6] 卡顿岛O.和R.Maceiras，计算奇偶自动机的rabin指数，RAIRO理论信息学和应用33（1999），pp.495{505.[7] Emerson，E.一、C. Jutla和A. Sistla，关于碎片的模型检查，- 微积分，在：CAV'93，LNCS697， 1993，pp.385{396.[8] Muller ， D. Schupp ， Alternating automata on in nite trees ， TheoreticalComputer Science54（1987），pp. 267{276.[9] Niwinski ， D. ， 在 x ed- 点 克 隆 中 ， 在 ： P roc 中 。 第 13 届 ICALP ，LNCS226，1986年，第13页。464{473.[10] Niwinski，D.，固点表征的nite状态系统的nitebehavour，理论计算机科学189（1997），pp. 1{69.[11] Niwi nski，D. 和I. 王文，张文忠，等.自动机的研究与应用.北京：科学出版社，1998.[12] Niwinski ， D.和 I.Walukiewicz ， Agappro pofdeterministict reelanguages（2002），to appear in TCS.75[13] 奥托，M.，消除μ演算中的递归，在：STACS'99，LNCS1563， 1999，pp. 531{540.[14] Park，D.，Concurrency and automata on inite sequences，in：5th GiConference on Theoretical Computer Science，LNCS104， 1981，pp.167{183.[15] Rabin，M.，二阶理论和自动机在nite树上的可判定性，trans.amer.math.soc.141（1969），pp. 1{35.[16] Rabin，M.，弱可定义关系和特殊自动机，在：Y.Bar-Hillel，编辑，集合论基础中的数理逻辑，1970页。1{23.[17] Seidl，H.，nite树自动机的判定等价性，SIAM Journal of Computing19（1990），pp. 424{437.[18] Urba“nski，T.，关于确定性语言是否存在的判定chiclass，in：ICALP'00，LNCS，2000，出现。[19] Wagner，K.， Eineto pol ogischeCharakterisierungeinigerKlassenregularerFolgenmengen，J. Inf. Process.赛博恩EIK13（1977），pp. 473{487.[20] Wilke，T.和H. Yoo，Computing the Rabin index of a regular language of innite words，Information and Computation130（1996），pp. 61{70.
我的内容管理
展开
