Vérification symbolique.

Cette technique est basée sur la représentation d'un nombre infini de configurations par des structures finis (automates) et le calcul de la fermeture transitive de relations régulières (qui représentent les transitions entre configurations du système). Pour les systèmes que nous comptons vérifier nous étendrons d'une part ces techniques à des structures et topologies plus complexes comme les DAG, les graphes, etc. pour tenir compte de tous les aspects importants. D'autre part nous considérerons des automates avec vocabulaires infinis qui permettent de raisonner sur des données infinis comme les entiers. Par exemple, une configuration d'un système composé d'un nombre paramétré de composantes utilisant chacune un entier est un mot sur le vocabulaire des entiers.

Les techniques de regular model checking doivent être étendues par des nouveaux formalismes pour représenter la structure de la mémoire dynamique, qui peut être vue comme un graphe. Ceci nécessite l'étude des transformations de graphes afin de trouver des applications pour la vérification. Plus précisément, il s'agit d'identifier les classes de problèmes décidables ainsi que développer des techniques d'accéleration pour les classes non décidables.