Recursive state machines are a well-accepted formalism for modelling the control ow 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, Buchi automata or LTL formulas. In this paper we extend these results to non-regular winning conditions by considering speci cations 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.
The interest for games naturally arises in many contexts. In the formal analysis
of systems, games are closely related to the controller synthesis problem and to
the veri cation of open systems, and are useful tools for solving decision problems
such as, for example, the model-checking of the -calculus formulas (see [
In controller synthesis, given a description of the system where some of the
choices depend upon the input and some represent uncontrollable internal
nondeterminism, the goal is to design a controller that supplies inputs to the system
? This work was partially funded by the MIUR grants FARB 2009-2010 Universita
degli Studi di Salerno (Italy).
so that the product of the controller and the system satis es the correctness
speci cation, that clearly corresponds to computing winning strategies in
twoplayer games. See [
In the open systems setting, for instance, the Alternating Temporal Logic
allows speci cation of requirements such as \module A can ensure delivery of
the message no matter how module B behaves" [
In this paper, we focus on pushdown systems. Pushdown systems accurately
model the control ow in programs of sequential imperative programming
languages with recursive procedure calls. A large number of hardware and software
systems can be captured by this model, such as programs of object oriented
languages, systems with distributed architectures and communication protocols.
The study of games on such systems has traditionally focused on determining
the existence of a winning strategy, that is a mapping that speci es for each
play ending into a controlled state the next move such that each resulting play
satis es the winning conditions [
Here, we consider modular strategies [
We extend the results on modular strategies to a more general class of winning
conditions. We allow winning conditions expressed as formulas of the temporal
logic CaRet [
Recursive game graph. A recursive game graph (RGG) is composed of game modules that are essentially two-player graphs (i.e., graphs whose vertices are partitioned into two sets depending on the player who controls the outgoing moves) with entry and exit nodes and two di erent kinds of vertices: the nodes and the boxes. A node is a standard graph vertex and a box corresponds to invocations of other game modules in a potentially recursive manner (in particular, entering into a box corresponds to a module call and exiting from a box corresponds to a return from a module). Each RGG has a distinct game module which is called the start module. A state of an RGG is composed by a call stack and a node. The notion of run can be de ned analogously to the computation of a standard procedural program (the modules corresponding to the procedures). A play of an RGG is a run starting from an entry node of the start module.
For a formal de nition of an RGG we refer the reader to [
Strategies. Given a player P , a strategy is a function that associates a move to every run that ends in a node controlled by P . A modular strategy consists of a set of local strategies, one for each game module, that are used together as a global strategy for a player . A local strategy for a module can only refer to the local memory of the module, i.e. the sequence of vertices that correspond to internal nodes, call or returns of the module. This sequence corresponds to the portion of the play concerning to the current invocation of the module.
For detailed comments and formal de nitions on recursive game graphs,
strategies and modular strategies we refer the reader to [
Syntax Semantics ' := p j ' _ ' j : ' j g' j a' j ' j ' Ug' j ' Ua' j ' U ' (where p 2 AP [ fcall, ret, intg ) for a word = 1; 2; 3; :::; n; ::: 2 ^! and n 2 N : { ( ; n) j= p i n = (X; d) and p 2 X or p = d { ( ; n) j= '1 _ '2 i ( ; n) j= '1 or ( ; n) j= '2 { ( ; n) j= :'g 'i i( (; n;)s2uc'cg (n)) j= ', i.e., i ( ; n + 1) j= ' { ( ; n) j= { ( ; n) j= a' i succa (n)) 6= ? and ( ; succa (n)) j= ' { ( ; n) j= ' i succ (n)) 6= ? and ( ; succ (n)) j= ' { ( ; n) j= '1 Ub'2 (for any b 2 fg; a; g) i there is a sequence of position i0; i1; :::; ik; where i0 = n; ( ; ik) j= '2 and for every 0 j k 1; ij + 1 = succb (ij)) and ( ; ij) j= '1
CaRet. Let = 2AP where AP is a nite set of atomic propositions. We consider the augmented alphabet of that is ^ = fcall; ret; intg.
The syntax and the semantics of CaRet are reported in Fig. 1. We refer the
reader to [
In this logic, three di erent notions of successor are used: { the global-successor (succg) which is the usual successor function. It points to next node, whatever module it belongs; { the abstract-successor (succa) which, for internal moves, corresponds to the global successor and for calls corresponds to the matching returns; { the caller successor (succ ) which is a "past" modality that points to the innermost unmatched call.
Typical properties that can be expressed by the logic CaRet are pre and post conditions. An example is the formula 2[(call ^ p ^ pA) ! aq]. If we assume that all calls to procedure A are characterized by the proposition pA, the formula expresses that if the pre-condition p holds when the procedure A is invoked, then the procedure terminates and the post-condition q is satis ed upon the return. This is the requirement of total correctness. Observe the use of the abstract next operator to refer to the return associated with the call. Modular CaRet games. A modular CaRet game is a pair hG; 'i where G is a RGG whose vertices (nodes, calls and returns) are labeled with a set of propositions and ' is a CaRet formula. Given a modular CaRet game hG; 'i we want solve the problem of deciding whether there exists a modular strategy such that the resulting plays are guaranteed to satisfy '.
Detailed comments and formal de nitions for modular CaRet games can be
found in [
In this section, we brie y sketch our solution to CaRet games. For the omitted
details, we refer the interested reader to [
Our solution consists of three main steps.
Let hG; 'i be a modular CaRet game.
The rst step consists of constructing from hG; 'i an equivalent game hG0; colori
with parity winning conditions such that jG0j = O(2j'j) . We build on the top
of the construction given in [
Also, notice that both G and ' can de ne context-free languages, and
problems such as inclusion and emptiness of intersection are undecidable for
contextfree languages [
The second step consists of constructing from the parity game hG0; colori a
two-way alternating parity tree automaton Awin similarly to what is done in [
For the last step of our solution, we observe that by using [
Since the constructed recursive game graph G0 is doubly exponential in the formula ' and linear in the recursive game graph G, color is constant and LTL games are already 2ExpTime-hard, we get: Theorem 1. Deciding modular CaRet games is 2ExpTime-complete.