## The Complexity of Boundedness for Guarded Logics

* Michael
Benedikt*, * Thomas Colcombet *, * Balder ten Cate * and * Michael Vanden Boom*
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.