On polynomial-size programs winning finite-state games

Abstract

Finite-state reactive programs are identified with finite automata which realize winning strategies in Büchi-Landweber games. The games are specified by finite “game graphs” equipped with different winning conditions (“Rabin condition”, “Streett condition” and “Muller condition”, defined in analogy to the theory of ω-automata). We show that for two classes of games with Muller winning condition polynomials are both an upper and a lower bound for the size of winning reactive programs. Also we give a new proof for the existence of no-memory strategies in games with Rabin winning condition, as well as an exponential lower bound for games with Streett winning condition.