Automates sur objets infinis

Les automates sur objets infinis lisent des entrées qui ne se terminent jamais, telles que des mots infinis ou des arbres infinis, et acceptent en fonction des états ou des transitions visités infiniment souvent, fournissant ainsi l'appareil mathématique pour raisonner sur les systèmes continus et non-terminaux.

Definition

Un oméga-automate est une machine à états finis dont les exécutions sont infinies, l'acceptation étant définie par une condition sur l'ensemble des états visités infiniment souvent ; de tels automates reconnaissent des ensembles de mots ou d'arbres infinis appelés langages oméga-réguliers.

Scope

Ce sujet couvre les automates de Büchi, Muller, Rabin et de parité sur les mots infinis, les conditions d'acceptation qui les distinguent, les résultats de déterminisation et de complémentation, les automates sur les arbres infinis, ainsi que les liens profonds entre ces automates, la logique monadique du second ordre et les jeux infinis utilisés en synthèse et en vérification.

Core questions

• Comment une machine finie peut-elle accepter ou rejeter une entrée qui n'a pas de fin ?
• Pourquoi les automates de Büchi non déterministes et déterministes diffèrent-ils en termes de puissance expressive ?
• Comment les automates sur objets infinis se rapportent-ils aux logiques de spécification du comportement des systèmes ?
• Qu'est-ce qui rend la complémentation de ces automates difficile, et pourquoi est-ce important ?

Key theories

Acceptation de Büchi et langages oméga-réguliers

Un automate de Büchi accepte un mot infini lorsqu'un état acceptant est visité infiniment souvent, et les langages ainsi reconnus, les langages oméga-réguliers, coïncident avec ceux définissables en logique monadique du second ordre sur les nombres naturels.

Déterminisation et la condition de parité

Les automates de Büchi non déterministes ne peuvent généralement pas être rendus déterministes sans modifier la condition d'acceptation, mais la construction de Safra les convertit en automates de Rabin ou de parité déterministes, ce qui est essentiel pour la complémentation et pour la résolution de jeux.

Clinical relevance

Les oméga-automates constituent l'épine dorsale algorithmique de la vérification de modèles (model checking) : un système réactif et une propriété de logique temporelle sont chacun traduits en automates sur mots infinis, et la vérification de la propriété se réduit à un test de vacuité, permettant la vérification automatisée du matériel, des protocoles et des logiciels concurrents.

History

Büchi a introduit les automates sur mots infinis vers 1960 pour décider la théorie monadique du second ordre des nombres naturels, McNaughton a montré comment les déterminiser avec des conditions d'acceptation plus fortes, et Rabin a étendu la théorie aux arbres infinis, des résultats qui sont devenus centraux pour la vérification après l'introduction de la logique temporelle en informatique à la fin des années 1970.

Key figures

• J. Richard Büchi
• Robert McNaughton
• Michael Rabin
• Shmuel Safra

Seminal works

• thomas1990
• graedel2002

Frequently asked questions

Comment une machine peut-elle accepter une entrée infinie ?

L'acceptation n'est pas définie par l'atteinte d'un état final à la fin, puisqu'il n'y a pas de fin, mais par les états qui se répètent. Un automate de Büchi, par exemple, accepte lorsqu'il passe infiniment souvent par un état acceptant désigné au cours de son exécution infinie.

Pourquoi ces automates sont-ils importants pour la vérification ?

Les systèmes non-terminaux tels que les systèmes d'exploitation et les protocoles réseau sont naturellement modélisés par des comportements infinis. Des propriétés comme « le système ne se bloque jamais » ou « chaque requête est finalement traitée » deviennent des langages oméga-réguliers, de sorte que leur vérification se réduit à des opérations d'automates qu'un vérificateur de modèles (model checker) peut effectuer automatiquement.