Analysis of Recursive Game Graphs Using Data Flow Equations

Analysis of Recursive Game Graphs Using Data Flow Equations

2004 | K. Etessami
This paper presents an analysis of recursive game graphs using data flow equations to determine reachability and Büchi winning strategies in open systems. Recursive game graphs are used to model interprocedural control flow in recursive programs, and are closely related to pushdown systems and pushdown games. The paper describes alternative algorithms for these problems, based on solutions to second-order data flow equations, which generalize the Datalog rules used in previous work for analyzing recursive state machines. These algorithms offer a conceptually simpler view of these well-studied problems and highlight the close links between program analysis and model checking techniques. The paper also discusses technical advantages of the equational approach, such as avoiding the exponential-space blow-up incurred by Walukiewicz's algorithms for pushdown games. Unlike previous approaches, this method does not rely on automata to represent winning configurations, but instead maintains only minimal sets of exits that can be forced. This provides potential for greater space efficiency and allows for an "automaton-free" version of previous algorithms. The paper also discusses the results of Walukiewicz, who showed that determining the existence of winning strategies under certain conditions is in EXPTIME. His algorithm involves constructing an exponentially larger game graph, which is not practical for large inputs. However, alternative algorithms based on regular sets of reaching configurations have been developed, which avoid this exponential blow-up but require the construction of alternating automata. The paper concludes by describing alternative algorithms for determining reachability and Büchi strategies on recursive game graphs, which are based on data flow equations and generalize previous approaches. These algorithms are closely related to those used for computing modular strategies, but differ in their complexity and approach.This paper presents an analysis of recursive game graphs using data flow equations to determine reachability and Büchi winning strategies in open systems. Recursive game graphs are used to model interprocedural control flow in recursive programs, and are closely related to pushdown systems and pushdown games. The paper describes alternative algorithms for these problems, based on solutions to second-order data flow equations, which generalize the Datalog rules used in previous work for analyzing recursive state machines. These algorithms offer a conceptually simpler view of these well-studied problems and highlight the close links between program analysis and model checking techniques. The paper also discusses technical advantages of the equational approach, such as avoiding the exponential-space blow-up incurred by Walukiewicz's algorithms for pushdown games. Unlike previous approaches, this method does not rely on automata to represent winning configurations, but instead maintains only minimal sets of exits that can be forced. This provides potential for greater space efficiency and allows for an "automaton-free" version of previous algorithms. The paper also discusses the results of Walukiewicz, who showed that determining the existence of winning strategies under certain conditions is in EXPTIME. His algorithm involves constructing an exponentially larger game graph, which is not practical for large inputs. However, alternative algorithms based on regular sets of reaching configurations have been developed, which avoid this exponential blow-up but require the construction of alternating automata. The paper concludes by describing alternative algorithms for determining reachability and Büchi strategies on recursive game graphs, which are based on data flow equations and generalize previous approaches. These algorithms are closely related to those used for computing modular strategies, but differ in their complexity and approach.
Reach us at info@study.space
[slides and audio] Analysis of Recursive Game Graphs Using Data Flow Equations