  Parikh automata extend finite automata by counters that can be tested for
membership in a semilinear set, but only at the end of a run, thereby
preserving many of the desirable algorithmic properties of finite automata.
Here, we study the extension of the classical framework onto infinite inputs:
We introduce reachability, safety, B\"uchi, and co-B\"uchi Parikh automata on
infinite words and study expressiveness, closure properties, and the complexity
of verification problems.
  We show that almost all classes of automata have pairwise incomparable
expressiveness, both in the deterministic and the nondeterministic case; a
result that sharply contrasts with the well-known hierarchy in the
$\omega$-regular setting. Furthermore, emptiness is shown decidable for Parikh
automata with reachability or B\"uchi acceptance, but undecidable for safety
and co-B\"uchi acceptance. Most importantly, we show decidability of model
checking with specifications given by deterministic Parikh automata with safety
or co-B\"uchi acceptance, but also undecidability for all other types of
automata. Finally, solving games is undecidable for all types.
