Document Open Access Logo

Optimally Resilient Strategies in Pushdown Safety Games

Authors Daniel Neider, Patrick Totzke , Martin Zimmermann

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2020.74.pdf
  • Filesize: 0.49 MB
  • 15 pages

Document Identifiers

Author Details

Daniel Neider
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Patrick Totzke
  • University of Liverpool, UK
Martin Zimmermann
  • University of Liverpool, UK

Funding

  • Zimmermann, Martin: Supported by the EPSRC grant EP/S032207/1.

Cite As Get BibTex

Daniel Neider, Patrick Totzke, and Martin Zimmermann. Optimally Resilient Strategies in Pushdown Safety Games. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 74:1-74:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.MFCS.2020.74

Abstract

Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resilience against non-antagonistic external influence. This concerns events where the observed system behavior differs from the intended one prescribed by the controller. For games played on finite arenas it is known that computing optimally resilient strategies only incurs a polynomial overhead over solving classical games.
This paper studies safety games with disturbances played on infinite arenas induced by pushdown systems. We show how to compute optimally resilient strategies in triply-exponential time. For the subclass of safety games played on one-counter configuration graphs, we show that determining the degree of resilience of the initial configuration is PSPACE-complete and that optimally resilient strategies can be computed in doubly-exponential time.

Subject Classification

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

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, and Patrick Totzke. Infinite-state energy games. In CSL-LICS 2014, pages 7:1-7:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603100.
  2. Shaull Almagor and Orna Kupferman. Latticed-LTL synthesis in the presence of noisy inputs. Discrete Event Dynamic Systems, 27(3):547-572, 2017. URL: https://doi.org/10.1007/s10626-017-0242-0.
  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: https://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 CAV 2009, volume 5643 of LNCS, pages 140-156. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_14.
  5. Stanislav Böhm, Stefan Göller, and Petr Jancar. Bisimulation equivalence and regularity for real-time one-counter automata. J. Comput. Syst. Sci., 80(4):720-743, 2014. URL: https://doi.org/10.1016/j.jcss.2013.11.003.
  6. Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jirí Srba. Infinite runs in weighted timed automata with energy constraints. In FORMATS 2008, volume 5215 of LNCS, pages 33-47. Springer, 2008. Google Scholar
  7. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc., 138:295-311, 1969. Google Scholar
  8. Thierry Cachat. Symbolic strategy synthesis for games on pushdown graphs. In ICALP 2002, volume 2380 of LNCS, pages 704-715. Springer, 2002. URL: https://doi.org/10.1007/3-540-45465-9_60.
  9. Thierry Cachat. Higher order pushdown automata, the caucal hierarchy of graphs and parity games. In ICALP 2003, volume 2719 of LNCS, pages 556-569. Springer, 2003. URL: https://doi.org/10.1007/3-540-45061-0_45.
  10. Arnaud Carayol and Matthew Hague. Optimal strategies in pushdown reachability games. In MFCS 2018, volume 117 of LIPIcs, pages 42:1-42:14. Schloss Dagstuhl - LZI, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.42.
  11. Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. Resource interfaces. In EMSOFT 2003, volume 2855 of LNCS, pages 117-133. Springer, 2003. Google Scholar
  12. Anne Condon. On algorithms for simple stochastic games. In Advances in Computational Complexity Theory, pages 51-73. American Mathematical Society, 1993. Google Scholar
  13. 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: https://doi.org/10.1109/CDC.2016.7799416.
  14. L. Doyen and J.-F. Raskin. Games with imperfect information: Theory and algorithms. In Lectures in Game Theory for Computer Scientists, pages 185-212. Cambridge University Press, 2011. Google Scholar
  15. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In ICSE 1999, pages 411-420. ACM, 1999. URL: https://doi.org/10.1145/302405.302672.
  16. Kousha Etessami and Mihalis Yannakakis. Recursive markov decision processes and recursive stochastic games. J. ACM, 62(2):11:1-11:69, 2015. URL: https://doi.org/10.1145/2699431.
  17. Wladimir Fridman and Martin Zimmermann. Playing pushdown parity games in a hurry. In GandALF 2012, volume 96 of EPTCS, pages 183-196, 2012. URL: https://doi.org/10.4204/EPTCS.96.14.
  18. 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: https://doi.org/10.1007/3-540-36387-4.
  19. Lukás Holík, Roland Meyer, and Sebastian Muskalla. Summaries for context-free games. In FSTTCS, volume 65 of LIPIcs, pages 41:1-41:16. Schloss Dagstuhl - LZI, 2016. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2016.41.
  20. Frederick A. Hosch and Lawrence H. Landweber. Finite delay solutions for sequential conditions. In ICALP 1972, pages 45-60. North-Holland, Amsterdam, 1972. Google Scholar
  21. 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: https://doi.org/10.1109/TSE.2015.2510001.
  22. Paul Hunter. Reachability in succinct one-counter games. In Mikołaj Bojańczyk, Slawomir Lasota, and Igor Potapov, editors, RP 2015, volume 9328 of LNCS, pages 37-49. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24537-9_5.
  23. Petr Jancar and Zdenek Sawa. A note on emptiness for alternating finite automata with a one-letter alphabet. Inf. Process. Lett., 104(5):164-167, 2007. URL: https://doi.org/10.1016/j.ipl.2007.06.006.
  24. Orna Kupferman and Moshe Y. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In CAV 2000, volume 1855 of LNCS, pages 36-52. Springer, 2000. URL: https://doi.org/10.1007/10722167_7.
  25. 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: https://doi.org/10.1145/2539036.2539044.
  26. David E. Muller and Paul E. Schupp. The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci., 37:51-75, 1985. URL: https://doi.org/10.1016/0304-3975(85)90087-8.
  27. Daniel Neider. Reachability games on automatic graphs. In CIAA 2010, volume 6482 of LNCS, pages 222-230. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-18098-9_24.
  28. Daniel Neider and Ufuk Topcu. An automaton learning approach to solving safety games over infinite graphs. In TACAS 2016, volume 9636 of LNCS, pages 204-221. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_12.
  29. Daniel Neider, Patrick Totzke, and Martin Zimmermann. Optimally resilient strategies in pushdown safety games. arXiv, 1912.04771, 2019. Google Scholar
  30. Daniel Neider, Alexander Weinert, and Martin Zimmermann. Synthesizing optimally resilient controllers. In CSL 2018, volume 119 of LIPIcs, pages 34:1-34:17. Schloss Dagstuhl - LZI, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.34.
  31. Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL 1995, pages 49-61. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199462.
  32. Thomas W. Reps, Akash Lal, and Nicholas Kidd. Program analysis using weighted pushdown systems. In FSTTCS 2007, volume 4855 of LNCS, pages 23-51. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-77050-3_4.
  33. Géraud Sénizergues. L(A)=L(B)? decidability results from complete formal systems. Theor. Comput. Sci., 251(1-2):1-166, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00285-1.
  34. Géraud Sénizergues. The bisimulation problem for equational graphs of finite out-degree. SIAM J. Comput., 34(5):1025-1106, 2005. URL: https://doi.org/10.1137/S0097539700377256.
  35. Olivier Serre. Parity games played on transition graphs of one-counter processes. In FOSSACS 2006, volume 3921 of LNCS, pages 337-351. Springer, 2006. URL: https://doi.org/10.1007/11690634_23.
  36. Jiří Srba. Roadmap of infinite results. In Gheorghe Paun, Grzegorz Rozenberg, and Arto Salomaa, editors, Current Trends in Theoretical Computer Science, pages 337–-350. World Scientific, 2004. URL: https://doi.org/10.1142/9789812562494_0054.
  37. 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: https://doi.org/10.1109/TAC.2014.2351632.
  38. 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: https://doi.org/10.4230/LIPIcs.CSL.2016.10.
  39. Ufuk Topcu, Necmiye Ozay, Jun Liu, and Richard M. Murray. On synthesizing robust discrete controllers under modeling uncertainty. In HSCC 2012, pages 85-94. ACM, 2012. URL: https://doi.org/10.1145/2185632.2185648.
  40. Leslie G. Valiant. Decision Procedures for Families of Deterministic Pushdown Automata. PhD thesis, University of Warwick, 1973. Google Scholar
  41. Yaron Velner and Alexander Rabinovich. Church synthesis problem for noisy input. In FoSSaCS 2011, volume 6604 of LNCS, pages 275-289. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_19.
  42. Igor Walukiewicz. Pushdown processes: Games and model-checking. Inf. Comput., 164(2):234-263, 2001. URL: https://doi.org/10.1006/inco.2000.2894.
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