One Deterministic-Counter Automata

We introduce one deterministic-counter automata (ODCA), which are one-counter automata where all runs labelled by a given word have the same counter effect, a property we call counter-determinacy. ODCAs are an extension of visibly one-counter automata - one-counter automata (OCA), where the input alphabet determines the actions on the counter. They are a natural way to introduce non-determinism/weights to OCAs while maintaining the decidability of crucial problems, that are undecidable on general OCAs. For example, the equivalence problem is decidable for deterministic OCAs whereas it is undecidable for non-deterministic OCAs. We consider both non-deterministic and weighted ODCAs. This work shows that the equivalence problem is decidable in polynomial time for weighted ODCAs over a field and polynomial space for non-deterministic ODCAs. As a corollary, we get that the regularity problem, i.e., the problem of checking whether an input weighted ODCA is equivalent to some weighted automaton, is also in polynomial time. Furthermore, we show that the covering and coverable equivalence problems for uninitialised weighted ODCAs are decidable in polynomial time. We also introduce a few reachability problems that are of independent interest and show that they are in P. These reachability problems later help in solving the equivalence problem.