TY - CHAP

T1 - Modular strategies for infinite games on recursive graphs

AU - Alur, Rajeev

AU - La Torre, Salvatore

AU - Madhusudan, P.

PY - 2003

Y1 - 2003

N2 - In this paper, we focus on solving games in recursive game graphs that can model the control flow of sequential programs with recursive procedure calls. The winning condition is given as an ω-regular specification over the observable, and, unlike traditional pushdown games, the strategy is required to be modular: resolution of choices within a component should not depend on the context in which the component is invoked, but only on the history within the current invocation of the component. We first consider the case when the specification is given as a deterministic Büchi automaton. We show the problem to be decidable, and present a solution based on two-way alternating tree automata with time complexity that is polynomial in the number of internal nodes, exponential in the specification and exponential in the number of exits of the components. We show that the problem is EXPTIME-complete in general, and NP-complete for fixed-size specifications. Then, we show that the same complexity bounds apply if the specification is given as a universal co-Büchi automaton. Finally, for specifications given as formulas of linear temporal logic LTL, we obtain a synthesis algorithm that is doubly-exponential in the formula and singly exponential in the number of exits of components.

AB - In this paper, we focus on solving games in recursive game graphs that can model the control flow of sequential programs with recursive procedure calls. The winning condition is given as an ω-regular specification over the observable, and, unlike traditional pushdown games, the strategy is required to be modular: resolution of choices within a component should not depend on the context in which the component is invoked, but only on the history within the current invocation of the component. We first consider the case when the specification is given as a deterministic Büchi automaton. We show the problem to be decidable, and present a solution based on two-way alternating tree automata with time complexity that is polynomial in the number of internal nodes, exponential in the specification and exponential in the number of exits of the components. We show that the problem is EXPTIME-complete in general, and NP-complete for fixed-size specifications. Then, we show that the same complexity bounds apply if the specification is given as a universal co-Büchi automaton. Finally, for specifications given as formulas of linear temporal logic LTL, we obtain a synthesis algorithm that is doubly-exponential in the formula and singly exponential in the number of exits of components.

UR - http://www.scopus.com/inward/record.url?scp=33644689137&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33644689137&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-45069-6_6

DO - 10.1007/978-3-540-45069-6_6

M3 - Chapter

AN - SCOPUS:33644689137

SN - 3540405240

SN - 9783540405245

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 67

EP - 79

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Hunt, Warren A.

A2 - Somenzi, Fabio

PB - Springer

ER -