Decidable Horn Systems with Difference Constraints Arithmetic

TL;DR

This paper establishes the decidability of solution existence for certain recursive Horn systems with difference constraints, introduces a tree automaton approach, and explores complexity bounds for these systems and related models.

Contribution

It proves decidability for a class of Horn systems with difference bounds, extends results to multivariate cases with flatness restriction, and encodes ABVASS reachability within this framework.

Findings

Decidability of solution existence for simple Horn systems with difference constraints.

Complexity bounds in NEXPtime and EXPtime for various classes of Horn systems.

Encoding of ABVASS reachability problems into Horn systems with flatness restriction.

Abstract

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}.