带长度约束的二次词方程、计数器系统与带可除性的普雷斯堡算术
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
AI总结：
本文研究带长度约束的二次词方程的可判定性，通过计数器系统与带可除性的普雷斯堡算术编码，证明了平坦情形下可判定，并扩展至正则定向词方程。
摘要：
词方程是字符串约束求解理论基础中的关键要素。词方程涉及两个由字符串变量和常量组成的词。其解是一个函数，将变量映射为常量字符串，使得方程左右两边相等。虽然求解词方程的问题是可判定的，但求解带长度约束（即约束词方程中词的长度的约束）的词方程的可判定性一直是一个长期未解决的开放问题。我们关注二次词方程的子类，即每个变量最多出现两次的方程。我们首先证明二次词方程解的长度抽象通常不是普雷斯堡可定义的。然后，我们描述一类具有普雷斯堡转移关系的计数器系统，该计数器系统能够捕获带正则约束的二次词方程的长度抽象。我们在带可除性的普雷斯堡算术（PAD）的存在性理论中提供了计数器系统简单循环效应的编码。由于PAD是可判定的（NP难且属于NEXP），我们获得了对相关计数器系统是平坦的（即所有节点至多属于一个环）的带长度约束的二次词方程的决策过程。特别地，我们证明了最近提出的词方程的NP完全片段——正则定向词方程——在添加长度约束时的可判定性结果（实际上，也是一个带PAD预言机的NP算法）。我们在存在正则约束的情况下扩展了这一可判定性结果（实际上，具有带PAD预言机的PSPACE复杂度上界）。
英文摘要：
Word equations are a crucial element in the theoretical foundation of constraint solving over strings. A word equation relates two words over string variables and constants. Its solution amounts to a function mapping variables to constant strings that equate the left and right hand sides of the equation. While the problem of solving word equations is decidable, the decidability of the problem of solving a word equation with a length constraint (i.e., a constraint relating the lengths of words in the word equation) has remained a long-standing open problem. We focus on the subclass of quadratic word equations, i.e., in which each variable occurs at most twice. We first show that the length abstractions of solutions to quadratic word equations are in general not Presburger-definable. We then describe a class of counter systems with Presburger transition relations which capture the length abstraction of a quadratic word equation with regular constraints. We provide an encoding of the effect of a simple loop of the counter systems in the existential theory of Presburger Arithmetic with divisibility (PAD). Since PAD is decidable (NP-hard and is in NEXP), we obtain a decision procedure for quadratic words equations with length constraints for which the associated counter system is flat (i.e., all nodes belong to at most one cycle). In particular, we show a decidability result (in fact, also an NP algorithm with a PAD oracle) for a recently proposed NP-complete fragment of word equations called regular-oriented word equations, when augmented with length constraints. We extend this decidability result (in fact, with a complexity upper bound of PSPACE with a PAD oracle) in the presence of regular constraints.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
