  In a one-counter automaton (OCA), one can produce a letter from some finite
alphabet, increment and decrement the counter by one, or compare it with
constants up to some threshold. It is well-known that universality and language
inclusion for OCAs are undecidable. In this paper, we consider OCAs with
counter observability: Whenever the automaton produces a letter, it outputs the
current counter value along with it. Hence, its language is now a set of words
over an infinite alphabet. We show that universality and inclusion for that
model are PSPACE-complete, thus no harder than the corresponding problems for
finite automata. In fact, by establishing a link with visibly one-counter
automata, we show that OCAs with counter observability are effectively
determinizable and closed under all boolean operations.
