Localized Attractor Computations for Infinite-State Games

Explore a 33-minute lecture on localized attractor computations for infinite-state games presented by Rayna Dimitrova from CISPA Helmholtz Center for Information Security. Delve into a novel technique for solving infinite-state games, commonly used to model reactive systems with unbounded data domains. Discover how this approach enhances symbolic game-solving by utilizing results from localized attractor computations in sub-games. Learn about the method of identifying useful sub-games through permissive winning strategy templates in finite abstractions. Examine the experimental evaluation demonstrating the technique's superior performance and its applicability to complex infinite-state games beyond current capabilities. Gain insights into this joint work with Philippe Heim, Satya Prakash Nayak, and Anne-Kathrin Schmuck, presented as part of the Games and Equilibria in System Design and Analysis series at the Simons Institute.