A Note on the Complexity of Model-Checking Bounded Multi-Pushdown Systems
本文给出了模型检验多下推系统的复杂性刻画。多下推系统对递归并发程序进行建模，其中任何顺序进程都具有有限控制。我们认为有界性的三个标准概念：上下文有界性，相位有界性和堆栈排序。逻辑形式主义是一个线性时间时态逻辑，扩展了著名的逻辑CaRet，但专用于多下推系统，其中抽象运算符（与调用和返回有关），例如下一次和直到被堆栈参数化。我们表明，这个问题是EXPTIME-完全的上下文有界的运行和一元编码的上下文开关的数量，我们还证明了这个问题是2 EXPTIME-完全的相位有界的运行和一元编码的相位开关的数量。在这两种情况下，值k都作为输入给出（因此它不是模型检验问题的常数），这在复杂性上产生了实质性的差异。在某些情况下，我们的结果改善了以前的复杂性结果。
2012-12-06 cs.FL cs.LO
Pushdown Timed Automata: a Binary Reachability Characterization and Safety Verification
我们认为下推时间自动机（PTA）的时间自动机（密集的时钟）增加了下推堆栈。PTA的配置包括控制状态、密集时钟值和堆栈字。通过使用模式技术，我们给出了二进制可达性的可判定特征（即，PTA的所有配置对的集合，使得一个可以到达另一个）。由于一个时间自动机可以被视为一个PTA没有下推栈，我们可以证明，二进制可达性的时间自动机是定义在实数和整数的加法理论。结果可用于验证稠密变量和无界离散变量上均包含线性关系的一类性质。这些性质以前不能用经典的区域技术来验证，也不能用时间自动机的时间时序逻辑和下推系统的CTL $^*$来表示。这些结果也被推广到时间自动机的其他推广。
2001-10-02 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
Reachability Analysis of Communicating Pushdown Systems
在可靠的FIFO通道上异步通信的递归程序的可达性分析要求限制以确保可判定性。我们的第一个结果描述了通信拓扑结构的可判定可达性问题，仅限于急切运行（即，消息在发送后立即被接收或从未被接收的情况下运行）。在可判定的情况下，问题是EXPTIME完全的。第二个结果是一个双指数时间算法的有界上下文分析在这种情况下，以及匹配的下限。这两个结果扩展和改进以前的工作从La Torre等人。
2012-09-28 cs.FL cs.LO
Deciding Asynchronous Hyperproperties for Recursive Programs
本文提出一种带新机制识别迹位置的异步超性质逻辑，在保持有限状态模型检测复杂度不变且更具表达力的同时，首次为递归程序超性质模型检测提供了合适方法。
2023-10-25 cs.FL cs.LO cs.PL
New results on pushdown module checking with imperfect information
开放下推系统的模型检验标准分支时态逻辑（下推模块检查或PMC）最近在文献中被研究，在具有关于系统的完美和不完美信息的环境的上下文中（在最后一种情况下，环境仅具有系统的控制状态和栈内容的部分视图）。对于标准CTL，不完全信息下的PMC是不可判定的。如果堆栈内容被假设为可见的，那么问题是可判定的，并且是2EXPTIME完全的（将PMC的复杂性与CTL的完美信息相匹配）。限制在堆栈内容的深度可见的情况下，具有针对CTL的不完全信息的PMC的可判定性状态是开放的。在本文中，我们表明，与此限制，PMC与不完美的信息对CTL仍然不可判定。另一方面，我们个性化一个有趣的子类OPDS与可见的堆栈内容深度，使PMC与不完善的信息对CTL的存在片段是可判定的，并在2EXPTIME。此外，我们表明，PMC的程序复杂性与不完美的信息和可见的堆栈内容对CTL是2EXPTIME完全的（因此，指数比PMC的程序复杂性与完美的信息，这是已知的EXPTIME完全）。
2011-06-07 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
A Tighter Bound for the Determinization of Visibly Pushdown Automata
可视下推自动机（VPA）是下推自动机的一个子类，它的堆栈行为完全由输入符号按照输入字母表的固定划分来决定。自其引入以来，VPA已被证明在各种情况下是有用的，例如，作为验证的规范形式主义和处理XML流的自动机模型。然而，由于复杂性高，基于VPA框架的形式化验证的实现是一个挑战。在本文中，我们考虑的问题，实现基于VPA的模型检验算法。为此，我们首先提出了一个改进的上限确定VPA。接下来，我们提出简单的动态算法来检查该自动机类的普适性和包含问题。然后，我们在一个原型工具中实现了所提出的算法。最后，我们对随机生成的VPA进行了实验。实验结果表明，所提出的算法是相当快的比标准的。
2009-11-17 cs.FL cs.LO
Decidable Models of Recursive Asynchronous Concurrency
异步通信下推系统（ACPS）满足空栈约束（下推进程只能在其栈为空时接收）是一种流行的可判定模型，用于具有异步原子过程调用的递归程序。我们研究放松空栈约束ACPS，允许并发和通信行动在任何堆栈高度，称为形栈约束，从而使更大的一类并发程序进行建模。我们建立了一个紧密的连接ACPS与形栈和一个新的扩展Petri网：网与嵌套着色令牌（NNCTs）。NNCT中的令牌有两种类型：简单和复杂。复杂标记携带任意数量的彩色标记。NNCT的规则可以同步复杂和简单的令牌，将彩色令牌注入复杂令牌，并将指定颜色集的所有令牌弹出到预定义的位置。我们证明了NNCT的可覆盖性问题是塔完全的。据我们所知，NNCT是Petri网的第一个扩展，在具有无限令牌类型集的网类中，具有原始递归可覆盖性。这一结果意味着塔完全覆盖ACPS与形状的堆栈。
2015-01-18 cs.CC 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
Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking
下推系统（PDS）是递归程序的一种抽象模型，下推系统的模型检验方法已得到研究。寄存器PDS（RPDS）是由寄存器扩展的PDS，以有限的方式处理来自无限域的数据值。一个线性时序逻辑（LTL）模型检验方法已被提出的RPDS与定期估值，但该方法要求用于表示一个定期估值的寄存器自动机（RA）是向后确定的。本文提出了另一种方法来解决同样的问题，其中的模型检验问题的RPDS归结为PDS的问题，通过构造一个PDS互模拟等价于一个给定的RPDS。所提出的方法的结构比以前的模型检验方法更简单，不需要RA确定性或后向确定性，互模拟等价性清楚地保证了这种减少的正确性。另一方面，所提出的方法要求每个RPDS（和RA）具有新鲜度属性，其中每当RPDS用未存储在任何寄存器或栈顶中的数据值更新寄存器时，该值应该是新鲜的。本文还表明，这种模型检验问题的定期评估定义的一般RA是不可判定的，因此新鲜度约束是必要的，在所提出的方法。
2022-03-22 cs.FL cs.LO
New Lower Bounds for Reachability in Vector Addition Systems
研究向量加法系统及其带下推栈扩展的可达性问题的维度参数复杂度，提出新构造将VASS的F_k-难度下界降至维度2k+3，并首次为下推VASS建立维度k/2+4的F_k-难度下界，表明其复杂度可能高于VASS。
2023-11-13 cs.FL cs.LO
Verification for Timed Automata extended with Unbounded Discrete Data Structures
研究了扩展为无界离散数据结构的时间自动机验证问题的可判定性。更详细地说，我们扩展时间自动机与下推堆栈。通过这种方式，我们获得了一个强大的模型，例如可以用来模拟实时程序与过程调用。这是长期以来已知的，该模型的可达性问题是可判定的。本文的目标是确定语言包含问题和相关问题是可判定的时间下推自动机的子类。
2015-09-21 cs.LO
Pushdown Model Checking Above the Cubic Bottleneck
Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；University of Warwick（华威大学）
本文从细粒度复杂度理论角度，基于3k-团等假设证明下推模型检测现有算法的时间下界，提出2NPDA(k)假设并通过线性归约网络佐证，解释该问题长期无更优算法的原因。
2026-08-26 cs.CC cs.FL cs.LO
Algorithmic Verification of Asynchronous Programs
异步编程是一种无处不在的系统编程习惯，用于管理与环境的并发交互。在这种风格中，程序员不是等待耗时的操作完成，而是对操作进行非阻塞调用，并将回调任务发布到任务缓冲区，该任务缓冲区稍后在耗时的操作完成时执行。协作调度器通过从任务缓冲区中挑选并执行回调任务来协调交互（这些回调可以发布更多的回调以供稍后执行）。编写正确的异步程序是困难的，因为回调的使用虽然有效，但模糊了程序控制流。我们提供了一个形式化的异步程序模型，并研究了这个模型的验证问题。我们证明了有限数据异步程序的安全验证问题是expspace完备的。我们证明了有限数据异步程序的活性验证是可判定的，并且多项式时间等价于Petri网的可达性。可判定性并不明显，因为即使数据是有限状态的，异步程序也构成了无限状态转换系统：挂起的异步调用的程序堆栈和任务缓冲区都可能是无限的。我们的主要技术结构是一个多项式时间的语义保持减少从异步程序的Petri网，反之亦然。这种简化允许在Petri网上使用算法技术来验证异步程序。我们还研究了几个扩展的异步程序的基本模型的灵感来自异步库的实现提供的额外功能，并分类这些扩展的验证问题的可判定性和不可判定性。
2011-11-14 cs.FL cs.LO
Products of Recursive Programs for Hypersafety Verification (Extended Version)
针对无限状态递归程序的自动超安全性验证问题，提出一类无限递归乘积程序，结合语言理论与并发理论构造算法，将超安全性验证简化为标准安全性验证，并通过实现和实验证明有效性。
2025-08-23 cs.LO cs.PL
