Synthèse de programmes
From Wikipedia, the free encyclopedia
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[1].
Synthèse à partir d'une spécification en logique du premier ordre
Manna et Waldinger[2] ont proposé une méthode déductive pour synthétiser un programme à partir d'une spécification en logique du premier ordre.
Synthèse à partir d'une spécification en logique temporelle linéaire
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[3]. En 2015, à la compétition DARPA Robotics en 2015[4], la synthèse de programmes a été implémentée dans un robot Atlas.
Idée générale
Plusieurs méthodes ont été proposés, par Büchi et Landweber[5] et par Rabin[6]. 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ée 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[7] et indépendamment par Abadi, Lamport et Wolper[8], en 1989. Les travaux de Pnueli et Rosner font suite aux travaux préliminaires de Clarke et Emerson[9] et ceux de Manna et Wolper[10], 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.
Algorithme
Pnueli et Rosner montre que des stratégies à mémoire finie suffisent pour gagner le jeu de réalisabilité et propose une méthode pour la synthèse à partir d'une spécification LTL φ :
- construire un automate de Büchi Bφ, de taille exponentielle en la taille de φ
- déterminiser l'automate de Büchi en un automate de Rabin déterministe, de taille doublement-exponentiel en la taille de φ
- Une fois l'automate de Rabin déterministe calculé, le jeu peut être résolu en temps nO(k), où n est le nombre d'état dans l'automate et k est le nombre de pairs acceptantes dans l'automate de Rabin (voir automates sur les mots infinis).
Pnueli et Rosner ont démontré que ce problème est 2EXPTIME-complet. Comme le souligne Piterman, Pnueli et Sa'ar[11], cette complexité est très haute et elle a découragé le développement d'outils pratiques de synthèse. A débuté alors une quête où le problème de synthèse peut être résolu plus efficacement.
Fragments efficaces
En 1998, Asarin, Maler, Pnueli et Sifakis présente un algorithme de synthèse d'automates temporisés[12], mais surtout, montre que le problème de synthèse peut être résolu en temps polynomial. Alur et La Torre montre que le problème de synthèse est entre PSPACE et EXPSPACE pour un fragment de LTL[13]. En 2006, Piterman, Pnueli et Sa'ar propose un fragment de LTL, appelé GR(1) pour Generalized reactivity(1), pour lequel le problème de synthèse est en temps O((mn|Σ|)3)[11], où m et n sont le nombre de clauses dans la formule GR(1) et Σ est l'ensemble des valuations. L'élaboration de GR(1) fait partie d'un projet appelé Prosyd[14].
Traces finies
Le problème de synthèse a aussi été étudié en 2015 par De Giacomo et Vardi pour des spécifications LTL et LDL (linear dynamic logic) sur des traces finies[15]. Aussi, le problème de planification conditionnelle avec observation totale peut être vu comme un cas particulier du problème de synthèse sur les traces finies. En 2016, le problème de synthèse a été étendu sous observation partielle, toujours sur les traces finies[16]. Là, c'est le problème de planification conditionnelle avec observation partielle qui peut être vu comme un cas particulier du problème de synthèse. En 2017, le problème de synthèse avec traces finis a été résolu avec une représentation symbolique de l'automate fini déterministe[17].
Implémentations
Plusieurs outils existent : Acacia+[18], Unbeast[19], Ratsy[20].
