Synthèse de programmes

En informatique, la synthèse de programmes consiste à construire automatiquement un programme à partir d'une spécification. La spécification est décrite dans un langage logique, par exemple en logique temporelle linéaire. La synthèse de programmes s'appuie sur des techniques de vérification formelle de programmes. Le problème de synthèse de programmes remonte aux travaux d'Alonzo Church. Manna et Waldinger ont proposé une méthode déductive pour synthétiser un programme à partir d'une spécification en logique du premier ordre. vignette|Un robot, comme l'Atlas, peut exécuter un programme synthétisé afin de réaliser une tâche et pouvoir réagir à toutes les éventualités de l'environnement. Le programme de synthèse de programmes consiste à générer un plan pour un agent (par exemple un robot) qui réussit face à toutes les éventualités de l'environnement. Par exemple, la synthèse de programme réactif avec une spécification en logique temporelle linéaire a été appliqué en robotique. En 2015, à la compétition DARPA Robotics en 2015, la synthèse de programmes a été implémentée dans un robot Atlas. Plusieurs méthodes ont été proposés, par Büchi et Landweber et par Rabin. Le problème de synthèse se réduit à tester si le langage d'un automate d'arbre est vide et de voir la solution comme un jeu à deux joueurs. Dans ces travaux préliminaires, la spécification du système était donné par une formule de S1S (logique monadique du second ordre avec un successeur). Le problème de synthèse et réalisabilité en logique temporelle linéaire (LTL) a été introduit par Pnueli et Rosner et indépendamment par Abadi, Lamport et Wolper, en 1989. Les travaux de Pnueli et Rosner font suite aux travaux préliminaires de Clarke et Emerson et ceux de Manna et Wolper, qui réduisent le problème de synthèse à un problème de satisfiabilité, en ignorant le fait que l'environnement doit être considéré comme un adversaire.