On Functionality of Visibly Pushdown Transducers
可见下推换能器形成下推换能器的子类，其（严格地）扩展具有堆叠的有限状态换能器。就像下推自动机一样，输入符号决定堆栈操作。在本文中，我们证明了功能是可判定的PSpace的可见下推传感器。这个证明是通过一个pumping参数完成的：如果一个有两个输出的单词有足够大的嵌套深度，那么就存在一个有两个输出的嵌套单词，其嵌套深度严格地更小。证明中运用了词组合学的技巧。作为功能的可判定性的结果，我们还表明，等价的功能明显下推换能器Exptime完成。
2010-02-07 cs.FL
Iterative pushdown automata and hyperbolic contour words
本文给出了迭代下推自动机在双曲平面上无穷多个分片中球和其它两个域的轮廓字上的应用。我们还给出了双曲三维空间的平铺{5，3，4}和双曲四维空间的平铺{5，3，3，4}的类似应用。
2009-07-28 cs.CG cs.FL
Two-Way Visibly Pushdown Automata and Transducers
自动机逻辑连接是正则语言理论的支柱。这样的连接是很难获得的换能器，但最近已经获得了重要的结果字到字的转换，表明以下三种模型是等效的：确定性双向换能器，一元二阶（MSO）换能器，和确定性单向自动机配备了有限数量的寄存器。嵌套词是具有嵌套结构的词，允许将未排名的树建模为它们的深度优先搜索线性化。在本文中，我们考虑从嵌套的单词到单词的转换，特别是允许产生未排名的树，如果输出的单词有一个嵌套结构。可见下推换能器的模型允许描述这样的变换，并且我们提出了具有双向移动的该模型的简单确定性扩展，其具有以下性质：i）它是简单的计算模型，其自然具有良好的评估复杂性; ii）它是表达性的：它包含嵌套的词到词的MSO转换器，并且使用简单的句法限制来恢复MSO转换器的精确表达; iii）它具有良好的算法/闭合特性：该模型在具有明确的单向字母到字母转换器的组合下是闭合的，该转换器在常规环视下给出闭合，并且具有可判定的等价问题。
2016-06-01 cs.FL
Edit Distance for Pushdown Automata
两个单词之间的编辑距离$w_1, w_2$是将$w_1$转换为$w_2$所需的最小单词操作数（字母插入、删除和替换）。编辑距离推广到语言$\mathcal{L}_1, \mathcal{L}_2$，其中从$\mathcal{L}_1$到$\mathcal{L}_2$的编辑距离是最小数目$k$，使得对于来自$\mathcal{L}_1$的每个单词，在$\mathcal{L}_2$中存在编辑距离最多为$k$的单词。研究了下推自动机与其子类之间的编辑距离计算问题。计算到下推自动机的编辑距离的问题是不可判定的，在实践中，有趣的问题是计算从下推自动机（实现，递归程序的标准模型）到正则语言（规范）的编辑距离。在这项工作中，我们提出了一个完整的图片的可判定性和复杂性的以下问题：（1）~决定是否，对于一个给定的阈值$k$，编辑距离从下推自动机到有限自动机是最多$k$，和（2）~决定是否编辑距离从下推自动机到有限自动机是有限的。
2017-09-22 cs.FL
Decision Problems for Deterministic Pushdown Automata on Infinite Words
本文调查了DPDA在无限词上的一些可判定性结果（Omega-DPDA）。我们总结了最近的一些结果的可判定性的正则性和等价性问题的类弱omega-DPDA。此外，我们提出了一些新的结果的奇偶指数问题的omega-DPDA。对于奇偶校验条件的规范，omega-DPDA的状态被分配优先级（自然数），并且如果在运行期间无限频繁出现的最高优先级是偶数，则运行是接受的。基本的简化问题是，是否可以确定接受给定Omega-DPDA语言所需的最小优先级数量。我们提供了一些决定性的结果，这个问题的变化，某些类别的欧米茄-DPDA。
2014-05-22 cs.FL
Higher-Order Pushdown Systems with Data
我们提出了一个新的高阶下推自动机的扩展，它允许使用一个无限的字母表。新的自动机识别语言的数据字（而不是正常的话），旁边的每个字母从一个有限的字母表有一个数据值从一个无限的字母表。这些数据值可以加载到自动机的堆栈中，稍后与输入上的一些更远的数据值进行比较。我们引入这些自动机的主要目的是它们可以帮助分析正常自动机（没有数据）。作为一个例子，我们给出了一个证明，确定性自动机的崩溃可以识别更多的语言比确定性自动机没有崩溃。这个证明比无数据的情况更简单。我们还提出了一个假设，如何新的自动机模型可以与原模型的高阶下推自动机。
2012-10-09 cs.FL
The (Nested) Word Problem
在这篇文章中，我们提供了一个新的视角，一组字的问题，使用嵌套的话的语言。这些是由Alfred和Madhusudan引入的，作为一种建模程序设计语言（如HTML）的方法。我们演示了如何嵌套的单词语言称为明显下推类可以用来研究字的问题，几乎自由的群体在一个自然的方式。
2014-10-27 cs.FL math.GR
Visibly Pushdown Languages in Groups
Technische Universität Berlin（柏林工业大学）；Heriot-Watt University（赫瑞-瓦特大学）
研究群中可见推导语言与有限生成群关联的词集，证明有限群的词问题属于VPL，自由约简不保持VPL，且在自由群中带VPL约束的方程解是不可判定的。
2026-04-24 cs.FL math.GR
Greibach Normal Form for $ω$-Algebraic Systems and Weighted Simple $ω$-Pushdown Automata
在加权自动机理论中，许多关于形式语言的经典结果被推广到定量的环境中。在这里，我们研究加权上下文无关语言的无限词，一个推广的$ω$ -上下文无关语言（科恩，黄金1977年）和扩展的加权上下文无关语言的有限词（乔姆斯基，Schützenberger 1963年）。在形式文法的理论中，这些加权上下文无关语言，或$ω$ -代数级数，可以表示为混合$ω$ -代数方程组的解和加权$ω$ -下推自动机。在我们的第一个主要结果中，我们证明了（混合）$ω$ -代数系统可以转化为Greibach范式。我们在第二个主要结果中使用Greibach范式证明了简单的$ω$ -复位下推自动机识别所有的$ω$ -代数级数。简单的$ω$ -复位自动机不使用$ε$ -转换，最多只能改变一个符号的堆栈。这些结果将上下文无关语言的基本性质推广到加权上下文无关语言。
2021-10-05 cs.FL
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
我们证明了高阶下推自动机（HOPDA）的对角问题，因此同时无界性问题，是可判定的。从最近的工作由Zetzsche这意味着，我们可以构建向下封闭的一套接受的话，一个给定的HOPDA。这也意味着我们可以构造HOPDA的Parikh像的下闭包。这两个结果在验证表示为HOPDA或安全高阶递归方案的并发高阶程序中起着重要作用。
2015-11-05 cs.FL
The theory of reachability in trace-pushdown systems
研究迹下推系统，该系统栈中存Mazurkiewicz迹，是图幺半群上价自动机特殊情况。确定一类系统可判定配置图带可达性的一阶理论，补充了相关研究成果。
2026-09-28 cs.FL
Weighted Automata and Logics for Infinite Nested Words
Nested words由Alfred和Madhusudan引入，用于捕获具有线性和层次顺序的结构，例如XML文档，而不会丢失有价值的闭包属性。此外，Büchi和Madhusudan为有限和无限嵌套词引入了自动机和等价逻辑，从而将Büchi定理扩展到嵌套词。最近，在定量系统中的权重的平均和折扣计算发现了很大的兴趣。在这里，我们将介绍和研究加权自动机模型和加权MSO逻辑无限嵌套的话。作为权重结构，我们考虑赋值幺半群，它包含权重的平均和折扣计算以及经典的半环。我们表明，在适当的假设下，两个分别。我们的加权逻辑的三个片段可以相互转换。此外，我们表明，逻辑片段具有相同的表达能力加权嵌套词自动机。
2015-06-23 cs.FL cs.LO
The No Endmarker Theorem for One-Way Probabilistic Pushdown Automata
Faculty of Engineering, University of Fukui（福井大学工学部）
本文证明单向概率下推自动机中的结束标记总是可以移除，通过概率变换以双指数栈状态复杂度为代价构造等价的无结束标记机器，且不损害错误概率，并统一涵盖确定性与非确定性模型。
2026-10-15 cs.CC cs.FL
Reachability in Trace-Pushdown Systems
本文研究以 Mazurkiewicz 迹为栈内容的下推系统，在两类自然转移条件下提出 lc-rational 关系理论，证明可达关系性质并给出多项式时间可判定结果。
2025-02-17 cs.FL
Streamability of nested word transductions
本文研究嵌套词转导的流式评估问题，证明可见下推转换器的高度有界内存可判定性，并提出一个充分条件，使内存需求随词高二次增长，涵盖所有可确定化 VPT。
2019-04-03 cs.FL
Rewriting Higher-Order Stack Trees
高阶下推系统和基树重写系统可以看作是后缀词重写系统的扩展。这两个类都生成具有有趣逻辑性质的无限图。事实上，一元二阶逻辑的模型检查问题（分别是具有可达性谓词的一阶逻辑）在这样的图上是可判定的。我们统一了这两种模式，通过引入栈树的概念，树的节点标记的高阶栈，并定义相应的类的高阶地面树重写系统。我们发现，这些图保留了地面树重写图的可判定性，同时推广了图的下推层次。
2015-02-16 cs.FL
Bidirectional Nested Weighted Automata
嵌套加权自动机（NWA）提供了一个强大的和方便的自动机理论的形式化定量规格。以前的作品认为NWA只在向前的方向处理输入的单词。允许自动机向后处理输入单词也是很自然的，例如，测量响应和前一个请求之间的最大或平均时间。因此，我们介绍和研究双向NWA，可以处理输入的话在两个方向。首先，我们表明，双向NWA可以表达有趣的定量属性，是不能只向前NWA。其次，对于空性和普遍性的基本决策问题，我们建立了新框架的可判定性和复杂性结果，这些结果与仅向前NWA的特殊情况下的最著名结果相匹配。因此，对于NWA，在没有额外的计算复杂性的情况下实现了双向性的增加的表现力。这与未加权的情况形成鲜明对比，在未加权的情况下，双向有限自动机并不比只向前的自动机更具表达力，但比只向前的自动机更简洁。
2017-06-26 cs.FL
POTL: A First-Order Complete Temporal Logic for Operator Precedence Languages
模型检验程序的问题促进了对上下文无关结构推理的时态逻辑定义的研究。其中最值得注意的是嵌套词的时态逻辑，如CaRet和NWTL。最近，基于操作符先后次序语言（OPL）类的逻辑OPTL被引入，它比嵌套字更强大。我们定义了新的基于OPL的逻辑POTL，证明了它的FO-完全性，并提供了一个模型检验过程。POTL改进了NWTL，使制定的要求，涉及前/后条件，堆栈检查，和其他的异常结构的存在。它在OPTL的基础上进行了改进，因为它是FO完备的，并且更容易表达堆栈检查和函数局部属性。
2020-10-31 cs.FL cs.LO
Nested Weighted Automata
最近，在形式化验证和综合中处理定量性质已经有了很大的努力。虽然有限和无限词上的加权自动机提供了一个自然和灵活的框架来表达定量属性，但可能令人惊讶的是，一些基本的系统属性，如平均响应时间，不能用加权自动机来表达，也不能用任何其他已知的可判定形式主义。在这项工作中，我们引入嵌套加权自动机作为一个自然的扩展加权自动机，这使得它可以表示重要的定量属性，如平均响应时间。在嵌套的加权自动机中，主自动机从加权的从自动机中分离并收集结果，每个从自动机沿着无限字的有限部分计算一个量。嵌套加权自动机可以看作是监视自动机的定量模拟，用于运行时验证。我们建立了一个几乎完整的嵌套加权自动机的基本决策问题的可判定性图片，并说明其在几个领域的适用性。特别是，嵌套加权自动机可以用来决定平均响应时间属性。
2015-04-23 cs.FL
Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words
本文研究有限与无限词上有理关系的判定问题，证明无限词上等价性不可判定，并给出自动关系可识别性的双指数判定算法，在有限词上改进为单指数时间。
2019-01-29 cs.FL
Nesting negations in FO2 over infinite words
我们考虑无限词上的二元一阶逻辑FO 2。限制嵌套否定的数量定义了一个无限的层次结构;它的级别通常被称为FO 2量词交替层次结构的半级。对于这个层次结构的每一个层次，我们给出了一个有效的表征。对于较低的水平，这个特征是一个代数和拓扑性质的组合。对于更高的层次，代数性质证明是足够的。在二元一阶逻辑中，每个代数性质都是Ω项的一个有序恒等式。拓扑性质与没有两变量限制的量词交替层次结构的下半层相同（即，Cantor拓扑和字母拓扑）。我们的结果推广了有限词的相应结果。证明使用新的技术，是基于一个完善的Mal'cev产品有序monoid。
2020-12-02 cs.FL cs.LO
Games for Active XML Revisited
本文研究了Active XML框架中内涵文档的重写机制，抽象为主动上下文无关游戏的形式。本文研究的安全重写问题是决定第一个玩家Juliet对于给定的游戏和（嵌套）单词是否有获胜策略，这对应于给定内涵文档的成功重写策略。本文探讨了几个扩展到积极的上下文无关的游戏。主要的扩展允许更多的表达模式（即XML模式和定期嵌套的单词语言）的目标和替换语言，并有效果的游戏玩嵌套的单词，而不是（平面）的话，在以前的研究。其他扩展考虑验证Web服务的输入参数，以及基于服务调用结果插入的替代语义。在一般情况下，安全重写问题的复杂性是非常棘手的（双指数时间），但该文件确定有趣的易处理的情况下。
2014-12-18 cs.DB cs.FL
On the Kanazawa--Salvati Conjecture
ZEN University（禅大学）
该研究将 Kanazawa--Salvati 猜想归结为显式组合问题，构造良嵌套多重上下文无关文法族，证明四字母类比 MIX_4 非此类语言，但原猜想仍开放。
2026-09-15 cs.FL
Extending QuAK with Nested Quantitative Automata
Institute of Science and Technology Austria (ISTA)（奥地利科学技术研究所）；Slovak University of Technology in Bratislava（布拉迪斯拉发斯洛伐克工业大学）；CISPA Helmholtz Center for Information Security（CISPA赫尔霍夫信息安全中心）；Sabancı University（萨班奇大学）
本文通过实现扁平化过程将嵌套定量自动机(NQA)转化为定量自动机(QA)，扩展了定量自动机工具包QuAK以支持NQA，从而能够处理无限值属性如平均响应时间，并保留阈值决策问题的可判定性。
2026-05-28 cs.FL cs.LO
Two-dimensional Dyck words
本文提出三种将 Dyck 语言从一维词推广到二维图片的方法：良好嵌套 Dyck、可中和 Dyck 和 Dyck 纵横字谜，并证明它们之间的严格包含关系，为定义上下文无关图片语言奠定基础。
2023-09-21 cs.FL
Polyregular Model Checking
本文提出一种面向多正则字符串转导的类 Python 高级语言，并通过归约到有限词一阶理论，实现基于 MONA、Z3 或 CVC5 的完备程序验证。
2025-05-15 cs.FL
Pointwise order of generalized Hofstadter functions G, H and beyond
IRIF Université Paris Cité, CNRS（IRIF 巴黎西岱大学 法国国家科学研究中心）；Hangzhou International Innovation Institute Beihang University（北京航空航天大学杭州国际创新学院）
本文通过引入无限形态词推广Fibonacci词，证明了广义Hofstadter函数族(F_k)满足逐点序F_k(n) ≤ F_{k+1}(n)，并利用Rocq证明助手进行了形式化验证。
2026-05-22 cs.DM cs.FL math.CO
