In [ABLS01], one addresses the problem of verifying safety and liveness properties of infinite-state systems, using symbolic reachability analysis. The models that are considered are fair parametric extended automata, i.e., counter automata with parametric guards, supplied with fairness conditions on their transitions. In previous work, it has been shown that symbolic reachability analysis using acceleration techniques can be used to generate finite abstractions (symbolic graphs) of the original infinite-state model. In this work, it is shown that this analysis can be also used to introduce fairness conditions on the generated abstract model allowing to model-check liveness properties. It is shown first how to translate faithfully the fairness conditions of the infinite-state original model to conditions on the generated finite symbolic graph. Then, it is shown that one can also synthesize automatically new fairness conditions allowing to eliminate infinite paths in the symbolic graph which do not correspond to valid behaviors in the original model. These infinite paths correspond to abstractions of boundedly iterable (nested) loops. Techniques are given for deciding this bounded iterability for a class of components in the symbolic graph. The application of these techniques has been illustrated with nontrivial examples.