Complexity of the Ackermann fragment with one leading existential quantifier
本文证明了带一个前导存在量词的Ackermann片段的可满足性问题是ExpTime-完全的。
2022-01-30 cs.LO
Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
自动结构是由同步有限状态自动机表示的无限结构。本文关注有限词和树（排名/排名）的自动结构。我们调查的“有向版本”的拉姆齐量词，它表示存在一个无限的有向集团。这包含了拉姆齐量词的标准“无向版本”。首先观察到Ramsey量词与验证中的两个问题之间的有趣联系：（1）规则模型检验中Büchi和广义Büchi条件的可达性可以看作是传递自动图上的Ramsey量化（即，其边关系是传递的），（2）检查一元可分解性（a.k.a.可识别性）可以被看作是在共传递自动图上的Ramsey量化（即，其边关系是传递的补集）。我们提供了一个全面的复杂性景观拉姆齐量词在这三种情况下（一般，传递，共传递），所有NL和EXP之间。反过来，这产生了大量具有精确复杂性的新结果，例如，子树/扁平前缀重写的验证，以及树自动关系上的一元分解。我们还获得了相当简单的证明，例如，对于词自动关系上的一元可分解性的NL复杂度（由DFA给出）。
2023-02-13 cs.LO
Reachability relations of timed pushdown automata
时间下推自动机（TPDA）是一种将递归与时间约束逻辑相结合的表达形式。我们证明了TPDA的可达性关系可以用线性算术表示，这是一种丰富的逻辑，推广了Presburger算术和有理算术。的主要技术成分是一个新的量词消去结果的时钟约束（用于简化TPDA转换的语法），使用时钟差关系来表达的分数时钟值的可达性关系，和应用帕里克定理重建的积分时钟值。
2020-12-30 cs.FL cs.LO
Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat
本文研究了带计数量词的两变量片段中加权一阶模型计数（WFOMC）的时间复杂度，指出现有方法的单元数量对计数量词参数呈指数依赖，并提出一种新方法将其降为二次依赖，获得更紧的上界，成为待超越的界限。
2024-08-23 cs.LO
The Complexity of Reachability in Parametric Markov Decision Processes
本文介绍了参数马尔可夫决策过程（pMDP）的可达性决策问题的复杂性，马尔可夫决策过程（MDP）的扩展，其中转移概率由多项式描述的一个有限的参数集。特别是，我们研究了这些参数的值，使诱导MDP满足一些最大或最小的可达性概率约束的复杂性。我们讨论不同的变体取决于比较运算符的约束和域的参数值。我们改进了所有已知的下界这个问题，并特别提供了ETR的完整性结果，这个问题的不同变体。
2020-09-28 cs.LO
The Cost of Parameterized Reachability in Mobile Ad Hoc Networks
我们调查的影响，自发运动的复杂性验证问题的自动机为基础的协议模型的网络与选择性广播通信。我们首先考虑错误状态的可达性，并证明参数化验证是可判定的多项式复杂性。然后，我们转向更丰富的查询，并显示当考虑具有否定或基数约束的属性时，复杂性如何变化。
2012-02-27 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
Taming Past LTL and Flat Counter Systems
平面计数器系统的可达性和LTL模型检测问题是已知的可判定的，但可达性问题可以用NP表示，后一个问题的最著名的复杂性上限是由几个指数组成的塔。在这里，我们表明，这个问题是NP完全的，即使LTL承认过去的时间运营商和计数器上的算术约束。实际上，NP上界是通过适当地结合过去LTL的一个新的口吃定理和无量词Presburger公式的小整数解的性质而得到的。其他复杂性的结果证明，例如限制类的平面计数器系统。
2013-02-08 cs.LO
The Dynamic Descriptive Complexity of k-Clique
在这项工作中的动态描述复杂性的k团查询进行了研究。它表明，当边缘可能只插入然后k-团可以保持由一个量化器免费更新程序的arity k-1，但它不能保持由一个量化器免费更新程序arity k-2（即使在存在的一元辅助函数）。这为插入下的无量词更新程序的图查询建立了一个arity层次结构。下界的证明使用Ramsey数的上界和下界。
2016-10-28 cs.LO
Vector Addition System Reversible Reachability Problem
向量加法系统的可达性问题是网理论的一个中心问题。这个问题已知是可判定的，但其复杂性仍然未知。而这个问题是EXPSPACE-硬的，没有基本的上限复杂性是已知的。在本文中，我们考虑可逆的可达性问题。这个问题包括决定两个配置是否彼此可达，或者等价地，如果它们在可达图的同一个强连通分量中。我们证明了这个问题是EXPSPACE完全的。作为所介绍的材料的应用，我们描述了一个矢量加法系统的可逆域。
2013-02-26 cs.LO
Complexity of the Guarded Two-Variable Fragment with Counting Quantifiers
该研究证明带计数量词的受护两变量片段的有限可满足性问题属于EXPTIME复杂度类，所用方法还为Kazakov近期提出的该片段可满足性问题属EXPTIME的结论给出了简单证明。
2006-01-26 cs.CC cs.LO
The Reachability Problem for Petri Nets is Not Primitive Recursive
我们提供了一个阿克曼复杂性下界检查程序的可达性问题，一个模型相当于Petri网。此外，在固定维数的$2d+4$中，我们证明了该问题是$\mathbb{F}_d$ -困难的.作为一个直接的推论，10维中的可达性问题不是基本的。
2021-09-02 cs.LO
Reachability is Tower Complete
向量加法系统可达性问题复杂性的完整刻画一直是一个悬而未决的问题。问题显示为塔完成。
2020-03-21 cs.LO
Small Term Reachability and Related Problems for Terminating Term Rewriting Systems
本文研究终止项重写系统中是否可到达大小不超过 n 的项，按终止性证明方法给出 NP、N2ExpTime/NExpTime 与 PSpace 等复杂性分类，并分析合流性及大项变体的影响。
2025-10-14 cs.LO
Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic
从计算复杂性的角度研究了分支时间逻辑CTL的可满足性问题。严格的上限和下限提供了每个时间操作符片段。在平行，最小模型的大小进行了研究，一个合适的概念极小。第三，研究了平坦的CTL，即，时态运算符嵌套深度非常低的公式。在复杂性和最小模型方面显示出尖锐的二分法：时间深度1具有低表达能力，而时间深度2相当于完整的CTL。
2017-02-24 cs.CC cs.LO
Dependence logic with a majority quantifier
本文研究了有限结构上依赖逻辑D的择多量词M的扩张。我们表明，由此产生的逻辑是equi-expressive与二阶逻辑的扩展，由二阶多数量词的所有种族。我们的结果意味着，从描述复杂性理论的角度来看，D（M）捕获的复杂性类计数层次。
2013-03-08 cs.LO math.LO
On The Complexity of Counter Reachability Games
对抗可达性博弈是由两个玩家在一个带有标签边的图上进行的。每次移动包括从当前位置拾取一条边，并将其标签添加到一个反向量。目标是在给定位置达到给定的计数器值。我们区分三种语义计数器可达性游戏，根据发生什么时，计数器值将成为负的：边缘被禁用，或启用，但计数器值变为零，或启用。我们考虑的问题，决定在计数器可达性游戏的赢家，并表明，在大多数情况下，它具有相同的复杂性下的所有语义。令人惊讶的是，在一种语义下，维度1的复杂性取决于目标值是零还是任何其他整数。
2013-07-19 cs.GT cs.LO
Data-Complexity of the Two-Variable Fragment with Counting Quantifiers
本文确定了带计数量词的两变量片段及其守护片段在数据复杂度上的精确界限，分别达到NP完全和co-NP完全。
2008-06-10 cs.AI cs.CC cs.LO
On the Complexity of Reachability in Parametric Markov Decision Processes
本文研究了参数马尔可夫决策过程（pMDP），它是马尔可夫决策过程（MDP）的一种扩展，其中转移概率由有限参数集上的多项式描述。固定所有参数的值会产生MDP。特别是，本文研究了这些参数的值，使诱导MDP满足一些可达性约束的复杂性。我们讨论不同的变体取决于比较运算符的约束和域的参数值。我们改进了该问题的所有已知下界，并特别提供了该问题不同变体的ETR完整性结果。此外，我们提供的见解在功能描述诱导可达性概率，以及如何pMDPs概括并发随机可达性游戏。
2019-04-02 cs.CC cs.LO
Reachability for dynamic parametric processes
在动态参数化过程中，每个子过程可以产生任意多个相同的子过程，这些子过程可以通过全局变量或与其父过程共享的局部变量进行通信。我们证明了动态参数过程的可达性在温和的假设下是可判定的。例如，如果各个过程由下推系统或甚至更高阶的下推系统实现，则满足这些假设。我们还提供了下推动态参数过程的子类的算法，与NP和DEXPTIME之间的复杂性。
2016-09-17 cs.LO
On the freeze quantifier in Constraint LTL: decidability and complexity
约束LTL是LTL在Presburger约束上的推广，通常被用作一种形式语言来描述具有约束的操作模型的行为。冻结量词可以是语言的一部分，如在一些实时逻辑中，但这种变量绑定机制在许多逻辑语言中（一阶时态逻辑，混合逻辑，序列图逻辑，导航逻辑，具有抽象的逻辑等）是相当普遍和普遍的。我们表明，约束LTL在简单的域（N，=）增加了冻结量词是不可判定的，这是一个令人惊讶的结果，鉴于穷人的语言约束（只有平等测试）。许多版本的无冻结约束LTL在具有定性谓词的域上是可判定的，我们的不可判定性结果实际上建立了Sigma_1^1-完备性。在积极的一面，我们提供的复杂性结果时，域是有限的（EXPSPACE-完备性）或当公式是平坦的，在某种意义上介绍的文件。我们的不可判定性的结果是尖锐的（即限制变量的数量），我们所有的复杂性特征确保完整性方面的一些复杂性类（主要是PSPACE和EXPSPACE）。
2006-09-29 cs.CC cs.LO
Dynamic Complexity of Parity Exists Queries
研究奇偶存在查询在动态复杂度框架中的可维护性，证明其无法用无量词一阶规则维护，但度受限变体可用完整一阶规则维护。
2021-11-15 cs.LO
Petri Net Reachability Graphs: Decidability Status of First Order Properties
我们调查的可判定性和复杂性状态的模型检查问题的无标签的可达图的Petri网，考虑一阶和模态语言没有标签的过渡或原子命题标记。我们考虑几个参数来区分可判定问题和不可判定问题。我们不仅能够提供精确的边界和系统的分析，而且还展示了我们证明技术的鲁棒性。
2012-10-19 cs.LO
The surprizing complexity of generalized reachability games
图上的游戏为反应系统提供了一个自然而强大的模型。在本文中，我们考虑广义可达目标，定义为合取的可达目标。我们首先证明，在这样的游戏中，决定赢家是$\PSPACE$ -完全的，虽然它是固定参数易处理的可达性目标的数量作为参数。此外，我们考虑了两个球员的记忆要求，并给出匹配的上界和下界的大小获胜的策略。为了允许更有效的算法，我们考虑广义可达性游戏的子类。我们表明，边界的可达集的大小给出了两个自然的子类，决定赢家可以有效地完成。
2012-02-03 cs.CC cs.GT cs.LO
The Complexity of Reachability Problems for Flat Counter Machines with Periodic Loops
本文证明了NP-完全性的可达性问题的类平面计数器的不同的界限，更一般地说，八边形关系，标签上的转变的循环。证明是基于这样的事实，即这种关系的功率序列$\{R^i\}_{i=1}^\infty$可以被编码为矩阵的周期序列，并且该序列的前缀和周期都是关系$R$的二进制编码$\bin{R}$的大小的$2^{\mathcal{O}(\bin{R})}$。这一结果允许表征计数器机器\cite{cav10,comon-jurski98}的最研究的类之一的可达性问题的复杂性，并具有潜在的影响，在程序验证的其他问题。
2016-02-14 cs.CC cs.LO
Existential Second-Order Logic Over Graphs: Parameterized Complexity
本文研究图上 ESO 公式按一阶量词序列分类的参数化复杂度，以二阶量化集合大小为参数，完整刻画各序列的复杂度高低及可处理性分界。
2023-10-02 cs.CC cs.LO
The Descriptive Complexity of Subgraph Isomorphism without Numerics
令$F$是一个具有$\ell$顶点的连通图。同构于$F$的子图的存在性可以在量词深度不比$\ell$好的一阶逻辑中定义，这仅仅是因为没有更小量词深度的一阶公式可以区分完全图$K_\ell$和$K_{\ell-1}$。证明了对某些$F$，\emph{sufficiently large}连通图中$F$子图的存在性是可用量词深度$\ell-3$定义的.另一方面，如果量词深度优于$\ell/2$，这是不可能的。然而，如果我们考虑具有足够大树宽的连通图上的定义，则对于某些$F$，量词深度可以与$\ell$相比任意小，但永远不会小于$F$的树宽。此外，高连通图上的定义要求量词深度严格大于$F$的密度。最后，我们确定了这些描述复杂性参数的确切值为所有连接模式图$F$的4个顶点。
2017-09-11 cs.CC cs.LO
The Complexity of Limited Belief Reasoning -- The Quantifier-Free Case
Fudan University（复旦大学）；Australian National University（澳大利亚国立大学）；University of New South Wales（新南威尔士大学）
认知逻辑的经典观点是，主体知道其知识库的所有逻辑结果。这种逻辑全知的假设通常是不现实的，并且使得推理在计算上难以处理。避免逻辑全知全能的一种方法是将推理限制在一定的信念水平，这直观地衡量了推理的深度。“本文研究了具有置信水平的推理的计算复杂性。首先，我们表明，虽然推理仍然听话，如果水平是恒定的，复杂性跳跃到PSPACE完成-也就是说，超越经典推理-当信仰水平是输入的一部分。然后，我们进一步细化的图片使用参数化的复杂性理论，研究如何信念水平和非逻辑符号的数量影响的复杂性。
2018-05-08 cs.AI cs.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
The Complexity of Reachability in Affine Vector Addition Systems with States
该研究刻画了仿射VASS中整数可达性的复杂性，给出三分法：重置类NP完全，转移/复制类PSPACE完全，其余不可判定；标准可达性仅置换类可判定，并探讨了固定实例的复杂性任意性。
2021-07-19 cs.CC cs.FL cs.LO
Flatness and Complexity of Immediate Observation Petri Nets
在以前的论文中，我们介绍了即时观察（IO）Petri网，一类感兴趣的研究人口协议和酶化学网络。在本文的第一部分中，我们表明，IO网是全球平坦的，所以他们的安全性能可以检查有效的符号模型检验工具，使用加速技术，如FAST。在第二部分中，我们研究了分支IO网（BIO网），其转换可以创建令牌。BIO网扩展了IO网和无通信网，也称为BPP网，这是一个广泛研究的类别。我们表明，虽然BIO网不再是全球平坦的，他们的可达标记集可能是非半线性的，他们仍然是局部平坦的。因此，BIO网的可覆盖性和可达性问题，甚至是它们的某个集合参数化版本，都在PSPACE中。这使得BIO网的第一个自然网类与非半线性可达性关系，可达性问题是可证明的简单比一般的Petri网。
2020-07-21 cs.LO
On the Descriptive Complexity of Vertex Deletion Problems
本文基于一阶逻辑公式的单个量词模式将顶点删除问题的复杂性从二分法细化为三分法，揭示了新的可处理片段及不同图类型下的可处理边界差异。
2024-06-26 cs.CC 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
The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes
Technische Universität Darmstadt（达姆施塔特工业大学）；Université libre de Bruxelles（布鲁塞尔自由大学）；Departement d’Informatique（计算机系）
研究了具有无限时域可达性目标的马尔可夫决策过程的永不变差关系。如果从p到达目标状态集的最大概率至多与从q到达的最大概率相同，则状态q永远不会比状态p差，而不考虑标记转移的概率。极端概率态、终结分量和本质态都是由NWR导出的等价关系的特例。使用NWR，可以折叠相同等价类中的状态。然后，可以移除导致次优状态的动作。我们证明了与计算NWR相关的自然决策问题是CONP完全的。最后，我们扩展了以前已知的不完全多项式时间迭代算法下近似的NWR。
2018-02-24 cs.AI cs.LO
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
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games
本文研究定量可达性博弈中SPE的复杂性，证明约束存在性问题是PSPACE完全的，并提出一种通过迭代约束至不动点来刻画SPE结果集的新算法。
2020-11-04 cs.GT cs.LO
Generalized Complexity of ALC Subsumption
描述逻辑ALC中关于术语的包含问题是EXPTIME完全的。我们调查的计算复杂性的片段，这个问题的允许布尔运算符。在这里，我们利用克隆的概念在波斯特格的上下文中。此外，我们认为所有四个可能的量词组合的克隆参数化的每个片段。我们将看到，根据可用的量词，分类将是三分的或四分的。
2012-05-03 cs.CC cs.LO
Team Semantics and Recursive Enumerability
众所周知，依赖逻辑捕获复杂性类NP，最近已经表明，包含逻辑捕获有序模型上的P。这些结果表明，团队语义描述复杂性理论提供了有趣的新的可能性。为了正确理解团队语义和描述复杂性之间的联系，我们引入了依赖逻辑的扩展D*，它可以精确定义有限模型的所有递归可重复类。因此，D* 提供了一种替代图灵机的计算方法。D* 的基本新功能是一个运营商，可以扩展域所考虑的模型由有限数量的新鲜元素。由于广义量词与神谕之间的密切关系，我们也研究了广义量词在团队语义中的应用。我们证明了通过引入相应的广义依赖原子，可以从一阶逻辑的量词扩张中规范地消除（1）型单调量词。
2014-08-18 cs.LO math.LO
Strategy Complexity of Concurrent Stochastic Games with Safety and Reachability Objectives
我们考虑有限状态并发随机博弈，由k>=2个参与者进行无限轮的博弈，其中在每一轮中，每个参与者同时且独立于其他参与者选择一个行动，此后，后继状态由当前状态和所选择的行动给出的概率分布确定。我们认为可达性目标，给定的目标集的状态要求，在目标中的一些状态被访问，和双重安全目标，给定的目标集要求，只有在目标集中的状态被访问。我们感兴趣的是固定策略的复杂性，衡量他们的耐心，这是定义为最小的非零概率的倒数。我们的主要结果如下：我们证明了在两人零和并发随机对策中，（一个局中人的可达性目标和另一个局中人的互补安全目标）：（i）对于两个局中人，最优策略和ε-最优策略的耐心的最优界都是双指数的;和（ii）即使在一个单一的非吸收状态指数（在行动的数量）耐心的游戏是必要的。在一般情况下，我们研究类的非零和游戏承认固定的ε-纳什均衡。我们证明了如果至少有一个局中人具有可达性目标，那么双指数耐心可能是必需的双-纳什均衡策略，而与此相反，如果所有局中人都具有安全目标，则双-纳什均衡策略的最优耐心界限仅是指数的。
2015-06-08 cs.GT cs.LO
Reachability analysis of first-order definable pushdown systems
我们研究下推系统的控制状态，堆栈字母表，和过渡关系，而不是有限的，是一阶定义在一个固定的可数无限结构。我们表明，可达性分析可以解决与众所周知的饱和技术的广泛的一类寡纯结构。此外，对于更严格的齐次结构，我们能够给出具体的复杂性上界。我们展示了充分的适用性，我们的技术提出了几个具体的例子，同质结构，包含，最佳的复杂性，从文献中已知的结果。我们表明，无穷多个这样的例子，可以得到均匀结构与经典的圈产品建设。
2015-07-17 cs.FL cs.LO
Quantifier Elimination Meets Treewidth
KLSS, Institute of Software Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；University of Oxford（牛津大学）；National Key Laboratory of Space Integrated Information System, Institute of Software Chinese Academy of Sciences（空间信息集成系统国家重点实验室，中国科学院软件研究所）；School of Mathematical Sciences, Peking University（北京大学数学科学学院）；School of Computer Science, Peking University（北京大学计算机学院）；Zhongguancun Laboratory（中关村实验室）
本文提出利用树宽参数的动态规划框架，通过量化消除过程中的结构稀疏性，将FME和CAD的复杂度从双指数降低到单指数。
2026-01-16 cs.CC cs.LO cs.SC
Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes
研究了具有状态的向量加法系统（VASSes）在固定维数下的可达性问题的复杂性。我们提供了四个改进目前已知的现有技术的下界：1）\np -一元平坦$4$ -血管（维度4中的血管）的硬度，2）\pspace -一元$5$ -血管的硬度，3）\expspace -二元$6$ -血管的硬度，和4）\tower -一元$8$ -血管的硬度。
2022-03-08 cs.FL cs.LO
Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
针对带嵌套零检测的VASS可达性问题，本文得出Ackermann型上界，并提出统一方法以相同复杂度解决半线性性、可分离性等相关问题，填补了普通VASS部分问题的复杂度研究空白。
2025-05-19 cs.FL cs.LO
Galois correspondence for counting quantifiers
我们介绍了一种新的类型的封闭操作的关系，最大实现，其较弱的模拟最大量化。然后，我们证明了这两种类型的封闭算子之间的近似保持减少计数约束满足问题（#CSP）。与以前的一些结果一起，这意味着计算CSP的近似复杂性由在这些新类型的闭包算子下另外闭合的关系的部分克隆决定。各种各样的伽罗瓦对应在CSP复杂性的研究中被证明是非常有用的。虽然我们无法确定在最大实现和最大量化下关闭的部分克隆的伽罗瓦对应关系，但我们获得了稍微不同类型的闭包算子，k-存在量化的结果。这种类型的量词在模型论中被称为计数量词，通常用于增强一阶逻辑语言。我们刻画了在k-存在量化下闭的关系的部分克隆为在满足k-子集满射性条件的部分函数集下不变的关系集。最后，我们给出了布尔极大共克隆的描述，即在极大实现下闭的{0，1}上的关系集。
2012-10-11 cs.CC 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
Craig Interpolation for Quantifier-Free Presburger Arithmetic
克雷格插值已成为一个通用的算法工具，以提高软件验证。例如，插值可以加速无限状态系统的不动点计算的收敛。它们还有助于改进迭代计算的惰性抽象的细化。有效的插值程序已经提出了只有少数理论。本文给出了一种完全的无量词Presburger算术公式的插值方法。我们提出了一个新的凸变量投影整数不等式和技术，将它们与等式。插值的推导在反驳证明的规模上具有低次多项式的复杂性，并且在实践中通常是快速的。
2008-11-21 cs.LO cs.SC
Embedded Finite Models Beyond Restricted Quantifier Collapse
该研究突破嵌入有限模型论的两种极端认知，证明可判定结构内逻辑求值复杂度范围极广且表达能力与复杂度可脱节，还证实有限域等理论不满足量词坍缩并给出域理论判定复杂度新下界。
2024-05-20 cs.LO math.LO
Dynamic Meta-theorems for Distance and Matching
可达性，距离和匹配是近年来动态复杂性理论特别感兴趣的一些最基本的图问题[DKMSZ 18，DMVZ 18，DKMTVZ 20]。可达性可以用一阶更新公式来维护，或者等价地在DynFO中具有n个节点的一般图中[DKMSZ 18]，即使在每步O（log n/loglog n）变化[DMVZ 18]。在可以处理多大数量的更改的上下文中，最近已经表明[DKMTVZ 20]，在多对数数量的更改下，可达性在DynFOpar中在平面，有界树宽和相关的图形类中-实际上在任何图形中，可以在NC中计算小的非零循环权重。我们继续这条线的调查，并延长元定理的可达性的距离和二部最大匹配相同的界限。这些是已知的最一般的图类，我们可以在不使用多数量词的情况下确定性地维护这些问题，甚至维护证人。对于二分匹配结果，我们改进了[FGT]的方法，将静态非零循环权值转换为动态匹配隔离权值。虽然可达性是在DynFOar下O（log n/loglog n）的变化，没有这样的界限是已知的距离或匹配在任何非平凡类的图下的非常数的变化。我们发现，在相同的类的图之前，二部最大匹配是在DynFOar下O（log n/loglog n）的变化每一步。在展示这一点的过程中，我们证明了矩阵的秩可以在DynFOar中保持，也可以在O（log n/loglog n）条目更改下保持，改进了以前的O（1）界[DKMSZ 18]。这意味着对一般图中最…
2021-09-07 cs.CC cs.LO
The Complexity of Concurrent Rational Synthesis
在本文中，我们研究了合理的合成问题的并发博弈结构的各种目标，从可达性的Muller条件。我们提出了一个新的算法，建立了非合作的理性综合问题，完全依赖于博弈论技术，而不是以前的方法，是基于逻辑的可判定性。由于这种方法，我们构建了一个零和回合制游戏，可以适应上述每一个目标，从而获得新的复杂性结果。特别是，我们表明，可达性，安全性，Büchi，和合作Büchi条件是PSpace完全的，穆勒，街，和拉宾是PSpace硬和ExpTime。
2018-06-08 cs.GT cs.LO
Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality
均匀一维片段UF 1 ^=是从一阶逻辑中获得的一种形式，通过将量化限制在存在（全称）量词块的应用中，使得在量化公式中最多有一个变量保持自由。片段在布尔运算下是闭合的，但附加的限制（称为一致性条件）适用于具有两个或多个变量的原子公式的组合。这个片段可以被看作是二元逻辑的规范化推广，定义它是为了能够处理任意的关系。最近引入了分片的概念，并证明了UF 1 ^=的无等式分片的可满足性问题是可判定的.本文证明了UF 1 ^=的可满足性和有限可满足性问题是NEXPTIME-完全的。我们还证明了具有计数量词的扩展UF ^=的相应问题是不可判定的。除了可判定性问题，我们还比较了UF ^=和二元逻辑与计数量词FOC^2的表达性。我们表明，虽然逻辑一般来说是不可比较的，但当注意力仅限于元数界为二的词汇时，UF 1 ^=严格包含在FOC^2中。
2014-09-02 cs.LO math.LO
The Complexity of Weighted Counting for Acyclic Conjunctive Queries
本文研究非循环合取查询解的加权计数问题（$\ACQ$）。这个问题的未加权量词自由版本已知是易于处理的（对于组合复杂性），但也知道即使引入单个量化变量也会使其成为$\sP$ -困难。我们首先表明，量化器免费$\ACQ$的加权计数仍然是易处理的，即使是最低限度的扩展问题导致硬的情况下。然后，我们引入了一个新的参数量化查询，允许隔离大岛屿的易处理性。我们表明，从参数化的复杂性的标准假设，这个参数充分表征计数加权解决方案的$\ACQ$查询听话的子类。因此，我们完全确定了$\ACQ$加权计数的易处理边界。
2011-12-07 cs.CC cs.LO math.LO
Proof Complexity of Symbolic QBF Reasoning
CNRS（法国国家科学研究中心）；Univ. Artois（阿尔图瓦大学）；TU Wien（维也纳工业大学）
我们介绍和调查量化布尔公式（QBF）的符号证明系统的有序二元决策图（OBDDs）。这些系统捕获执行符号量词消去的QBF求解器，并因此承认有界路径宽度和量词复杂性的公式的简短证明。因此，我们从标准子句证明系统中获得指数分离，特别是（长距离）QU-Resolution和IR-Calc。我们进一步开发了一个下界技术的符号QBF证明系统的基础上，从通信复杂性的战略提取，升降机已知的下界。这使我们能够推导出强大的下界对符号QBF证明系统是独立的变量排序的基础OBDDs，并举行，即使证明系统被允许访问一个NP-预言。
2021-04-06 cs.AI cs.CC cs.LO
Logical complexity of graphs: a survey
本文讨论了一阶逻辑中有限图的可定义性，它具有两个表示顶点邻接和相等的关系符号。图$G$的逻辑深度$D(G)$等于定义$G$直到同构的句子的最小量词深度。逻辑宽度$W(G)$是在这样的句子中出现的变量的最小数目。逻辑长度$L(G)$是最短定义语句的长度。我们调查已知的估计，这些图的参数，并讨论他们的关系到其他主题（如效率的Weisfeiler-Lehman算法在同构测试，随机图的演变，定量特征的零一律，或贡献的弗兰克拉姆齐的研究希尔伯特的Entscheidungsproblem）。此外，我们跟踪一个图的描述性复杂性的行为，因为逻辑变得更加严格（例如，只允许定义有限数量的变量或量词交替）或更可表达（后与计数量词供电）。
2013-04-29 cs.CC cs.LO math.CO
Reachability is in DynFO
Patnaik和Immerman介绍了数据库查询的动态复杂度类DynFO，它可以通过一阶动态程序在边的插入和删除下借助辅助关系来维护（Patnaik和Immerman 1997）。这篇文章证实了他们的猜想，可达性查询是在DynFO。作为一个副产品，它示出了具有小值的矩阵的秩可以在DynFO（+，x）中保持。它进一步表明，（的大小）最大匹配的图可以保持在非均匀DynFO，DynFO的另一个扩展，与非均匀初始化的辅助关系。
2017-04-05 cs.CC cs.DS cs.LO
