PROFILPELAJAR.COM

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é 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 n^O(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|Σ|)³)^[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

↑ Alonzo Church, « Application of Recursive Arithmetic to the Problem of Circuit Synthesis », Journal of Symbolic Logic, vol. 28, n^o 4,‎ 1963, p. 289–290 (lire en ligne, consulté le 7 février 2018)
↑ Zohar Manna et Richard Waldinger, « A Deductive Approach to Program Synthesis », ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 2, n^o 1,‎ 1^er janvier 1980, p. 90–121 (ISSN 0164-0925, DOI 10.1145/357084.357090, lire en ligne, consulté le 7 février 2018)
↑ H. Kress-Gazit, T. Wongpiromsarn et U. Topcu, « Correct, Reactive, High-Level Robot Control », IEEE Robotics Automation Magazine, vol. 18, n^o 3,‎ septembre 2011, p. 65–74 (ISSN 1070-9932, DOI 10.1109/MRA.2011.942116, lire en ligne, consulté le 16 février 2018)
↑ 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),‎ mai 2016, p. 4192–4199 (DOI 10.1109/ICRA.2016.7487613, lire en ligne, consulté le 16 février 2018)
↑ (en) J. Richard Buchi et Lawrence H. Landweber, The Collected Works of J. Richard Büchi, Springer, New York, NY, 1990 (ISBN 978-1-4613-8930-9 et 9781461389286, DOI 10.1007/978-1-4613-8928-6_29, lire en ligne), p. 525–541
↑ (en) Michael Oser Rabin, Automata on Infinite Objects and Church's Problem, Providence (R.I.), American Mathematical Society, 1^er janvier 1972, 21 p. (ISBN 0-8218-1663-2, lire en ligne)
↑ (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,‎ 11 juillet 1989, p. 652–671 (ISBN 9783540513711, DOI 10.1007/BFb0035790, lire en ligne, consulté le 7 février 2018)
↑ Martín Abadi, Leslie Lamport et Pierre Wolper, « Realizable and Unrealizable Specifications of Reactive Systems », ICALP, Springer-Verlag,‎ 11 juillet 1989, p. 1–17 (ISBN 354051371X, lire en ligne, consulté le 8 février 2018)
↑ (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,‎ 4 mai 1981, p. 52–71 (ISBN 9783540112129, DOI 10.1007/BFb0025774, lire en ligne, consulté le 8 février 2018)
↑ (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,‎ 4 mai 1981, p. 253–281 (ISBN 9783540112129, DOI 10.1007/BFb0025786, lire en ligne, consulté le 8 février 2018)
↑ ^{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,‎ 8 janvier 2006, p. 364–380 (ISBN 9783540311393, DOI 10.1007/11609773_24, lire en ligne, consulté le 7 février 2018) :
« Theorem 1, p. 372 »
↑ (en) « Controller Synthesis for Timed Automata », IFAC Proceedings Volumes, vol. 31, n^o 18,‎ 1^er juillet 1998, p. 447–452 (ISSN 1474-6670, DOI 10.1016/S1474-6670(17)42032-5, lire en ligne, consulté le 7 février 2018)
↑ Rajeev Alur et Salvatore La Torre, « Deterministic generators and games for Ltl fragments », ACM Transactions on Computational Logic (TOCL), vol. 5, n^o 1,‎ 1^er janvier 2004, p. 1–25 (ISSN 1529-3785, DOI 10.1145/963927.963928, lire en ligne, consulté le 7 février 2018)
↑ « Prosyd », sur www.prosyd.org (consulté le 8 février 2018)
↑ Giuseppe De Giacomo et Moshe Y. Vardi, « Synthesis for LTL and LDL on finite traces », IJCAI, AAAI Press,‎ 25 juillet 2015, p. 1558–1564 (ISBN 9781577357384, lire en ligne, consulté le 7 février 2018)
↑ Giuseppe De Giacomo et Moshe Y. Vardi, « LTL f and LDL f synthesis under partial observability », IJCAI, AAAI Press,‎ 9 juillet 2016, p. 1044–1050 (ISBN 9781577357704, lire en ligne, consulté le 7 février 2018)
↑ Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi, « Symbolic LTLf Synthesis », IJCAI,‎ 2017, p. 1362-1369 (lire en ligne)
↑ (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,‎ 7 juillet 2012, p. 652–657 (ISBN 9783642314230, DOI 10.1007/978-3-642-31424-7_45, lire en ligne, consulté le 7 février 2018)
↑ (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,‎ 26 mars 2011, p. 272–275 (ISBN 9783642198342, DOI 10.1007/978-3-642-19835-9_25, lire en ligne, consulté le 7 février 2018)
↑ Roderick Bloem, Krishnendu Chatterjee, Karin Greimel et Thomas A. Henzinger, « Synthesizing robust systems », Acta Informatica, vol. 51, n^os 3-4,‎ 1^er juin 2014, p. 193–220 (ISSN 0001-5903, DOI 10.1007/s00236-013-0191-5, lire en ligne, consulté le 7 février 2018)

[1] Alonzo Church, « Application of Recursive Arithmetic to the Problem of Circuit Synthesis », Journal of Symbolic Logic, vol. 28, n^o 4,‎ 1963, p. 289–290 (lire en ligne, consulté le 7 février 2018)

[2] Zohar Manna et Richard Waldinger, « A Deductive Approach to Program Synthesis », ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 2, n^o 1,‎ 1^er janvier 1980, p. 90–121 (ISSN 0164-0925, DOI 10.1145/357084.357090, lire en ligne, consulté le 7 février 2018)

[3] H. Kress-Gazit, T. Wongpiromsarn et U. Topcu, « Correct, Reactive, High-Level Robot Control », IEEE Robotics Automation Magazine, vol. 18, n^o 3,‎ septembre 2011, p. 65–74 (ISSN 1070-9932, DOI 10.1109/MRA.2011.942116, lire en ligne, consulté le 16 février 2018)

[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),‎ mai 2016, p. 4192–4199 (DOI 10.1109/ICRA.2016.7487613, lire en ligne, consulté le 16 février 2018)

[5] (en) J. Richard Buchi et Lawrence H. Landweber, The Collected Works of J. Richard Büchi, Springer, New York, NY, 1990 (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, 1^er janvier 1972, 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,‎ 11 juillet 1989, p. 652–671 (ISBN 9783540513711, DOI 10.1007/BFb0035790, lire en ligne, consulté le 7 février 2018)

[8] Martín Abadi, Leslie Lamport et Pierre Wolper, « Realizable and Unrealizable Specifications of Reactive Systems », ICALP, Springer-Verlag,‎ 11 juillet 1989, p. 1–17 (ISBN 354051371X, lire en ligne, consulté le 8 février 2018)

[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,‎ 4 mai 1981, p. 52–71 (ISBN 9783540112129, DOI 10.1007/BFb0025774, lire en ligne, consulté le 8 février 2018)

[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,‎ 4 mai 1981, p. 253–281 (ISBN 9783540112129, DOI 10.1007/BFb0025786, lire en ligne, consulté le 8 février 2018)

[:0-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,‎ 8 janvier 2006, p. 364–380 (ISBN 9783540311393, DOI 10.1007/11609773_24, lire en ligne, consulté le 7 février 2018) :
« Theorem 1, p. 372 »

[12] (en) « Controller Synthesis for Timed Automata », IFAC Proceedings Volumes, vol. 31, n^o 18,‎ 1^er juillet 1998, p. 447–452 (ISSN 1474-6670, DOI 10.1016/S1474-6670(17)42032-5, lire en ligne, consulté le 7 février 2018)

[13] Rajeev Alur et Salvatore La Torre, « Deterministic generators and games for Ltl fragments », ACM Transactions on Computational Logic (TOCL), vol. 5, n^o 1,‎ 1^er janvier 2004, p. 1–25 (ISSN 1529-3785, DOI 10.1145/963927.963928, lire en ligne, consulté le 7 février 2018)

[14] « Prosyd », sur www.prosyd.org (consulté le 8 février 2018)

[15] Giuseppe De Giacomo et Moshe Y. Vardi, « Synthesis for LTL and LDL on finite traces », IJCAI, AAAI Press,‎ 25 juillet 2015, p. 1558–1564 (ISBN 9781577357384, lire en ligne, consulté le 7 février 2018)

[16] Giuseppe De Giacomo et Moshe Y. Vardi, « LTL f and LDL f synthesis under partial observability », IJCAI, AAAI Press,‎ 9 juillet 2016, p. 1044–1050 (ISBN 9781577357704, lire en ligne, consulté le 7 février 2018)

[17] Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi, « Symbolic LTLf Synthesis », IJCAI,‎ 2017, 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,‎ 7 juillet 2012, p. 652–657 (ISBN 9783642314230, DOI 10.1007/978-3-642-31424-7_45, lire en ligne, consulté le 7 février 2018)

[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,‎ 26 mars 2011, p. 272–275 (ISBN 9783642198342, DOI 10.1007/978-3-642-19835-9_25, lire en ligne, consulté le 7 février 2018)

[20] Roderick Bloem, Krishnendu Chatterjee, Karin Greimel et Thomas A. Henzinger, « Synthesizing robust systems », Acta Informatica, vol. 51, n^os 3-4,‎ 1^er juin 2014, p. 193–220 (ISSN 0001-5903, DOI 10.1007/s00236-013-0191-5, lire en ligne, consulté le 7 février 2018)

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

PROFILPELAJAR.COM

Synthèse de programmes

Synthèse à partir d'une spécification en logique du premier ordre

Synthèse à partir d'une spécification en logique temporelle linéaire

Idée générale

Algorithme

Fragments efficaces

Traces finies

Implémentations

Notes et références

Read other articles:

Coppa Italia Dilettanti (Fase C.N.D.) 1997-1998

Putri yang Ditukar

Enrique Krauze

Kontroversi nama kode Geronimo

Chailey

SIGA Technologies

Человек прямоходящий

Energy in Cyprus

BTG Homeinns

Héctor Enrique

Pine Knot (cabin)

Daftar negara menurut PDB (KKB) per kapita

コルク

1611 en arts plastiques

Septimus Heap

2016年美國總統選舉

土库曼斯坦总统

WVLK-FM

Torpedo

Inherit the Wind (1960 film)