Non-Deterministic Register Automata with a Dense Order

Get Complete Project Material File(s) Now! »

Les systèmes réactifs

Les automates

ce titre, les programmes représentables par des machines à états finis, ou automates, constituent une classe de choix. Comme leur nom l’indique, de telles machines sont dotées d’un ensemble fini d’états. Elle traitent leur entrée lettre par lettre de gauche à droite, en utilisant leurs états pour stocker l’information. Elles sont notamment utilisées pour modéliser les systèmes embarqués ou les circuits électroniques. Dans leur forme la plus pure, ils consistent en des accepteurs pour un langage qui, étant donné une séquence de lettres, ou mot, répondent Oui ou Non selon que le mot appartient au langage ou non. Un langage est ainsi un ensemble (fini ou infini) de mots. Pour prendre un exemple simple, considérons le langage des mots qui contiennent un nombre impair de 0. Pour déterminer si un mot donné appartient au langage, un programme n’a pas besoin de compter le nombre de 0, seulement de garder en mémoire la parité de ce nombre. La Figure 2.1 représente un automate qui reconnaît ce langage. Dans cet exemple, lorsqu’il est Le lecteur connaisseur, qui sait déjà ce qu’est un automate, peut se rendre à la Section 1.2.2.
Figure 1.1. : Un automate avec deux états mémoire qui détermine si son entrée contient un nombre impair de 0. Les états sont représentés par des cercles, et les transitions par des flèches. Par exemple, quand l’automate est dans l’état « pair » et lit un 0, il transitionne vers l’état « impair ». Comme indiqué par la flèche entrante, il commence dans l’état « pair ». La machine répond Oui si et seulement si son exécution termine dans un état final, distingué par un double cercle (ici, seul l’état « impair » est acceptant). Pour illustrer notre propos, nous invitons le lecteur ou la lectrice à méditer sur le comportement de l’automate lorsqu’il lit le mot 100. Tout d’abord, il commence dans son état initial « pair », puisque avant de lire le mot, il a lu 0 occurrences de la lettre 0, et 0 est pair. Lorsqu’il lit la lettre 1, il suit la boucle sur l’état « pair » et reste dans cet état (puisque 1 n’est pas 0). Ensuite, il lit 0 et va dans l’état « impair ». Enfin, il lit 0 de nouveau, et retourne dans l’état « impair ». Il répond alors Non, puisque « pair » n’est pas un état acceptant. Il est aisé de vérifier que lors d’une exécution quelconque, l’automate est dans l’état « pair » précisément lorsqu’il a vu un nombre pair de 0 (et inversement pour « impair »).
dans un état donné et lit une lettre, l’automate a une seule transition possible ; on dit alors qu’il est déterministe. En général, il est pratique de doter ces machines de la possibilité de « deviner » la transition à prendre parmi plusieurs possibles ; de telles machines sont appelées non-déterministes ». Examinons par exemple le langage des mots dont l’antépénultième lettre est un 0. Puisque l’automate lit son entrée de gauche à droite, il ne peut pas savoir à l’avance combien de lettres il lui reste à lire avant la fin. La Figure 1.2 représente un automate non-déterministe qui reconnaît ce langage. Dans la pratique, un programme Dans la définition d’un automate non-déterministe, il n’est pas requis qu’il ait plusieurs transitions possibles parmi les-quelles choisir, au sens où la notion d’au-tomate non-déterministe généralise celle d’automate déterministe. Un automate déterministe est donc, en particulier, non-déterministe.
Figure 1.2. : Un automate non-déterministe qui vérifie que l’antépénultième lettre est un 0. Il commence dans l’état « attendre ». Lorsqu’il lit une lettre qui n’est pas un 0, il reste dans cet état. Lorsqu’il lit un 0, il doit faire un choix : ou bien rester dans l’état « attendre » en prenant la boucle, ou bien transitionner vers l’état 2. Pour faire un tel choix, il devine si le 0 qu’il lit est deux lettres avant la fin du mot. Si c’est le cas, il va dans l’état 2, et vérifie qu’il a deviné correctement en lisant les deux lettres suivantes. Si le mot se termine à ce moment-là, il répond Oui, puisqu’il est alors dans l’état 0, qui est acceptant. S’il y a encore des lettres à lire, l’exécution échoue puisqu’il n’y a pas de transition à prendre depuis l’état 0. Par définition, un automate non-déterministe répond Oui si et seulement si au moins une de ses exécutions termine dans un état acceptant. Par exemple, sur l’entrée 01011, lorsqu’il lit le premier 0, l’automate peut soit aller dans l’état 2, soit rester dans l’état « attendre ». S’il opte pour la première possibilité, lorsqu’il a lu 010, il est dans l’état 0 et a encore deux lettres à lire, et l’exécution échoue. Dans le second cas, il doit à nouveau faire ce choix en lisant le second 0. S’il reste dans l’état « attendre », il y reste jusqu’à la fin de l’exécution puisqu’il n’y a plus de 0 à lire, et l’exécution n’est pas acceptante puisqu’elle termine dans un état non-acceptant. Cependant, s’il transitionne vers 2, l’exécution termine dans l’état 0 et l’automate accepte. Ainsi, il existe une exécution acceptante, ce qui signifie que 01011 est accepté par l’automate, qui répond Oui.
n’est pas capable de « deviner » la bonne exécution, sauf en exécutant tous les calculs en parallèle et en vérifiant qu’il en existe au moins un qui est acceptant. Par conséquent, le non-déterminisme devrait être interprété comme une manière compacte de représenter un ensemble de comportements possibles. Il est bien connu que les automates non-déterministes admettent toujours un équivalent déterministe, qui peut cependant être exponentiellement plus grand (en termes de nombre d’états).
Pour représenter des spécifications, nous aurons également recours aux automates universels, ou co-non-déterministes. Plutôt que de demander qu’au moins une exécution est acceptante, nous demandons à ce qu’elles le soient toutes. Si nous revenons à l’automate de la Figure 1.2, vu comme un automate universel et en intervertissant les états acceptants et rejetants, il accepte précisément les mots dont l’antépénultième lettre n’est pas un 0. Plus généralement, les sémantiques non-déterministes et universelles sont duales : en interprétant un automate non-déterministe avec la sémantique d’un automate universel, et en intervertissant les états acceptants et rejetants, nous obtenons un automate qui reconnaît le complément du langage.

Les transducteurs

Souvent, nous attendons d’un programme qu’il fournisse plus d’infor-mation que le seul fait d’accepter ou de rejeter un mot. Par exemple, si nous revenons à l’automate de la Figure 1.1, nous pourrions lui de-mander de signaler tout au long du calcul si le nombre de 0 qu’il a vus jusqu’à présent est impair. Sur l’entrée 010, il produirait alors la séquence impair impair pair (si l’on suppose qu’il lit d’abord une lettre avant de produire une sortie). Dans ce cas particulier, il suﬃt de demander à l’automate d’aﬃcher son état courant le long de son exécution. Cepen-dant, en général, il est plus pratique de distinguer les états internes de la machine et ses interactions avec son environnement. Pour ce faire, nous enrichissons plutôt les transitions avec des lettres de sortie : à chaque fois qu’elle lit une lettre d’entrée, la machine transitionne vers un état, et, ce faisant, produit une lettre de sortie. Cela permet de représenter des programmes qui eﬀectuent des transformations de leur entrée, par exemple remplacer 0 par 1, 1 par 2 et 2 par 0 lorsqu’un nombre pair de 0 a été lu, et inversement 0 ! 2 ! 1 ! 0 lorsque ce nombre est impair (cf Figure 1.3).
Figure 1.3. : Un transducteur séquentiel qui permute son entrée, dans un sens ou dans l’autre selon qu’il a lu un nombre pair de 0. Pour simplifier, nous supposons qu’il lit seulement des mots dont les lettres sont issues de l’alphabet f0 1 2g. Les entrées sont colorées en rouge, les sorties en vert, et une transition « pair! impair » se lit « lorsque l’on est dans l’état “pair” et que l’on lit un 0, on produit 1 et transitionne vers l’état “impair” ». Par exemple, sur l’entrée 01102, le transducteur produit la sortie 10020.À l’instar des automates, les transducteurs bénéficient d’un mécanisme d’acceptance : on peut demander à ce que la machine n’accepte que les mots contenant un nombre impair de 0 en considérant l’état « impair » comme le seul état acceptant.

Transducteurs

Dans notre cadre d’analyse, nous sommes principalement intéressés par l’interaction entre le programme et son environnement, c’est-à-dire la relation entre ses entrées et ses sorties, plus que par sa terminaison. En d’autres termes, nous considérons le cas d’un système en interaction constante avec son environnement. Ce dernier fournit un signal d’entrée, modélisé comme l’élément (lettre) d’un ensemble fini (alphabet). Ensuite, le système réagit par une lettre de sortie, et ceci indéfiniment. Leur interaction donne lieu à une suite infinie de signaux d’entrée et de sortie entrelacés. Nous supposons que l’interaction ne termine jamais, puisque l’étude est focalisée sur le contrôle du système, plutôt que sur son aspect calculatoire. Un tel système est appelé réactif. Précisons en passant qu’il y a un procédé d’abstraction à l’œuvre ici, intrinsèque à la démarche de modélisation : nous avons besoin d’objets qui soient manipulables algo-rithmiquement, que nous construisons en abstrayant système réellement existant. Ainsi, nous travaillons toujours sous l’hypothèse que le modèle mathématique est en adéquation avec le système considéré.
Un exemple paradigmatique de système réactif est celui d’un serveur en interaction avec ses clients : ces derniers adressent des requêtes au serveur, qu’il doit satisfaire en temps voulu. Ici, nous présentons une variation sur le même thème, qui présente essentiellement les mêmes caractéristiques, à savoir le cas d’une machine à café, modélisée comme le système, qui intéragit avec ses utilisateurs qui constituent collectivement son environnement. Les utilisateurs fournissent les signaux d’entrée via les boutons de la machine, qui réagit avec des signaux de sortie consistant
eﬀectuer des actions (démarrer, verser le café, aﬃcher des informations sur l’écran, s’éteindre, etc). Typiquement, une interaction consiste en un utilisateur qui allume la machine, commande un café, le reçoit et éteint la machine. Si personne n’utilise la machine jusqu’à la fin des temps, elle reste inactive indéfiniment. Une telle interaction peut être modélisée par le mot infini suivant :
La machine est guidée par un contrôleur qui réagit en temps réel aux signaux d’entrée. S’il est encodé dans un puce éléctronique, il a un nombre d’états fini, et peut donc être modélisé par un transducteur déterministe qui opère sur des mots infinis ; nous les appelons $-transducteurs. Nous pourrions alors modéliser notre machine à café par l’$-transducteur de la Figure 1.4. En général, nous supposons que de tels programmes acceptent toutes les séquences d’entrées possibles, aussi tous leurs états sont-ils implicitement acceptants. Insistons sur le fait que l’interaction Par convention, les entrées sont colorées en rouge, et les sorties en vert. Le symbole dénote la concaténation.
Figure 1.4. : Un $-transducteur qui modélise une machine à café. Elle est initialement éteinte, et peut être allumée en appuyant sur on ». Lorsqu’elle est éteinte, les autres commandes n’ont aucun eﬀet. Lorsqu’elle est allumée, il est possible de commander un café, auquel cas la machine s’exécute diligemment.
doit être imaginée sur l’ensemble du cycle de vie de la machine. Par exemple, lorsqu’elle s’éteint, l’interaction n’est pas terminée, puisqu’elle peut être rallumée par la suite. Le cycle de vie global est lui-même fini, car la machine cessera un jour de fonctionner en dépit de tous les eﬀorts pour la maintenir en vie, ne serait-ce qu’au moment de l’eﬀondrement du système solaire qui adviendra dans un temps long mais fini. Cependant, focaliser l’étude sur l’interaction peremt d’exprimer plus aisément des réquisits qui concernent une fin prématurée de l’exécution, par exemple lorsque la machine s’éteint sans crier gare. C’est le cas par exemple de la séquence fautive appuyer_sur_on demarrer commander_cafe eteindre „inactif inactif”$, où la machine s’éteint avant d’avoir servir un café commandé. Ainsi, une spécification typique pourrait requérir que chaque occurrence de commander_cafe est immédiatement suivie de verser_cafe. Une telle exigence pourrait être trop élevée. Premièrement, on ne peut pas attendre d’une machine qu’elle serve un café en étant éteinte, aussi cette condition devrait-elle être limitée aux périodes ouvertes par une occurrence de demarrer, qui ne contiennent pas eteindre. Cependant, une telle spécification est trivialement satisfaite par une machine qui ne s’allume jamais, aussi faudrait-il également spécifier de quelle manière la machine démarre. Par ailleurs, il est possible que la machine prenne du temps pour servir un café, par exemple si elle doit eﬀectuer des oéprations internes à cette fin, comme moudre le café, chauﬀer l’eau, etc. Par conséquent, elle n’est peut-être pas capable de réagit immédiatement, auquel cas nous pouvons relâcher la spécification et demander à ce que le café soit servi dans les : unités de temps suivantes pour un certain : fixé, voire simplement que la machine finisse par servir un café (sans borne de temps).

READ Cooking 101: Begin in the Kitchen Today

La synthèse réactive et le problème de Church

En définitive, une spécification met en relation des suites infinies de si-gnaux d’entrée avec les suites infinies de signaux de sortie qui constituent des comportements acceptables pour le système. Puisque nous nous intéressons aux systèmes réactifs qui sont en interaction constante avec leur environnement, il est souvent plus pratique de voir la spécification de manière entrelacée, c’est-à-dire comme les mots qui consistent en l’en-trelacement d’une suite infinie d’entrées et d’une suite correspondante de sorties acceptable. Par exemple, si l’on demande que verser_cafe advienne au bout d’un moment, et ce après chaque occurrence de commander_cafe, cela correspond à la spécification qui contient tous les mots satisfaisant cette propriété.
Le problème de la synthèse réactive consiste alors, étant donné une spécification (représentée de manière finie), à générer un programme réactif qui satisfait la spécification si un tel programme existe, et de fournir un témoin d’infaisabilité dans le cas contraire. Ce problème fut posé par Church en 1957 qui définit ce qui est désormais connu comme le problème de Church [5] :
Étant donné une exigence à laquelle un circuit doit satisfaire, nous pouvons supposer qu’un tel réquisit est exprimé dans un formalisme adapté qui est une extension de l’arithmétique limitée [c’est-à-dire la théorie du second ordre des entiers naturels, restreinte à l’addition]. Le problème de la synthèse consiste alors à trouver une fonction calculable qui représente un circuit satisfaisant à cette exigence (ou, alternativement, de déterminer qu’un tel circuit n’existe pas). ([4], notre traduction) Les systèmes réactifs sont notoirement diﬃciles à concevoir correctement, et l’objectif de la synthèse est de générer automatiquement des systèmes qui sont corrects par construction. Dans le cadre défini par Church, la classe des implémentations consiste en les programmes réactifs qui peuvent être exécutés par des circuits booléens, c’est-à-dire utilisant une quantité finie de mémoire. Autrement dit, des $-transducteurs.

La logique monadique du second ordre (MSO)

Concernant le formalisme de spécification, Church a principalement considéré la logique monadique du second ordre (MSO) sur les mots infinis avec le prédicat ‚1 (ou, de manière équivalente, ), et des pré-dicats pour les lettres de l’alphabet d’entrée et de sortie. Cette logique
Dans le cadre de Church, les lettres sont en réalité encodées en binaire, mais il est plus pratique de se doter de prédicats spécifiques. est capable d’exprimer les diﬀérentes spécifications que nous avons ébauchées précédemment. Par exemple, l’on peut demander à ce que verser_cafe advienne après commander_cafe (sans borne de temps) de la manière suivante :

La synthèse vue comme un jeu

Dans un rapport technique non publié [6], McNaughton remarqua que le problème de la synthèse peut être vu comme un jeu à deux joueurs à durée infini [7], que nous appelons le jeu de Church. Un joueur modélise le système, l’autre, son environnement. L’objectif du système est de satisfaire la spécification ; l’environnement est antagoniste et cherche à ce qu’elle soit enfreinte∗. Dans cette perspective, une stratégie gagnante pour le système correspond à une implémentation de la spécification, tandis qu’une stratégie gagnante pour l’environnement témoigne de l’infaisabilité de la spécification. En 1969, Büchi et Landweber ont résolu le problème pour les spécifications MSO à l’aide de méthodes issues de la théorie des jeux [8]. L’idée est de convertir la formule logique qui exprime la spécification en une machine à états finis qui reconnaît les interactions valides (plus précisément un $-automate, c’est-à-dire un automates à états finis qui reconnaît des mots infinis), autrement dit les entrelacements d’entrées avec leurs sorties acceptables. Cette machine constitue alors un « observateur » pour le jeu, et définit sa condition de victoire. Reste alors à résoudre le jeu pour en déterminer le vainqueur, ce qui peut être fait par un calcul de points fixes — ou attracteurs — dans le cas des jeux de parité (voir par exemple [9]). Par la suite, Rabin a élaboré une solution qui repose sur les automates d’arbres [10] : une stratégie peut être modélisée par un arbre infini, et il est possible de construire un automate qui reconnaît exactement les stratégies gagnantes dans le cas des jeux $-réguliers (i.e. dont la condition de gain est reconnaissable par une formule MSO ou, équivalemment, un automate). Dans cette thèse, nous adoptons la présentation « ludique », qui permet de tirer parti de résultats connus sur les jeux de parité, et qui fournit un formalisme élégant pour décrire les implémentations. Nous suivons globalement l’approche proposée par Thomas dans [5] concernant le problème de Church.
[6]: McNaughton (1965), Finite-state infi-nite games, cité dans [5].
[7]: McNaughton (1993), « Infinite Games Played on Finite Graphs »
[8]: J.R. Büchi et L.H. Landweber (1969),
Solving sequential conditions finite-state strategies »
[9]: Bloem, Chatterjee et Jobstmann (2018), « Graph Games and Reactive Syn-thesis »
[10]: Rabin (1972), Automata on Infinite Objects and Church’s Problem
[5]: Thomas (2009), « Facets of Synthesis :
Revisiting Church’s Problem »

La logique temporelle linéaire (LTL)

Lorsque la spécification est exprimée par une formule MSO, le problème de Church hérite de la borne inférieure de complexité du problème de la satisfaisabilité de ces formules, qui est non-élémentaire [11]. Cette complexité inouïe a longtemps empêché l’application concrète des algo-rithmes de synthèse. L’introduction de la Logique Temporelle Linéaire (LTL) [12] constitua une première tentative pour l’apprivoiser, dans le contexte voisin de la vérification formelle. Ce problème est le jumeau (plus sympathique) du problème de la synthèse : étant donné une spécifi-cation et un système, ce dernier satisfait-il la spécification ? A contrario, la [11]: Meyer (1975), « Weak monadic se-cond order theory of succesor is not elementary-recursive » synthèse consiste à construire le système à partir de la spécification. Pnueli montra qu’un tel problème est PSpace-complet, puis que le problème de la synthèse est 2-ExpTime-complet [13]. Ce fossé entre la complexité des deux problèmes est l’une des raisons pour lesquelles la vérification formelle est aujourd’hui appliquée plus largement que la synthèse [14]. Cependant, au cours de la décennie écoulée, l’apparition de méthodes eﬃcaces pour la synthèse a déclenché un renouveau d’intérêt pour le domaine [3, 15, 16], désormais très actif [9, 17-20].
Pour donner une idée du fonctionnement de LTL, signalons que la spécification précédemment citée « verser_cafe apparaît après chaque occurrence de commander_cafe » (sans borne de temps) peut être expri-mée par la formule G„commander_cafe ) F„verser_cafe””, où G (pour globally ») signifie que la propriété est vraie tout au long de l’exécution, et F (pour « finally ») qu’elle sera vraie à un certain moment dans le futur. Ainsi, la formule ci-dessus se lit « Tout au long de l’exécution, il doit être vrai que si l’on rencontre commander_cafe, alors on rencontre verser_cafe par la suite ».

Table of contents :

1. Introduction en français
1.1. Synthèse de programmes
1.2. Les systèmes réactifs
1.3. La synthèse réactive et le problème de Church
1.4. Extension aux alphabets infinis
1.5. Extension au cas asynchrone
1.6. Plan
1.7. Comment lire cette thèse ?
2. Introduction in English
2.1. Program Synthesis
2.2. Reactive Systems
2.3. Reactive Synthesis and the Church Problem
2.4. Extension to the Infinite Alphabet Case
2.5. Further Extension to the Asynchronous Case
2.6. Outline
2.7. How to Read this Thesis?
I. Reactive Synthesis
3. Reactive Synthesis over Finite Alphabets
3.1. Relations and Functions
3.2. Uniformisation and Program Synthesis
3.3. The Reactive Synthesis Problem
3.4. The Church Synthesis Problem
3.5. Games for Reactive Synthesis
4. Register Automata over a Data Domain
4.1. DataWords
4.2. Tests and Valuations
4.3. Register Automata
4.4. General Properties
4.5. Non-Deterministic Register Automata with Equality
4.6. Non-Deterministic Register Automata with a Dense Order
4.7. Register Automata with a Discrete Order
4.8. Universal Register Automata
4.9. Register Automata and Arithmetic
4.10. Extensions of the Model
5. Synthesis Problems over DataWords
5.1. Reactive Synthesis over DataWords
5.2. Data Automatic Specifications
5.3. Register Transducers
5.4. The Church Synthesis Problem
6. Register-Bounded Synthesis of Register Transducers
6.1. A Generic Approach
6.2. Universal Register Automata Specifications
6.3. Non-Deterministic Register Automata Specifications
7. Unbounded Synthesis of Register Transducers
7.1. Non-Deterministic Register Automata Specifications
7.2. Universal Register Automata Specifications
7.3. Deterministic Register Automata Specifications
8. Partial Versus Total Domain
8.1. Domains of Specification Automata
8.2. Uniformisation Problem
8.3. Good-Enough Synthesis
9. Conclusion
II. Computability of Functions Defined by Transducers over Infinite Alphabets
10. Non-Deterministic Asynchronous Register Transducers
10.1. The Model
10.2. Register Transducers and Register Automata
10.3. Functions Recognised by Transducers
10.4. Closure under Composition
11. $-Computability and Continuity
11.1. Computability
11.2. Continuity
11.3. $-Computability versus Continuity
12. Exploration of Various Data Domains
12.1. Data Domains with Equality
12.2. Oligomorphic Data Domains
12.3. Discretely Ordered Data Domains
13. Conclusion
14. Thesis Conclusion
14.1. Abstraction of the Behaviour of Register Automata
14.2. Generalisation to Other Formalisms
14.3. Minimisation and Learning