带长度约束的二次字方程、计数器系统与含整除的Presburger算术
计算机科学中的逻辑
2018-05-18 v1
摘要
字方程是字符串约束求解理论基础中的关键要素,近年来受到大量关注。字方程关联两个关于字符串变量与常量的词。其解是一个将变量映射到常数字符串并使方程左右两边相等的函数。虽然字方程的求解问题是可判定的,但求解带长度约束(即关联字方程中各词长度之约束)的字方程问题的可判定性长期悬而未决。本文关注二次字方程子类,即每个变量至多出现两次。我们首先证明二次字方程解的长度抽象一般不是Presburger可定义的。然后我们描述一类具有Presburger转移关系的计数器系统,其捕获带正则约束的二次字方程的长度抽象。我们给出计数器系统简单循环之效应在带整除的存在Presburger算术(PAD)理论中的编码。由于PAD可判定,我们得到了对于关联计数器系统为\emph{平坦}的(即所有节点属于至多一个环)二次字方程带长度约束的判定过程。我们给出对近来提出的称为正则定向字方程的NP完全字方程片段连同长度约束的可判定性结果(事实上,也是一个带PAD预言机的NP算法)。当约束额外扩展为具有1-弱控制结构的正则约束时,可判定性成立。
引用
@article{arxiv.1805.06701,
title = {Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility},
author = {Anthony W. Lin and Rupak Majumdar},
journal= {arXiv preprint arXiv:1805.06701},
year = {2018}
}
备注
18 pages