Counter systems are a well-known and powerful modeling notation for
specifying infinite-state systems.  In this paper we target the problem
of checking liveness properties in counter systems.  We propose two semi
decision techniques towards this, both of which return a formula that
encodes the set of reachable states of the system that satisfy a given
liveness property. A novel aspect of our techniques is that they
use reachability analysis techniques, which are well studied in the
literature, as black boxes, and are hence able to compute precise answers
on a much wider class of systems than previous approaches for the same
problem.  Secondly, they compute their results by iterative expansion or
contraction, and hence permit an approximate solution to be obtained at any
point.  We state the formal properties of our techniques, and also provide
experimental results using standard benchmarks to show the usefulness of
our approaches. Finally, we sketch an extension of our liveness checking
approach to check general CTL properties.