Visibly Pushdown Modular Games
递归博弈图上的博弈可以用来推理递归顺序程序的控制流。在递归博弈图上的博弈中，最自然的策略概念是模策略，即，一种策略，它是模块的本地策略，不受先前模块调用的影响，因此不依赖于调用的上下文。在这项工作中，我们研究了第一次模块化的策略，就可以表示的下推自动机的获胜条件。我们表明，这样的游戏是不可判定的一般，并成为可判定的明显下推自动机规范。我们的解决方案依赖于减少到模块化游戏的有限状态自动机获胜的条件，这是已知的文献。我们仔细描述所考虑的决策问题的计算复杂性。特别是，我们表明，模块化的游戏与一个普遍的Buchi或co Buchi明显下推获胜条件是EXPTIME-完全的，当获胜条件是由一个CARET或NWTL时序逻辑公式的问题是2 EXPTIME-完全的，它仍然是2 EXPTIME-困难的，即使是这些逻辑的简单片段。作为进一步的贡献，我们提出了一个不同的解决方案，模块化游戏的有限状态自动机获胜的条件，运行速度比已知的解决方案大规格和许多出口。
2014-08-26 cs.CC cs.FL cs.GT
Visibly Tree Automata with Memory and Constraints
2001年引入了单记忆树自动机。他们推广了下推（字）自动机和树自动机与Bogaert和Tison兄弟之间的平等约束。虽然它有一个可判定的空性问题，但该模型的主要缺点是缺乏良好的封闭性。我们提出了一个推广的明显下推自动机的Madhur和Madhusudan的一个家庭的树识别器进行沿其（自下而上）的计算辅助无界存储器的树结构（而不是一个符号栈）。换句话说，这些识别器，所谓的可见树自动机与内存（VTAM）定义了一个子类的树自动机与一个内存享有布尔闭包属性。我们特别证明了它们是可确定的，并且对于VTAM，空性、成员、包含和普适性等问题是可判定的。此外，我们提出了几个扩展的VTAM的过渡可能会受到不同种类的测试之间的记忆和约束一个香格里拉Bogaert和Tison比较兄弟子树在输入树。我们表明，这些类的约束VTAM保持良好的封闭性和可判定性，我们证明了他们的表现力与树语言的相关例子。
2008-06-17 cs.LO
Reasoning about strategies on collapsible pushdown arenas with imperfect information
不完全信息策略逻辑（Strategy Logic with Imperfect Information，SLiR）是一种非常具有表现力的逻辑，旨在表达分布式系统中策略能力的复杂属性。SLiR以前的工作集中在有限系统，并表明，模型检查问题是可判定的，当系统的控制状态的信息是分层的球员或系统的组件，这意味着球员或组件可以完全根据他们各自的状态知识排序。我们表明，从有限到无限的系统产生的可折叠（高阶）下推系统保留可判定性，自然的限制下，堆栈内容是可见的。证明遵循与有限系统相同的路线，但需要使用（可折叠）交替下推树自动机。这种自动机是不可判定的，但半交替下推树自动机被引入并证明是可判定的，研究了两个局中人下推系统的策略问题。为了解决多个球员的层次信息，我们进一步完善这些自动机：我们定义方向引导（可折叠）下推树自动机，并表明它们是稳定的投影，非确定性和缩小。对于后一种操作，用于处理不完美的信息，稳定性在某些假设下保持，当用于具有可见堆栈的系统时，该假设是满足的。然后，我们使用这些自动机来证明我们的主要结果。
2020-07-30 cs.LO
Model Checking Probabilistic Pushdown Automata
我们考虑概率下推自动机（pPDA）的模型检验问题和各种概率逻辑中可表达的属性。我们开始与属性，可以制定为一个广义的随机游走问题的实例。我们证明了定性和定量的模型检验这类性质和pPDA是可判定的。然后，我们证明了模型检验的定性片段的逻辑PCTL和pPDA也是可判定的。此外，我们开发了一个容错的模型检验算法的PCTL和无状态pPDA的子类。最后，我们考虑了一类ω-正则性质，并证明了pPDA的定性和定量模型检验都是可判定的。
2006-03-09 cs.LO
Adding Time to Pushdown Automata
在本教程中，我们将通过示例说明如何结合两个经典模型，即下推自动机（PDA）和时间自动机，以获得时间下推自动机（TPDA）。此外，我们描述了如何可达性问题TPDA可以减少到PDA的可达性问题。
2012-12-17 cs.FL cs.LO
POPACheck: A Model Checker for Probabilistic Pushdown Automata
TU Wien（维也纳工业大学）
POPACheck 是一种用于概率下推自动机的模型检查工具，支持时序逻辑规范，能处理概率程序的行为验证。
2025-06-04 cs.LO
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
我们研究了一个扩展了模块和分数时钟约束的时间下推自动机的表达模型。我们表明，二进制可达性关系是有效的混合线性算术与合理的整数排序表示。这包含了类似的可表达性结果，以前已知的有限和下推定时自动机与不定时堆栈。作为关键的技术工具，我们使用量词消去的混合线性算术的一个片段和循环顺序原子，并减少注册下推自动机循环顺序原子。
2018-04-28 cs.FL cs.LO
Logics for Context-free Hyperproperties
Technische Universität Ilmenau（伊尔梅瑙工业大学）；Université Paris Cité, CNRS, IRIF（巴黎西岱大学，法国国家科学研究中心，信息研究与研究所）；Aalborg University（奥尔堡大学）
提出一种用于指定上下文无关超性质的逻辑，通过迹量化扩展可视下推自动机，并证明单量词交替下的模型检测可判定性及不可判定性边界。
2026-10-04 cs.FL cs.LO
Model-Checking of Ordered Multi-Pushdown Automata
我们解决了有序多下推自动机的验证问题：下推自动机的多栈扩展，具有对栈转换的约束，使得弹出只能在第一个非空栈上执行。首先，我们证明了有序多下推自动机的空问题是在2 ETIME。然后，我们证明了，对于一个有序的多下推自动机，一个正则配置集的所有前身的集合是一个有效的可构造正则集。我们利用这一结果来解决全球模型检验，其中包括在计算一个有序的多下推自动机，满足给定的w-正则性质（可表示在线性时间的时间逻辑或线性时间μ演算）的所有配置的集合。作为一个直接的后果，我们得到了一个2 ETIME上界的有序多下推自动机的w-正则性质的模型检验问题（匹配其下限）。
2012-09-19 cs.FL cs.LO
The $\mathsf{AC}^0$-Complexity Of Visibly Pushdown Languages
School of Electrical Engineering
本文研究哪些可见下推语言属于AC^0复杂性类，并提出一种新的中间VPL子类，探讨其在AC^0中的包含性问题，提出算法判定语言是否属于AC^0或更复杂的复杂性类。
2026-08-28 cs.CC cs.FL cs.LO
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
Bisimilarity of Probabilistic Pushdown Automata
研究了概率下推自动机及其子类的双相似性问题。我们的定义pPDA允许概率和非确定性的分支，概括了下推自动机的经典概念（没有ε-转换）。我们的第一个贡献是一个一般的建设，减少检查的概率转换系统的双相似性检查的非确定性转换系统。这种构造直接产生pPDA的双相似性的可判定性，以及概率基本过程代数的子类上的双相似性问题的基本上界，即，单态pPDA。我们进一步表明，通过仔细的分析，一般的减少可以用来证明一个EXPTIME上界的概率可见下推自动机的双相似性。这里我们还提供了一个匹配的下限，建立EXPTIME-完全性。最后，我们证明了概率单计数器自动机（pPDA的另一个子类）的判定双相似性是PSPACE完全的。在这里，我们使用一个更专门的参数来获得最佳的复杂度界限。
2012-10-08 cs.FL cs.LO
Verification for Timed Automata extended with Unbounded Discrete Data Structures
研究了扩展为无界离散数据结构的时间自动机验证问题的可判定性。更详细地说，我们扩展时间自动机与下推堆栈。通过这种方式，我们获得了一个强大的模型，例如可以用来模拟实时程序与过程调用。这是长期以来已知的，该模型的可达性问题是可判定的。本文的目标是确定语言包含问题和相关问题是可判定的时间下推自动机的子类。
2015-09-21 cs.LO
On a Non-Context-Free Extension of PDL
在过去的25年里，人们在寻找命题动态逻辑（PDL）的可判定非正则扩展方面做了大量的工作。直到最近，PDL的表达扩展，允许可见下推自动机（VPAs）作为一种形式主义来描述程序，被引入并证明有一个确定性的双指数时间的可满足性问题完成。最近，VPA形式主义被扩展到所谓的k-阶段多栈可见下推自动机（k-MFPAs）。与VPA类似，已经表明k-MVPAs的语言具有期望的有效闭包属性，并且空性问题是可判定的。在引入k-MPPA之际，有人问，用k-MPPA扩展PDL是否仍然导致可判定逻辑。这个问题在这里得到了否定的回答。我们已经证明了，对于PDL的扩展与2阶段MPPA与两个堆栈的可满足性成为1^_1^1-完全。
2007-07-18 cs.LO
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
Fast zone-based algorithms for reachability in pushdown timed automata
由于时间自动机的多功能性，大量的工作已经发展到考虑时间自动机的扩展。一个已经引起很多兴趣的扩展是具有可能无界堆栈的时间自动机，也称为下推时间自动机（PDTA）模型。虽然不同的算法已经给出了这个模型的不同变体的可达性，这些结果中的大多数是纯理论的，并没有产生有效的实现。其中一个主要原因是这些算法（以及现有的实现）都没有使用所谓的基于区域的抽象，而是依赖于区域抽象或其他方法，这些方法很难实现。在本文中，我们表明，一个天真的扩展的区域为基础的可达性算法的控制状态可达性问题的时间自动机是不健全的堆栈的存在。为了更好地理解这一点，我们给出了一个基于归纳规则的时间自动机的区域可达性算法。这个替代视图允许我们分析和调整规则，使其也适用于下推时间自动机。我们得到了第一个基于区域的算法PDTA是终止，健全和完整的。我们实现了我们的算法在工具中的Tendash和进行实验，以显示其有效性，从而为更实用的方法来验证下推定时系统的方式。
2021-07-19 cs.FL cs.LO
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
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
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
C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation
高阶递归模式（HORS）作为高阶函数程序的一个有用的抽象，受到了广泛的关注，许多新的验证技术采用HORS模型检查作为其核心。我们给一个帐户的C-SHORe工具，这有助于正在进行的追求一个真正可扩展的模型检查HORS提供一个不同的，自动机理论的角度来看。C-SHORe实现了第一个实用的模型检查算法，该算法作用于下推自动机的泛化，与HORS等表达，称为可折叠下推系统（CPDS）。其核心是CPDS的向后饱和算法。此外，它能够使用从近似向前可达性分析中收集的信息来指导其向后搜索。此外，它使用了一种算法，修剪的CPDS模型检查之前，并提取反例的方法，在负的情况下。我们提供了C-SHORe与HORS最先进验证工具的最新比较。该工具和其他材料可从http://cshore.cs.rhul.ac.uk获得。
2018-09-17 cs.LO
Pushdown Automata and Context-Free Grammars in Bisimulation Semantics
本文在反应式图灵机及互模拟语义下，通过引入带中间接受的序列算子与状态感知概念，恢复了下推自动机与上下文无关文法之间的经典对应关系。
2023-03-01 cs.FL cs.LO
Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata
本文通过博弈刻画概率双模拟，将其归约为非概率情形，并应用于概率下推自动机及其子类，分别得到PSPACE、EXPTIME和2-EXPTIME上界，且下界同样成立。
2018-11-14 cs.FL cs.LO
On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata
本文研究概率下推自动机定量界证书与期望终止时间的关系，借助底层多项式方程组 Jacobian 的谱半径等性质，证明正几乎必然终止总存在易验证证书。
2023-04-23 cs.FL cs.LO
A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct
本文研究历史确定性下推自动机（HD-PDA）的表达力与简洁性，证明其语言类严格介于 DPDA 与 CFL 之间且与无歧义 CFL 正交，并给出与 DPDA、PDA、VPA 之间的指数级或双指数级简洁性界限，同时刻画了 HD 性判定复杂度及消解器的可实现性。
2024-01-10 cs.FL cs.LO
Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems
资源受限的多智能体系统的验证一般是不可判定的。在许多这样的设置中，资源对于代理是私有的。本文研究了基于交替时序逻辑（ATL）的资源逻辑在共享资源下的模型检验问题。资源可以被消耗和生产到任何数量。我们表明，模型检验问题是不可判定的，如果两个或两个以上的这样的无界资源。我们的主要技术成果是，在一个单一的共享资源的情况下，问题变得可判定。虽然直观，可判定性的证明是不平凡的。我们减少模型检验的问题交替Büchi下推系统。一个中间结果连接到一般的基于自动机的验证：我们表明，模型检验计算树逻辑（CTL）（紧凑）交替Büchi下推系统是可判定的。
2015-08-14 cs.LO
Recognizers for Graph-Encoding Languages
Tampere University（坦佩雷大学）；University of Helsinki（赫尔辛基大学）
本文提出循环事件自动机（RIAs）这一新自动机模型，通过分解双栈可见下推计算来识别图编码语言，并证明非确定性RIA语言对并、交、连接、Kleene星和反转封闭，确定性RIA对布尔运算封闭但空性不可判定。
2026-10-06 cs.CC cs.DM cs.FL
Model Checking Probabilistic Operator Precedence Automata
TU Wien（维也纳工业大学）；AIT Austrian Institute of Technology（奥地利技术研究院）
本文针对概率下推自动机，引入概率算子优先级自动机，并针对POTLf$\chi$规范开发了最优的EXPTIME/EXPSPACE概率模型检测算法，同时支持LTL规范，为递归概率程序验证提供了首个最优上下文无关逻辑。
2026-09-23 cs.LO cs.PL
Separation of Test-Free Propositional Dynamic Logics over Context-Free Languages
对于一类语言L，让PDL[L]是命题动态逻辑的扩展，它允许程序使用L语言而不仅仅是正则的。如果L包含非正则语言，则PDL[L]可以表示非正则属性，与纯PDL相反。对于规则的，可见的下推和确定性上下文无关的语言，各自的PDL的分离可以通过自动机理论技术来证明。然而，这些技术在自动机方面引入了非确定性。由于非确定性也是DCFL和CFL之间的区别，因此这些技术似乎不适合将PDL[DCFL]与PDL[CFL]分开。然而，这种分离是显示，但程序没有测试操作符。
2011-06-07 cs.LO
Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete
Sénizergues（1998，2005）证明了两个具有限制静默动作的下推自动机是否弱双相似。我们提供了第一个已知的复杂性上界这个著名的问题，在等效设置的一阶文法。这ACKERMANN上限是最佳的，我们还表明，强双相似性是连续递归的自动机的状态数是固定的。
2019-01-22 cs.FL cs.LO
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence
本文提出 PDNF 互模拟，利用无栈 LTS、调用栈即时饱和与 up-to 技术，使具有局部状态的高阶程序在无界栈和未知函数输入下仍可判定上下文等价性。
2023-11-02 cs.LO cs.PL
Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
本文将非周期性、无星性和一阶可定义性的经典等价关系扩展至算子优先语言，通过引入OP表达式和文法变换完成证明，并指出该方法同样适用于可见下推语言。
2023-11-21 cs.FL cs.LO
A Navigation Logic for Recursive Programs with Dynamic Thread Creation
本文提出时序逻辑NTL，用于推理动态下推网络中递归程序的调用、返回及动态线程创建行为，并证明其模型检测与可满足性问题的复杂度不高于下推系统上的LTL，为验证此类程序提供了新途径。
2023-10-30 cs.FL cs.LO
Descriptive Set Theory and $ω$-Powers of Finitary Languages
$ω$ -有限语言L在有限字母表$Σ$上的幂是由L $\infty$定义的$Σ$上的无限词的语言：= {w 0 w 1. .. $\in$ $Σ$ $ω$| $\forall$ i $\in$ $ω$ w i $\in$ L}。$ω$ -幂在理论计算机科学中很自然地出现在被各种自动机接受的几类无限词语言的特征中，如B{ü}chi自动机或B{ü}chi下推自动机。本文综述了描述集理论与$ω$ -幂之间的联系。
2020-07-15 cs.LO math.LO
