首页/论文/cs/9906007

arXiv cs/99060071999-06-04cs.LOcs.CC

MSO可定义串变换和双向有限状态变换器

MSO definable string transductions and two-way finite state transducers

Joost Engelfriet, Hendrik Jan Hoogeboom

备注：: 63 pages, LaTeX2e. Extended abstract presented at 26-th ICALP, 1999

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

在一元二阶（mso）逻辑中可定义的串转换（不使用参数）正是那些由确定性双向有限状态转换器实现的转换。非确定性mso可定义的串转换（即，可使用参数定义的那些）对应于具有有限访问特性的两个非确定性双向有限状态换能器的组合。mso可定义的串转换的两个家族都用Hennie机来表征，即，允许重写其输入带的具有有限访问特性的双向有限状态转换器。

英文摘要：

String transductions that are definable in monadic second-order (mso) logic (without the use of parameters) are exactly those realized by deterministic two-way finite state transducers. Nondeterministic mso definable string transductions (i.e., those definable with the use of parameters) correspond to compositions of two nondeterministic two-way finite state transducers that have the finite visit property. Both families of mso definable string transductions are characterized in terms of Hennie machines, i.e., two-way finite state transducers with the finite visit property that are allowed to rewrite their input tape.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

MSO 转换的范畴

The category of MSO transductions

本文研究 MSO 转换构成的范畴，并证明可识别性、树分解等语言理论概念可仅借助 MSO 转换及其复合进行抽象定义。

2023-05-29cs.LO

在字符串上学习MSO可定义的假设

Learning MSO-definable hypotheses on string

RWTH Aachen University（亚琛工业大学）

本文研究了一元二阶逻辑MSO公式所指定的假设条件下字符串数据的分类问题。目标是设计学习算法，使其在训练集大小的时间多项式中运行，与整个数据集的大小无关或至少是次线性的。我们证明了消极和积极的结果。如果数据集是一个未处理的字符串，我们的算法有本地访问，那么学习在次线性时间是不可能的，即使是在一个小片段的一阶逻辑定义的假设。如果我们允许对字符串数据进行线性时间预处理以构建索引数据结构，则MSO可定义的假设的学习可以在训练集的大小的时间多项式中进行，而与整个数据集的大小无关。

2017-08-27cs.LGcs.LO

MSO +U逻辑的组合性

Compositionality of the MSO+U Logic

我们证明了MSO+U逻辑在以下意义上是合成的：MSO+U公式在树T中是否成立仅取决于T的根和T的直接从根下面开始的子树的MSO+ U可定义性质。另一种复合性如下：每个MSO+U公式，其所有自由变量的范围仅在有限的节点集上（特别是，其所有自由变量都是一阶的），可以重写为MSO公式，该MSO公式可以访问由MSO+U语句（没有自由变量）定义的子树的属性。

2020-05-05cs.LO

CMSO-transducing树状图分解

CMSO-transductions for tree-like graph decompositions

本文提出CMSO-transductions，实现图的模分解、分裂分解和双连接分解，改进了Courcelle的结果，展示了C₂MSO-transductions在弱部分集系统和弱双部分系统中的应用。

2026-11-02cs.CCcs.DMcs.FL

确定性MSO树变换器的等价性问题是可判定的

The Equivalence Problem for Deterministic MSO Tree Transducers is Decidable

对于确定性的MSO可定义的图到字符串或图到树转换器，它们在上下文无关的图集合上是否等价是可判定的。

2005-06-06cs.LO

高维自动机的逻辑与语言

Logic and Languages of Higher-Dimensional Automata

本文从逻辑角度研究有限高维自动机，证明其语言与MSO可定义的有限有界宽度带接口区间偏序集在序扩张下相互对应，并由此得出该类集合的序扩张仍保持MSO可定义性。

2024-03-28cs.FLcs.LO

更多相关论文收起更多论文

MSO的基数关系展开

Expansions of MSO by cardinality relations

研究了（N，<）的弱一元二阶理论的基数关系的扩展，即谓词R（X1，. Xn），其真值仅取决于集合X1，...，Xn.本文首先给出了（N，<）中基数关系可定义性的一个（可定义的）判据，并利用它证明了：对于任何在（N，<）中不可定义的基数关系R，都存在一个在（N，<，R）中可定义而在（N，<）中不可定义的一元基数关系。这些结果类似于Presburger算术的Muchnik和Michaux-Villemaire定理。证明了对于在（N，<，R）中不可定义的势关系R，+和x在（N，<，R）中可定义。这意味着（N，<，R）的WMSO理论的不可判定性。我们还考虑了有限序类的相关可满足性问题，即语言{<，R}中的MSO语句是否允许有限模型M，其中<被解释为线性序，R作为某些（固定）基数关系对M的定义域的限制。我们证明了这个问题是不可判定的任何基数关系R，这是不可定义的（N，<）。

2013-12-04cs.LOmath.LO

有限空间中序不变MSO强于计数MSO

Order-Invariant MSO is Stronger than Counting MSO in the Finite

我们比较了一元二阶逻辑（MSO）的两个扩展在有限结构类上的表现力。第一个是计数一元二阶逻辑（CMSO），它用一阶模计数量词扩展了MSO，允许表达像“结构中元素的数量是偶数”这样的查询。第二个扩展允许使用一个额外的二进制谓词，不包含在查询结构的签名中，必须解释为在其宇宙中的任意线性顺序，获得顺序不变的MSO。虽然每一个CMSO公式都可以直接转化为一个等价的阶不变MSO公式，但其逆命题尚未解决。Courcelle证明了对于有限类的结构，序不变的MSO和CMSO都具有同样的表达能力，但他强调，一般来说，序不变的MSO比CMSO更强。我们肯定了这一猜想，提出了一类结构，是顺序不变的定义在MSO，但不能定义在CMSO。

2008-03-20cs.LO

单调第二阶逻辑可定义图的上下文无关集的特征化

Characterizations of Monadic Second Order Definable Context-Free Sets of Graphs

Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG（格勒诺布尔阿尔卑斯大学、法国国家科学研究中心、格勒诺布尔理工学院、VERIMAG）；Institute of Logic and Computation, Technische Universität Wien（维也纳工业大学逻辑与计算研究所）

本文特征化了由单调第二阶逻辑和上下文无关文法定义的图集，通过树宽、可解析性及树转换等方法证明其等价性。

2026-03-09cs.FLcs.LO

优化树分解中的 MSO

Optimizing tree decompositions in MSO

本文证明树分解优化问题可在 MSO 转导中解决，并实现线性固定参数时间，推广了 Bodlaender 和 Kloks 的经典算法。

2022-02-02cs.DMcs.DScs.LO

具有多项式大小输出的字符串到字符串解释

String-to-String Interpretations with Polynomial-Size Output

串到串的MSO解释类似于Courcelle的MSO转换，除了单个输出位置可以使用输入位置的元组而不是单个输入位置来表示。特别地，输出长度是输入长度的多项式，与具有线性长度的输出的MSO转换相反。我们表明，弦到弦的MSO解释正是多正则函数。后一类具有各种特征，其中之一是它由卵石换能器识别的弦到弦函数组成。我们的主要结果暗示了一个令人惊讶的事实，即弦到弦的MSO解释在组合下是封闭的。

2019-05-30cs.FLcs.LO

无限状态系统的综合

Synthesis of Infinite State Systems

Tel Aviv University（特拉维夫大学）

本文系统研究了无限状态系统的综合问题，核心方法是将问题归约为MSO可定义奇偶博弈的综合，主要贡献是找到了这类博弈的MSO可定义均匀无记忆获胜策略。

2026-10-19cs.LO

公平顶点问题参数化于聚类顶点删除

Fair Vertex Problems Parameterized by Cluster Vertex Deletion

University of Warsaw（华沙大学）

本文研究了参数化于聚类顶点删除数的公平MSO_1可定义问题，证明此类问题在一般情况下无法在FPT时间内解决，但给出了在特定条件下可被解决的充分条件。

2026-04-24cs.CCcs.DScs.LO

无限词的确定正则函数

Deterministic regular functions of infinite words

无限词的正则函数是由具有无限前视的确定性双向换能器实现的（部分）函数。Equipments，Escheriche et.等人已经表明，它们对应于由确定性Muller流弦换能器实现的功能，以及由MSO-转换定义的功能。然而，常规功能是不可计算的一般（图灵可计算性的经典扩展到无限输入），我们认为在本文中的类确定性正则函数的无限的话，实现了确定性的双向换能器没有前瞻性。我们证明，这是一个良好的行为类的功能：他们是可计算的，封闭的组合，其特征在于由保护片段的MSO-transductions，由确定性的Büchi流串换能器，由确定性的双向换能器有限的前瞻性，并通过有限的组合物的顺序功能和一个固定的基本功能称为映射复制反向。

2023-02-13cs.FLcs.LO

有理转换的逻辑与代数刻画

Logical and Algebraic Characterizations of Rational Transductions

本文将有界非周期语言的可判定性提升至有理转换，证明可判定给定同余类中的转换，并建立逻辑-代数等价传递，从而判定一阶可定义性，且该问题为PSPACE完全。

2019-12-18cs.FLcs.LO

压缩词上的排名 MSO 枚举

Ranked MSO-enumeration over compressed words

Universität Siegen（锡根大学）

本文研究在文法压缩字符串上，固定 MSO 查询的排名查询枚举问题，实现了线性预处理和常数延迟，并推广了 polyregular 函数的符号枚举结果。

2026-06-02cs.DBcs.DScs.LO

从双向到单向有限状态传感器

From Two-Way to One-Way Finite State Transducers

任何双向有限状态自动机都等价于某个单向有限状态自动机。这个著名的结果，由Rabin和Scott以及Shepherdson独立证明，指出双向有限状态自动机（甚至是非确定性的）表征了正则语言的类。我们也知道这个结果并不适用于有限弦转换：（确定性的）双向有限状态转换器严格地扩展了（功能性的）单向转换器的表达能力。特别是确定性的双向传感器捕捉正是类的有限字符串的MSO转导。在本文中，我们解决以下定义性问题：给定一个功能定义的双向有限状态转换器，它是可定义的单向有限状态转换器？通过扩展拉宾和斯科特的证明转导，我们表明，这个问题是可判定的。我们的程序建立一个单向换能器，这是等效的双向换能器，只要一个存在。

2013-04-26cs.FLcs.LO

有限结构的非齐次化类

Non-Homogenizable Classes of Finite Structures

均匀化是驯服一类有限结构的强大方法，在不同领域有几个有趣的应用，从组合学中的Ramsey理论到计算机科学中的约束满足问题（CSP），通过（有限）模型理论。一类有限结构允许均匀化的几个充分条件是已知的，这里我们提供一个必要条件。这让我们证明某些自然类是不可齐化的：1）二元域或任何有限阿贝尔群上的局部相容线性方程组类，以及2）禁止来自树宽为2的特定MSO可定义结构类的同态的有限结构类。结合已知的结果，第一个例子表明，到PP-可解释性，CSP是可解的局部一致性方法的区别于其余的事实，他们的类的局部一致的实例是同质化的。第二个例子表明，对于MSO可定义的禁止模式类，树宽1与2是均匀性的分界线。

2019-06-04cs.LOmath.COmath.LO

双向词转换器的一向可定义性

One-way definability of two-way word transducers

本文针对双向词转换器是否可由单向转换器实现的问题，提出一种双指数空间复杂度的新算法，并在扫描转换器情形下将复杂度降低一个指数，同时给出最优构造。

2018-12-06cs.FLcs.LO

飞行自动机、模型检验与可识别性

Fly-automata, model-checking and recognizability

可识别性定理指出，如果一组有限图可由一元二阶（Monadic Second Order，MSO）语句定义，则它相对于图代数是可识别的，而图宽度的定义是基于图代数的。可识别性是一个代数概念，用同余来定义，也可以用有限自动机来描述所考虑的图。该定理要求MSO图属性的验证，或者等价地，有限二元关系结构上的MSO逻辑的模型检验问题，对于由表示属性的公式和输入图或结构的树宽度（或树宽度）组成的参数是固定参数可处理的（FPT）。相应的算法可以通过飞行自动机来实现，其转换是在飞行中计算的，而不是列表。我们回顾了两个版本的可识别性，我们目前的苍蝇自动机的例子表明，他们也可以计算值附加到图。我们表明，飞自动机与无限的状态集产生一个简单的证明强版本的可识别性定理。这个证明以前没有发表过。

2014-09-18cs.LO

树自动机/转换器的多项式增长结构及MSO集合查询

The structure of polynomial growth for tree automata/transducers and MSO set queries

Universität Bremen（不来梅大学）；Aix-Marseille University（艾克斯-马赛大学）；CNRS（法国国家科学研究中心）

本文研究了树自动机/转换器的多项式增长结构及MSO集合查询，提出了多项式增长度数的决策方法，并探讨了相关树到树函数的增长率和子类成员问题。

2026-01-06cs.FLcs.LO

类型化 λ-演算中的隐式自动机 II：流式转换器与范畴语义学的对比

Implicit automata in typed $λ$-calculi II: streaming transducers vs categorical semantics

本文将正则字符串转换刻画为带加法算子的线性 λ-演算程序，通过编码无复制流式字符串转换器并利用范畴语义学建立等价关系，进而将结果推广至树结构并揭示其与线性逻辑的联系。

2021-08-25cs.FLcs.LO

流串传感器与HDT0L系统

On Streaming String Transducers and HDT0L Systems

R.在2010年，P.Cerny和P.Cerny提出了一个单向确定性自动机模型来定义有限字符串的转换。无拷贝SST用一组寄存器扩展确定性有限状态自动机，在其中存储中间输出串，并且这些寄存器可以以线性方式沿着运行进行组合和更新，即，在转换时不能复制寄存器内容。众所周知，无拷贝SST精确地捕获了由B. Courcelle和确定性双向换能器的表达相同。它们具有良好的算法特性。最值得注意的是，它们有可判定的等价问题（在PSpace中）。在本文中，我们表明，他们仍然有可判定的等价问题，即使没有复制的限制。证明减少到HDT0L序列等价问题，这是已知的可判定的。我们还表明，后者的问题是困难的SST等价问题，模线性时间减少。

2014-12-01cs.FLcs.LO