Symbolic reachability analysis often generate finite state abstractions which may be used for checking safety properties. However, such abstractions can not be used for checking liveness (progress) properties, since fairness conditions are often not preserved, making almost all liveness properties trivially false in the concrete model. The papers [BLS01] and [ABLS01] address this problem in the context of parametrized systems. The papers present nontrivial techniques for automatic synthesis of fairness conditions in the abstract model from those in the concrete model. These techniques are applied for verification of mutual exclusion protocols such as Szymanski's protocol [BLS01], and counter automata with parametric guards [ABLS01].