This article is cited in 3 papers

On a class of counter machines

E. V. Kuzmin, D. Yu. Chalyy

P. G. Demidov Yaroslavl State University

Abstract: 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.

Keywords: abstract counter machines, automaton counter machine, Communicating Colouring Automata, verification, decidability.

UDC: 519.7

Received: 20.03.2009