This paper by K. Etessami from the University of Edinburgh's School of Informatics explores the analysis of recursive game graphs to model interprocedural control flow in open systems. The authors use these models, which are closely related to pushdown systems and pushdown games, to determine whether there are input sequences that can lead the system into "bad/good" executions. The paper introduces alternative algorithms for solving well-studied problems such as reachability and Büchi winning strategies in such games. These algorithms are based on solutions to second-order data flow equations, generalizing the Datalog rules used in previous work on recursive state machines. The approach offers a simpler conceptual view and provides technical advantages over existing methods, particularly in terms of space efficiency, by avoiding the exponential space blow-up associated with certain algorithms and not relying on automata to represent winning configurations. The results are closely related to the work of Walukiewicz and Cachat, but offer a more efficient and "automaton-free" solution.This paper by K. Etessami from the University of Edinburgh's School of Informatics explores the analysis of recursive game graphs to model interprocedural control flow in open systems. The authors use these models, which are closely related to pushdown systems and pushdown games, to determine whether there are input sequences that can lead the system into "bad/good" executions. The paper introduces alternative algorithms for solving well-studied problems such as reachability and Büchi winning strategies in such games. These algorithms are based on solutions to second-order data flow equations, generalizing the Datalog rules used in previous work on recursive state machines. The approach offers a simpler conceptual view and provides technical advantages over existing methods, particularly in terms of space efficiency, by avoiding the exponential space blow-up associated with certain algorithms and not relying on automata to represent winning configurations. The results are closely related to the work of Walukiewicz and Cachat, but offer a more efficient and "automaton-free" solution.