On a class of counter machines

In this paper we propose abstract counter machines as a general framework for analysing state systems with counters. We use this framework to define weak counter machines and a new class of counter machines — automaton counter machines which can be modeled by Communicating Coloured Automata (introduced in [11]). Particular emphasis has been placed on comparing automaton counter machines with weak counter machines which can be modeled by Petri nets. We show undecidability of boundedness, inclusion, equivalence and a special case of reachability for automaton counter machines. This implies that the same holds for Communicating Colouring Automata.