=Paper=
{{Paper
|id=None
|storemode=property
|title=Winning CaRet Games with Modular Strategies
|pdfUrl=https://ceur-ws.org/Vol-810/paper-s01.pdf
|volume=Vol-810
|dblpUrl=https://dblp.org/rec/conf/cilc/CrescenzoT11
}}
==Winning CaRet Games with Modular Strategies==
https://ceur-ws.org/Vol-810/paper-s01.pdf
Winning CaRet Games with Modular
Strategies?
Ilaria De Crescenzo and Salvatore La Torre
Dipartimento di Informatica
Università degli Studi di Salerno
Abstract. Recursive state machines are a well-accepted formalism for
modelling the control flow of systems with potentially recursive proce-
dure calls. In the open systems setting, i.e., systems where an execution
depends on the interaction of the system with the environment, the nat-
ural 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 Introduction
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 verification of open systems, and are useful tools for solving decision problems
such as, for example, the model-checking of the µ-calculus formulas (see [6, 9]).
In controller synthesis, given a description of the system where some of the
choices depend upon the input and some represent uncontrollable internal non-
determinism, 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 Università
degli Studi di Salerno (Italy).
so that the product of the controller and the system satisfies the correctness
specification, that clearly corresponds to computing winning strategies in two-
player games. See [10] for a survey.
In the open systems setting, for instance, the Alternating Temporal Logic
allows specification of requirements such as “module A can ensure delivery of
the message no matter how module B behaves” [2]; module checking deals with
the problem of checking whether a module behaves correctly no matter in which
environment it is placed [8].
In this paper, we focus on pushdown systems. Pushdown systems accurately
model the control flow in programs of sequential imperative programming lan-
guages 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 specifies for each
play ending into a controlled state the next move such that each resulting play
satisfies the winning conditions [5, 12].
Here, we consider modular strategies [4], that are strategies where the next
move is determined only looking at the local memory of the current activation
of the current module. It is known that modular reachability games are NP-
complete [4]. Also, modular strategies have been considered for winning condi-
tions expressed as an ω-regular language, using Büchi, Co-Büchi automata or
linear temporal logic formulas, and in particular, modular LTL games are known
to be 2ExpTime-complete [3].
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 [1]. The logic CaRet combines the temporal modalities of LTL
with different kinds of successor (global, abstract and caller ) and can express
both regular requirements and a variety of non-regular properties such as partial
and total correctness of program blocks or inspection of the stack. By using
an automaton theoretic approach, we show that solving the modular CaRet
games is decidible within double exponential time. Since modular LTL games
are already 2ExpTime-hard and CaRet sintactically includes LTL, we get that
also modular CaRet games are 2ExpTime-complete.
2 Preliminary
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 different 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 partic-
ular, 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 defined 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 definition of an RGG we refer the reader to [4].
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 definitions on recursive game graphs,
strategies and modular strategies we refer the reader to [4].
−
Syntax ϕ := p | ϕ ∨ ϕ | ¬ ϕ | g
ϕ| a
ϕ| ϕ | ϕ U g ϕ | ϕ U a ϕ | ϕ U − ϕ (where
p ∈ AP ∪ {call, ret, int} )
Semantics for a word α = α1 , α2 , α3 , ..., αn , ... ∈ Σ̂ ω and n ∈ N :
– (α, n) |= p iff αn = (X, d) and p ∈ X or p = d
– (α, n) |= ϕ1 ∨ ϕ2 iff (α, n) |= ϕ1 or (α, n) |= ϕ2
– (α, n) |= ¬ϕ iff (α, n) 2 ϕ
– (α, n) |= g ϕ iff (α, succg α (n)) |= ϕ, i.e., iff (α, n + 1) |= ϕ
– (α, n) |= a ϕ iff succa a
α (n)) 6= ⊥ and (α, succα (n)) |= ϕ
– (α, n) |= − ϕ iff succ− α (n)) 6
= ⊥ and (α, succ −
α (n)) |= ϕ
– (α, n) |= ϕ1 U b ϕ2 (for any b ∈ {g, a, −}) iff there is a sequence of position
i0 , i1 , ..., ik , where i0 = n, (α, ik ) |= ϕ2 and for every 0 ≤ j ≤ k − 1, ij + 1 =
succbα (ij )) and (α, ij ) |= ϕ1
Fig. 1. Syntax and semantics of CaRet.
CaRet. Let Σ = 2AP where AP is a finite set of atomic propositions. We
consider the augmented alphabet of Σ that is Σ̂ = Σ × {call, ret, int}.
The syntax and the semantics of CaRet are reported in Fig. 1. We refer the
reader to [1] for a detailed definition of CaRet.
In this logic, three different 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 ) → a q]. 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 satisfied
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 definitions for modular CaRet games can be
found in [13].
3 Solving modular CaRet games
In this section, we briefly sketch our solution to CaRet games. For the omitted
details, we refer the interested reader to [13].
Our solution consists of three main steps.
Let hG, ϕi be a modular CaRet game.
The first step consists of constructing from hG, ϕi an equivalent game hG0 , colori
with parity winning conditions such that |G0 | = O(2|ϕ| ) . We build on the top
of the construction given in [1] for model checking CaRet formulas. The main
differences are that we apply the construction to the negation of the formula
ϕ instead of to the formula ϕ directly, and introduce fresh nodes to ensure the
correct semantics of the interaction of the two players. Negating the formula is
needed to use correctly the construction from [1]. We recall that this construc-
tion, such as all the constructions which are tableau based, are nondeterministic
and therefore cannot be directly combined with a game graph in a cross product.
Starting from the negated formula, we can apply the same tableau construction
but now interpreting the nondeterminism as universality, and thus dualizing also
the winning conditions we obtain a game graph which is equivalent to the start-
ing one with respect to the considered decision problem. The resulting winning
condition is the conjunction of a Büchi condition with a generalized co-Büchi
one, that can be simplified to a single pair Rabin condition and thus to an
equivalent parity condition.
Also, notice that both G and ϕ can define context-free languages, and prob-
lems such as inclusion and emptiness of intersection are undecidable for context-
free languages [7]. Therefore, translating ϕ into an automaton and then inter-
secting it with the recursive game graph does not seem feasible.
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 [3].
The resulting automaton accepts a strategy tree iff it corresponds to a winning
modular strategy.
For the last step of our solution, we observe that by using [11] we can convert
Awin to a one-way nondeterministic tree automaton and take its intersection
with the Astrat that is a tree automaton accepting strategy trees. Thus, we get a
one-way nondeterministic automaton A0 which accepts a tree iff it corresponds
to a winning strategy tree. Checking the emptiness of this automaton takes
polynomial time in the number of states and exponential in the number of colors
in the parity condition [10].
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.
References
1. R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and
returns. In Proc. of the 10th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems, TACAS’04, LNCS 2988, pages 467–481.
Springer, 2004.
2. R. Alur, T. Henzinger, and O. Kupferman. Alternating-time temporal logic. Jour-
nal of the ACM, 49(5):1–42, 2002.
3. R. Alur, S. La Torre, and P. Madhusudan. Modular strategies for infinite games
on recursive graphs. In Proc. of the 15th International Conference on Computer
Aided Verification, CAV’03, LNCS 2725, pages 67-79. Springer, 2003.
4. R. Alur, S. La Torre, and P. Madhusudan. Modular strategies for recursive game
graphs. In Proc. 9th Intern. Conf. on Tools and Algorithms for the Construction
and the Analysis of Systems, TACAS’03, LNCS 2619, pages 363–378. Springer,
2003.
5. T. Cachat. Symbolic strategy synthesis for games on pushdown graphs. In Au-
tomata, Languages and Programming, 29th Int’l Coll., ICALP, Malaga, Spain, July
8-13, 2002, Proceedings, LNCS 2380, pages 704–715. Springer.
6. E. A. Emerson. Model checking and the mu-calculus. In N. Immerman and P. Ko-
laitis, editors, Proceedings of the DIMACS Symposium on Descriptive Complexity
and Finite Models, pages 185–214. American Mathematical Society Press, 1997.
7. J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages,
and Computation. Addison-Wesley, 1979.
8. O. Kupferman, M. Vardi, and P. Wolper. Module checking. Information and
Computation, 164(2):322–344, 2001.
9. W. Thomas. Languages, automata, and logic. Handbook of Formal Language
Theory, III:389–455, 1997.
10. W. Thomas. Infinite games and verification. In Proceedings of the International
Conference on Computer Aided Verification CAV’02, LNCS 2404, pages 58–64.
Springer, 2002.
11. M. Vardi. Reasoning about the past with two-way automata. In Proc. 14th Intern.
Coll. on Automata, Languages, and Programming, ICALP’98, LNCS 1443 , pages
628–641. Springer, 1998.
12. I. Walukiewicz. Pushdown processes: Games and model-checking. Information and
Computation, 164(2):234–263, January 2001.
13. Giochi su Grafi Pushdown rispetto a Strategie Modulari.
http://www.dia.unisa.it/professori/latorre/ilaDec/tesi2011.pdf, 2011