  Among the approximation methods for the verification of counter systems, one
of them consists in model-checking their flat unfoldings. Unfortunately, the
complexity characterization of model-checking problems for such operational
models is not always well studied except for reachability queries or for Past
LTL. In this paper, we characterize the complexity of model-checking problems
on flat counter systems for the specification languages including first-order
logic, linear mu-calculus, infinite automata, and related formalisms. Our
results span different complexity classes (mainly from PTime to PSpace) and
they apply to languages in which arithmetical constraints on counter values are
systematically allowed. As far as the proof techniques are concerned, we
provide a uniform approach that focuses on the main issues.
