Generalisation of Alternating Automata over Infinite Alphabets
Généralisation d’Automates Alternatifs sur des Alphabets Infinis
Résumé
The language inclusion problem is recognised as being central to verification in different domains, such as hardware, communication protocols, software systems, etc. There we might face two challenges: non-determinism and infinite alphabets.
We propose two models of alternating automata over infinite alphabets: (i) alternating data automata (ADA) and (ii) first-order alternating data automata (FOADA). They both recognise the data words over infinite alphabets. In ADA model, the control states are Booleans and the transition rules are specified by a set of formulae in a combined first-order theory of states (Booleans) and data that relate past values of variables with current values of variables. But a restriction of the ADA model is that, there is not hidden variable, hence all the data values taken by the variables are visible in the input. But in FOADA model, the arguments of a predicate atom track the values of the internal variables associated with the state, and these values are invisible in the input sequence, which overcomes the restriction of the ADA model.
With these two alternating models, Boolean operations of union, intersection and complement can be done in linear time, thus matching the complexity of performing these operations in the finite-alphabet case. However, the price to be paid here is that the emptiness checking becomes undecidable. For this reason, we provide two efficient semi-algorithms for emptiness checking: (i) lazy predicate abstraction and (ii) IMPACT method. These semi-algorithms are proven to terminate by returning a word from the language of the given automaton if one exists; but if the language of the given automaton is empty, then the termination is not guaranteed.
The main application of our models is checking inclusions between various classes of automata extended with variables ranging over infinite domains that recognise languages over infinite alphabets. The most widely known classes of this kind are timed automata and finite- memory (register) automata. Another application is checking safety (mutual exclusion, absence of deadlocks, etc.) and liveness (termination, lack of starvation, etc.) properties of parameterised concurrent programs.
Besides the theoretical parts, we also have developed a tool - FOADA Checker, mainly used for checking inclusion between two automata or checking emptiness of an automaton. FOADA Checker is written in Java, via Java-SMT interface and using Z3 SMT solver for spuriousness, coverage queries and interpolant generation. The IMPACT semi-algorithm has been implemented in the tool to check the emptiness of an automaton.
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 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.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...