« Synthèse de programmes » : différence entre les versions

Un article de Wikipédia, l'encyclopédie libre.
Navigation interactive dans l’historique
← Modification précédenteModification suivante →
Contenu supprimé Contenu ajouté
VisuelWikicode
Rehtse (discuter | contributions)
Administrateurs
133 387 modifications
m v1.43 - Correction syntaxique (Section « Notes et références » manquante)
Fschwarzentruber (discuter | contributions)
8 056 modifications
Ligne 5 : Ligne 5 :


== Synthèse à partir d'une spécification en logique temporelle linéaire ==
== Synthèse à partir d'une spécification en logique temporelle linéaire ==
Rabin a remarqué que la théorie des automates sert la synthèse de programmes<ref>{{Ouvrage|prénom1=Michael Oser|nom1=Rabin|titre=Automata on Infinite Objects and Church's Problem|éditeur=American Mathematical Society|date=1972-01-01|isbn=0821816632|lire en ligne=http://dl.acm.org/citation.cfm?id=540412|consulté le=2018-02-07}}</ref>. Le problème de synthèse en [[logique temporelle linéaire]] (LTL) a été introduit par Pnueli et Rosner<ref>{{Article|langue=en|prénom1=Amir|nom1=Pnueli|prénom2=Roni|nom2=Rosner|titre=On the synthesis of an asynchronous reactive module|périodique=Automata, Languages and Programming|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=1989-07-11|isbn=9783540513711|doi=10.1007/BFb0035790|lire en ligne=https://link.springer.com/chapter/10.1007/BFb0035790|consulté le=2018-02-07|pages=652–671}}</ref> en 1989. Ils ont démontré que ce problème est 2EXPTIME-complet. En 1998, Asarin, Maler, Pnueli et Sifakis présente un algorithme de synthèse d'automates temporisés<ref>{{Article|langue=en|titre=Controller Synthesis for Timed Automata|périodique=IFAC Proceedings Volumes|volume=31|numéro=18|date=1998-07-01|issn=1474-6670|doi=10.1016/S1474-6670(17)42032-5|lire en ligne=https://www.sciencedirect.com/science/article/pii/S1474667017420325|consulté le=2018-02-07|pages=447–452}}</ref>. Alur et La Torre montre que le problème de synthèse est entre PSPACE et EXPSPACE pour un fragment de LTL<ref>{{Article|prénom1=Rajeev|nom1=Alur|prénom2=Salvatore|nom2=La Torre|titre=Deterministic generators and games for Ltl fragments|périodique=ACM Transactions on Computational Logic (TOCL)|volume=5|numéro=1|date=2004-01-01|issn=1529-3785|doi=10.1145/963927.963928|lire en ligne=http://dl.acm.org/citation.cfm?id=963927.963928|consulté le=2018-02-07|pages=1–25}}</ref>. 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 polynomial<ref>{{Article|langue=en|prénom1=Nir|nom1=Piterman|prénom2=Amir|nom2=Pnueli|prénom3=Yaniv|nom3=Sa’ar|titre=Synthesis of Reactive(1) Designs|périodique=Verification, Model Checking, and Abstract Interpretation|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=2006-01-08|isbn=9783540311393|doi=10.1007/11609773_24|lire en ligne=https://link.springer.com/chapter/10.1007/11609773_24|consulté le=2018-02-07|pages=364–380}}</ref>. 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<ref>{{Article|langue=|auteur1=|prénom1=Giuseppe|nom1=De Giacomo|prénom2=Moshe Y.|nom2=Vardi|titre=Synthesis for LTL and LDL on finite traces|périodique=IJCAI|éditeur=AAAI Press|date=2015-07-25|isbn=9781577357384|issn=|lire en ligne=http://dl.acm.org/citation.cfm?id=2832415.2832466|consulté le=2018-02-07|pages=1558–1564}}</ref>. 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<ref>{{Article|langue=|auteur1=|prénom1=Giuseppe|nom1=De Giacomo|prénom2=Moshe Y.|nom2=Vardi|titre=LTL f and LDL f synthesis under partial observability|périodique=IJCAI|éditeur=AAAI Press|date=2016-07-09|isbn=9781577357704|issn=|lire en ligne=http://dl.acm.org/citation.cfm?id=3060621.3060766|consulté le=2018-02-07|pages=1044–1050}}</ref>. 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<ref>{{Article|langue=|auteur1=Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi|titre=Symbolic LTLf Synthesis|périodique=IJCAI|date=2017|issn=|lire en ligne=https://www.ijcai.org/proceedings/2017/0189.pdf|pages=p. 1362-1369}}</ref>.
Plusieurs méthodes ont été proposés, par Büchi et Landweber<ref>{{Ouvrage|langue=en|prénom1=J. Richard|nom1=Buchi|prénom2=Lawrence H.|nom2=Landweber|titre=The Collected Works of J. Richard Büchi|passage=525–541|éditeur=Springer, New York, NY|date=1990|isbn=9781461389309|isbn2=9781461389286|doi=10.1007/978-1-4613-8928-6_29|lire en ligne=https://link.springer.com/chapter/10.1007/978-1-4613-8928-6_29|consulté le=2018-02-08}}</ref> et par Rabin<ref>{{Ouvrage|prénom1=Michael Oser|nom1=Rabin|titre=Automata on Infinite Objects and Church's Problem|éditeur=American Mathematical Society|date=1972-01-01|isbn=0821816632|lire en ligne=http://dl.acm.org/citation.cfm?id=540412|consulté le=2018-02-07}}</ref>. 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 en [[logique temporelle linéaire]] (LTL) a été introduit par Pnueli et Rosner<ref>{{Article|langue=en|prénom1=Amir|nom1=Pnueli|prénom2=Roni|nom2=Rosner|titre=On the synthesis of an asynchronous reactive module|périodique=Automata, Languages and Programming|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=1989-07-11|isbn=9783540513711|doi=10.1007/BFb0035790|lire en ligne=https://link.springer.com/chapter/10.1007/BFb0035790|consulté le=2018-02-07|pages=652–671}}</ref> en 1989. Ils ont démontré que ce problème est 2EXPTIME-complet. En 1998, Asarin, Maler, Pnueli et Sifakis présente un algorithme de synthèse d'automates temporisés<ref>{{Article|langue=en|titre=Controller Synthesis for Timed Automata|périodique=IFAC Proceedings Volumes|volume=31|numéro=18|date=1998-07-01|issn=1474-6670|doi=10.1016/S1474-6670(17)42032-5|lire en ligne=https://www.sciencedirect.com/science/article/pii/S1474667017420325|consulté le=2018-02-07|pages=447–452}}</ref>. Alur et La Torre montre que le problème de synthèse est entre PSPACE et EXPSPACE pour un fragment de LTL<ref>{{Article|prénom1=Rajeev|nom1=Alur|prénom2=Salvatore|nom2=La Torre|titre=Deterministic generators and games for Ltl fragments|périodique=ACM Transactions on Computational Logic (TOCL)|volume=5|numéro=1|date=2004-01-01|issn=1529-3785|doi=10.1145/963927.963928|lire en ligne=http://dl.acm.org/citation.cfm?id=963927.963928|consulté le=2018-02-07|pages=1–25}}</ref>. 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 polynomial<ref>{{Article|langue=en|prénom1=Nir|nom1=Piterman|prénom2=Amir|nom2=Pnueli|prénom3=Yaniv|nom3=Sa’ar|titre=Synthesis of Reactive(1) Designs|périodique=Verification, Model Checking, and Abstract Interpretation|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=2006-01-08|isbn=9783540311393|doi=10.1007/11609773_24|lire en ligne=https://link.springer.com/chapter/10.1007/11609773_24|consulté le=2018-02-07|pages=364–380}}</ref>. 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<ref>{{Article|langue=|auteur1=|prénom1=Giuseppe|nom1=De Giacomo|prénom2=Moshe Y.|nom2=Vardi|titre=Synthesis for LTL and LDL on finite traces|périodique=IJCAI|éditeur=AAAI Press|date=2015-07-25|isbn=9781577357384|issn=|lire en ligne=http://dl.acm.org/citation.cfm?id=2832415.2832466|consulté le=2018-02-07|pages=1558–1564}}</ref>. 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<ref>{{Article|langue=|auteur1=|prénom1=Giuseppe|nom1=De Giacomo|prénom2=Moshe Y.|nom2=Vardi|titre=LTL f and LDL f synthesis under partial observability|périodique=IJCAI|éditeur=AAAI Press|date=2016-07-09|isbn=9781577357704|issn=|lire en ligne=http://dl.acm.org/citation.cfm?id=3060621.3060766|consulté le=2018-02-07|pages=1044–1050}}</ref>. 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<ref>{{Article|langue=|auteur1=Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi|titre=Symbolic LTLf Synthesis|périodique=IJCAI|date=2017|issn=|lire en ligne=https://www.ijcai.org/proceedings/2017/0189.pdf|pages=p. 1362-1369}}</ref>.


Plusieurs outils existent : Acacia+<ref>{{Article|langue=en|prénom1=Aaron|nom1=Bohy|prénom2=Véronique|nom2=Bruyère|prénom3=Emmanuel|nom3=Filiot|prénom4=Naiyong|nom4=Jin|titre=Acacia+, a Tool for LTL Synthesis|périodique=Computer Aided Verification|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=2012-07-07|isbn=9783642314230|doi=10.1007/978-3-642-31424-7_45|lire en ligne=https://link.springer.com/chapter/10.1007/978-3-642-31424-7_45|consulté le=2018-02-07|pages=652–657}}</ref>, Unbeast<ref>{{Article|langue=en|prénom1=Rüdiger|nom1=Ehlers|titre=Unbeast: Symbolic Bounded Synthesis|périodique=Tools and Algorithms for the Construction and Analysis of Systems|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=2011-03-26|isbn=9783642198342|doi=10.1007/978-3-642-19835-9_25|lire en ligne=https://link.springer.com/chapter/10.1007/978-3-642-19835-9_25|consulté le=2018-02-07|pages=272–275}}</ref>, Ratsy<ref>{{Article|prénom1=Roderick|nom1=Bloem|prénom2=Krishnendu|nom2=Chatterjee|prénom3=Karin|nom3=Greimel|prénom4=Thomas A.|nom4=Henzinger|titre=Synthesizing robust systems|périodique=Acta Informatica|volume=51|numéro=3-4|date=2014-06-01|issn=0001-5903|doi=10.1007/s00236-013-0191-5|lire en ligne=http://dl.acm.org/citation.cfm?id=2629836.2629889|consulté le=2018-02-07|pages=193–220}}</ref>.
Plusieurs outils existent : Acacia+<ref>{{Article|langue=en|prénom1=Aaron|nom1=Bohy|prénom2=Véronique|nom2=Bruyère|prénom3=Emmanuel|nom3=Filiot|prénom4=Naiyong|nom4=Jin|titre=Acacia+, a Tool for LTL Synthesis|périodique=Computer Aided Verification|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=2012-07-07|isbn=9783642314230|doi=10.1007/978-3-642-31424-7_45|lire en ligne=https://link.springer.com/chapter/10.1007/978-3-642-31424-7_45|consulté le=2018-02-07|pages=652–657}}</ref>, Unbeast<ref>{{Article|langue=en|prénom1=Rüdiger|nom1=Ehlers|titre=Unbeast: Symbolic Bounded Synthesis|périodique=Tools and Algorithms for the Construction and Analysis of Systems|série=Lecture Notes in Computer Science|éditeur=Springer, Berlin, Heidelberg|date=2011-03-26|isbn=9783642198342|doi=10.1007/978-3-642-19835-9_25|lire en ligne=https://link.springer.com/chapter/10.1007/978-3-642-19835-9_25|consulté le=2018-02-07|pages=272–275}}</ref>, Ratsy<ref>{{Article|prénom1=Roderick|nom1=Bloem|prénom2=Krishnendu|nom2=Chatterjee|prénom3=Karin|nom3=Greimel|prénom4=Thomas A.|nom4=Henzinger|titre=Synthesizing robust systems|périodique=Acta Informatica|volume=51|numéro=3-4|date=2014-06-01|issn=0001-5903|doi=10.1007/s00236-013-0191-5|lire en ligne=http://dl.acm.org/citation.cfm?id=2629836.2629889|consulté le=2018-02-07|pages=193–220}}</ref>.

Version du 8 février 2018 à 12:13

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

Plusieurs méthodes ont été proposés, par Büchi et Landweber[3] et par Rabin[4]. 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 en logique temporelle linéaire (LTL) a été introduit par Pnueli et Rosner[5] en 1989. Ils ont démontré que ce problème est 2EXPTIME-complet. En 1998, Asarin, Maler, Pnueli et Sifakis présente un algorithme de synthèse d'automates temporisés[6]. Alur et La Torre montre que le problème de synthèse est entre PSPACE et EXPSPACE pour un fragment de LTL[7]. 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 polynomial[8]. 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[9]. 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[10]. 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[11].

Plusieurs outils existent : Acacia+[12], Unbeast[13], Ratsy[14].

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. ↑ (en) J. Richard Buchi et Lawrence H. Landweber, The Collected Works of J. Richard Büchi, Springer, New York, NY, (ISBN 9781461389309 et 9781461389286, DOI 10.1007/978-1-4613-8928-6_29, lire en ligne), p. 525–541
  4. ↑ Michael Oser Rabin, Automata on Infinite Objects and Church's Problem, American Mathematical Society, (ISBN 0821816632, lire en ligne)
  5. ↑ (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 )
  6. ↑ (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 )
  7. ↑ 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 )
  8. ↑ (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 )
  9. ↑ 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 )
  10. ↑ 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 )
  11. ↑ Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi, « Symbolic LTLf Synthesis », IJCAI,‎ , p. 1362-1369 (lire en ligne)
  12. ↑ (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 )
  13. ↑ (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 )
  14. ↑ 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 )
Ce document provient de « https://fr.wikipedia.org/w/index.php?title=Synthèse_de_programmes&oldid=145287619 ».