On a reachability set of automaton counter machines

Properties of automaton counter machines are investigated. We prove that reachability sets of automaton one-counter machines are semilinear. An algorithm of construction of these semilinear reachability sets is resulted. Besides, it is shown that reachability sets of reversal-bounded automaton counter machines and reachability sets of flat automaton counter machines are also semilinear.