Hanf normal form for first-order logic with unary counting quantifiers

We study the existence of Hanf normal forms for extensions FO(Q) of first-order logic by sets Q subset of P(N) of unary counting quantifiers. A formula is in Hanf normal form if it is a Boolean combination of formulas zeta (x(overbar)) describing the isomorphism type of a local neighbourhood around its free variables x and statements of the form "the number of witnesses y of psi (y) belongs to (Q+k)" where Q is an element of Q, k is an element of N, and psi describes the isomorphism type of a local neighbourhood around its unique free variable y. We show that a formula from FO(Q) can be transformed into a formula in Hanf normal form that is equivalent on all structures of degree <= d if, and only if, all counting quantifiers occurring in the formula are ultimately periodic. This transformation can be carried out in worst-case optimal 3-fold exponential time. In particular, this yields an algorithmic version of Nurmonen's extension of Hanf's theorem for first-order logic with modulo-counting quantifiers. As an immediate consequence, we obtain that on finite structures of degree <= d, model checking of first-order logic with modulo-counting quantifiers is fixed-parameter tractable.