Document Open Access Logo

Optimal Assumptions for Synthesis

Author Romain Brenguier

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.8.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Author Details

Romain Brenguier

Cite As Get BibTex

Romain Brenguier. Optimal Assumptions for Synthesis. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.8

Abstract

Controller synthesis is the automatic construction a correct system from its specification.
  This often requires assumptions about the behaviour of the environment.
  It is difficult for the designer to identify the assumptions that ensures the existence of a correct controller, and doing so manually can lead to assumptions that are stronger than necessary.
  As a consequence the generated controllers are suboptimal in terms of robustness.
  In this work, given a specification, we identify the weakest assumptions that ensure the existence of a controller.
  We also consider two important classes of assumptions: the ones that can be ensured by the environment and assumptions that restricts only inputs of the systems.
  We show that optimal assumptions correspond to strongly winning strategies, admissible strategies and remorse-free strategies depending on the classes.
  Using these correspondences, we then propose an algorithm for computing optimal assumptions that can be ensured by the environment.

Subject Classification

Keywords
  • Controller synthesis
  • Parity games
  • Admissible strategies

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Dietmar Berwanger. Admissibility in infinite games. In STACS, volume 4393 of LNCS, pages 188-199. Springer, February 2007. Google Scholar
  2. Roderick Bloem, Rüdiger Ehlers, Swen Jacobs, and Robert Könighofer. How to handle assumptions in synthesis. In SYNT, pages 34-50, 2014. URL: http://dx.doi.org/10.4204/EPTCS.157.7.
  3. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Acacia+, a tool for LTL synthesis. In Computer Aided Verification, pages 652-657. Springer, 2012. Google Scholar
  4. Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. In CONCUR, volume 42 of LIPIcs, pages 100-113. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.100.
  5. Romain Brenguier, Jean-François Raskin, and Mathieu Sassolas. The complexity of admissibility in omega-regular games. In CSL-LICS '14, 2014. ACM, 2014. URL: http://dx.doi.org/10.1145/2603088.2603143.
  6. Krishnendu Chatterjee and Thomas A Henzinger. Assume-guarantee synthesis. In TACAS'07, volume 4424 of LNCS. Springer, 2007. Google Scholar
  7. Krishnendu Chatterjee, Thomas A. Henzinger, and Barbara Jobstmann. Environment assumptions for synthesis. In CONCUR, pages 147-161. Springer, 2008. Google Scholar
  8. Werner Damm and Bernd Finkbeiner. Does it pay to extend the perimeter of a world model? In FM 2011: Formal Methods, pages 12-26. Springer, 2011. Google Scholar
  9. E Allen Emerson and Charanjit S Jutla. Tree automata, mu-calculus and determinacy. In 32nd Annual Symposium on Foundations of Computer Science, pages 368-377. IEEE, 1991. Google Scholar
  10. Marco Faella. Admissible strategies in infinite games over graphs. In MFCS 2009, volume 5734 of Lecture Notes in Computer Science, pages 307-318. Springer, 2009. Google Scholar
  11. Rachel Faran and Orna Kupferman. Spanning the spectrum from safety to liveness. In Automated Technology for Verification and Analysis, pages 183-200. Springer, 2015. Google Scholar
  12. Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. An antichain algorithm for LTL realizability. In Computer Aided Verification, pages 263-277. Springer, 2009. Google Scholar
  13. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag, New York, NY, USA, 2002. Google Scholar
  14. Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, and Adam Walker. The first reactive synthesis competition (SYNTCOMP 2014). Int J Softw Tools Technol Transfer, pages 1-24, 2016. URL: http://dx.doi.org/10.1007/s10009-016-0416-3.
  15. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 179-190. ACM, 1989. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact