The Cost of Parameterized Reachability in Mobile Ad Hoc Networks
我们调查的影响，自发运动的复杂性验证问题的自动机为基础的协议模型的网络与选择性广播通信。我们首先考虑错误状态的可达性，并证明参数化验证是可判定的多项式复杂性。然后，我们转向更丰富的查询，并显示当考虑具有否定或基数约束的属性时，复杂性如何变化。
2012-02-27 cs.LO
Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations
我们引入了一类新的图变换系统，其中重写规则可以由节点邻域上的普遍量化条件来保护。这些条件是通过特殊的图形模式定义的，这些图形模式也可以通过规则进行转换。对于图重写规则的新类，我们提供了一个符号化的过程，工作在向上封闭的配置集的最小表示。我们证明了重写规则的分类表示以及所涉及的顺序，并使用结构良好的过渡系统的结果的过程的正确性和有效性。我们将由此产生的程序的分析分布式用餐哲学家协议的任意网络结构。
2014-07-18 cs.LO
Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN
我们提出了DAB --BPMN事实标准的一个数据感知扩展，它具有对case和持久数据进行操作的能力（分为只读目录和读写存储库），并在表达能力和支持安全属性的参数化验证的可能性之间进行平衡。特别是，我们从工件系统验证的文献中获得灵感，并且考虑其中与只读目录的内容无关地检查安全属性的验证问题，可能考虑目录和储存库中的活动情况和元组的无限数量。这些问题的解决使用完全实现的基于阵列的向后可达性技术属于良好的SMT模型检验的传统。我们还确定了相关类的DAB的MCMT阵列为基础的模型检查器中实现的向后可达性程序是健全和完整的，然后进一步加强这些类，以确保终止。
2019-06-20 cs.LO
Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version)
我们调查了一些结果的自动验证参数化程序没有身份。这些系统由任意多个组件组成，所有组件都运行完全相同的有限状态程序。我们讨论的复杂性，决定没有组件达到不安全的状态。这篇文章主要针对理论计算机科学家。
2014-05-08 cs.FL cs.LO
Parameterized Synthesis
我们研究的综合问题的分布式架构的参数数量的有限状态组件。参数化的规格说明在综合设置中自然出现，但到目前为止，还不清楚如何检测可实现性以及如何在参数化设置中执行综合。使用一个经典的结果验证，我们表明，一类规格的索引LTL \X，参数化合成令牌环网络是等效的分布式合成网络组成的一个单一的过程的几个副本。适应一个著名的结果，从分布式综合，我们表明，后者的问题是不可判定的。我们描述了一个半决策过程的参数化合成问题的令牌环，有界合成的基础上。我们扩展的方法参数化合成令牌传递网络与任意拓扑结构，并显示一个简单的案例研究的适用性。最后，我们勾勒出一个通用的框架，参数化综合的基础上截断和其他参数化验证技术。
2014-02-12 cs.LO
Parameterized Verification of Quantum Circuits (Technical Report)
本文提出了一种自动框架用于验证参数化量子电路的输入输出正确性与等价性，采用同步加权树自动机模型并提供决策算法，通过实验展示了框架的高效性与表达力。
2025-12-02 cs.FL cs.LO
Safety Verification of Parameterized Systems under Release-Acquire
研究了参数化系统在发布-获取语义下的安全性验证问题。已经表明，对于具有对原子比较和交换（CAS）指令的无限访问的系统，该问题是棘手的。我们表明，从验证的角度来看，近似结果的帮助，这是过于悲观。我们研究参数化系统组成的无限数量的环境线程执行相同的，但CAS免费的程序和一个固定数量的区别线程是不受限制的。我们的第一个贡献是一个新的语义，大大简化了RA，但仍然相当于上述系统的安全验证。我们将这个（一般）结果应用于我们模型的两个子类。我们表明，安全验证是唯一的\pspace-完成的有界模型检验问题的区别线程是无循环的。有趣的是，我们仍然可以负担无限的环境。我们表明，复杂性跳转到\nexp-完成线程模块化验证，其中一个不受限制的区别'自我'线程与环境的CAS-自由线程加循环区分线程（如在前面的设置）。除了验证的有用性，结果是强大的，因为它们划定了一个既定的语义的易处理性边界。
2022-05-05 cs.LO cs.PL
Parameterized Verification of Asynchronous Shared-Memory Systems
我们的特点的复杂性的安全验证问题的参数化系统组成的领导者进程和任意多个匿名和相同的贡献者。进程通过共享的有界值寄存器进行通信。虽然寄存器上的每个操作都是原子的，但是没有同步原语来原子地执行操作序列。我们分析了安全验证问题的复杂性时，过程建模的有限状态机，下推机，和图灵机。当所有进程都是有限状态机时，这个问题是coNP完全的;当它们都是下推机时，这个问题是PSPACE完全的。当每个图灵机被允许与寄存器有限制地进行许多交互时，复杂性仍然是coNP完全的。我们的证明使用组合特征的模型中的计算，并在下推系统的情况下，一些独立的利益语言理论的建设。
2013-07-12 cs.FL cs.LO
Parameterized Verification of Disjunctive Timed Networks
本文提出了一种基于新颖区域图算法的析取时间网络（DTNs）参数化验证新技术，通过解决最小时间可达性问题构建摘要时间自动机，避免了指数级截断系统的构建，并在特定时钟不变式条件下扩展了适用性。
2024-01-02 cs.FL cs.LO
Parameterized Verification of Coverability in Well-Structured Broadcast Networks
针对不同类型的模型和拓扑结构，研究了有限状态过程广播网络可覆盖性的参数化验证。在本文中，我们试图发展一个理论的广播网络中的进程可以是结构良好的过渡系统。由此产生的形式主义被称为结构良好的广播网络。给出了一个在允许节点间链路重构的情况下判定良结构广播网络可覆盖性的算法。此外，对于各种类型的通信拓扑结构，我们也证明了在静态情况下的可覆盖性的可判定性。我们这样做是通过显示，对于这些类型的静态通信拓扑结构，广播网络本身是一个结构良好的过渡系统，从而证明了广播网络的可覆盖性的可判定性。
2018-09-10 cs.DC cs.LO
Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
我们介绍了一种用于容错分布式算法（FTDA）的自动参数化验证方法。FTDA由进程数和假定的拜占庭故障进程的最大数目参数化。在我们的技术的中心是一个参数区间抽象（PIA）的区间边界是参数的算术表达式。使用PIA的数据抽象和一种新形式的计数器抽象，我们减少了参数化的问题，有限状态模型检验。我们证明了我们的方法的实际可行性，通过验证Srikanth和Toueg著名的分布式算法的几个变种。我们的半决策程序的补充和动机的不可判定性证明FTDA验证，即使在没有进程间通信。据我们所知，这是第一篇实现拜占庭FTDA参数化自动验证的论文。
2013-02-03 cs.DC cs.LO
Parameterized Verification of Deterministic MPI Programs
University of Delaware（特拉华大学）
研究确定性MPI程序验证问题，通过用户提供特定函数将程序转换为参数化顺序程序，利用Frama-C/Wp扩展实现该验证方法。
2026-07-21 cs.LO cs.PL
Parameterized safety verification of round-based shared-memory systems
我们考虑分布式算法的参数化验证问题，其目标是开发技术来证明给定算法的正确性，而不管参与进程的数量。受异步二进制共识算法的启发[J. Aspnes，Fast deterministic consensus in a noisy environment. Journal of Algorithms，2002]，我们考虑了基于轮的分布式算法与共享内存通信。这些系统中的一个特殊挑战是：1）进程的数量是无限的，更重要的是，2）每一轮都有一组新的寄存器。因此，验证算法需要管理两个无穷大的来源。在这种情况下，我们证明了安全验证问题，其中包括在决定是否所有可能的执行避免给定的错误状态，是PSPACE完整的。对于安全验证问题的负实例，我们还提供了指数下限和上限的最小数目的过程中所需的错误执行和最小轮上的错误状态可以覆盖。
2022-04-25 cs.DC cs.FL cs.LO
On Parameterized Verification Over Tree Topologies
LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP（拉布里实验室，波尔多大学，法国国家科学研究中心，波尔多理工学院）
针对树拓扑上有限状态进程的 rendez-vous 同步，研究了深度有界和相位有界两种约束下的安全性检查复杂度，分别得到与快速增长层级相关的复杂度和 EXPSPACE/2EXPSPACE 完备性结果。
2026-06-26 cs.FL cs.LO
Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems
Univ Rennes, Inria, CNRS, IRISA（雷恩大学、法国国家信息与自动化研究所、法国国家科学研究中心、IRISA）；The University of Sydney（悉尼大学）
针对无限状态异步轮次分布式算法，提出归约到有限计数器系统的参数化验证方法，并证明其完备性，通过nuXmv验证了共识与领导者选举算法。
2026-06-29 cs.FL cs.LO
Parameterized Verification of Coverability in Infinite State Broadcast Networks
本文提出良结构广播网络形式体系，证明静态拓扑下可覆盖性可判定，并给出允许链路重配置及底层进程为下推自动机时的判定算法。
2023-04-21 cs.DC cs.LO
Complete Local Reasoning About Parameterized Programs Over Topologies (Extended Version)
University of Toronto（多伦多大学）
本文研究了无限状态参数化并发程序在丰富通信拓扑上的算法安全验证问题，提出通过全局量化归纳不变量自动证明正确性的方法，并通过多个拓扑的基准测试验证了该方法的有效性。
2026-07-22 cs.LO cs.PL
Parameterized verification of synchronization in constrained reconfigurable broadcast networks
可重构广播网络提供了一个方便的形式主义建模和推理的移动代理广播消息到其他代理的网络以下一些（不断发展的）通信拓扑结构。这些模型的参数化验证旨在检查给定的属性是否与初始配置（代理数量，初始状态和初始通信拓扑结构）无关。我们在这里集中在同步属性，询问是否所有代理收敛到一组目标状态后，一些执行。这个问题是已知的，在多项式时间内，当没有约束的通信拓扑结构的演变（而它是不可判定的静态广播网络）是可判定的。在本文中，我们研究如何重新配置的各种约束影响的可判定性和复杂性的同步问题。特别是，我们表明，当绑定的数量重新配置的链接之间的两个通信步骤由一个常数，同步变得不可判定;另一方面，同步仍然是可判定的PTIME时，绑定的代理数量的增长。
2018-02-23 cs.DC cs.FL cs.LO
Structural Invariants for the Verification of Systems with Parameterized Architectures
我们考虑参数化并发系统组成的一个有限的，但数量未知的组件，通过复制一组给定的有限状态自动机。组件通过执行原子交互进行通信，原子交互的参与者同时更新它们的状态。我们引入了一个交互逻辑来指定交互的类型（例如\广播）和系统的拓扑结构（例如\管道、环）。该逻辑可以很容易地嵌入到一元二阶逻辑中，因此是可判定的。证明这样的参数化系统的安全属性，如死锁自由或互斥，需要推断出包含所有系统实例的所有可达状态的归纳不变量，并且没有不安全状态。我们提出了一种方法来自动合成归纳不变量直接从公式描述的相互作用，没有昂贵的不动点迭代。我们的实验证明，这个不变量是强大到足以验证大量的系统，包括教科书的例子（哲学家用餐，同步计划），经典的互斥算法，缓存一致性协议和自稳定算法的安全性能，为任意数量的组件。
2021-09-07 cs.DC cs.LO
Parameterized Verification of Systems with Global Synchronization and Guards
受分布式应用程序的启发，使用共识或其他协议的全球协调，我们定义了一个新的计算模型参数化系统，是基于一个通用的全球同步原语，并允许全球过渡警卫。我们的模型推广了许多现有的模型在文献中，包括广播协议和守护协议。我们表明，可达性属性是可判定的系统没有警卫，并给出充分条件下，他们仍然可判定的警卫。此外，我们调查截止的可达性属性，并提供了足够的条件，在一些情况下，我们的目标应用程序的启发小截止。
2021-05-06 cs.DC cs.FL cs.LO
On A Parameterized Theory of Dynamic Logic for Operationally-based Programs
College of Software, Nanjing University of Aeronautics and Astronautics（南京航空航天大学软件学院）
DLp是一种基于操作性程序的动态逻辑参数化理论，通过提供模型无关的推理框架和循环推理机制，简化了程序验证过程。
2026-02-10 cs.LO
Local Reasoning for Parameterized First Order Protocols
一阶逻辑（FOL）是一种功能强大的程序验证推理工具.最近的工作表明，常春藤FOL是非常适合验证参数化的分布式系统。然而，在FOL中指定许多自然对象（如环形拓扑）出乎意料地不方便。我们提出了一个框架的基础上FOL指定分布式多进程协议在一个进程本地的方式与隐式网络拓扑结构。在规范框架中，我们提供了一个自动主动分析技术，在本地的协议，在一个过程模块化的方式。我们的目标是反映设计人员经常描述和推理协议的方式。通过隐藏FOL结构背后的拓扑结构，我们简化了建模，但使推理复杂化。为了解决这个问题，我们使用一个拓扑的预言来开发一个合理的和相对完整的证明规则，将隐式拓扑的推理减少到纯FOL。这完全避免了将拓扑公理化的需要。使用的规则，我们建立了一个属性，减少验证到一个固定数量的本地邻域的大小为界的过程。我们展示了如何使用框架上的两个例子，包括领导人选举环。
2019-03-07 cs.LO cs.MA
Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
本文提出参数化动态逻辑DLp，通过引入程序配置标签支持符号执行与语法结构推理，构建循环预证明系统保证无限证明树可靠性，为通用程序规约与验证提供灵活框架。
2025-01-29 cs.LO cs.SE
Model Checking Parameterized Asynchronous Shared-Memory Systems
我们描述了参数化系统的活性验证的复杂性，由一个领导者进程和任意多个匿名和相同的贡献者进程。进程通过共享的有界值寄存器进行通信。虽然寄存器上的每个操作都是原子的，但是没有同步原语来原子地执行操作序列。我们分析的情况下，过程中建模的有限状态机或下推机和属性是由一个Büchi自动机的字母表的读取和写入行动的领导者。我们证明了这个问题是可判定的，并且具有令人惊讶的低复杂性：当所有进程都是有限状态机时，它是NP完全的，并且当它们是下推机时，它是PSPACE-hard和NEXPTIME。这种复杂性低于非参数化的情况：多个有限状态机的活性验证是PSPACE完全的，并且对于两个下推机是不可判定的。对于有限状态机，我们的证明使用存在性抽象和半线性约束来表征无限行为。对于下推机，我们展示了如何贡献者计算高栈高可以模拟计算的许多贡献者，每个低栈高。总之，我们的研究结果特征的匿名性和匿名性的假设下，参数化系统的验证的复杂性。
2015-05-25 cs.DC cs.FL cs.LO
Rewrite based Verification of XML Updates
我们考虑XML文档更新的访问控制问题。在XML编程的上下文中，类型可以被视为对冲自动机，静态类型检查相当于验证程序总是将有效的源文档转换为有效的输出文档。给定一组更新操作，我们特别感兴趣的是检查安全属性，例如在任何更新序列中保存文档类型。我们还感兴趣的相关政策的一致性问题，即检测是否授权的操作序列可以模拟禁止的。我们减少这些问题的类型检查问题，解决了计算变种的对冲自动机特征的祖先和后代的初始文档类型的参数化重写规则关闭。
2009-07-29 cs.LO
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
本文综述了基于阈值自动机的参数化验证技术，重点介绍拜占庭模型检查器（ByMC）如何自动验证阈值守卫容错分布式算法，确保其在任意进程数和故障数下正确性。
2023-01-16 cs.DC cs.LO
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
我们考虑的问题，自动验证一个参数化的概率并发系统的家庭终止的概率为1的所有实例对抗对抗的竞争对手。一个参数化的族定义了一个无限状态系统：对于每个数n，这个族由一个实例和n个有限状态进程组成。与安全性相比，活性的参数化验证目前仍然被认为是极具挑战性的，特别是在模型中存在概率的情况下。一个主要的挑战是提供一个足够强大的象征性框架。一个著名的符号框架的参数化验证的非概率并发系统是定期模型检验。虽然该框架最近扩展到概率系统，将公平性的框架-通常是至关重要的验证终止-一直特别困难，由于存在无限数量的公平性约束（每个过程一个）。我们的主要贡献是一个系统的，正则保持，编码有限的公平性（一个现实的公平性的概念，提出了由Henzinger）定期模型检验的概率参数化系统的框架。我们的编码减少了终止有限的公平性，以验证参数化的终止没有公平性的概率系统在定期模型检验（验证框架已经存在）。我们表明，我们的算法可以验证终止许多有趣的例子，从分布式算法（赫尔曼的协议）和进化生物学（莫兰过程，细胞周期开关），这并不符合标准的公平概念。据我们所知，我们的算法是第一个全自动的方法，可以证明这些例子的终止。
2017-10-30 cs.DC cs.FL cs.LO
A case study on parametric verification of failure detectors
本文通过形式化验证Chandra和Toueg故障检测器在部分同步模型下的安全性和活性，引入对称点对点算法类并证明其截止性，利用TLA+、IVy和计数器自动机进行参数化验证。
2023-03-03 cs.LO
Checking Presence Reachability Properties on Parameterized Shared-Memory Systems
本文研究由任意数量异步进程组成的参数化共享内存系统的验证问题，证明基于轮次模型的存在性可达性质参数化验证是 PSPACE 完全的，而无轮次模型降至 NP 完全，并给出多项式时间可解的限制条件。
2023-07-31 cs.DC cs.FL cs.LO
Parameterized Verification of Algorithms for Oblivious Robots on a Ring
IRIF - Univ Paris Diderot（巴黎狄德罗大学 IRIF）；Sorbonne Universités, UPMC Univ Paris 06（索邦大学 皮埃尔和玛丽·居里大学）
我们研究验证问题的自主群的移动机器人，自组织和合作，以解决全球目标。特别是，我们专注于在本文中提出的模型由铃木和山下的匿名机器人在一个离散的空间与有限数量的位置（在这里，一个环）。已经提出了大量的算法工作的环，其大小不是先验固定的，因此可以被认为是一个参数。这些算法的手工正确性证明已被证明是容易出错的，最近的注意力已经给予了正式的方法来自动证明这些应用程序。我们的工作是第一个研究的验证问题，这样的算法在参数化的情况下。我们表明，安全性和可达性问题是不可判定的机器人异步进化。在积极的一面，我们表明，安全属性是决定在同步的情况下，以及在异步的情况下，一类特定的算法。协议的几个属性也可以决定。决策过程依赖于Presburger算法公式中的编码，该公式可以通过SMT求解器进行验证。我们的方法的可行性证明了几个案例研究的编码。
2017-06-16 cs.CC cs.DC cs.DS
Verification of Data-Aware Processes via Array-Based Systems (Extended Version)
我们研究验证的一个一般模型的工件为中心的系统，以评估（参数化）的安全属性无关的初始数据库实例。我们认为这样的工件系统基于数组的系统，这使我们能够检查安全性，通过适应向后可达性，建立了第一次符合模型检验的基础上满意度模理论（SMT）。要做到这一点，我们利用模型理论的机器模型完成，这令人惊讶地证明是一个有效的工具，验证关系系统，并代表了本文的主要原始贡献。这样，我们追求双重目的。一方面，我们重建（限于安全性）的本质，在文献中获得的一些重要的可判定性结果的神器为中心的系统，我们设计了一个真正新颖的类的可判定的情况下。另一方面，我们能够在实现中利用SMT技术，建立在著名的MCMT模型检查器的基于阵列的系统，并扩展它，使我们所有的基础结果完全可操作。
2019-02-27 cs.LO
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
计算机控制系统（CCS）是混合系统的一个子类，其中控制元件与时间的周期关系是至关重要的。由于它们也是许多安全关键设备的核心，因此正确建模此类系统并确保它们根据安全要求正确运行至关重要。微分动态逻辑$d\mathcal{L}$是一种对混合系统建模和证明其正确性的强大逻辑。我们贡献了一个基于组件的建模和推理框架，$d\mathcal{L}$，分离成组件的定时保证，如控制器的反应性和连续动态的可控性模型。组件以并行方式运行，具有粗粒度交织、周期性执行和通信。我们提出的技术，自动化系统的安全性证明，从隔离，模块化，并可能机械化的组件属性参数化的时间特性的证明。
2019-07-08 cs.LO
Regular Model Checking Revisited (Technical Report)
在这方面的贡献，我们重温定期模型检验，一个强大的框架，已成功地应用于验证的无限状态系统，特别是参数化系统（并发系统与任意数量的进程）。我们提供了一个重新制定的定期模型检验与长度保持传感器在存在的二阶理论在自动结构。我们认为，这是一个自然的配方，使我们能够利用强大的综合技术，已被广泛研究的软件验证社区。更确切地说，在这个公式中，一阶部分表示所需正确性属性的验证条件（我们有完整的求解器），而存在量化的二阶变量表示要合成的关系。我们表明，许多有趣的正确性可以用这种方式制定，例如安全，活性，双相似性，和游戏。更重要的是，我们表明，这种新的配方允许新的有趣的基准（和旧的定期模型检验基准，以前被认为是困难的），特别是在参数化系统验证领域，要解决。
2021-11-21 cs.FL cs.LO
Symmetric Proofs of Parameterized Programs
University of Toronto（多伦多大学）
本文提出了一种参数证明空间系统，用于验证无限状态参数化程序的安全性，通过利用程序中的对称性，实现对同构邻域的证明重用，并在特定条件下将其转化为决策过程。
2026-01-26 cs.LO cs.PL
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Technical University of Munich（慕尼黑工业大学）；Vali-e-Asr University of Rafsanjan（拉夫桑贾德瓦利阿斯尔大学）；Masaryk University（马萨里克大学）；Institute of Science and Technology（科学技术研究院）
针对参数化MDP的状态空间爆炸问题，提出利用决策树学习将小实例的最优策略泛化至大实例，无需显式探索大型模型状态空间，在远超现有工具处理规模的模型上表现良好。
2025-04-01 cs.AI cs.LG cs.LO
Automated Software Verification of Hyperliveness
针对现有超属性验证多聚焦$k$-安全性的局限，提出基于约束的自动化算法，结合可靠完备程序逻辑与参数化最强后置条件，验证含超活性的$\forall^k\exists^l$属性，工具ForEx实验效果良好。
2024-03-05 cs.LO cs.PL
Practical Livelock Analysis in Parameterized Unidirectional Rings
本文提出一种实用框架，用于分析自禁用单向环协议中的死锁。通过将分析从转移空间提升到等价积空间，构建了产品转移图，有效验证了死锁自由性。算法在多项式时间内完成，并通过回溯搜索确定死锁存在。
2026-05-01 cs.DC cs.DM cs.FL
Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems (technical report)
我们提出了一个通用的框架，建模和验证的认识属性参数化的多智能体系统，通过真实的公告进行通信。在我们的框架中，代理的数量或某些资源的数量被参数化（即先验未知），相应的验证问题询问给定的认知属性是否为真，而不管参数的实例化。例如，在一个泥泞的儿童拼图中，人们可以问每个孩子是否最终都会发现他是否泥泞，而不管孩子的数量。我们的框架是定期模型检验（RMC）为基础的，其中同步有限状态自动机（相当于一元二阶逻辑的话）被用来指定系统。我们提出了一个公共声明逻辑的扩展作为规约语言。特别感兴趣的是增加了所谓的迭代公共公告运营商，这是至关重要的推理知识参数化系统。虽然运营商的模型检验问题不可判定的，我们表明，这成为一个适当的“消失关系”时，可判定的。此外，我们展示了如何Angluin的L* 算法学习有限自动机可以应用到找到一个消失的关系，这是保证终止，如果它是正规的。我们已经实现了该算法，并将其应用于这样的例子，如泥泞的儿童拼图，俄罗斯卡问题，大数挑战。
2021-03-08 cs.FL cs.LO cs.MA
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
本文研究可重构广播、带标识符寄存器的多智能体参数化网络，证明一般可覆盖性可判定但非原始递归，其他同步问题不可判定，而单寄存器情形为 NP 完全。
2024-03-04 cs.DC cs.FL cs.LO
Fine-Grained Complexity of Safety Verification
我们研究了细粒度的复杂性的领导贡献者可达性（LCR）和有界阶段可达性（BSR），两个变种的安全验证问题的共享内存并发程序。对于这两个问题，内存是有限数据域上的单个变量。我们的贡献是新的验证算法和下界。后者基于指数时间假设（ETH），问题集覆盖和交叉组合。LCR是一个指定的领导者线程在与一定数量的同等贡献者线程交互时是否会达到不安全状态的问题。我们建议两个参数化：（1）通过数据域D的大小和领导者L的大小，以及（2）通过贡献者C的大小。我们提出了这两种情况下的算法。其关键技术是紧凑证人和动态规划。算法的运行时间为O*（（L（D+1））^（LD）* D^D）和O*（2^C），这表明两种参数化都是固定参数的。我们通过（匹配）基于ETH和Set Cover的下界来补充上界。此外，我们证明了多项式核的情况下。对于BSR，我们考虑涉及t个不同线程的程序。我们将分析限制在写权限在线程之间更改s次的计算上。BSR询问给定的配置是否可以通过这样的s阶段计算到达。当用P（线程的最大大小）和t参数化时，有趣的观察是，问题有大量的困难实例。形式上，我们表明，没有多项式核，没有压缩算法，减少数据域D的大小或阶段s的数量多项式依赖于P和t。这表明，符号方法可能更难找到这个问题。
2020-01-10 cs.DC cs.DS cs.LO
Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report)
本文提出基于层级同步树自动机的量子电路符号验证方法，将门操作复杂度降至至多二次方，并支持参数化验证，实验表明其可处理规模远超现有工具的问题。
2024-10-24 cs.FL cs.LO
The Complexity of Nested Reset Counter Systems
Max Planck Institute for Software Systems (MPI-SWS)（马克斯·普朗克软件系统研究所）；Technical University of Munich (TUM)（慕尼黑工业大学）
本文研究嵌套重置计数器系统(NRCS)的覆盖性问题，证明其复杂度为F_{Ω_k}-完全，扩展了嵌套计数器系统(NCS)并改进了XML处理等领域的上界。
2026-05-14 cs.CC cs.FL cs.LO
