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[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

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[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é 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].

Notes et références

  1. ↑ Alonzo Church, « Application of Recursive Arithmetic to the Problem of Circuit Synthesis », Journal of Symbolic Logic, vol. 28, no 4,‎ , p. 289–290 (lire en ligne, consulté le )
  2. ↑ Zohar Manna et Richard Waldinger, « A Deductive Approach to Program Synthesis », ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 2, no 1,‎ , p. 90–121 (ISSN 0164-0925, DOI 10.1145/357084.357090, lire en ligne, consulté le )
  3. ↑ H. Kress-Gazit, T. Wongpiromsarn et U. Topcu, « Correct, Reactive, High-Level Robot Control », IEEE Robotics Automation Magazine, vol. 18, no 3,‎ , p. 65–74 (ISSN 1070-9932, DOI 10.1109/MRA.2011.942116, lire en ligne, consulté le )
  4. ↑ S. Maniatopoulos, P. Schillinger, V. Pong et D. C. Conner, « Reactive high-level behavior synthesis for an Atlas humanoid robot », 2016 IEEE International Conference on Robotics and Automation (ICRA),‎ , p. 4192–4199 (DOI 10.1109/ICRA.2016.7487613, lire en ligne, consulté le )
  5. ↑ (en) J. Richard Buchi et Lawrence H. Landweber, The Collected Works of J. Richard Büchi, Springer, New York, NY, (ISBN 978-1-4613-8930-9 et 9781461389286, DOI 10.1007/978-1-4613-8928-6_29, lire en ligne), p. 525–541
  6. ↑ (en) Michael Oser Rabin, Automata on Infinite Objects and Church's Problem, Providence (R.I.), American Mathematical Society, , 21 p. (ISBN 0-8218-1663-2, lire en ligne)
  7. ↑ (en) Amir Pnueli et Roni Rosner, « On the synthesis of an asynchronous reactive module », Automata, Languages and Programming, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ , p. 652–671 (ISBN 9783540513711, DOI 10.1007/BFb0035790, lire en ligne, consulté le )
  8. ↑ Martín Abadi, Leslie Lamport et Pierre Wolper, « Realizable and Unrealizable Specifications of Reactive Systems », ICALP, Springer-Verlag,‎ , p. 1–17 (ISBN 354051371X, lire en ligne, consulté le )
  9. ↑ (en) Edmund M. Clarke et E. Allen Emerson, « Design and synthesis of synchronization skeletons using branching time temporal logic », Logics of Programs, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ , p. 52–71 (ISBN 9783540112129, DOI 10.1007/BFb0025774, lire en ligne, consulté le )
  10. ↑ (en) Zohar Manna et Pierre Wolper, « Synthesis of communicating processes from Temporal Logic specifications », Logics of Programs, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ , p. 253–281 (ISBN 9783540112129, DOI 10.1007/BFb0025786, lire en ligne, consulté le )
  11. ↑ a et b (en) Nir Piterman, Amir Pnueli et Yaniv Sa’ar, « Synthesis of Reactive(1) Designs », Verification, Model Checking, and Abstract Interpretation, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ , p. 364–380 (ISBN 9783540311393, DOI 10.1007/11609773_24, lire en ligne, consulté le ) :

    « Theorem 1, p. 372 »
  12. ↑ (en) « Controller Synthesis for Timed Automata », IFAC Proceedings Volumes, vol. 31, no 18,‎ , p. 447–452 (ISSN 1474-6670, DOI 10.1016/S1474-6670(17)42032-5, lire en ligne, consulté le )
  13. ↑ Rajeev Alur et Salvatore La Torre, « Deterministic generators and games for Ltl fragments », ACM Transactions on Computational Logic (TOCL), vol. 5, no 1,‎ , p. 1–25 (ISSN 1529-3785, DOI 10.1145/963927.963928, lire en ligne, consulté le )
  14. ↑ « Prosyd », sur www.prosyd.org (consulté le )
  15. ↑ Giuseppe De Giacomo et Moshe Y. Vardi, « Synthesis for LTL and LDL on finite traces », IJCAI, AAAI Press,‎ , p. 1558–1564 (ISBN 9781577357384, lire en ligne, consulté le )
  16. ↑ Giuseppe De Giacomo et Moshe Y. Vardi, « LTL f and LDL f synthesis under partial observability », IJCAI, AAAI Press,‎ , p. 1044–1050 (ISBN 9781577357704, lire en ligne, consulté le )
  17. ↑ Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi, « Symbolic LTLf Synthesis », IJCAI,‎ , p. 1362-1369 (lire en ligne)
  18. ↑ (en) Aaron Bohy, Véronique Bruyère, Emmanuel Filiot et Naiyong Jin, « Acacia+, a Tool for LTL Synthesis », Computer Aided Verification, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ , p. 652–657 (ISBN 9783642314230, DOI 10.1007/978-3-642-31424-7_45, lire en ligne, consulté le )
  19. ↑ (en) Rüdiger Ehlers, « Unbeast: Symbolic Bounded Synthesis », Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ , p. 272–275 (ISBN 9783642198342, DOI 10.1007/978-3-642-19835-9_25, lire en ligne, consulté le )
  20. ↑ Roderick Bloem, Krishnendu Chatterjee, Karin Greimel et Thomas A. Henzinger, « Synthesizing robust systems », Acta Informatica, vol. 51, nos 3-4,‎ , p. 193–220 (ISSN 0001-5903, DOI 10.1007/s00236-013-0191-5, lire en ligne, consulté le )