Games on pushdown graphs and extensions

Two player games are a standard model of reactive computation, where e.g. one player is the controller and the other is the environment. A game is won by a player if she has a winning strategy, ie, if she can win every play. Given a finite description of the game, our aim is to compute the winner and a winning strategy. For finite graphs these problems have been solved for a long time, although some complexity questions remain open. We consider several classes of infinite graphs, from transition graphs of pushdown automata up to graphs of the Caucal hierarchy, and we investigate different winning conditions: reachability, recurrence (Büchi), parity, and the a called Sigma_3-condition. Two kinds of techniques are developed: a symbolic approach based on finite automata recognizing infinite sets of configurations and a game simulation which reduces a given game into a simpler one and solves it. Different kinds of strategies are also constructed: either positional or based on pushdown stack memories.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2003

Author dc:creator

• Cachat, Thierry

Contributors dc:contributor

• Thomas, Wolfgang

• info:eu-repo/classification/ddc/004
• Zweipersonen-Nullsummenspiel
• Unendliches Spiel
• Unendlicher Graph
• Berechnungskomplexität
• Endlicher Automat
• Informatik
• infinite games
• verification
• pushdown graph

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-114327%22

OAI record oai:identifier

https://publications.rwth-aachen.de/oai2d?verb=GetRecord&metadataPrefix=oai_dc&identifier=oai%3Apublications.rwth-aachen.de%3A52085