On the Existence of Universal Finite or Pushdown Automata
我们调查（不）-存在的通用自动机的某些类别的自动机，如有限自动机和下推自动机，特别是表示和编码功能的影响。另一种方法，使用过渡系统，也提出。
2012-07-31 cs.FL
On the determinization of event-clock input-driven pushdown automata
输入驱动下推自动机（英语：Input-driven pushdown automata），也称为可视下推自动机（visible pushdown automata）和嵌套词自动机（nested word automata），是确定下推自动机的一个子类，也是括号语言的一个超类。Nguyen和Ogawa（“Event-clock visibly pushdown automata”，SOFSEM 2009）定义了这些自动机在事件时钟模型下的时间扩展，并表明该模型可以使用区域构造的方法来确定。本文定义了一个进一步的扩展，这个模型的事件时钟的调用返回操作，并提出了一个新的，直接确定这些自动机的过程：一个$n$状态不确定自动机与$k$不同的时钟约束转换为一个确定性自动机与$2^{n^2}$状态，$2^{n^2+k}$堆栈符号和相同的时钟约束，在原来的自动机。该结构被证明是渐近最优的状态数和堆栈符号的数量。
2021-03-06 cs.FL
A Proof of the Pumping Lemma for Context-Free Languages Through Pushdown Automata
上下文无关语言的泵引理是关于下推自动机的一个结果，它与著名的正则语言的泵引理惊人地相似。然而，虽然正则语言的引理是简单地证明使用鸽子洞原则的确定性自动机，下推自动机的引理是通过一个等价的上下文无关语言和通过更强大的奥格登引理证明。本文给出了上下文无关语言的泵引理的一个证明，它依赖于下推自动机而不是上下文无关文法。
2013-07-07 cs.FL
Structural Complexity of Multi-Valued Partial Functions Computed by Nondeterministic Pushdown Automata
本文继续对CFL函数的结构性质进行了系统和全面的研究，CFL函数通常是由配备只写输出带（或下推转换器）的单向单头非确定下推自动机计算的多值部分函数，其中CFL指与上下文无关语言的相关性。CFL函数的行为往往与其相应的上下文无关语言完全不同。我们广泛地讨论了包含，分离，并通过应用布尔运算，功能组合，多-一相对化，图灵相对化从CFL功能得到的各种类别的功能之间的细化。特别是，图灵相对化有助于构建CFL函数类的层次结构。我们还分析了优化函数的计算复杂性，即寻找CFL函数的最优值，并讨论了它们与相关语言的关系。
2015-08-24 cs.CC cs.FL
Random Generation and Enumeration of Accessible Determinisitic Real-time Pushdown Automata
本文提出了一个确定性实时的【形】可达下推自动机的均匀随机生成的一般框架。提出了一个多项式时间算法，用于随机生成一个具有固定栈操作总大小的下推自动机。研究了接受条件（空栈、最终状态）对生成自动机可达性的影响。
2015-12-18 cs.FL
Visibly pushdown automata on trees: universality and u-universality
一个自动机是通用的，如果它接受每一个可能的输入。我们研究了u-普适性的概念，它断言自动机接受以u开头的所有输入。非确定树自动机的普适性和u-普适性都是EXPTIME困难的。我们提出了有效的基于反链的技术，以解决这些问题，明显下推自动机上运行的树。我们的方法之一产生算法的普遍性和u-普遍性的对冲自动机。
2012-05-13 cs.FL
Detecting Useless Transitions in Pushdown Automata
下推自动机可能包含在自动机的任何接受运行中从未使用的转换。我们提出了一个算法来检测这种无用的过渡。在下推自动机运行期间捕获可能的堆栈内容的有限自动机首先在前向过程中构造以确定哪些转换是可达的，然后在后向过程中使用以确定这些转换中的哪些可以导致最终状态。
2013-06-08 cs.FL
Serializing the Parallelism in Parallel Communicating Pushdown Automata Systems
Infosys Technologies Limited（印孚瑟斯技术有限公司）
考虑了并行通信下推自动机系统（PCPA），定义了一个称为已知通信的性质，并利用这个性质证明了PCPA的一个变种，称为返回集中式并行通信下推自动机（RCPCPA）的幂与多头下推自动机的幂是等价的.上面的结果提出了一个新的子类返回并行通信下推自动机系统（RPCPA）称为简单RPCPA，我们表明，它可以写为有限的交集的多头下推自动机系统。
2009-07-29 cs.CL cs.DC cs.FL
Adding Time to Pushdown Automata
在本教程中，我们将通过示例说明如何结合两个经典模型，即下推自动机（PDA）和时间自动机，以获得时间下推自动机（TPDA）。此外，我们描述了如何可达性问题TPDA可以减少到PDA的可达性问题。
2012-12-17 cs.FL cs.LO
A Note on Pushdown Automata Systems
In（Csuhaj-Varju et.下推自动机的并行通信系统（PCPA）被引入，并且被证明能够模拟返回模式下的不确定的单向多头下推自动机，即使通信被限制为具有单个目标组件的单向。单向多头下推自动机（Balan 2009）对这种集中式PCPA的模拟结果是不完整的（Otto 2012）。随后，它被证明，集中返回PCPA是普遍的，即使组件的数量是2（彼得森2013），因此是从单向多头下推自动机分离。另一项研究修改了PCPA的定义，使通信是异步的（Otto 2013）。虽然单向多头下推自动机的模拟仍然是可能的，现在一个逆向构造表明，在返回模式下，该模型在非常精确的意义上等价于单向多头下推自动机。它是开放的，非集中返回PCPA的程度二是普遍的。在本文的第一部分中，我们证明了这一点。然后我们将注意力转向统一分布式下推自动机系统（UDPAS）。这些自动机系统轮流在一条磁带上工作。我们表明，接受空栈的CNOAS不形成一个层次结构，取决于组件的数量和成员资格问题是NP完全的，回答两个开放的问题（阿罗约等。2012）。
2014-04-04 cs.FL
The Power of Centralized PC Systems of Pushdown Automata
在（Csuhaj-Varj{ú} et. 2000），并且在它们的集中式变体中示出能够模拟非确定性单向多头下推自动机。一个声称的返回模式的逆模拟（Balan 2009）被证明是不完整的（Otto 2012），并提出了一种语言来将这些二度（下推自动机的数量）的PCPA与非确定性单向双头下推自动机分离。我们表明，建议的语言可以接受后者的计算模型。我们提出了一个不同的例子，在一个单一的字母表确实排除了模型之间的模拟的可能性。然后，通过证明它们是通用的，解决了关于在返回模式下工作的集中式PCPA的功率的公开问题。由于构造是可能的，使用系统的程度2，这也改善了以前的边界3生成所有递归可重复的语言。最后，PCPA被限制在这样一种方式，通过多头自动机的模拟是可能的。
2012-08-13 cs.FL
Minimization of visibly pushdown automata is NP-complete
本文证明可见下推自动机最小化是NP完全的，通过引入浸入概念并证明其最小化NP完全性，再归约到原问题。
2020-02-12 cs.FL
Input-Driven Double-Head Pushdown Automata
我们介绍并研究了输入驱动的确定性和非确定性双头下推自动机。双头下推自动机是普通下推自动机的一个轻微的推广，它使用两个在公共输入带上以相反方向移动的输入头。在每一步中，移动一个头，如果头相遇，自动机决定接受。要求自动机以输入驱动的方式工作，要求每个输入符号唯一地定义下推存储上的操作（push，pop，state change）。通常，这是由输入字母表的分区建模的，称为签名。由于我们的自动机模型与两个头一起工作，要么两个头都尊重相同的签名，要么每个头都有自己的签名。这导致了两个变种的输入驱动双头下推自动机。从语言描述能力、闭包性质和决策问题等方面研究了输入驱动双头下推自动机上的诱导语言族。
2017-08-22 cs.FL
Partial Derivatives for Context-Free Languages: From $μ$-Regular Expressions to Pushdown Automata
我们将Antimirov的偏导数从正则表达式扩展到$μ$ -描述上下文无关语言的正则表达式。我们证明了偏导数的正确性以及迭代偏导数集合的有限性。后者被用来作为下推符号在我们的建设一个不确定的下推自动机，这推广了Antimirov的NFA建设。
2017-01-02 cs.FL
Deterministic pushdown automata and unary languages
从计算复杂性的角度研究了有限状态自动机对单字母表上的确定性下推自动机的模拟问题。我们表明，每个一元确定性下推自动机的大小s可以模拟一个确定性的有限自动机的状态数是指数的s。我们证明了这个模拟是紧的。此外，它的成本不能降低，即使它是由一个双向不确定自动机。我们还证明，有确定性下推自动机不能比有限自动机指数更简洁的一元语言。为了说明这一结果，我们研究了确定性下推自动机到上下文无关文法的转换。我们证明，在一元的情况下，所得到的语法中的变量的数量是严格小于在nonunary字母表的情况下所需的变量的数量。
2009-05-08 cs.FL
Unary Pushdown Automata and Straight-Line Programs
我们考虑一元字母表上的确定性下推自动机（简称udpda）的决策问题。Udpda是一种简单的计算模型，它完全接受一元正则语言，但比有限状态自动机更简洁。我们完成了udpda的复杂性景观表明，空性（从而普遍性）是P-硬，等价和压缩的成员资格问题是P-完全的，包含是coNP-完全的。我们的上限是基于一个翻译定理之间的udpda和直线程序的二进制字母表（SLP）。我们发现，任何udpda的特征序列可以表示为一对SLP-一个前缀，一个套索-具有线性的大小的udpda的大小，可以在多项式时间计算。因此，udpda上的决策问题被简化为SLP上的决策问题。相反，任何SLP都可以在对数空间中转换为udpda，这构成了我们的下界证明的基础。我们展示了SLP的有序匹配问题的CoNP-硬度，从中我们推导出包含的CoNP-硬度。此外，我们完成了一元不确定下推自动机的复杂性景观显示的普遍性问题是$Π_2 \mathrm P$硬，使用一类新的整数表达式。我们的技术有超越udpda的应用。我们表明，我们的研究结果意味着$Π_2 \mathrm P$ -完整的Presburger算法和压缩匹配问题与一个字符的通配符的coNP下界的自然片段。
2014-03-03 cs.CC cs.FL
Quantum Pushdown Automata with a Garbage Tape
人们提出了几种量子下推自动机模型，并对它们的计算能力进行了深入的研究。然而，对于一些量子下推自动机模型，量子模型是否至少与经典模型一样强大还不清楚。这是由于可逆性限制。在本文中，我们引入了一个新的量子下推自动机模型，它具有一个垃圾带。该模型利用垃圾带存储弹出符号，克服了可逆性限制。我们表明，该模型可以模拟任何量子下推自动机与经典堆栈以及任何概率下推自动机。我们还表明，我们的模型可以解决一定的承诺问题，而确定性下推自动机不能。这些结果表明，我们的模型是严格更强大的设置中的精确，单侧误差和非确定性计算比经典的同行。
2014-10-02 cs.CC cs.FL quant-ph
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
我们研究了一个扩展了模块和分数时钟约束的时间下推自动机的表达模型。我们表明，二进制可达性关系是有效的混合线性算术与合理的整数排序表示。这包含了类似的可表达性结果，以前已知的有限和下推定时自动机与不定时堆栈。作为关键的技术工具，我们使用量词消去的混合线性算术的一个片段和循环顺序原子，并减少注册下推自动机循环顺序原子。
2018-04-28 cs.FL cs.LO
Deterministic pushdown automata can compress some normal sequences
本文构造了一个确定性下推转换器，成功压缩了一个正规数字序列，从而肯定解决了先前论文中遗留的开放问题。
2024-08-09 cs.FL
Model-Checking of Ordered Multi-Pushdown Automata
我们解决了有序多下推自动机的验证问题：下推自动机的多栈扩展，具有对栈转换的约束，使得弹出只能在第一个非空栈上执行。首先，我们证明了有序多下推自动机的空问题是在2 ETIME。然后，我们证明了，对于一个有序的多下推自动机，一个正则配置集的所有前身的集合是一个有效的可构造正则集。我们利用这一结果来解决全球模型检验，其中包括在计算一个有序的多下推自动机，满足给定的w-正则性质（可表示在线性时间的时间逻辑或线性时间μ演算）的所有配置的集合。作为一个直接的后果，我们得到了一个2 ETIME上界的有序多下推自动机的w-正则性质的模型检验问题（匹配其下限）。
2012-09-19 cs.FL cs.LO
Hankel Matrices for Weighted Visibly Pushdown Automata
词函数和图参数的Hankel矩阵（又名连接矩阵）在自动机理论、图论和机器学习中有着广泛的应用。我们给出了嵌套词上实值函数的一个特征，该特征可由加权可见下推自动机识别，并可由嵌套词上的Hankel矩阵表示。这补充了C。用加权一元二阶逻辑刻划Mathissen。
2016-06-27 cs.FL
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
我们证明了高阶下推自动机（HOPDA）的对角问题，因此同时无界性问题，是可判定的。从最近的工作由Zetzsche这意味着，我们可以构建向下封闭的一套接受的话，一个给定的HOPDA。这也意味着我们可以构造HOPDA的Parikh像的下闭包。这两个结果在验证表示为HOPDA或安全高阶递归方案的并发高阶程序中起着重要作用。
2015-11-05 cs.FL
Unified Analysis of Collapsible and Ordered Pushdown Automata via Term Rewriting
我们的模型可折叠和有序的下推系统与长期重写，编码高阶堆栈和多个堆栈到树。我们展示了一个统一的逆保存的可识别性结果的长期重写系统，这是通过扩展经典的基于饱和度的方法。这一结果包含和统一了对可塌缩和有序下推系统的类似分析。尽管有丰富的文献逆保存的可识别性长期重写系统，我们的结果似乎并不遵循任何以前的研究。
2014-10-15 cs.FL
Adaptive Synchronisation of Pushdown Automata
我们引入自适应同步的概念下推自动机，其中有一个外部观察员谁没有关于下推自动机的当前状态的知识，但可以观察到的堆栈的内容。然后，观察者想要决定是否有可能通过以\emph{adaptive}方式向自动机提供输入来将自动机从任何状态带入某个预定状态，即，要给出的下一个输入字母可以取决于堆栈的内容在当前输入字母之后如何改变。我们证明了对于非确定性下推自动机，这个问题是2-EXPTIME-完全的，对于确定性下推自动机，我们证明了EXPTIME-完全性。为了证明下界，我们首先介绍（不同的变种）子集同步，并表明这些问题是多项式时间等价的自适应同步问题。然后，我们证明硬度的子集同步问题的结果。为了证明上界，我们考虑的问题，决定如果一个给定的交替下推系统有一个接受运行最多$k$叶，我们提供了一个$n^{O(k^2)}$时间算法这个问题。
2021-02-13 cs.FL
Iterative pushdown automata and hyperbolic contour words
本文给出了迭代下推自动机在双曲平面上无穷多个分片中球和其它两个域的轮廓字上的应用。我们还给出了双曲三维空间的平铺{5，3，4}和双曲四维空间的平铺{5，3，3，4}的类似应用。
2009-07-28 cs.CG cs.FL
Turn Complexity of Context-free Languages, Pushdown Automata and One-Counter Automata
Università degli Studi di Milano（米兰大学）；Dipartimento di Informatica（计算机系）
研究了推导机和一计数器机在有限turn内的接受复杂度，证明了某些语言在亚线性但非常数数量的turn内被接受，并展示了复杂性层次的无限性。
2026-03-09 cs.FL
Higher-Order Pushdown Systems with Data
我们提出了一个新的高阶下推自动机的扩展，它允许使用一个无限的字母表。新的自动机识别语言的数据字（而不是正常的话），旁边的每个字母从一个有限的字母表有一个数据值从一个无限的字母表。这些数据值可以加载到自动机的堆栈中，稍后与输入上的一些更远的数据值进行比较。我们引入这些自动机的主要目的是它们可以帮助分析正常自动机（没有数据）。作为一个例子，我们给出了一个证明，确定性自动机的崩溃可以识别更多的语言比确定性自动机没有崩溃。这个证明比无数据的情况更简单。我们还提出了一个假设，如何新的自动机模型可以与原模型的高阶下推自动机。
2012-10-09 cs.FL
Enforcing Operational Properties including Blockfreeness for Deterministic Pushdown Automata
我们提出了一种算法，该算法修改了确定性下推自动机（DPDA），使得（i）标记语言被保留，（ii）生命锁被移除，（iii）死锁被移除，（iv）所有状态和边缘都是可访问的，以及（v）建立操作块自由性（即，在每个初始衍生可以继续到标记配置的意义上的可共访问性）。这个问题对于确定性有限自动机（DFA）可以很容易地解决，但对于标准的Petri网类是不可解的。该算法是需要一个操作扩展的监督控制问题（SCP）的情况下，规格建模的DPDA。
2014-03-21 cs.FL
Equivalence of pushdown automata via first-order grammars
给出了一阶文法互模拟等价的可判定性证明。它是Sénizergues（1998，2005）的一个结果的另一种证明，该结果包含了他对确定性下推自动机的著名可判定性问题的肯定解。所提出的证明是概念上更简单，一个特别的新颖性是，它不是作为两个半决策程序，但它提供了一个明确的算法，可能是服从复杂性分析。
2020-08-17 cs.FL cs.LO
Reachability Problem for Weak Multi-Pushdown Automata
本文研究了多下推自动机的一个受限子类的可达性分析。我们假设自动机的控制状态是偏序的，并且自动机的所有转换都是相对于顺序向下的。我们证明了可达性问题的可判定性和向后可达集的可计算性。作为主要的贡献，我们确定相关的子类的可达性问题成为NP完全。这与无通信向量加法系统（无状态多下推自动机的特殊情况）的相同问题的复杂性相匹配。
2013-09-20 cs.FL cs.LO
Average Stack Cost of Buechi Pushdown Automata
研究了Buechi下推自动机（Buechi PDA）的平均栈代价.我们将非负价格与每个堆栈符号相关联，并将堆栈的成本定义为所有元素的成本之和。我们介绍和研究的平均堆栈成本问题（ASC），它问是否存在一个接受运行的一个给定的Buechi PDA，使长期运行的平均堆栈成本低于一些给定的阈值。ASC问题推广了均值-收益目标，可以用来表达下推系统的定量性质。特别地，我们可以使用ASC问题计算平均响应时间。我们证明了ASC问题可以在多项式时间内求解。
2017-10-12 cs.FL
Greibach Normal Form for $ω$-Algebraic Systems and Weighted Simple $ω$-Pushdown Automata
在加权自动机理论中，许多关于形式语言的经典结果被推广到定量的环境中。在这里，我们研究加权上下文无关语言的无限词，一个推广的$ω$ -上下文无关语言（科恩，黄金1977年）和扩展的加权上下文无关语言的有限词（乔姆斯基，Schützenberger 1963年）。在形式文法的理论中，这些加权上下文无关语言，或$ω$ -代数级数，可以表示为混合$ω$ -代数方程组的解和加权$ω$ -下推自动机。在我们的第一个主要结果中，我们证明了（混合）$ω$ -代数系统可以转化为Greibach范式。我们在第二个主要结果中使用Greibach范式证明了简单的$ω$ -复位下推自动机识别所有的$ω$ -代数级数。简单的$ω$ -复位自动机不使用$ε$ -转换，最多只能改变一个符号的堆栈。这些结果将上下文无关语言的基本性质推广到加权上下文无关语言。
2021-10-05 cs.FL
The No Endmarker Theorem for One-Way Probabilistic Pushdown Automata
Faculty of Engineering, University of Fukui（福井大学工学部）
本文证明单向概率下推自动机中的结束标记总是可以移除，通过概率变换以双指数栈状态复杂度为代价构造等价的无结束标记机器，且不损害错误概率，并统一涵盖确定性与非确定性模型。
2026-10-15 cs.CC cs.FL
Language Acceptors with a Pushdown: Characterizations and Complexity
University of California, Santa Barbara（加利福尼亚大学圣塔芭芭拉分校）；University of Saskatchewan（萨斯喀彻温大学）
研究有限转向下推自动机及其带逆转有界计数器的变体，用多带NFA刻画并证明其语言在NLOG中，非有限转向情形在DSPACE(log²n)和P中。
2026-06-15 cs.FL
Bisimilarity of Probabilistic Pushdown Automata
研究了概率下推自动机及其子类的双相似性问题。我们的定义pPDA允许概率和非确定性的分支，概括了下推自动机的经典概念（没有ε-转换）。我们的第一个贡献是一个一般的建设，减少检查的概率转换系统的双相似性检查的非确定性转换系统。这种构造直接产生pPDA的双相似性的可判定性，以及概率基本过程代数的子类上的双相似性问题的基本上界，即，单态pPDA。我们进一步表明，通过仔细的分析，一般的减少可以用来证明一个EXPTIME上界的概率可见下推自动机的双相似性。这里我们还提供了一个匹配的下限，建立EXPTIME-完全性。最后，我们证明了概率单计数器自动机（pPDA的另一个子类）的判定双相似性是PSPACE完全的。在这里，我们使用一个更专门的参数来获得最佳的复杂度界限。
2012-10-08 cs.FL cs.LO
Pushdown automata, lambda-graph systems and C*-algebras
一个$λ$ -图系统是一个带有某种附加结构的标号Bratteli图，它表示一个子移位并产生一个$C^*$ -代数.本文从下推自动机出发构造了一个$λ$ -图系统，使得该自动机所接受的语言与$λ$ -图系统所给出的子移位的可接受词的语言一致.给出了接受Markov-Dyck移位和sofic-Dyck移位语言的下推自动机的$λ$ -图系统。
2014-07-26 cs.FL math.DS math.OA
Simulation of Two-Way Pushdown Automata Revisited
重新讨论了Cook和Jones构造的2路确定下推自动机（2DPDA）的线性时间模拟。根据Jones的基于语义的方法，给出了一个解释器，当扩展随机存取存储器时，执行2DPDA的线性时间模拟。递归解释器在没有原始构造的转储列表的情况下工作，这使得Cook对指数时间自动机的线性时间模拟的洞察更加直观，复杂性论证更加清晰。模拟，然后扩展到2路非确定性下推自动机（2NPDA），以提供一个上下文无关的语言的实时识别。运行最终构造所需的时间取决于非确定性的程度。实现多项式时间模拟的关键机制是通过记忆化共享计算。
2013-09-20 cs.FL cs.PL
Input-driven automata on well-nested infinite strings: automata-theoretic and topological properties
自20世纪80年代以来，人们一直在研究在嵌套括号串上操作的自动机，称为输入驱动下推自动机和可视下推自动机。它们被Mr. Bagur和Madhusudan扩展到无限字符串的情况（“Visibly Pushdown languages”，STOC 2004）。本文研究了这些自动机的性质的假设下，一个给定的无限字符串总是良好嵌套。这个限制使得一个完整的表征相应的$ω$ -语言的经典$ω$ -正则语言和输入驱动的自动机有限字符串。这种特性导致这些自动机的确定性结果，以及他们的Wadge度的第一个结果。
2020-12-06 cs.FL
Notes on Stack Machines and Quantum Stack Machines
本文通过定义多栈机，展示了推导自动机和确定性有限自动机是其特例，并提出量子推导自动机和量子栈机的简洁定义。
2025-11-21 cs.FL
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
研究了不确定弱层次可视下推自动机的状态空间约简问题。VPA识别上下文无关语言的一个健壮且算法上易于处理的片段，这对于建模程序是自然的。我们定义了一个等价关系，这是足够的语言保持的VPA的解释。我们的定义允许合并具有不同行为的状态，只要它们对可达的等价堆栈显示相同的行为。我们编码存在这样的关系作为一个布尔部分最大可满足性（PMax-SAT）问题，并提出了一个算法，快速找到满意的分配。这些分配是PMax-SAT问题的次优解决方案，但仍然可以导致状态的显着减少。我们将我们的方法集成在基于自动机的软件验证器Ultimate Automizer中，并在软件验证竞赛SV-COMP的基准测试中显示性能改进。
2017-04-18 cs.FL
Reachability relations of timed pushdown automata
时间下推自动机（TPDA）是一种将递归与时间约束逻辑相结合的表达形式。我们证明了TPDA的可达性关系可以用线性算术表示，这是一种丰富的逻辑，推广了Presburger算术和有理算术。的主要技术成分是一个新的量词消去结果的时钟约束（用于简化TPDA转换的语法），使用时钟差关系来表达的分数时钟值的可达性关系，和应用帕里克定理重建的积分时钟值。
2020-12-30 cs.FL cs.LO
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
本文研究一类非常一般的无限秩树的逻辑性质，即由高阶递归方案生成的无限秩树。我们考虑，对于一元二阶逻辑和模态μ演算，三个主要问题：模型检查，逻辑反射（又名全局模型检查，要求公式成立的元素集的有限描述）和选择（要求，如果存在的话，要求具有二阶自由变量的MSO公式成立的元素集的有限描述）。对于每一个问题，我们都提供了有效的解决方案。这是由于高阶递归方案和可折叠下推自动机之间的已知连接，并在以前的工作有关奇偶校验游戏上的过渡图的可折叠下推自动机。
2021-03-02 cs.FL cs.LO
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
概率下推自动机（probabilitypushdownautomata，pPDA）是离散概率程序的标准模型，它具有过程和递归的特点.在pPDA中，许多定量性质都被刻画为多项式方程组的最小不动点。在本文中，我们研究的问题，证明这些量位于一定的范围内。为此，我们首先描述了多项式系统，承认易于检查的证书验证其最小不动点的界限。其次，我们提出了一个健全的和完整的乐观值迭代算法计算这样的证书。第三，我们将展示如何证书多项式系统可以转移到证书的各种定量pPDA属性。实验表明，我们的算法计算简洁的证书，几个复杂的例子程序，以及随机上下文无关文法与$> 10^4$产生式规则。
2023-02-26 cs.FL
The Triple-Pair Construction for Weighted $ω$-Pushdown Automata
设S是完备星-Ω半环，Sigma是字母表.对于状态集为1的加权Ω-下推自动机P. n，n ≥ 1，证明了在完备半环-半模对（（S<<Sigma*>>）^nxn，（S<<Sigma^omega>>）^n）上存在一个混合代数系统，使得||P||是这个系统的解的一个分量。当基本半环是布尔半环或自然数半环（无穷大增广）时，我们证明了存在一个混合上下文无关文法，||P||.由P构造的混合上下文无关文法是著名的三元组构造的推广，现在称为Ω-下推自动机的三元对构造。
2017-08-22 cs.FL
Input-Driven Pushdown Automata with Translucent Input Letters
本文研究具有半透明输入字母的输入驱动下推自动机，证明非确定性模型在返回与非返回模式下均强于确定性模型，并分析了语言族的布尔封闭性和可判定性问题。
2025-07-21 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
A Tighter Bound for the Determinization of Visibly Pushdown Automata
可视下推自动机（VPA）是下推自动机的一个子类，它的堆栈行为完全由输入符号按照输入字母表的固定划分来决定。自其引入以来，VPA已被证明在各种情况下是有用的，例如，作为验证的规范形式主义和处理XML流的自动机模型。然而，由于复杂性高，基于VPA框架的形式化验证的实现是一个挑战。在本文中，我们考虑的问题，实现基于VPA的模型检验算法。为此，我们首先提出了一个改进的上限确定VPA。接下来，我们提出简单的动态算法来检查该自动机类的普适性和包含问题。然后，我们在一个原型工具中实现了所提出的算法。最后，我们对随机生成的VPA进行了实验。实验结果表明，所提出的算法是相当快的比标准的。
2009-11-17 cs.FL cs.LO
Fast zone-based algorithms for reachability in pushdown timed automata
由于时间自动机的多功能性，大量的工作已经发展到考虑时间自动机的扩展。一个已经引起很多兴趣的扩展是具有可能无界堆栈的时间自动机，也称为下推时间自动机（PDTA）模型。虽然不同的算法已经给出了这个模型的不同变体的可达性，这些结果中的大多数是纯理论的，并没有产生有效的实现。其中一个主要原因是这些算法（以及现有的实现）都没有使用所谓的基于区域的抽象，而是依赖于区域抽象或其他方法，这些方法很难实现。在本文中，我们表明，一个天真的扩展的区域为基础的可达性算法的控制状态可达性问题的时间自动机是不健全的堆栈的存在。为了更好地理解这一点，我们给出了一个基于归纳规则的时间自动机的区域可达性算法。这个替代视图允许我们分析和调整规则，使其也适用于下推时间自动机。我们得到了第一个基于区域的算法PDTA是终止，健全和完整的。我们实现了我们的算法在工具中的Tendash和进行实验，以显示其有效性，从而为更实用的方法来验证下推定时系统的方式。
2021-07-19 cs.FL cs.LO
Emptiness of Stack Automata is NEXPTIME-complete: A Correction
可折叠下推系统的饱和算法发表在ICALP 2012上。本文介绍了一类用于识别规则可折叠下推配置集的栈自动机。结果表明，这些自动机形成了一个有效的布尔代数，具有线性时间成员问题，并相当于LICS 2010中出现的另一种自动机表示。也有人声称堆栈自动机的空问题是PSPACE完全的。不幸的是，这种说法是不正确的。我们表明，当被接受的堆栈是可折叠的下推堆栈，而不是ICALP 2012中使用的注释堆栈时，这个问题实际上是NEXPTIME完成的。
2018-05-30 cs.FL
Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes
Broadbent和Göller（FSTTCS 2012）证明了无ε二阶下推自动机生成的过程的互模拟等价性的不可判定性。我们添加了一些关于所使用的证明技术的注释，称为Defender's forcing，以及具有ε转换的一阶下推自动机的相关不可判定性证明（Jančar and Srba，JACM 2008）。
2013-03-04 cs.FL cs.LO
An Experiment in Ping-Pong Protocol Verification by Nondeterministic Pushdown Automata
通过一个实验证明了一类密码协议（Dolev-Yao入侵者模型）的安全性可以用双向非确定下推自动机（2NPDA）来验证.非确定性下推程序检查正则语言（要验证的协议）和包含所有取消字的给定Dyck语言的交集是否为空。如果不是，入侵者可以泄露可信用户之间发送的秘密消息。在2NPDA模拟器上，保证验证最多在立方时间内终止。在这个实验中使用的解释性方法简化了验证，通过分离的非确定性下推逻辑和程序控制，并使其更可预测。我们描述的解释方法和已知的转换解决方案，并显示他们共享有趣的功能。同样值得注意的是，自动机理论的抽象结果如何通过程序设计语言手段解决实际问题。
2018-03-27 cs.FL cs.LO cs.PL
Parikh Image of Pushdown Automata
我们比较下推自动机（PDA的短）对其他表示。首先，我们表明，有一个家庭的PDA在一元字母表的$n$状态和$p \geq 2n + 4$堆栈符号，接受一个单一的长字，每一个等价的上下文无关文法需要$Ω(n^2(p-2n-4))$变量。这个家庭表明，经典的算法转换PDA到一个等效的上下文无关文法是最佳的，即使当字母表是一元。此外，我们观察到，语言等价和Parikh等价，它忽略了符号之间的顺序，这个家庭相吻合。我们的结论是，当假设这种较弱的等价性，转换算法也是最佳的。其次，Parikh定理激发了PDA与有限状态自动机的比较。特别是，同一个家庭的一元PDA给出了一个下界的状态数的每一个帕里克等价的有限状态自动机。最后，我们研究的情况下，一元确定性PDA。我们展示了一个新的建设转换成一个等价的上下文无关文法，达到最佳已知的界限一元确定性PDA。
2017-06-26 cs.FL
Collapsible Pushdown Parity Games
本文研究了无限图上的一类两人完全信息回合制奇偶博弈，即由可折叠下推自动机生成的博弈。研究这些游戏的主要动机来自于可折叠下推自动机和高阶递归方案的连接，这两种模型对于生成无限树都是同等表达的。我们的主要结果是建立这样的游戏的可判定性，并提供一个有效的代表性的获胜区域以及获胜的策略。因此，这里得到的结果提供了所有必要的工具，深入研究的逻辑属性的树产生的可折叠下推自动机/递归计划。
2020-10-13 cs.FL cs.LO
Timed pushdown automata revisited
本文给出了下推自动机（PDA）的时间扩张的两个结果。作为我们的第一个结果，我们证明了Abdulla等人的密集时间PDA模型的崩溃：它在表达上等价于具有无时间堆栈的密集时间PDA。出于这一结果，我们主张的框架，一阶可定义的PDA，一个专门的PDA在原子集，作为正确的设置来定义和调查的时间扩展的PDA。这样得到的一般模型是图灵完备的。作为我们的第二个结果，我们证明了NEXPTIME上界复杂性的非空性问题的表达子类。作为一个副产品，我们得到了一个严格的EXPTIME复杂性约束的一个更严格的子类PDA与永恒的堆栈，从而包含已知的密集定时PDA的复杂性约束。
2015-04-17 cs.FL cs.LO
