Reachability Games and Game Semantics: Comparing Nondeterministic Programs

11 years 11 months ago
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...
Andrzej S. Murawski
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Where LICS
Authors Andrzej S. Murawski
Comments (0)