具有差分约束的可判定Horn系统算法
Decidable Horn Systems with Difference Constraints Arithmetic
摘要：
研究了Horn子句递归系统解的存在性问题，其中二阶变量被解释为整数关系，并利用无量词差界算法.我们从证明问题的可判定性开始“系统有解吗？“对于一类具有一个二阶变量和一个非线性递归规则的简单Horn系统，证明依赖于一个树自动机的建设，承认在加权图对应的每一个展开树的霍恩系统的所有周期。我们约束树识别只有负权重的周期，通过添加一个Presburger公式，利用每个规则被解雇的次数，并减少我们的问题的普适性Presburger约束树自动机。我们研究了这个问题的复杂性，发现它是在\textsc{NEXPtime}与\textsc{EXPtime} -硬下界。其次，我们放弃了单变量的限制，并考虑多变量二阶Horn系统的结构限制，称为\emph{flatness}。这类更一般的霍恩系统被发现是可判定的，在相同的复杂性范围内。最后，我们使用Horn系统对交替分支向量加法系统（ABVASS）的可达性问题进行了编码，并证明了对于平坦ABVASS，该问题是在co- \textsc{NEXPtime}中的。
英文摘要：
This paper tackles the problem of the existence of solutions for recursive systems of Horn clauses with second-order variables interpreted as integer relations, and harnessed by quantifier-free difference bounds arithmetic. We start by proving the decidability of the problem "does the system have a solution ?" for a simple class of Horn systems with one second-order variable and one non-linear recursive rule. The proof relies on a construction of a tree automaton recognizing all cycles in the weighted graph corresponding to every unfolding tree of the Horn system. We constrain the tree to recognize only cycles of negative weight by adding a Presburger formula that harnesses the number of times each rule is fired, and reduce our problem to the universality of a Presburger-constrained tree automaton. We studied the complexity of this problem and found it to be in \textsc{NEXPtime} with an \textsc{EXPtime}-hard lower bound. Second, we drop the univariate restriction and consider multivariate second-order Horn systems with a structural restriction, called \emph{flatness}. This more general class of Horn systems is found to be decidable, within the same complexity bounds. Finally, we encode the reachability problem for Alternating Branching Vector Addition Systems (ABVASS) using Horn systems and prove that, for flat ABVASS, this problem is in co-\textsc{NEXPtime}.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
