Simulation and bisimulation over one-counter processes

摘要

We show an effective construction of (a periodicity description of) the maximal simulation relation for a given one-counter net. then we demonstrate how to reduce simulation problems over one-counter nets to analogous bisimulation problems over one-counter automata. we use this to demonstrate the decidability of various problems, specifically testing regularity and strong regularity of one-counter nets with respect to simulation equivalence, and testing simulation equivalence between a one-counter net and a deterministic pushdown automaton. various obvious generalisations of these problems are known to be undecidable.