Complete Robust Hybrid Systems Reachability
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文提出鲁棒微分动态逻辑，证明其对混合系统可达性问题的绝对完备性，为精确语义的混合系统提供自动验证方法。
2026-07-24 cs.LO
The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)
我们研究了著名的度量区间时态逻辑MITL[U_I，S_I]的两个一元片段，并确定了它们的表达性和满足复杂性.我们证明了MITL[F_ \inf，P_ \inf ]对于偏序双向确定时间自动机（po 2DTA）是（令人惊讶的）表达完备的，并且从逻辑到自动机的约简给出了它的NP完全可满足性.我们还证明了一元模态只有有界区间的片段MITL[F_b，P_b]具有\nexptime -完全可满足性.但奇怪的是，MITL[F_b，P_b]严格地说不如MITL[F_ \inf，P_ \inf ]有表达性。我们提供了一个全面的图片的可判定性和表现力的各种一元片段的MITL。
2013-05-14 cs.FL cs.LO
The Implication Problem for Functional Dependencies and Variants of Marginal Distribution Equivalences
该研究针对函数依赖与两类一元边际概率依赖的蕴含问题，构建了可靠完备的无穷公理系统并证明无有穷公理化，同时提出多项式时间算法确定其蕴含问题的复杂度上界。
2024-05-17 cs.LO
A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems
我们引入了一个健全的和完整的共归纳证明系统的可达性的性质在过渡系统中产生的逻辑约束项重写规则的顺序排序签名模内置。微积分的一个关键特征是循环证明规则，它允许获得无限共归纳证明的有限表示。
2018-04-23 cs.LO
Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees
研究了有限无秩树上一阶逻辑二元片段的可满足性问题。我们使用的签名由一些一元谓词和二元导航谓词child、right sibling以及它们各自的传递闭包组成。我们证明了包含所有这些谓词的逻辑的可满足性问题是EXPSPACE-完全的。此外，我们考虑了结构类对奇异树的限制，即，我们假设在每个节点处恰好有一个一元谓词成立。我们观察到，完整的逻辑，甚至无序树保持有限奇异树的EXPSPACE-完全，但复杂性降低一些较弱的逻辑。也就是说，具有一个二元谓词的逻辑，后代是NEXPTIME-完全的，并且其保护版本是有限奇异树上的PSPACE-完全的，即使这两个逻辑在任意有限树上都是EXPSPACE-完全的。
2014-10-21 cs.LO
Memoization for Unary Logic Programming: Characterizing PTIME
我们给出了确定性多项式时间计算的一个特征的基础上的代数结构称为决议半环，其元素可以被理解为逻辑程序或一阶项重写规则集。更确切地说，我们研究的限制，这个框架的条款（和逻辑程序，重写规则）只使用一元符号。我们证明了它是完全的多项式时间计算，使用下推自动机的编码。然后，我们引入记忆化技术的代数对应物，以表明其PTIME的合理性。最后，我们将我们的方法和复杂性的结果，逻辑编程的复杂性。作为我们的技术的应用，我们展示了一个PTIME完整性的结果，一类逻辑编程查询只使用一元函数符号。
2015-02-04 cs.CC cs.LO math.LO
Vector Addition System Reversible Reachability Problem
向量加法系统的可达性问题是网理论的一个中心问题。这个问题已知是可判定的，但其复杂性仍然未知。而这个问题是EXPSPACE-硬的，没有基本的上限复杂性是已知的。在本文中，我们考虑可逆的可达性问题。这个问题包括决定两个配置是否彼此可达，或者等价地，如果它们在可达图的同一个强连通分量中。我们证明了这个问题是EXPSPACE完全的。作为所介绍的材料的应用，我们描述了一个矢量加法系统的可逆域。
2013-02-26 cs.LO
Robust Almost-Sure Reachability in Multi-Environment MDPs
本文研究 MEMDP 中对所有环境鲁棒满足几乎必然可达性的策略合成问题，证明其存在性判定为 PSPACE 完全，并实现算法在多个基准上验证有效性。
2024-12-06 cs.LO
The algebra of functions with antidomain and range
本文给出了一元部分函数代数在复合、Domain、反Domain、值域和交运算下的完备的、有限的拟方程公理化。这完成了广泛的计划分类代数的一元部分职能的组合下，这些业务。我们看看方程理论的复杂性，并提供了一个非确定性的多项式上界。最后，我们看看问题的有限representability和表明，有限代数可以表示为一个集合的一元函数在一个有限的基集提供的交集是不是在签名。
2014-10-15 cs.LO math.LO
Reachability in Vector Addition Systems is Ackermann-complete
向量加法系统和等价Petri网是一种成熟的并发模型。向量加法系统的核心算法问题是可达性问题，它询问是否存在从一个给定配置到另一个给定配置的运行。我们解决了它的复杂性是阿克曼完全的，从而关闭了45年的问题。特别是，我们证明了这个问题是$\mathcal{F}_k$ -困难的向量加法系统的状态在维度$6k$，其中$\mathcal{F}_k$是$k$ -th复杂性类的层次结构的快速增长的复杂性类。
2022-10-25 cs.FL cs.LO
Monus semantics in vector addition systems with states
研究了带状态向量加法系统（VASS）的 monus 过近似语义，允许递减零值计数器，证明全程使用该语义时可达性保持可判定，并全面刻画了可达性、零可达性和覆盖性问题的复杂度。
2023-09-12 cs.FL cs.LO
Levels of Undecidability in Infinitary Rewriting: Normalization and Reachability
在[EGZ 09]中，已经证明了无穷强正规化（SNi）是Pi-1-1-完全的。令人惊讶的是，无穷弱规范化（WNi）是一个更难的问题，是Pi-1-2-完全的，因此在分析层次中严格较高。
2010-03-04 cs.CC cs.LO
Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints
本文研究了具有非负速率的矩形混合自动机（RHA+）的时间有界可达性问题。这个问题最近被证明是可判定的[Brihaye et al，ICALP 11]（即使对于非常简单的混合自动机类，无界可达性问题也是不可判定的）。然而，[Brihaye等人，ICALP 11]没有提供时间有界可达性问题的复杂性的精确表征。本文件的贡献有三个方面。首先，我们提供了一个新的NExpTime算法来解决RHA+上的时间有界可达性问题。该算法对[Brihaye等人，ICALP 11]的算法进行了至少一个指数改进。其次，我们证明了这种新算法是最优的，通过建立一个匹配的下限：时间有界的RHA+的可达性，因此是NExpTime完成。第三，我们在实际的方向上扩展了这些结果，通过证明我们可以有效地计算不动点，这些不动点覆盖可达的状态集（分别为）。共同可达）。
2012-11-06 cs.LO
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One
分支VASS（BVASS）通过允许在两个控制状态之间非确定性地分配计数器值的特殊分支转换来概括具有状态的向量加法系统。因此，BVASS的运行成为一棵树，可达性决定给定的配置是否是可达性树的根。本文证明了BVASS在一维上可达性的P-完全性，这是迄今为止已知的BVASS子类中可达性的第一个可判定性结果。此外，我们还证明了BVASS在一维上的可覆盖性和有界性也是P-完全的。
2016-05-06 cs.FL cs.LO
Delta-Complete Analysis for Bounded Reachability of Hybrid Systems
Carnegie Mellon University（卡内基梅隆大学）
本文提出了一种用于混合系统有界可达性问题的Delta-完全分析框架，通过求解实数上的Delta决策问题进行有界可达性检查，并考虑系统在数值扰动下的鲁棒性。
2014-04-28 cs.LO cs.SY eess.SY
Reachability in 3-VASS is in Tower
本文研究固定维数 VASS 的可达性复杂度，证明 3 维 VASS 可达性属于 Tower，将此前 2019 年的 $\mathbf{F}_7$ 上界改进为塔式高度。
2023-08-21 cs.FL cs.LO
Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
参数时间自动机（PTA）是时间自动机的扩展，其中时钟可以与参数进行比较。可达性问题要求存在一个非负整数的参数分配，使得可达性在底层的时间自动机中保持。PTA的可达性问题长期以来被认为是不可判定的，已经超过了三个参数时钟。几年前，Bundala和Ouaknine证明了对于两个参数时钟和一个参数的PTA，可达性问题是可判定的，并且还证明了复杂度类PSPACE^NEXP的下界。我们的主要结果是，具有一个参数的两参数时间自动机的可达性问题是EXPSPACE-完全的。我们的贡献是双重的。对于EXPSPACE下界，我们利用复杂性理论的深层结果，即EXPSPACE的可串行化表征（基于巴林顿定理）和中国剩余表示中的数字的对数空间翻译为二进制表示。对于EXPSPACE上界，我们给出了一个仔细的指数时间减少PTA两个参数的时钟和一个参数的参数单计数器自动机（POCA）的一个参数的基础上轻微的调整，由于Bundala和Ouaknine建设的一个子类。我们提供了一系列的技术来分区一个虚构的运行的POCA到几个精心选择的子运行，使我们能够证明，它是足够的，只考虑指数量级的参数值。这使我们能够显示一个双指数上界的值的唯一参数的PTA在两个参数时钟和一个参数。我们希望我们的技术的扩展导致最终建立的可达性参数时间自动机与两个参数时钟（和任意多个参数）的长期开放的问题的可判定性。
2020-11-13 cs.FL cs.LO
Reachability in Geometrically $d$-Dimensional VASS
针对向量加法状态系统（VASS）的可达性问题，本文提出几何d维VASS的概念，并证明当d>2时其可达性仍属于F_d复杂度类，拓展了现有d维VASS的复杂度结果。
2025-03-05 cs.CC cs.FL cs.LO
Optimal Label Splitting for Embedding an LTS into an arbitrary Petri Net Reachability Graph is NP-complete
对于一个给定的标号变迁系统（LTS），综合的任务是找到一个同构的可达图的非标号Petri网。即使只要求嵌入到可达图中而不是同构，也不能保证解决方案。在这种情况下，标签分割是一种选择，即重新标记LTS的边缘，使得不同标记的边缘保持不同。通过适当的标签分裂，我们总是可以获得合成或嵌入问题的解决方案。使用标签分裂，我们可以构造一个带有预期的baker-our的标签Petri网（例如，将给定的LTS嵌入其可达图中）。由于标记的Petri网可以有大量的转换，可能需要优化，限制标签分裂产生的标签的数量。我们表明，这样的限制将成为一个NP-完全问题，从可解的问题在多项式时间。
2020-02-12 cs.CC cs.DS cs.FL
Reachability in timed automata with diagonal constraints
我们考虑了具有对角约束（如x-y < 5）的时间自动机的可达性问题。时间自动机的最佳算法是通过枚举其配置的可达集来进行的，这些配置以称为“区域”的数据结构的形式存储。区域之间的仿真关系对于确保终止和效率至关重要。该算法采用了模拟测试“是Z模拟Z”？“，这表明区域Z不到达比区域Z '更多的状态，因此不需要从Z进一步枚举。没有有效的模拟已知的时间自动机包含对角约束作为警卫。本文提出了一种对角约束时间自动机的模拟关系LU-d。在消极的一面，我们证明了决定Z-不是-LU-d-simulated-by-Z'是NP-完全的。在积极的一面，我们确定了证人的非模拟，并提出了一种算法来决定这样的证人使用SMT求解器的存在。证人的形状表明，模拟测试在实践中可能是有效的。
2018-06-28 cs.LO
Inductive Reachability Witnesses
在这项工作中，我们考虑的基本问题的可达性分析的命令式程序与实变量。可达性属性要求程序在执行过程中可以达到某些目标状态。以前的工作，解决可达性分析要么无法处理程序组成的一般循环（如符号执行），或缺乏完整性的保证（如抽象解释），或不自动化（如不正确逻辑/反向霍尔逻辑）。相比之下，我们提出了一种新的方法，可达性分析，可以处理一般的程序，是（半）完整的，可以完全自动化的广泛的家庭的程序。我们的方法扩展技术从不变的生成和排名功能合成的可达性分析，通过（通用）归纳可达性证人（IRWs/UIRWs）的概念。虽然传统的不变式生成使用过近似的可达状态，我们认为下近似的一组程序状态，可以达到一个目标状态的自然对偶问题。然后，我们应用一个类似于排名函数的参数，以确保我们的欠近似中的所有状态确实可以在许多步骤中达到目标集。
2020-07-28 cs.LO cs.PL cs.SE
Reachability in Fixed-Dimensional Continuous VASS
University of Liverpool（利物浦大学）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；University of Warsaw（华沙大学）
研究固定维度连续向量加法系统（CVASS）的可达性和覆盖性问题，在有理数和整数转移向量下，证明维度1时问题属于AC^1，维度≥2时NP完全。
2026-06-29 cs.CC cs.FL cs.LO
The Complexity of Reachability in Affine Vector Addition Systems with States
该研究刻画了仿射VASS中整数可达性的复杂性，给出三分法：重置类NP完全，转移/复制类PSPACE完全，其余不可判定；标准可达性仅置换类可判定，并探讨了固定实例的复杂性任意性。
2021-07-19 cs.CC cs.FL cs.LO
Reachability in Vector Addition System with States Parameterized by Geometric Dimension
本文从几何维度视角研究带状态向量加法系统（VASS）的可达性问题，通过扩展泵引理技术，证明几何1维和2维VASS的可达性问题均为PSPACE完全。
2024-12-19 cs.FL cs.LO
Reachability in Two-Dimensional Vector Addition Systems with States: One Test is for Free
状态向量加法系统是一种普遍存在的计算模型，在计算机科学中有着广泛的应用。向量加法系统的可达性问题是中心问题，因为许多其他问题都归结为这个问题。该问题是可判定的，最近证明了向量加法系统的维数是复杂性的一个重要参数。在大于2的固定维度中，复杂度是未知的（具有巨大的复杂度差距）。在二维中，Blondin等人在2015年证明了可达性问题是PSPACE完全的。我们考虑这个模型的扩展，称为2-TVASS，其中第一个计数器可以测试为零。该模型自然地扩展了单计数器自动机（OCA）的经典模型。我们证明了2-TVASS的可达性在多项式空间中仍然是可解的。正如Blondin等人的工作一样，我们的方法依赖于通过连接多项式多个循环而获得的小的可达性证书的存在。
2020-07-17 cs.FL cs.LO
Reachability-time games on timed automata
在可达性-时间博弈中，玩家Min和Max选择移动，使得在时间自动机中到达最终状态的时间分别最小化或最大化。Asarin和Maler使用值迭代算法证明了强非Zeno时间自动机上可达时间博弈的可判定性。本文补充他们的工作，提供了一个战略改进算法的问题。由于所提出的策略改进算法解决了所有时间自动机上的可达时间博弈，因此也推广了他们的可判定性结果。精确的计算复杂性解决可达时间游戏也建立：问题是EXPTIME完全的时间自动机至少有两个时钟。
2009-07-20 cs.CC cs.DS cs.GT
Farkas certificates and minimal witnesses for probabilistic reachability constraints
本文介绍了Farkas证书的最小和最大可达概率在马尔可夫决策过程（MDP），我们使用的MDP变体的Farkas引理的上下界。所有这些证书的集合被示出为形成多胞形，其点对应于模型和属性的见证子系统。利用这种对应关系，我们可以将寻找最小见证人的问题转化为寻找具有最大数量的零的顶点的问题。虽然计算这样的顶点是计算困难的一般情况下，我们从我们的配方，表现出竞争力的性能相比，最先进的技术，我们得到新的算法。作为一个论点，渐近更好的算法不能希望，我们发现，即使是非循环马尔可夫链的决策版本的最小证人是NP完全的。
2020-02-05 cs.LO math.OC
On parametrized verification of asynchronous, shared-memory pushdown systems
我们考虑参数化的异步共享内存下推系统的模型，在[海牙'11]中介绍。在最近的一系列论文中，已经证明了该模型的可达性是PSPACE完全的[Esparza，Ganty，Majumdar'13]，并且活性在NEXPTIME中是可判定的[Durand-Gasselin，Esparza，Ganty，Majumdar'15]。我们在这里证明了活性问题是PSPACE完全的。我们还介绍了普遍的可达性问题。我们证明了它是可判定的，并且是coNEXPTIME完全的。最后，利用这些结果，我们证明了在NEXPTIME中，满足一定条件的执行轨迹的验证正则性也是可判定的。
2016-07-15 cs.FL cs.LO
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
时间弧Petri网（TAPN）是Petri网模型的一种著名的时间扩展，并且已经针对该模型提出了几种时间自动机的网络转换。我们提出了一个直接的，基于数据库管理的算法向前可达性分析的有界TAPN扩展的运输弧，抑制弧和年龄不变。我们也给出了一个完整的证明其正确性，包括减少技术的基础上对称性和外推。最后，我们增加了一种新的状态空间减少技术的算法，引入了标记上的单调排序，并证明其可靠性，即使在存在的单调性破坏功能，如年龄不变量和抑制弧。我们实现的算法内的模型检查器TAPAAL和实验结果文件一个令人鼓舞的性能相比，验证方法，翻译TAPN模型UPPAAL时间自动机。
2012-11-27 cs.DS cs.LO
Fast zone-based algorithms for reachability in pushdown timed automata
由于时间自动机的多功能性，大量的工作已经发展到考虑时间自动机的扩展。一个已经引起很多兴趣的扩展是具有可能无界堆栈的时间自动机，也称为下推时间自动机（PDTA）模型。虽然不同的算法已经给出了这个模型的不同变体的可达性，这些结果中的大多数是纯理论的，并没有产生有效的实现。其中一个主要原因是这些算法（以及现有的实现）都没有使用所谓的基于区域的抽象，而是依赖于区域抽象或其他方法，这些方法很难实现。在本文中，我们表明，一个天真的扩展的区域为基础的可达性算法的控制状态可达性问题的时间自动机是不健全的堆栈的存在。为了更好地理解这一点，我们给出了一个基于归纳规则的时间自动机的区域可达性算法。这个替代视图允许我们分析和调整规则，使其也适用于下推时间自动机。我们得到了第一个基于区域的算法PDTA是终止，健全和完整的。我们实现了我们的算法在工具中的Tendash和进行实验，以显示其有效性，从而为更实用的方法来验证下推定时系统的方式。
2021-07-19 cs.FL cs.LO
Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
本文扩展 Reachability Types，引入循环引用、浅层限定符追踪和带引用子类型的逃逸规则，在 $\mathsf{F}_{<:}^{\circ}$-演算中证明类型可靠性并展示更强表达力。
2025-08-29 cs.LO cs.PL cs.SE
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
Reachability Switching Games
本文研究零人、一人和两人可达性切换博弈的获胜者判定问题，证明其复杂度分别为NL难、NP完全和PSPACE难且在EXPTIME内，并表明切换变体比随机版本更难。
2021-04-21 cs.FL cs.GT cs.LO
LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties
Sapienza University of Rome（罗马第一大学）；University of Oxford（牛津大学）；ENS Rennes（雷恩高等师范学校）；The University of Sydney（悉尼大学）
本文系统研究了环境规范下LTLf合成问题，针对可达性和安全性属性提出完整算法框架，并证明各算法在复杂度上最优且正确。
2023-08-29 cs.AI cs.FL cs.LO
