Reachability Games in Dynamic Epistemic Logic
我们定义的可达性游戏的基础上动态认知逻辑（DEL），玩家的行动被精细描述为DEL行动模型。我们首先考虑设置一个外部控制器与完美的信息与环境的相互作用，并旨在达到一些认识的目标状态关于系统的被动代理。我们研究了控制器的策略存在性问题，它概括了经典的认知规划问题，我们解决了几种类型的行动，如公共公告和公共行动。然后，我们考虑一个更丰富的设置，代理人本身是球员，其策略必须基于他们的观察。我们建立了几个（联合国）的分布式策略的存在问题的可判定性结果，根据玩家可以使用的行动类型，并将它们与文献中的结果与不完美信息的多人游戏。
2019-05-29 cs.LO
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
可达性逻辑是一种形式主义，可用于表达迁移系统的部分正确性。在本文中，我们提出了三个证明系统的形式主义，所有这些都是健全的和完整的，并继承了共归纳逻辑的性质。然而，证明系统在几个方面有所不同。首先，他们使用归纳和共归纳的比例不同。第二个方面是组合性，广义上意味着它们能够在较小的系统上证明更简单的公式，并将这些公式作为引理重用于较大的系统上的更复杂的公式。第三方面是它们的合理性证明的困难。我们发现，更多的归纳证明系统的使用，更专业的是它的使用coinduction（相对于我们的问题域），更组成的证明系统，但更困难的合理性证明变得。我们还简要地介绍了这些结果在Isabelle/HOL和Coq证明助手的机制。
2019-09-04 cs.LO
Logics of polyhedral reachability
本文针对含类Until空间模态词的多面体可达性逻辑，提出公理系统并通过两步证明其相对于多面体语义学的完备性，为3D网格模型检测等应用提供理论支撑。
2024-06-23 cs.LO
A Constructor-Based Reachability Logic for Rewrite Theories
可达性逻辑作为程序的语言类属逻辑，已被应用于$\mathbb{K}$重写基于规则的语言定义。为了能够验证不仅是代码，而且分布式系统设计，一个新的重写理论通用可达性逻辑，并证明了广泛的重写理论的声音。通过基于构造器的语义统一、匹配和可满足性过程，提高了逻辑的自动化程度。开发了新的方法来证明可能永远不会终止的分布式系统的不变量，并提出了一个原型实现的实验，说明了新的证明方法。
2017-09-15 cs.LO cs.PL
Verification of the IBOS Browser Security Properties in Reachability Logic
本文给出了Illinois浏览器操作系统（IBOS）的重写逻辑规范，定义了可达性逻辑中的同源策略（SOP）等安全属性。它展示了如何使用我们的基于构造器的可达性逻辑定理证明器来演绎验证这些属性。本文还强调了证明中使用的推理技术和三个模块化原则，这些原则对扩大规模和完成验证工作至关重要。
2020-05-25 cs.CR cs.FL cs.LO
On Reachability for Hybrid Automata over Bounded Time
本文研究了混合自动机的时间有界可达性问题。这个问题询问给定的混合自动机是否可以在T个时间单位内到达给定的目标位置，其中T是一个常数有理值。我们表明，在经典的（无界）的可达性问题，时间有界的版本是可判定的矩形混合自动机只允许非负率。这类系统具有实际意义，其中包括秒表自动机类。我们还表明，问题变得不可判定，如果允许的对角线约束或负和正利率。
2011-04-28 cs.LO
Complete Robust Hybrid Systems Reachability
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文提出鲁棒微分动态逻辑，证明其对混合系统可达性问题的绝对完备性，为精确语义的混合系统提供自动验证方法。
2026-07-24 cs.LO
Modular Verification of Heap Reachability Properties in Separation Logic
许多算法和数据结构的正确性依赖于可达性属性，即依赖于堆中对象之间引用链的存在。关于可达性的推理是困难的，主要有两个原因。首先，任何堆修改都可能影响无限数量的引用链，这会使模块化验证（特别是框架）复杂化。其次，SMT求解器不支持一般图的可达性，这阻碍了自动验证。本文提出了一种分离逻辑可达性的模块化描述和验证技术。对于每个方法，我们只在方法操作的堆的片段中本地指定可达性。一种新形式的可达性框架相对凸的子堆允许一个扩展的可达性属性从堆片段的调用者的更大的片段，使精确的过程模块化推理。我们的技术支持实际上重要的堆结构，即无环图与有界的出度以及（潜在的循环）图，每对节点之间最多有一个路径（模循环）。集成到分离逻辑允许我们以统一的方式推理可达性和其他属性，验证并发程序，并通过现有的分离逻辑验证器自动化我们的技术。我们证明，我们的验证技术是适合SMT为基础的验证编码到毒蛇验证基础设施的基准测试的例子。
2019-08-16 cs.LO cs.PL
Probabilistic bounded reachability for hybrid systems with continuous nondeterministic and probabilistic parameters
本文提出了一种计算混合系统有界可达概率的算法，系统在有限数量的离散转换内到达不安全区域的概率。特别是，我们专注于混合动力系统的非线性常微分方程的解决方案（可能不确定的初始条件和参数），并给出了概率行为的初始参数分布为连续（可能无限支持）和离散随机变量的连续动态。我们的方法是定义一个适当的松弛（不可判定）的可达性问题，使它可以解决的$δ$ -完全决策程序。特别是，对于连续随机参数的系统，我们开发了一个有效的集成程序，计算一个任意小的区间，保证包含的可达性概率。在更一般的情况下，系统的不确定性和概率参数，我们的程序计算一个有保证的外壳的范围内的可达性概率。我们已经将我们的方法应用到一些非线性混合模型，并通过与Monte Carlo模拟的比较验证了结果。
2015-05-11 cs.LO
Nested Sequents for First-Order Modal Logics via Reachability Rules
本研究提出首个支持多种论域与路径条件的一阶模态逻辑无切割嵌套矢列系统，通过可达性规则与结构精化方法构建，证明了结构精化可扩展至一阶模态逻辑领域。
2023-11-08 cs.LO math.LO
Simulating reachability using first-order logic with applications to verification of linked data structures
本文介绍了如何利用现有的一阶逻辑定理证明器自动验证执行动态存储分配和破坏性更新的指针值结构字段的命令式程序的安全属性。其中一个主要的障碍是指定和证明（缺乏）的可达性动态分配的细胞之间的属性。主要的技术贡献是使用一阶公式以保守的方式模拟可达性的方法-该公式描述了一组程序状态的超集，如果有一个精确的方式来表达可达性，则会指定该超集。这些方法用于半自动程序验证（即，使用程序员提供的循环不变量），例如标记并清除垃圾回收和单链表的破坏性反转。(The标记和扫描的例子以前已经被报道为超出了ESC/Java的能力。
2009-05-27 cs.LO cs.PL
A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems
针对组合混合系统可达性分析中乘积自动机位置爆炸的问题，提出以CEGAR为核心的有界可达性分析算法，结合不同组合语义与缓存优化，在SAT-Reach工具中实现并验证了可扩展性优势。
2025-09-03 cs.LO
A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability
自从交替时间时序逻辑（ATL）被引入以来，许多逻辑被提出来推理系统中智能体的不同策略能力。特别是，一些逻辑已经被设计成这样的代理商的统一的无记忆策略的原因。这些策略是智能体可以通过只看他们从当前状态观察到的东西来有效地发挥作用的策略。ATL_ir可以被看作是推理这种统一策略的核心逻辑。然而，它的模型检查问题是困难的（它需要对NP预言机的多项式次数的调用），并且解决它的实用算法直到最近才出现。本文提出了一种模型检验统一无记忆策略技术。现有技术通过系统的前向遍历从感兴趣的状态（诸如初始状态）构建策略。另一方面，所提出的方法通过向后遍历从目标状态构建获胜策略，确保只探索统一的策略。然而，从头开始构建策略将其适用性仅限于受限的可达性目标。本文详细介绍了这种方法，并将其与现有的方法实现到一个基于BDD的框架实验比较。这些实验表明，该技术是有竞争力的情况下，它可以处理。
2017-09-07 cs.LO
Reachability Analysis for Spatial Concurrent Constraint Systems with Extrusion
空间并发约束编程（SCCP）是基于约束的过程演算中的空间模态的代数模型;它可以用于推理分布在系统的代理之间的空间信息。本文提出了一个可执行的重写逻辑语义的SCCP挤出（即，进程移动性），它使用重写模SMT，这是一种结合了项重写、匹配算法和SMT求解的新技术。在这种设置中，约束被编码为理论中的公式，该理论具有由SMT求解器决定的满意度关系，而空间层次结构的拓扑被编码为符号状态的术语结构的一部分。通过可执行性，重写逻辑规范为基于约束的模型中的可达性分析的固有符号和挑战性任务提供了支持。该方法说明了与分布式空间和层次系统的容错性，一致性和隐私的自动验证的例子。
2018-05-18 cs.LO
All-Path Reachability Logic
本文提出全路径可达性逻辑，一种语言无关的证明系统，用于验证非确定性程序的可达性属性，具有可靠性和相对完备性，并在 Coq 中机械化验证，已实现于 K 框架。
2019-04-29 cs.FL cs.LO cs.PL
Reachability relations of timed pushdown automata
时间下推自动机（TPDA）是一种将递归与时间约束逻辑相结合的表达形式。我们证明了TPDA的可达性关系可以用线性算术表示，这是一种丰富的逻辑，推广了Presburger算术和有理算术。的主要技术成分是一个新的量词消去结果的时钟约束（用于简化TPDA转换的语法），使用时钟差关系来表达的分数时钟值的可达性关系，和应用帕里克定理重建的积分时钟值。
2020-12-30 cs.FL cs.LO
Bounded Reachability Problems are Decidable in FIFO Machines
本文针对一般FIFO机不可判定的可达性问题，提出输入有界运行的欠近似，通过归约为受限零测试计数器机证明有理可达性等可判定，为构建验证工具奠定基础。
2022-01-19 cs.FL cs.LO
Verification of Parametric Markov Automata under Time-bounded Reachability
Eindhoven University of Technology（埃因霍温理工大学）
针对参数化马尔可夫自动机（pMA），提出通过离散化为参数化马尔可夫决策过程（pMDP）并分析，解决时间有界可达性概率的合成问题，实现参数空间的满足/违反区域划分。
2026-06-23 cs.LO
Reasoning about Data Repetitions with Counter Systems
我们研究线性时间时态逻辑解释数据字多属性。我们将原子公式限制为连续位置中属性值的相等性和未来或过去属性值的重复性。我们证明了逻辑的可满足性问题和计数器系统的可达性决策问题之间的对应关系。我们表明，允许/不允许原子公式表示重复的值在过去对应的可达性/覆盖性问题的Petri网。这给了我们几个可满足性问题的2 EXPSPACE上界。我们证明匹配下界减少从一个新引入的一类计数器系统的可达性问题。这个新类是向量加法系统的简洁版本，其中计数器通过指针访问，这在其他上下文中是一个潜在的有用功能。我们进一步加强了数据逻辑和计数器系统之间的对应关系，通过描述逻辑的片段，扩展和变体的复杂性。例如，我们精确地描述了逻辑中允许的属性数量与计数器系统中所需的计数器数量之间的关系。
2016-07-29 cs.LO
The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems
本文研究线性动力系统伪轨道上的基本可达性问题。伪轨道可以被看作是一个有限精度的计算模型，而伪可达性可以被看作是经典可达性的一个鲁棒版本。利用基于$o$ -极小性的$\reals_{\exp}$，我们证明了可对角化线性动力系统的任意半代数目标的离散时间伪可达性问题的可判定性。我们还表明，我们的方法可以用来减少连续时间的伪可达性问题的（经典）时间有界的可达性问题，这是已知的条件判定。
2022-07-05 cs.LO
Uncertainty Removal in Verification of Nonlinear Systems against Signal Temporal Logic via Incremental Reachability Analysis
U2IS, ENSTA, Institut Polytechnique de Paris（巴黎理工学院 U2IS）
本文通过增量可达性分析方法，解决非线性系统在验证信号时间逻辑规范时的不确定性问题，有效减少满足模糊性。
2026-09-28 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
Symbolic Optimal Reachability in Weighted Timed Automata
加权时间自动机在2000年初被定义用于建模实时系统中的资源消耗或分配问题。在加权时间自动机中，最优可达性是可判定的，并提出了一种符号前向算法来解决这一问题。该算法使用所谓的定价区域，即具有成本函数的标准区域的扩展。为了确保终止，该算法要求时钟有界。对于未定价的时间自动机，已经做了很多工作来开发适合于时间自动机的前向探索的合理抽象，确保在不限制时钟的情况下终止模型检查算法。在本文中，我们利用最近的发展抽象的时间自动机，并提出了一个算法，允许符号分析的所有加权时间自动机，而不需要有界的时钟。
2016-02-01 cs.LO
Fully Automated Verification of Linear Time-Invariant Systems against Signal Temporal Logic Specifications via Reachability Analysis
本文提出一种面向线性系统的全自动验证器，通过自动细化可达性分析参数并结合可达集时序逻辑与依赖保持，实现对信号时序逻辑规范的自动证明或证伪。
2024-04-08 cs.LO cs.SY eess.SY
On Decidability of Time-bounded Reachability in CTMDPs
考虑连续时间马氏决策过程的时间有界可达性问题。我们证明了这个问题是可判定的Schanuel猜想。我们的决策过程依赖于结构的最优政策和条件的可判定性（根据Schanuel的猜想）的理论的实数扩展指数和三角函数在有界域。我们进一步表明，任何无条件可判定性的结果将意味着无条件可判定的有界连续Skolem问题，或等价地，检查的问题，如果一个指数多项式有一个非切零在有界区间。我们注意到，后者的问题也是可判定的Schanuel的猜想，但寻找无条件的决策程序仍然是长期悬而未决的问题。
2020-06-09 cs.LO cs.SY eess.SY
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
University of California, Berkeley（加州大学伯克利分校）
提出pacSTL框架，结合PAC有界可达集预测与区间STL，通过优化问题计算原子鲁棒性上下界并传播，实现规范级别的PAC有界鲁棒性评估，用于不确定动态系统的验证与监控。
2026-07-24 cs.LO cs.RO
XPL: An extended probabilistic logic for probabilistic transition systems
广义概率逻辑（Generalized Probabilistic Logic，GPL）是一种基于模态μ演算的时态逻辑，用于描述反应概率系统的属性。我们探讨XPL，GPL的扩展，允许在马尔可夫决策过程（MDPs）中存在的非确定性的语义。XPL的表达能力足够强，许多独立研究的问题--例如递归MDP（RMDP）的终止、MDP的PCTL* 模型检验和分支MDP的可达性--都可以转换为XPL上的模型检验。多出口RMDPs的终止是不可判定的;因此，XPL中的模型检验一般是不可判定的。我们定义了一个子类，称为可分离的XPL，其中模型检验是可判定的。可判定的问题，如1-出口RMDP的终止，MDP的PCTL* 模型检验，以及分支MDP的可达性，可以减少到模型检验可分离的XPL。因此，XPL形成了一个统一的框架，用于研究涉及具有非确定性和概率行为的系统的问题，而可分离的XPL提供了一种解决这些问题的可判定片段的方法。
2017-05-09 cs.LO
On Higher-Order Reachability Games vs May Reachability
该研究探讨高阶函数式程序的可达性博弈与可能可达性的关系，证明二者可通过阶数调整相互归约，用高阶不动点逻辑形式化归约并验证正确性，为高阶程序验证提供新方法。
2024-09-13 cs.LO cs.PL
Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
本文提出用混合zonotope后向可达性分析构造时序逻辑树，以计算高效且能表示非凸、不相交几何形状的方式形式化验证自主系统的LTL规范。
2024-04-04 cs.LO cs.SY eess.SY
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
时间弧Petri网（TAPN）是Petri网模型的一种著名的时间扩展，并且已经针对该模型提出了几种时间自动机的网络转换。我们提出了一个直接的，基于数据库管理的算法向前可达性分析的有界TAPN扩展的运输弧，抑制弧和年龄不变。我们也给出了一个完整的证明其正确性，包括减少技术的基础上对称性和外推。最后，我们增加了一种新的状态空间减少技术的算法，引入了标记上的单调排序，并证明其可靠性，即使在存在的单调性破坏功能，如年龄不变量和抑制弧。我们实现的算法内的模型检查器TAPAAL和实验结果文件一个令人鼓舞的性能相比，验证方法，翻译TAPN模型UPPAAL时间自动机。
2012-11-27 cs.DS cs.LO
Inductive Reachability Witnesses
在这项工作中，我们考虑的基本问题的可达性分析的命令式程序与实变量。可达性属性要求程序在执行过程中可以达到某些目标状态。以前的工作，解决可达性分析要么无法处理程序组成的一般循环（如符号执行），或缺乏完整性的保证（如抽象解释），或不自动化（如不正确逻辑/反向霍尔逻辑）。相比之下，我们提出了一种新的方法，可达性分析，可以处理一般的程序，是（半）完整的，可以完全自动化的广泛的家庭的程序。我们的方法扩展技术从不变的生成和排名功能合成的可达性分析，通过（通用）归纳可达性证人（IRWs/UIRWs）的概念。虽然传统的不变式生成使用过近似的可达状态，我们认为下近似的一组程序状态，可以达到一个目标状态的自然对偶问题。然后，我们应用一个类似于排名函数的参数，以确保我们的欠近似中的所有状态确实可以在许多步骤中达到目标集。
2020-07-28 cs.LO cs.PL cs.SE
On The Reachability Problem for Recursive Hybrid Automata with One and Two Players
受有限状态机有界模型检验框架成功的启发，Ouaknine和Worrell提出了实时验证的时间有界理论，认为对有限时间的限制恢复了与实时验证相关的几个关键决策问题的可判定性。为了支持这一理论，最近的列表不可判定的问题证明在时间有界的限制下可判定的是相当令人印象深刻的：语言包含的时间自动机，空问题交替时间自动机，空问题矩形混合自动机。我们研究的目的是恢复一般递归时间自动机的可判定性-也许递归混合自动机-在时间有界的限制下，以提供一个有吸引力的验证框架，强大的建模环境，如Stateflow/Simulink。不幸的是，然而，我们回答这个问题的否定表明，时间有界的可达性问题保持不可判定的递归时间自动机与五个或更多的时钟。虽然坏消息继续，即使当一个考虑行为良好的子类的递归混合自动机，我们恢复可判定性考虑递归混合自动机与有界上下文使用通过引用机制，或通过限制变量的数量为2，率在$\{0,1\}$。
2014-08-15 cs.FL cs.LO
Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs
针对有界Petri网非阻塞性验证问题，提出基于极小极大基可达图的半结构化方法，无需构建完整可达图即可完成验证，适用范围广。
2021-06-08 cs.LO cs.SY eess.SY
Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
Technische Universität Dresden（德累斯顿工业大学）；University of Bologna（博洛尼亚大学）
本文提出了一种无割的嵌套序列系统，用于处理具有内外域的量模态逻辑，通过可达规则实现域条件的自然定义，并证明了系统的完备性和证明论性质。
2026-04-20 cs.LO math.LO
Improved Undecidability Results for Reachability Games on Recursive Timed Automata
我们研究递归时间自动机（RTA）上的可达性游戏，推广Alur-Dill时间自动机的递归过程调用机制类似于递归状态机。对于具有两个或多个时钟的自动机，RTA上的可达性博弈中的胜者判定问题是不可判定的，而对于只有一个时钟的自动机，该问题是可判定的。Ouaknine和Worrell最近提出了一个实时验证的时间有界理论，声称对有界时间的限制恢复了与实时验证相关的几个关键决策问题的可判定性。我们重新审视了具有时间限制的递归时间自动机上的博弈，希望能恢复可判定性。然而，我们发现，这个问题仍然是不可判定的递归时间自动机与三个或更多的时钟。使用类似的证明技术，我们的特点是一个可判定性边境的推广RTA递归秒表自动机。
2014-08-26 cs.FL cs.LO
The reachability problem for vector addition systems with a stack is not elementary
通过适应迭代码构造Stockmeyer，我们证明了向量加法系统的可达性问题与堆栈不具有初等复杂性。作为一个推论，同样的下界也适用于树上的二元一阶逻辑的可满足性问题，其中无界数据只能标记叶节点。这两个问题是否可以解决仍然是一个悬而未决的问题。
2013-10-07 cs.FL cs.LO
Decision Problems for Petri Nets with Names
我们证明了nu-PN，纯名称创建和名称管理的P/T网的扩展的可判定性和不可判定性的结果。通过将具有抑制弧的网的可达性归结为可达性，给出了可达性不可判定性的一个简单证明，从而证明了nu-PN网的表达能力严格优于P/T网。我们证明了nu-PN是结构良好的转移系统。特别地，我们得到了可覆盖性和可终止性的可判定性，从而没有达到图灵机的表达能力。此外，它们是严格良结构的，因此有界性问题也是可判定的。我们考虑两个属性，宽度有界性和深度有界性，分解有界性。宽度有界性已经被证明是可判定的。我们在这里证明深度有界的不可判定性。最后，我们得到阿克曼硬度的结果，我们所有的可判定的决策问题。
2010-11-17 cs.LO
Low rank MSO
该研究引入低秩MSO这一图性质描述新逻辑，证明其在弱稀疏图类、有界VC维图类及所有图上分别与分隔符逻辑、翻转连通性逻辑、翻转可达性逻辑表达能力等价，并指出无向图中其可表达性质可多项式时间判定。
2025-02-12 cs.LO
On Multi-step Fuzzy Inference in Goedel Logic
本文在带真值常量的Goedel逻辑中研究Mamdani-Assilian型多步模糊推理，将可达性、稳定性和k-循环问题归约为不可满足性问题，并利用超归结演算求解。
2023-12-01 cs.LO
Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems
该研究提出基于良基有界并半格与伽罗瓦连通函数的伽罗瓦能量博弈通用判定过程，可实例化求解多类定量可达性问题，算法在图规模上多项式、维度上指数，且配有形式化证明与实现。
2025-04-22 cs.CC cs.LO
Characterizing Structural Hardness of Logic Programs: What makes Cycles and Reachability Hard for Treewidth?
答案集编程（ASP）是一个问题建模和解决框架的几个问题，在KR与日益增长的工业应用。ASP也是近年来研究计算复杂性和深入理解计算难度及其来源的一个热点。这些研究导致了富有成效的表征方面的复杂性类，细粒度的见解形式的二分法风格的结果，以及详细的参数化的复杂性景观。最近，这导致了一个新的结果，建立的措施树宽，它捕获的程序的结构密度，评估的知名类正常的程序预计将稍微困难比决定可满足性（SAT）。然而，目前还不清楚如何利用ASP的这种结构性力量。本文论述了一种新的减少SAT到正常的ASP，超越了众所周知的编码：我们明确利用ASP的结构功率，从而我们次线性地减少树的宽度，这可能无法显着改善。然后，与现有的结果相比，这通过建立依赖图的周期长度（SCC大小）对树宽的所需函数依赖来以细粒度的方式表征硬度。
2023-01-18 cs.AI cs.DM cs.LO
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
本文讨论了有限状态马尔可夫决策过程（MDP）的整数权重分配给每个状态动作对。提出了新的算法来分类端组件根据其限制行为相对于累积的权重。这些算法被用来提供两种类型的整数加权MDPs的基本问题的解决方案。首先，一个多项式时间算法的经典随机最短路问题，推广已知的结果，特殊类的加权MDPs。其次，定性概率约束的重量有界（重复）的可达性条件的解决。其中，它示出的问题，以决定是否一个析取的重量有界的可达性条件下，几乎肯定持有一些调度属于$\textrm{NP}\cap \textrm{coNP}$，是可解的伪多项式时间，是至少一样难，解决两个球员的平均支付游戏，而相应的问题，泛量化的竞争对手是可解的多项式时间。
2018-04-30 cs.LO
On the Decidability of Reachability in Continuous Time Linear Time-Invariant Systems
研究了连续时间线性定常控制系统状态到状态可达性的判定问题。我们分析这个问题的允许控制集，这是假设下的单位超立方体的线性映射的图像。这自然地对有界（有时称为饱和）控制进行建模。控制集是$\mathbb{R}^n$的仿射子空间的可达性问题的判定性是控制理论中的一个基本结果。我们的第一个结果是二维可判定性（$n=2$），如果矩阵$A$满足某些谱条件，以及一般的条件可判定性。如果变换矩阵$A$是对角的有理元素（或同一代数数的有理倍数），则可达性问题是可判定的。如果变换矩阵$A$只有实特征值，则可达性问题是条件可判定的。时间有界可达性问题在二维上是条件可判定的，也是无条件可判定的。我们的一些可判定性结果是有条件的，因为它们依赖于某些数学理论的可判定性，即指数实数理论（$\mathfrak{R}_{\exp}$）和有界正弦实数理论（$\mathfrak{R}_{\exp,\sin}$）。我们还得到了一个硬度的问题，其中目标是简单的集合（超立方体的尺寸$n-1$或超平面），而不是一个点，控制集是凸有界多面体的温和推广的结果。在这种情况下，我们表明，该问题至少是一样难的\emph{Continuous Positivity problem}或\emph{Nontangential Continuous Positivity problem}。
2021-03-15 cs.LO cs.SY eess.SY
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability
随机布尔可满足性（SSAT）问题是由Papadimitriou在1985年通过随机量化给命题可满足性增加一个不确定性的概率模型时提出的。SSAT有许多应用，其中概率有界模型检验（PBMC）的符号表示的马尔可夫决策过程。本文确定了克雷格插值的SSAT框架的概念，并开发了一个算法，计算这样的插值的基础上的分辨率演算SSAT。作为一个潜在的应用领域，这个新的概念克雷格插值，我们解决概率系统的符号分析。我们首先调查使用插值的概率状态可达性分析，把证伪过程采用PBMC概率安全属性的验证技术。此外，我们提出了一种基于插值的方法来概率区域稳定性，能够验证在某些区域内稳定的概率足够大。
2012-06-25 cs.LO
Reachability Analysis of Communicating Pushdown Systems
在可靠的FIFO通道上异步通信的递归程序的可达性分析要求限制以确保可判定性。我们的第一个结果描述了通信拓扑结构的可判定可达性问题，仅限于急切运行（即，消息在发送后立即被接收或从未被接收的情况下运行）。在可判定的情况下，问题是EXPTIME完全的。第二个结果是一个双指数时间算法的有界上下文分析在这种情况下，以及匹配的下限。这两个结果扩展和改进以前的工作从La Torre等人。
2012-09-28 cs.FL cs.LO
Bounded Linear Logic, Revisited
我们提出QBAL，Girard，Scedrov和Scott的有界线性逻辑的扩展。该系统的主要新颖之处是量化资源变量的可能性。这种推广使得有界线性逻辑更加灵活，同时在多项式时间内保持可靠性和完备性。特别是，我们提供了合成嵌入Leivant的RRW和霍夫曼的LFPL到QBAL。
2010-12-23 cs.LO
Senescent Ground Tree Rewrite Systems
已知具有状态的基础树重写系统具有不可判定的控制状态可达性问题。从最近引入的范围有界的多栈下推系统的灵感，我们定义衰老地面树重写系统。这些是具有状态的基础树重写系统的限制，使得树的节点在已经见证了先验固定数量的控制状态改变之后不再被重写。以及推广范围有界的多栈下推系统，我们表明-通过减少和重置Petri网-这些系统有一个阿克曼完全控制状态可达性问题。然而，正规树集的可达性仍然是不可判定的。
2013-11-19 cs.FL cs.LO
Dynamic Epistemic Logic Games with Epistemic Temporal Goals
Université de Rennes（雷恩大学）；ENS Rennes（雷恩高等师范学校）
动态认知逻辑（英语：Dynamic Epistemic Logic，DEL）是一个逻辑框架，在这个框架中，人们可以非常详细地描述行为是如何被代理感知的，以及它们如何影响世界。DEL游戏最近被引入作为一种定义具有不完美信息的游戏类别的方法，其中玩家可用的动作被非常精确地描述。这个框架可以很容易地定义，例如，玩家只能使用公共行动或公共公告的游戏类别。这些游戏已被研究的可达性目标，其目的是达到一种情况下，满足一些认知属性表示在认知逻辑，几个（UN）decidability结果已经建立。在这项工作中，我们表明，可达性目标获得的可判定性结果扩展到一个更一般的类获胜的条件，即那些表达在认知时序逻辑LTLK。要做到这一点，我们建立的DEL公共行动所产生的无限博弈结构是经常的，我们描述了如何获得有限的表示，我们依赖于解决这些问题。
2020-01-20 cs.AI cs.LO cs.MA
Monitoring Diameters of Causal Communication Graph with Spatio-Temporal Logic
LIX, CNRS, École polytechnique, Institut Polytechnique de Paris（巴黎综合理工学院，巴黎理工学院，法国国家科学研究中心）
针对连续时间空间中的多智能体系统，提出扩展时空逻辑MuTGL，引入空间界限算子以表达通信链距离，增强对分布式协议图论性质（如直径）的监控能力，并给出集中式离线监控算法。
2026-06-23 cs.LO cs.MA
Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete
状态向量加法系统（VASS）可达性问题的复杂性判定是计算机科学中一个长期存在的公开问题。长期以来，这个问题被认为是可判定的，直到今天，它还没有任何复杂性的上限。本文证明了二维的【形】VASS的可达性是PSPACE-完全的。这改善了以前已知的双指数时间界限由豪厄尔，Rosier，Huynh和严在1986年建立。可覆盖性和有界性问题也是PSPACE完备的。此外，对于二维的【形】VASS和整数VASS中的可达性问题，给出了一些复杂性结果。
2014-12-13 cs.CC cs.FL cs.LO
How hard is it to verify flat affine counter systems with the finite monoid property ?
研究了具有由凸多面体定义的保护和由仿射变换定义的更新的计数器系统的几个决策问题。在一般情况下，可达性问题是不可判定的，这样的系统。可判定性可以通过施加两个限制来实现：（i）计数器系统的控制结构是平坦的，这意味着禁止嵌套循环，以及（ii）对于系统中的任何仿射更新矩阵，矩阵幂的集合是有限的。我们提供了严格的复杂性界限，这样的系统的几个决策问题，通过证明过去的线性时序逻辑的可达性和模型检查是完整的第二层的多项式层次$Σ^P_2$，而模型检验一阶逻辑是PSPACE完成。
2016-05-19 cs.CC cs.LO
Maximally Permissive Controlled System Synthesis for Modal Logic
Eindhoven University of Technology（埃因霍温理工大学）
本文提出一种非确定自动机受控系统综合新方法，支持死锁自由、不变量和可达性表达。通过限制Kripke结构的行为，使系统符合模态逻辑要求，实现最大宽容性，融合Ramadge-Wonham监督控制的核心概念。
2014-08-14 cs.FL cs.LO cs.SY
Continuous Pushdown VASS in One Dimension are Easy
本文研究一维下推向量加法系统，通过将计数器更新连续化，证明其可达性、可覆盖性和有界性可在多项式时间内判定，并进一步给出带下界守卫扩展模型的 NP 与 coNP 复杂度结果。
2024-02-20 cs.FL cs.LO
The Reachability Problem for Petri Nets is Not Elementary
Petri网，也被称为向量加法系统，是一种建立已久的并发模型，广泛应用于硬件，软件和数据库系统以及化学，生物和商业过程的建模和分析。Petri网的核心算法问题是可达性：从给定的初始配置是否存在一系列有效的执行步骤，达到给定的最终配置。这个问题的复杂性自20世纪60年代以来一直没有得到解决，它是验证理论中最突出的开放问题之一。可判定性是由Mayr在他的开创性的STOC 1981工作中证明的，目前最好的已发表的上限是LICS 2019的Leroux和Schmitz的非原始递归阿克曼。我们建立了一个非初等的下界，即可达性问题需要一个时间和空间的指数塔。直到这项工作，最好的下界一直是指数空间，由于利普顿在1976年。新的下界是一个重大突破，原因有几个。首先，它表明可达性问题比可覆盖性问题困难得多（即，状态可达性）问题，这也是普遍存在的，但自20世纪70年代后期以来，已知对于指数空间是完备的。其次，它意味着大量的问题，从形式语言，逻辑，并发系统，过程演算和其他领域，这是已知的承认减少从Petri网的可达性问题，也不是基本的。第三，它使目前最好的下界的可达性问题的两个关键扩展的Petri网：分支和下推栈。
2019-04-11 cs.FL cs.LO
