Perspective Games with Notifications

Authors Orna Kupferman, Noam Shenwald

Thumbnail PDF


  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

Orna Kupferman
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel
Noam Shenwald
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel

Cite AsGet BibTex

Orna Kupferman and Noam Shenwald. Perspective Games with Notifications. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 51:1-51:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


A reactive system has to satisfy its specification in all environments. Accordingly, design of correct reactive systems corresponds to the synthesis of winning strategies in games that model the interaction between the system and its environment. The game is played on a graph whose vertices are partitioned among the players. The players jointly generate a path in the graph, with each player deciding the successor vertex whenever the path reaches a vertex she owns. The objective of the system player is to force the computation induced by the generated infinite path to satisfy a given specification. The traditional way of modelling uncertainty in such games is observation-based. There, uncertainty is longitudinal: the players partially observe all vertices in the history. Recently, researchers introduced perspective games, where uncertainty is transverse: players fully observe the vertices they own and have no information about the behavior of the computation between visits in such vertices. We introduce and study perspective games with notifications: uncertainty is still transverse, yet a player may be notified about events that happen between visits in vertices she owns. We distinguish between structural notifications, for example about visits in some vertices, and behavioral notifications, for example about the computation exhibiting a certain behavior. We study the theoretic properties of perspective games with notifications, and the problem of deciding whether a player has a winning perspective strategy. Such a strategy depends only on the visible history, which consists of both visits in vertices the player owns and notifications during visits in other vertices. We show that the problem is EXPTIME-complete for objectives given by a deterministic or universal parity automaton over an alphabet that labels the vertices of the game, and notifications given by a deterministic satellite, and is 2EXPTIME-complete for LTL objectives. In all cases, the complexity in the size of the graph and the satellite is polynomial - exponentially easier than games with observation-based partial visibility. We also analyze the complexity of the problem for richer types of satellites.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Logic and verification
  • Games
  • Incomplete Information
  • Automata


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


  1. S. Agarwal, M. S. Kodialam, and T. V. Lakshman. Traffic engineering in software defined networks. In Proc. 32nd IEEE International Conference on Computer Communications, pages 2211-2219, 2013. Google Scholar
  2. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. Google Scholar
  3. D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, and T. A. Henzinger. Strategy construction for parity games with imperfect information. Information and Computation, 208(10):1206-1220, 2010. Google Scholar
  4. R. Bloem, K. Chatterjee, and B. Jobstmann. Graph games and reactive synthesis. In Handbook of Model Checking., pages 921-962. Springer, 2018. Google Scholar
  5. K. Chatterjee and L. Doyen. The complexity of partial-observation parity games. In Proc. 16th Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning, pages 1-14. Springer, 2010. Google Scholar
  6. K. Chatterjee, L. Doyen, T. A. Henzinger, and J-F. Raskin. Algorithms for ω-regular games with imperfect information. In Proc. 15th Annual Conf. of the European Association for Computer Science Logic, volume 4207 of Lecture Notes in Computer Science, pages 287-302, 2006. Google Scholar
  7. D. Fisman and O. Kupferman. Reasoning about finite-state switched systems. In 5th International Haifa Verification Conference, volume 6405 of Lecture Notes in Computer Science, pages 71-86. Springer, 2009. Google Scholar
  8. O. Kupferman and G. Vardi. Perspective games. In Proc. 34th IEEE Symp. on Logic in Computer Science, pages 1-13, 2019. Google Scholar
  9. O. Kupferman and M.Y. Vardi. Synthesis with incomplete information. In Advances in Temporal Logic, pages 109-127. Kluwer Academic Publishers, 2000. Google Scholar
  10. O. Kupferman and M.Y. Vardi. Safraless decision procedures. In Proc. 46th IEEE Symp. on Foundations of Computer Science, pages 531-540, 2005. Google Scholar
  11. D. Liberzon. Switching in Systems and Control. Birkhauser, 2003. Google Scholar
  12. Y. Lustig and M.Y. Vardi. Synthesis from component libraries. Software Tools for Technology Transfer, 15(5-6):603-618, 2013. Google Scholar
  13. M. Margaliot. Stability analysis of switched systems using variational principles: an introduction. Automatica, 42(12):2059-2077, 2006. Google Scholar
  14. D.A. Martin. Borel determinacy. Annals of Mathematics, 65:363-371, 1975. Google Scholar
  15. B. Puchala. Asynchronous omega-regular games with partial information. In 35th Int. Symp. on Mathematical Foundations of Computer Science, pages 592-603. Springer, 2010. Google Scholar
  16. J.H. Reif. The complexity of two-player games of incomplete information. Journal of Computer and Systems Science, 29:274-301, 1984. Google Scholar
  17. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. Google Scholar