  We study several extensions of linear-time and computation-tree temporal
logics with quantifiers that allow for counting how often certain properties
hold. For most of these extensions, the model-checking problem is undecidable,
but we show that decidability can be recovered by considering flat Kripke
structures where each state belongs to at most one simple loop. Most decision
procedures are based on results on (flat) counter systems where counters are
used to implement the evaluation of counting operators.
