We present a general method for proving DP-hardness of
equivalence-checking problems on one-counter automata.
For this we show a reduction of the Sat-Unsat problem to
the truth problem for a fragment of (Presburger) arithmetic.
The fragment contains only special formulas with one free
variable, and is particularly apt for transforming to
simulation-like equivalences on one-counter automata.
In this way we show that the membership problem for any
relation subsuming bisimilarity and subsumed by simulation
preorder is DP-hard (even) for one-counter nets (where the
counter cannot be tested for zero). We also show
DP-hardness for deciding simulation between one-counter
automata and finite-state systems (in both directions).
