Winning CaRet Games with Modular Strategies
Ilaria De Crescenzo, Salvatore La Torre · 2011
Abstract. Recursive state machines are a well-accepted formalism for modelling the control flow of systems with potentially recursive procedure calls. In the open systems setting, i.e., systems where an execution depends on the interaction of the system with the environment, the natural counterpart is two-player recursive game graphs which essentially are recursive state machines where vertices are split into two sets each controlled by one of the players. We focus on solving games played on such graphs with respect to winning conditions expressed by a formula of the temporal logic CaRet and such that the protagonist can only use modular strategies (modular CaRet games). In a modular strategy, the protagonist may use as memory only the portion of the play which is local to the current activation of the current module. Therefore, every time a module is entered, the memory used by the protagonist gets reset. The main motivation for considering modular strategies is related to the synthesis of system controllers. In fact, a modular strategy would correspond to a modular controller for the considered system. Modular strategies have been already studied with winning conditions expressed as reachability, safety, Büchi automata or LTL formulas. In this paper we extend these results to non-regular winning conditions by considering specifications expressed in CaRet. In particular, we show that deciding whether the protagonist has a winning modular strategy in a CaRet game is 2ExpTime-complete, that matches the complexity of deciding modular LTL games. 1