Generalisation of Alternating Automata over Infinite Alphabets
Xiao Xu · 2020
Généralisation d'automates alternatifs sur des alphabets infinis Le problème de l’inclusion linguistique est reconnu comme étant au cœur de la vérification dans différents domaines, tels que le matériel, les protocoles de communication, les systèmes logiciels, etc. Nous pouvons être confrontés à deux défis: le non-déterminisme et les alphabets infinis.Nous proposons deux modèles d’automates alternatifs sur des alphabets infinis : (i) les automates alternatifs de données (ADA) et (ii) les automates alternatifs de données du premier ordre (FOADA). Ils reconnaissent tous deux les mots de données sur des alphabets infinis. Dans le modèle ADA, les états de contrôle sont des booléens et les règles de transition sont spécifiées par un ensemble de formules combinées dans une théorie des états du premier ordre (booléens) et des données associant les valeurs passées des variables aux valeurs actuelles des variables. Mais le modèle ADA a une restriction : il n’y a pas de variable cachée, ainsi toutes les valeurs de données prises par les variables sont visibles dans l’entrée. Pourtant dans le modèle FOADA, les arguments d’un atome de prédicat tracent les valeurs des variables internes associées à l’état, et ces valeurs sont invisibles dans la séquence d’entrée, ce qui surmonte la restriction du modèle ADA.Avec ces deux modèles en alternance, les opérations booléennes d’union, d’intersection et de complément peuvent être effectuées en temps linéaire, ce qui correspond à la complexité de l’exécution de ces opérations dans le cas d’un alphabet fini. Cependant, le prix à payer ici est que la vérification du vide devient indécidable. Pour ceci, nous fournissons deux semi-algorithmes efficaces pour la vérification du vide : (i) abstraction de prédicats paresseux et (ii) méthode IMPACT. S’il existe un mot du langage de l’automate donné, il est prouvé que ces semi-algorithmes se terminent en le retournant; mais si la langue de l’automate donné est vide, la terminaison n’est pas garantie.La principale application de nos modèles est de vérifier l’inclusion entre différentes classes d’automates étendues avec des variables allant de domaines infinis reconnaissant les langues à des alphabets infinis. Les plus connues de ce genre de classes sont les automates temporisés et les automates à mémoire finie (registre). Une autre application est de vérifier les propriétés de sécurité (exclusion mutuelle, absence de blocages, etc.) et de vitalité (résiliation, absence de famine, etc.) des programmes concurrents paramétrés.Outre les parties théoriques, nous avons également développé un outil - FOADA Checker, en général à l’usage de la vérification de l’inclusion entre deux automates ou de la vérification du vide d’un automate. FOADA Checker est écrit en Java, via l’interface Java-SMT et en utilisant le solveur Z3 SMT [53] pour les parasites, les requêtes de couverture et la génération d’interpolation. Le semi-algorithme IMPACT a été implémenté dans l’outil pour vérifier le vide d’un automate.