We address the problem of verifying safety and liveness properties
for infinite-state systems, using symbolic reachability analysis.
The models we consider are fair parametric extended automata, i.e.,
counter automata with parametric guards, supplied with fairness
conditions on their transitions. We show that symbolic reachability
analysis using acceleration techniques can be used to generate
finite abstractions (symbolic graphs) of the original infinite-state
model. Moreover, we show that this analysis can be used to introduce
fairness conditions on the generated abstract model allowing to
model-check liveness properties.
We show first how to translate faithfully the fairness conditions of
the infinite-state original model to conditions on the generated
finite symbolic graph. Then, we show that we can also synthesize
automatically new fairness conditions allowing to eliminate infinite
paths in the symbolic graph which do not correspond to valid
behaviours in the original model. These infinite paths correspond
to abstractions of boundedly iterable loops, or nested loops.
We show techniques allowing to decide this bounded iterability for
a class of components in the symbolic graph. We illustrate the
application of these techniques to nontrivial examples.
