Reachability Games and Game Semantics: Comparing Nondeterministic Programs

We investigate the notions of may- and mustapproximation in Erratic Idealized Algol (a nondeterministic extension of Idealized Algol), and give explicit characterizations of both inside its game model. Notably, must-approximation is captured by a novel preorder on nondeterministic strategies, whose definition is formulated in terms of winning regions in a reachability game. The game is played on traces of one of the strategies and its objective is reaching a complete position without encountering any divergences. The concrete accounts of may- and must-approximation make it possible to derive tight complexity bounds for the corresponding decision problems in the finitary (finite datatypes) variant EIAf of Erratic Idealized Algol. In fact we give a complete classification of the complexity of may- and must-approximation for fragments of EIAf of bounded type order (for terms in β-normal form). The complexity of the decidable cases ranges from PSPACE to 2EXPTIME for may-approximation...

• Type: Conference
• Year: 2008
• Where: LICS
• Authors: Andrzej S. Murawski
• Keywords: Computer Science, Erratic Idealized Algol, Idealized Algol, LICS 2008, Nondeterministic Strategies