Approximating bisimulation in one-counter nets

One-counter nets are finite-state machines operating on a variable (counter), which ranges over the natural numbers. Each transition can increase or decrease the counter’s value, and a decrease is possible only if the result is nonnegative; hence, zero testing is not allowed. The class of one-counter nets is equivalent in terms of its expressive power to the class of Petri nets with one unbounded place and to the class of pushdown automata where the stack alphabet contains one symbol. We present a specific method of approximating the largest bisimulation of a one-counter net based on single-periodic arithmetic and the notion of stratified bisimulation.