网址：http://www.elsevier.nl/locate/entcs/volume51.html7页一元二阶逻辑及其片断贾科莫·伦齐1;2波尔多第一大学信息研究学院33405 Talence Cedex，法国摘要给出了关于一元二阶逻辑及其片断的各种最新结果。这些结果是在欧盟德涅斯特河沿岸摩尔多瓦共和国项目GETGRATS的框架内取得的。1引言：一元二阶逻辑在这份报告中，我们感兴趣的是一元二阶逻辑（MSOL）及其片段。回想一下，MSOL是一阶逻辑加上集合上的变量和量化器。在这个介绍中，我们激发了我们对这个主题的兴趣。它是现在普遍接受的逻辑可以是有用的，在验证正确性计算机系统（无论是硬件或软件）的属性。在系统验证的逻辑方法中，系统被建模为一个转换系统，即一组状态加上一组改变系统状态的动作。然后，正确性的性质表示在某种逻辑语言，使检查系统的正确性减少到验证模型和公式之间的满足关系。通常，该过程可以自动化（至少部分自动化），从而降低出错的风险现在，MSOL是有趣的系统验证，因为它包含了许多逻辑目前在计算机科学领域中使用的系统验证（无论是硬件还是软件），例如：模态逻辑，时态逻辑，μ {演算，树自动机等。MSOL的另一个重要方面是描述性复杂性。这最后一个概念是由Fagin在70年代提出的，是一种解决计算复杂性基本问题的方法;而普通的计算复杂性是一种复杂性问题。1 这项研究得到了欧洲委员会TMR网络GETGRATS（图形转换系统的一般理论）和意大利CNR的部分支持。2 电子邮件地址：lenzi@labri.u-bordeaux.frc 2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2复杂性研究解决问题所需的资源量，如时间或空间，描述性复杂性侧重于逻辑系统中问题的可表达性。本文讨论了一元二阶逻辑及其片断的可表示性。事实上，根据标准的塔斯基语义学，每个逻辑公式都定义了一组结构，所以人们可以问哪一类结构是由哪种逻辑公式定义的。在接下来的部分中，我们将概述GETGRATS项目中本主题所获得的一些结果。我们注意到MSOL是完整二阶逻辑的一元片段（也就是说，二阶量化器在集合上而不是在任何nite arity的关系上的片段）。然而，由于在本文中，我们只对一元二阶公式感兴趣，有时我们可能会在谈论二阶公式时省略“一元”一词2逻辑结构在接下来的几节中，我们将讨论一些逻辑。这些逻辑总是在变迁系统上被解释，变迁系统由一组状态给出，这些状态具有一个或多个二元关系，并且具有称为系统根的特殊状态。系统也可以用一些一元谓词来丰富（由系统的状态集来解释图的定义类似于转移系统，但它们只允许有一个关系。在过渡系统中，我们有n{ary}树。对任意正整数n，设Tn是由完全n叉树给出的转移系，f1; ：;ng，用关系r; ：; r givenby：xry当且仅当1n i如果y = Xi。33与2这是与波尔多大学的大卫·雅宁的合作回想一下，对于每个整数n，（一元）n是MSOL的所有公式的集合，其中存在二阶量化器和通用二阶量化器之间有n个交替，从存在一个开始。n也是这样定义的，但n中的公式必须以一个普适的二阶量子开始。我们考虑的逻辑MSOL解释超过T2;这种逻辑是已知的名称S2S（二阶理论的两个继任者）。著名的拉宾定理说：定理3.1[15]S2 S是可判定的;S 2 S崩溃到3。3nnn第二个结果告诉我们，在T2上，n层次崩溃;这个事实应该与[14]的结果形成对比，[14]说，n层次在任意转移系统上是nite的（即使在nite图上）。文[6]证明了Rabin的第二个结果是最优的，即：定理3.2在T2上，S2 S不坍缩为2;同样在T2上，S2S甚至不会坍缩为2的布尔组合。当然，第二个更强有力的结果是通过建立在第一。4关于μ演算及其层次问题回想一下，在[10]中引入的模态μ演算（C）是模态逻辑加上最小xpoint运算符和最大xpoint运算符。 直觉，至少 xpoints表示某些计算的终止，xpoints表示非终止。 最不 单调函数幂集上的F总是存在的（根据Tarski的经典定理[16]），并表示为X：F（X），其中X是x点变量;对偶地，最大F的x点总是存在，并表示为X：F（X）。像模态逻辑一样，μ演算在转换系统上解释注意，在任何树型结构Tn上，模态逻辑中与每个关系ri相关联的盒算子和菱形算子重合，我们用ri简单地表示它们。也就是说，如果是一个mu{演算公式，ri表示在当前节点的第i在C中，可以定义一个由最大x点和最小x点之间的交替数给出的层次结构，从最大的x点开始。是以同样的方式定义的，但公式必须以最小xpoint。mu{演算的xpoint交替层次是否在nite中已经开放了十年。从1996年开始，取得了以下一系列成果：定理4.1 [4]hierarchy is in nite（on transition systems）.然而，本文没有给出“硬”公式的显式例子。第二个成果是：定理4.2（见博士论文[11]）设a = r1，b = r2，c = r3. 在T3上的模态μ {演算中有一个明确的公式，它需要三个交替的x点，即：=X：（P^ I（ cJ（ cX）;其中：4nnnP是一元谓词;I（）意味着在字母a; b上有一条不规则路径，它包含了不规则的许多节点，形式上：I（）= Y：Z：（（^（aZ_ bZ））_ aY_ bY）;并且对偶地，J（）意味着沿着a; b上的所有路径，只有 非常多;形式上：J（）=Y： Z：（（_（aZ^ bZ））^ aY^ bY）：对于每个n，考虑在T n上没有否定的mu{演算。在这个逻辑中有一个公式n，它需要n个交替;n，连同它的“对偶”公式n，归纳地被定义为：0（P）=0（P）= P;n+1（P）=Xn：（P^n（rnXn））;n+1（P）=Xn：（P_n（rnXn））.在GETGRATS的框架下，第一个结果已在期刊版本[13]最后，关于层次问题的一个完全令人满意的结果是：定理4.3 [2]对任意n，存在μ-演算公式W n，它对于二叉树（用任意有限字母表修饰）的度量空间中的压缩约简是完备的。直觉上，Wn表示在一个合适的博弈中，一个参与者的获胜策略的存在从上面的结果，层次结构的本质（上T2）后接一个对角线参数。同样，Arnold也证明了上面的序列n是很难的。n2（再次w.r.t.）收缩）;由于n仅用两个xpoint变量，这证明了只剩下两个变量的层次结构晚上见。52对Buchi自动机在二叉树上，可以认为Buchi自动机，由Bu提出的一种自动机[5]中的方法研究了可判定性问题。这些自动机由下式给出：状态的集合Q;夜场字母;一组规则q！q1; q2，其中是字母， q; q1; q2是状态;初始状态的集合Q 0;A组接受状态。5nBuC/H自动机在二叉树上工作，其中N个节点用的元素装饰。设tbesuch是一棵树，即一个来自f1;2g的函数 到. 自动机的一次运行是从f1;2g开始的函数r 对Q，则根状态是初始的，并且对于每个w2f1;2 g，四元组r（w）;t（w）;r（w1）;r（w2）匹配自动机的某个规则。如果沿着每一条路径都有一个接受状态的集合，那么运行就是接受。ABuchi自动机对一棵树进行接收运算时，它将其重新组合，如果它是该自动机识别的所有树的集合，则该自动机定义一个装饰二叉树集合。在[12]中，我们有以下内容：定理5.1二叉树的一个装饰集可由一个BuX自动机当且仅当它可由2级公式定义 的S 2 S，提供了一个不把前x排序的语法后一个逻辑（相反，拉宾的原始定义的S 2 S）。在文献[8]中，我们把这个结果推广到了所有的树。 然而，必须指出的是，该扩展已经在论文[7]中使用，下一节将对此进行更多说明。6关于互模拟不变量n这是一个联合工作与大卫Janin。我们说一个公式是互模拟下不变，如果，无论何时M，M0是双相似的转移系统，且M满足，则M0 也很满意。我们注意到，一些MSOL公式在互模拟下是不变的（例如，任何公式都说\在谓词P中有一个状态，可以从根”到达“），有些则不能（例如，\谓词P至少包含两个状态”）。我们从一个关于mu{calculus和MSOL之间关系的好结果开始，即：定理6.1[9]在图上，MSOL的互模拟不变片段与mu{演算一致。同样，在[7]中，我们展示了以下内容：定 理 6.2n 的 互 模 拟 不 变 片 段 与 mu{ 演 算 的 对 应 x 点 交 替 水 平 一 致（即，），如果且仅当n = 0; 1;2.必须说，n = 0的情况已经知道了，见[17]。7封闭一元1个层级这是与Andr e Arnold（波尔多）和Jerzy Marcinkowski（弗罗茨瓦夫）的联合作品。62MSOL中的封闭（一元）n层次结构已在[1]中提出用于描述复杂性。这个想法是在二阶量化器之间自由地散布一阶量化器。以这种方式获得的类似乎比普通类n更健壮。封闭的n层次是否崩溃是开放的（对于n，正如我们所说的，层次是nite by[14]）。特别地，我们考虑类封闭1，并且我们根据第一阶量化器和第二阶（必然存在的）量化器之间的交替次数对其进行分层。在论文[3]中，我们证明了以下内容：定理7.1在T2上，闭1层次在第2层坍缩。换句话说，要表达任何封闭的1公式，使用二阶量化器就足够了，然后是第一阶，然后是第二阶，然后是第一阶。此外，在T2上，闭1与1（）重合，即1在T的符号上与排序关系f1;2 g重合。证明需要引入一种新的树自动机，我们称之为\search自动机”，并刻画了二叉树上的闭18结论当然，关于MSOL及其片段的许多问题仍然是开放的。其中最有趣的，我们记得：定理6.1是否也对夜间图表？μ演算是否包含在对于一些n？模 型检验问题在于判定给定的尼特转换系统是否验证给定的μ演算公式。问题出在NP上。在P？最后一个问题可能是最有趣的;证明答案是肯定的将给系统验证带来巨大的好处;证明答案是否定的将是复杂性理论的一大步引用[1] Ajtaj，M.，R. Fagin和L.张文，一元NP的封闭性，IBM研究报告，编号RJ10092，1997。[2] Arnold，A.，深度层次结构对二叉树是严格的，RAIRO{TheoreticalInformatics and Applications33（1999），329{339.[3] Arnold，A.，G. Lenzi和J. Marcinkowski，《封闭单子1 在2001年LICS上被接受的在夜间二叉树上崩溃。7[4] 布拉德·菲尔德，J.，模态mu{演算交替层次结构是严格的，在：proc中。的CONCUR '96，计算机科学讲义1119，233{246.[5] Bu嗨，J。R.， 关于严 格 代 数 中 的 一种 判定方法，见E.Nagel编，《逻辑学、方法论与科学哲学》，1960年，第11页。[6] Janin，D.，和G. Lenzi，关于二叉树的一元逻辑的结构，在：MFCS'99的论文集，计算机科学讲义1672，第310-320页。[7] Janin，D.，和G. Lenzi，关于mu{演算层次结构的层次相对于一元层次结构的层次的表达性，在LICS2001会议上接受。[8] Janin，D.， 和G. Lenzi，Asedo r derCharacterizationofBu在任意树上的chi自动机，提交。[9] Janin，D.，和I. Walukiewicz，关于命题μ {演算相对于一元二阶逻辑的表达完备性，在：Proc. of CONCUR '96，LNCS1119（1996），263{277.[10] Kozen，D.，关于命题的结果{演算，理论计算机科学27（1983），333{354。[11] Lenzi ， G. ， \μ 演 算 和 层 次 问 题 ” ， 博 士 。 毕 业 论 文 ， Scuola NormalePizziore，比萨，1997年。[12] Lenzi，G.，一种新的Bu几何特征Chi自动机，in：pr oc. 的STACS2001，Lecture Notes in Computer Science2010（2001），467{477.[13] Lenzi，G.，Mu深度3大于2：博弈论证明，计算机科学中的数学结构11（2001），273{297。[14] Matz，O.，和W. Thomas，The monadic quanti er alternation hierarchy overnite graphs是在nite中，在Proc. of LICS '97，236{244.[15] Rabin ， M. ， 二 阶 理 论 和 自 动 机 在 nite 树 上 的 可 判 定 性 ，trans.amer.math.soc.141（1969），1{35}。[16] 塔 斯 基 ， A. ， 格 点 定 理 及 其 应 用 ， 上 海 交 通 大 学 学 报 。 数 学 5（1955），285{309.[17] Van Bentham，J.，模态对应理论”，博士学位论文论文，阿姆斯特丹大学，1976年
我的内容管理
展开
