Document Open Access Logo

Synthesizing Optimally Resilient Controllers

Authors Daniel Neider, Alexander Weinert, Martin Zimmermann

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2018.34.pdf
  • Filesize: 0.5 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Controller Synthesis
  • Infinite Games
  • Resilient Strategies
  • Disturbances

Metrics

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

Abstract

Recently, Dallal, Neider, and Tabuada studied a generalization of the classical game-theoretic model used in program synthesis, which additionally accounts for unmodeled intermittent disturbances. In this extended framework, one is interested in computing optimally resilient strategies, i.e., strategies that are resilient against as many disturbances as possible. Dallal, Neider, and Tabuada showed how to compute such strategies for safety specifications.
In this work, we compute optimally resilient strategies for a much wider range of winning conditions and show that they do not require more memory than winning strategies in the classical model. Our algorithms only have a polynomial overhead in comparison to the ones computing winning strategies. In particular, for parity conditions optimally resilient strategies are positional and can be computed in quasipolynomial time.

Cite As Get BibTex

Daniel Neider, Alexander Weinert, and Martin Zimmermann. Synthesizing Optimally Resilient Controllers. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.34

Author Details

Daniel Neider
  • Max Planck Institute for Software Systems, 67663 Kaiserslautern, Germany
Alexander Weinert
  • Reactive Systems Group, Saarland University, 66123 Saarbrücken, Germany
Martin Zimmermann
  • Reactive Systems Group, Saarland University, 66123 Saarbrücken, Germany

Funding

  • Weinert, Alexander: Supported by the Saarbrücken Graduate School of Computer Science.
  • Zimmermann, Martin: Supported by the project "TriCS" (ZI 1516/1-1) of the German Research Foundation (DFG).

References

  1. Paul C. Attie, Anish Arora, and E. Allen Emerson. Synthesis of fault-tolerant concurrent programs. ACM Trans. Program. Lang. Syst., 26(1):125-185, 2004. URL: http://dx.doi.org/10.1145/963778.963782.
  2. Julien Bernet, David Janin, and Igor Walukiewicz. Permissive strategies: from parity games to safety games. ITA, 36(3):261-275, 2002. URL: http://dx.doi.org/10.1051/ita:2002013.
  3. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, and Robert Könighofer. Synthesizing robust systems. Acta Inf., 51(3-4):193-220, 2014. URL: http://dx.doi.org/10.1007/s00236-013-0191-5.
  4. Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, and Barbara Jobstmann. Better quality in synthesis through quantitative objectives. In Ahmed Bouajjani and Oded Maler, editors, CAV 2009, volume 5643 of LNCS, pages 140-156. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02658-4_14.
  5. Roderick Bloem, Rüdiger Ehlers, Swen Jacobs, and Robert Könighofer. How to handle assumptions in synthesis. In Krishnendu Chatterjee, Rüdiger Ehlers, and Susmit Jha, editors, SYNT 2014, volume 157 of EPTCS, pages 34-50, 2014. URL: http://dx.doi.org/10.4204/EPTCS.157.7.
  6. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of Reactive(1) designs. J. Comput. Syst. Sci., 78(3):911-938, 2012. URL: http://dx.doi.org/10.1016/j.jcss.2011.08.007.
  7. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Benjamin Monmege, Guillermo A. Pérez, and Gabriel Renault. Quantitative games under failures. In FSTTCS 2015, volume 45 of LIPIcs, pages 293-306. Schloss Dagstuhl - LZI, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.293.
  8. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, STOC 2017, pages 252-263. ACM, 2017. URL: http://dx.doi.org/10.1145/3055399.3055409.
  9. Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theor. Comput. Sci., 458:49-60, 2012. URL: http://dx.doi.org/10.1016/j.tcs.2012.07.038.
  10. Eric Dallal, Daniel Neider, and Paulo Tabuada. Synthesis of safety controllers robust to unmodeled intermittent disturbances. In CDC 2016, pages 7425-7430. IEEE, 2016. URL: http://dx.doi.org/10.1109/CDC.2016.7799416.
  11. Ali Ebnenasir, Sandeep S. Kulkarni, and Anish Arora. FTSyn: a framework for automatic synthesis of fault-tolerance. STTT, 10(5):455-471, 2008. URL: http://dx.doi.org/10.1007/s10009-008-0083-0.
  12. Rüdiger Ehlers and Ufuk Topcu. Resilience to intermittent assumption violations in reactive synthesis. In Martin Fränzle and John Lygeros, editors, HSCC 2014, pages 203-212. ACM, 2014. URL: http://dx.doi.org/10.1145/2562059.2562128.
  13. Alain Girault and Éric Rutten. Automating the addition of fault tolerance with discrete controller synthesis. Form. Meth. in Sys. Des., 35(2):190-225, 2009. URL: http://dx.doi.org/10.1007/s10703-009-0084-y.
  14. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-36387-4.
  15. Chung-Hao Huang, Doron A. Peled, Sven Schewe, and Farn Wang. A game-theoretic foundation for the maximum software resilience against dense errors. IEEE Trans. Software Eng., 42(7):605-622, 2016. URL: http://dx.doi.org/10.1109/TSE.2015.2510001.
  16. Rupak Majumdar, Elaine Render, and Paulo Tabuada. A theory of robust omega-regular software synthesis. ACM Trans. Embedded Comput. Syst., 13(3):48:1-48:27, 2013. URL: http://dx.doi.org/10.1145/2539036.2539044.
  17. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102:363-371, 1975. Google Scholar
  18. Daniel Neider, Alexander Weinert, and Martin Zimmermann. Synthesizing optimally resilient controllers. arXiv, 1709.04854, 2017. URL: https://arxiv.org/abs/1709.04854.
  19. Paulo Tabuada, Sina Yamac Caliskan, Matthias Rungger, and Rupak Majumdar. Towards robustness for cyber-physical systems. IEEE Trans. Automat. Contr., 59(12):3151-3163, 2014. URL: http://dx.doi.org/10.1109/TAC.2014.2351632.
  20. Paulo Tabuada and Daniel Neider. Robust linear temporal logic. In CSL 2016, volume 62 of LIPIcs, pages 10:1-10:21. Schloss Dagstuhl - LZI, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.10.
  21. Ufuk Topcu, Necmiye Ozay, Jun Liu, and Richard M. Murray. On synthesizing robust discrete controllers under modeling uncertainty. In Thao Dang and Ian M. Mitchell, editors, HSCC 2012, pages 85-94. ACM, 2012. URL: http://dx.doi.org/10.1145/2185632.2185648.
  22. Johan van Benthem. An essay on sabotage and obstruction. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, volume 2605 of LNCS, pages 268-276. Springer, 2005. URL: http://dx.doi.org/10.1007/978-3-540-32254-2_16.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact