2001 | OriginalPaper | Buchkapitel
Analyzing Fair Parametric Extended Automata
verfasst von : Ahmed Bouajjani, Aurore Collomb-Annichini, Yassine Lakhnech, Mihaela Sighireanu
Erschienen in: Static Analysis
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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. In previous work, we 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 paper, we show that this analysis can be also 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 (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.