On the Efficient Representation of an Unbounded Resource with the Aid of One-Counter Circuits

A class of infinite-state automata with a simple periodic behaviour and a convenient graphical representation is studied. A positive one-counter circuit is defined as a strongly connected one-counter net (one-counter nondeterministic finite automata without zero-testing) with at least one positive cycle. It is shown that in a positive circuit an infinite part of a reachability set is an arithmetic progression; numerical properties of this progression are estimated. A specific graphical representation of circuits is presented. General one-counter nets are equivalent to Petri Nets with at most one unbounded place and to pushdown automata with a single-symbol stack alphabet. It is shown that an arbitrary one-counter net can be represented by a finite tree of circuits. A one-counter net is called sound, if a counter is used only for “infinite-state” (periodic) behaviour. It is shown that for an arbitrary one-counter net an equivalent sound net can be effectively constructed from the corresponding tree of circuits.