The Complexity of Boundedness for Guarded Logics

Given a formula phi(x, X) positive in X, the bounded ness problem asks whether the fix point induced by phi is reached within some uniform bound independent of the structure (i.e. Whether the fix point is spurious, and can in fact be captured by a finite unfolding of the formula). In this paper, we study the bounded ness problem when phi is in the guarded fragment or guarded negation fragment of first-order logic, or the fix point extensions of these logics. It is known that guarded logics have many desirable computational and model theoretic properties, including in some cases decidable bounded ness. We prove that bounded ness for the guarded negation fragment is decidable in elementary time, and, making use of an unpublished result of Colcombet, even 2EXPTIME-complete. Our proof extends the connection between guarded logics and automata, reducing bounded ness for guarded logics to a question about cost automata on trees, a type of automaton with counters that assigns a natural number to each input rather than just a boolean.