L'analyse de systemes complexes necessite souvent la consideration de
modeles puissants dont le nombre des etats (configurations) est infini,
et
de ce fait, elle se trouve hors de portee des techniques de
verification
automatiques usuelles (e.g., model-checking des systemes finis).
Nous nous interessons dans notre travail a definir des techniques
algorithmiques pour la verification de systemes infinis tels que:
- les automates a compteurs/horloges
- les automates a pile
- lesautomates a files d'attente
- les reseaux parametres de processus (systemes avec un
nombre arbitraire de composants)
Les techniques que nous proposons sont basees sur des representations
symboliques des espaces d'etats, et des techniques permettant de
calculer
automatiquement ces representations. Les representations que nous
utilisons sont basees, selon le cas, sur certaines classes d'automates
ou
d'expressions regulieres, ou sur des classes de contraintes
arithmetiques,
ou sur des combinaisons de ces deux sortes de representations.