Given a formula positive in X, the boundedness problem asks whether the fixpoint induced by the formulas is reached within some uniform bound independent of the structure (i.e.~whether the fixpoint is spurious, and can in fact be captured by a finite unfolding of the formula). In this paper, we study the boundedness problem when the formula is in the guarded fragment or guarded negation fragment of first-order logic, or the fixpoint extensions of these logics. It is known that guarded logics have many desirable computational and model theoretic properties, including in some cases decidable boundedness. We prove that boundedness for guarded negation fixpoint logic is decidable, and even 2exptime-complete. Our proof extends the connection between guarded logics and automata, reducing boundedness 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.
Accepted at LICS 2015. 12 pages.
© 2015 Michael Benedikt, Thomas Colcombet, Balder ten Cate , and Michael Vanden Boom.