Benjamin Aminof

Axel Legay
email: alegay@irisa.fr

Aniello Murano
email: murano@na.infn.it

Olivier Serre
email: olivier.serre@liafa.jussieu.fr

Moshe Y Vardi
email: vardi@cs.rice.edu

Pushdown Module Checking with Imperfect Information ✩

Keywords: Model checking, open systems, infinite-state systems, branching-time temporal-logics, games

The model checking problem for finite-state open systems (module checking) has been extensively studied in the literature, both in the context of environments with perfect and imperfect information about the system. Recently, the perfect information case has been extended to infinite-state systems (pushdown module checking). In this part, we extend pushdown module checking to the imperfect information setting; i.e., to the case where the environment has only a partial view of the system's control states and pushdown store content. We study the complexity of this problem with respect to the branching-time temporal logics CTL, CTL * and the propositional µ-calculus. We show that pushdown module checking, which is by itself harder than pushdown model checking, becomes undecidable when the environment has imperfect information.

We also show that undecidability relies on hiding information about the pushdown store. Indeed, we prove that with imperfect information about the control states, but a visible pushdown store, the problem is decidable and its complexity is 2Exptime-complete for CTL and the propositional µ-calculus, and 3Exptime-complete for CTL * .

Introduction

In system modeling we distinguish between closed and open systems [START_REF] Harel | On the development of reactive systems[END_REF]. In a closed system all the nondeterministic choices are internal, and resolved by the system. In an open system there are also external nondeterministic choices, which are resolved by the environment [START_REF] Hoare | Communicating Sequential Processes[END_REF]. In order to check whether a closed system satisfies a required property, we translate the system into some formal model, specify the property with a temporal-logic formula, and check formally that the model satisfies the formula. Hence, the name model checking for the verification methods derived from this viewpoint ( [START_REF] Clarke | Design and verification of synchronization skeletons using branching time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent programs in Cesar[END_REF]).

In [START_REF] Kupferman | Module checking[END_REF][START_REF] Kupferman | Module Checking[END_REF], Kupferman, Vardi, and Wolper studied open finite-state systems. In their framework, the open finite-state system is described by a labeled state-transition graph called a module, whose set of states is partitioned into a set of system states (where the system makes a transition) and a set of environment states (where the environment makes a transition). Given a module M describing the system to be verified, and a temporal logic formula ϕ specifying the desired behavior of the system, the problem of model checking a module, called module checking, asks whether for all possible environments M satisfies ϕ. In particular, it might be that the environment does not enable all the external nondeterministic choices. Module checking thus involves not only checking that the full computation tree T M , V M obtained by unwinding M (which corresponds to the interaction of M with a maximal environment) satisfies the specification ϕ, but also that every tree obtained from it by pruning children of environment nodes (this corresponds to the different choices of different environments) satisfy ϕ.

For example, consider an ATM machine that allows customers to deposit money, withdraw money, check balance, etc. The machine is an open system and an environment for it is a subset of the set of all possible infinite lines of customers, each with its own plans. Accordingly, there are many different possible environments to consider. It is shown in [START_REF] Kupferman | Module checking[END_REF][START_REF] Kupferman | Module Checking[END_REF] that for formulas in branching time temporal logics, module checking open finite-state systems is exponentially harder than model checking closed finite-state systems.

In [START_REF] Kupferman | Module checking revisited[END_REF] module checking has been extended to a setting where the envi-ronment has imperfect information1 about the state of the system (see also [START_REF] Chatterjee | Semiperfect-information games[END_REF][START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF], for related work regarding imperfect information). In this setting, every state of the module is a composition of visible and invisible variables, where the latter are hidden from the environment. While a composition of a module M with an environment with perfect information corresponds to arbitrary disabling of transitions in M, the composition of M with an environment with imperfect information is such that whenever two computations of the system differ only in the values of internal variables along them, the disabling of transitions along them coincide. For example, in the above ATM machine, a person does not know, before he asks for money, whether or not the ATM has run out of paper for printing receipts. Thus, the possible behaviors of the environment are independent of this missing information. Given an open system M with a partition of M's variables into visible and invisible ones, and a temporal logic formula ϕ, the module-checking problem with imperfect information asks whether ϕ is satisfied by all trees obtained by pruning children of environment nodes from T M , V M , according to environments whose nondeterministic choices are independent of the invisible variables. One of the results shown in [START_REF] Kupferman | Module checking revisited[END_REF] is thatCTL module checking with imperfect information is Exptime-complete.

In recent years, model checking of pushdown systems has received a lot of attention (see for example [START_REF] Walukiewicz | Pushdown processes: Games and Model Checking[END_REF][START_REF] Walukiewicz | Model checking CTL properties of pushdown systems[END_REF][START_REF] Bouajjani | Reachability Analysis of Pushdown Automata: Application to Model-Checking[END_REF][START_REF] Esparza | Model checking LTL with regular valuations for pushdown systems[END_REF]), largely due to the ability of pushdown systems to capture the flow of procedure calls and returns in programs [START_REF] Alur | Analysis of recursive state machines[END_REF]. Recently, [START_REF] Bozzelli | Pushdown module checking[END_REF] extended these techniques by introducing open pushdown systems (with perfect information) that interact with their environment. It is shown in [START_REF] Bozzelli | Pushdown module checking[END_REF] that CTL pushdown module checking is 2Exptime-complete and thus much harder than pushdown model checking.

Consider again the example of the ATM machine, where the information regarding the presence of printing paper is invisible to the customers. Suppose also that the ATM machine shows advertisements, and that it works under the constraint that the number of advertisements the customer must view, before the card can be taken out of the machine, is equal to the number of operations the customer performed. The described machine can be modeled as an open pushdown system M where control states take care of the operation performed by the ATM (interacting with customers), and the pushdown store is used to keep track of the advertisements that remain to be shown. Now, suppose that we want to verify that in all possible environments, it is always possible for an inserted card to be ejected. This requirement can be modeled by the CTL formula ϕ = AG(insert-card → EF eject-card). Since the presence of printing paper is invisible to the customers, we have imperfect information about the control states of the module. If we allow the ATM to push, after each operation the customer makes, an invisible number (possibly zero) of pending advertisements, then we also have invisible information in the pushdown store.

In this work we extend pushdown module checking by considering environments with imperfect information about the system's control state and pushdown store content. To this aim, we first have to define how a pushdown system keeps part of its internal configuration invisible to the environment and another part visible. In [START_REF] Peterson | Multiple-person alternation[END_REF], a private pushdown store automata is defined to be a Turing machine with two tapes: a read only public (visible) one-way input tape, and a possibly private (invisible) work tape, simulating a pushdown store. Unfortunately, their definition is not suitable for our purpose as it allows for only two levels of information hiding: either the pushdown store and control state are completely visible, or completely invisible. The definition we use instead is an extension of the idea used for finite-state systems. Like in the finite case, we assume the control states are assignments to boolean control variables, some of which are visible and some of which are invisible. Similarly, symbols of the pushdown store are assignments to boolean visible and invisible pushdown store variables.

In [START_REF] Kupferman | Module checking revisited[END_REF], each state is partitioned into input, output, and invisible variables, where the environment supplies the input variables, and the system supplies the output and invisible variables. This idea works well for finite statesystems but not when we have to deal with imperfect information about the pushdown store. Note that a symbol pushed now, influences the computation much later, when it becomes the top of the pushdown store. Indeed, asking the environment to supply as input part of each symbol in the pushdown, is asking it to intimately participate in the internals of the computation, which is less natural. We find it more natural to think of the environment as choosing the possible transitions at certain points of the computation. For example, if the environment supplies the current reading of a physical sensor, we think of it as disabling all the transitions that are irrelevant for this reading. Thus, we model an open pushdown system with imperfect information by partitioning configurations into system and environment configurations, and also partitioning states and pushdown store symbols into visible and invisible variables, combining features from both [START_REF] Kupferman | Module checking[END_REF] and [START_REF] Kupferman | Module checking revisited[END_REF].

We study the pushdown module-checking problem with imperfect information, with respect to the branching-time logics CTL, CTL * and the propositional µ-calculus. We show that the problem is undecidable in the general case, and that undecidability relies on hiding information about the pushdown store. In other words, the problem becomes decidable with imperfect information about the internal control states, but a visible pushdown store. We derive both the undecidability and the decidability results using an automata theoretic approach. For the undecidability, we give a reduction of the universality problem of nondeterministic pushdown automata on finite words, which is undecidable [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF], to the CTL pushdown module-checking problem with imperfect information. In order to derive the decidability results, we reduce the pushdown module-checking problem with imperfect state information to the emptiness problem of a new automata model that we call semi-alternating pushdown tree automata. These are alternating pushdown tree automata [START_REF] Kupferman | Pushdown specifications[END_REF] (see also [START_REF] Ladner | Alternating pushdown and stack automata[END_REF]), where the universality is not allowed on the pushdown store content. That is, two copies of the automaton that read the same input, from two configurations that have the same top of pushdown store, must push the same value into the pushdown store.

We consider two types of acceptance conditions for semi-alternating pushdown tree automata, one is the Büchi condition which is suitable for handling CTL, and the other is the parity condition which is suitable for CTL * and µ-calculus. We show that, for both acceptance conditions, semi-alternating pushdown tree automata can be translated to equivalent nondeterministic pushdown tree automata (with the same acceptance condition), for which the emptiness problem is decidable in exponential time [START_REF] Kupferman | Pushdown specifications[END_REF]. It is important to note that alternating pushdown automata, in contrast to the semi-alternating ones, are not equivalent to nondeterministic pushdown automata. Indeed, since the emptiness problem of the intersection of two context free languages is undecidable [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF], the emptiness problem of alternating pushdown automata is undecidable already in the case of finite words.

Overall, based on the above translations, we are able to show that the pushdown module checking problem with imperfect state information is decidable and 2Exptime-complete for CTL and propositional µ-calculus specifications, and is 3Exptime-complete for CTL * specifications. Hence, in all cases, it is not harder than perfect information pushdown module checking.

Preliminaries

Trees

Let Υ be a set. An Υ-tree is a prefix closed subset T ⊆ Υ * . The elements of T are called nodes and the empty word ε is the root of T . For v ∈ T , the set of

children of v (in T ) is child(T, v) = {v • x ∈ T | x ∈ Υ}. Given a node v = u • x,
with u ∈ Υ * and x ∈ Υ, we define last(v) to be x. We also say that v corresponds to x. The complete Υ-tree is the tree Υ * . For v ∈ T , a (full) path π of T from v is a minimal set π ⊆ T such that v ∈ π and for each v ′ ∈ π such that child(T, v ′ ) = ∅, there is exactly one node in child(T, v ′ ) belonging to π. Note that every infinite word w ∈ Υ ω can be thought of as an infinite path in the tree Υ * , namely the path containing all the finite prefixes of w. For an alphabet Σ, a Σ-labeled Υ-tree is a pair T, V where T is an Υ-tree and V : T → Σ maps each node of T to a symbol in Σ.

The propositinal µ-Calculus

The µ-calculus is a propositional modal logic augmented with least and greatest fixpoint operators. We consider a µ-calculus where formulas are constructed from Boolean propositions with Boolean connectives, the temporal operators EX ("exists next") and AX ("for all next"), as well as least (µ) and greatest (ν) fixpoint operators. We assume that µ-calculus formulas are written in positive normal form (negation only applied to atomic propositions).

Formally, let AP and Var be finite and pairwise disjoint sets of atomic propositions and propositional variables. The set of µ-calculus formulas over AP and Var is the smallest set such that • true and false are formulas;

• p and ¬p, for p ∈ Prop, are formulas;

• x ∈ Var is a formula;

• ϕ 1 ∨ ϕ 2 and ϕ 1 ∧ ϕ 2 are formulas if ϕ 1 and ϕ 2 are formulas;

• AXϕ and EXϕ are formulas if ϕ is a formula;

• µy.ϕ(y) and νy.ϕ(y) are formulas if y is a propositional variable and ϕ(y) is a formula containing y as a free variable.

Observe that we use positive normal form, i.e., negation is applied only to atomic propositions.

We call µ and ν fixpoint operators and use λ to denote a fixpoint operator µ or ν. A propositional variable y occurs free in a formula if it is not in the scope of a fixpoint operator λy, and bounded otherwise. Note that y may occur both bounded and free in a formula. A sentence is a formula that contains no free variables. For a formula λy.ϕ(y), we write ϕ(λy.ϕ(y)) to denote the formula that is obtained by one-step unfolding, i.e., replacing each free occurrence of y in ϕ with λy.ϕ(y).

The closure cl(ϕ) of a µ-calculus sentence ϕ is the smallest set of µcalculus formulas that contains ϕ and is closed under sub-formulas (that is, if ψ is in the closure, then so do all its sub-formulas that are sentences) and fixpoint applications (that is, if λy.ϕ(y) is in the closure, then so is ϕ(λy.ϕ(y))). For every µ-calculus formula ϕ, the number of elements in cl(ϕ) is linear in the length of ϕ. Accordingly, we define the size |ϕ| of ϕ to be the number of elements in cl(ϕ). A µ-calculus formula is guarded if for every variable y, all the occurrences of y that are in a scope of a fixpoint modality λ are also in a scope of a modality AX or EX that is itself in the scope of λ. Thus, a µ-calculus sentence is guarded if for all y ∈ Var , all the occurrences of y are in the scope of a next modality. Given a µ-calculus formula, it is always possible to construct in linear time an equivalent guarded formula (c.f., [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF][START_REF] Bonatti | The complexity of enriched µ-calculi[END_REF]).

The semantics of the µ-calculus is defined with respect to a Kripke structure K = AP , W, R, w 0 , L , where AP is a set of atomic propositions, W is a finite set of states, R ⊆ W × W is a transition relation that must be total (i.e., for every w ∈ W there exists w ′ ∈ W such that (w, w ′ ) ∈ R), w 0 is an initial state, and L : W → 2 AP maps each state to the set of atomic propositions true in that state. If (w, w ′ ) ∈ R, we say that w ′ is a successor of w. A path in K is an infinite sequence of states, π = w 0 , w 1 , . . . such that for every i ≥ 0, (w i , w i+1 ) ∈ R. We denote the suffix w i , w i+1 , . . . of π by π i . We define the size |K| of K as |W | + |R|.

Informally, a formula EXϕ holds at a state w of a Kripke structure K if ϕ holds at least in one successor of w. Dually, the formula AXϕ holds in a state w of a Kripke structure K if ϕ holds in all successors of w. Readers not familiar with fixpoints might want to look at [START_REF] Kozen | Results on the propositional mu-calculus[END_REF][START_REF] Streett | An automata theoretic decision procedure for the propositional µ-calculus[END_REF][START_REF] Bradfield | Modal µ-calculi[END_REF] for instructive examples and explanations of the semantics of the µ-calculus. To formalize the semantics, we introduce valuations that allow to associate sets of points to variables. Given a Kripke structure K = AP , W, R, w 0 , L and a set {y 1 , . . . , y n } of propositional variables in Var, a valuation V : {y 1 , . . . , y n } → 2 W is an assignment of subsets of W to the variables y 1 , . . . , y n . For a valuation V, a variable y, and a set W ′ ⊆ W , we denote by V[y ← W ′ ] the valuation obtained from V by assigning W ′ to y. A formula ϕ with free variables among y 1 , . . . , y n is interpreted over the structure K as a mapping ϕ K from valuations to 2 W , i.e., ϕ K (V) denotes the set of states that satisfy ϕ under valuation V. The mapping ϕ K is defined inductively as follows:

• true K (V) = W and false K (V) = ∅; • for p ∈ AP , we have p K (V) = L(p) and (¬p) K (V) = W \ L(p);
• for y ∈ Var, we have y K (V) = V(y);

• (ϕ 1 ∧ ϕ 2 ) K (V) = ϕ K 1 (V) ∩ ϕ K 2 (V) • (ϕ 1 ∨ ϕ 2 ) K (V) = ϕ K 1 (V) ∪ ϕ K 2 (V); • (EXϕ) K (V) = {w ∈ W : ∃w ′ .(w, w ′ ) ∈ R and w ′ ∈ ϕ K (V)}; • (AXϕ) K (V) = {w ∈ W : ∀w ′ .if (w, w ′ ) ∈ R then w ′ ∈ ϕ K (V)}; • (µy.ϕ(y)) K (V) = {W ′ ⊆ W : ϕ K (V[y ← W ′ ]) ⊆ W ′ }; • (νy.ϕ(y)) K (V) = {W ′ ⊆ W : W ′ ⊆ ϕ K (V[y ← W ′ ])}.
Note that no valuation is required for a sentence. Let K = AP , W, R, w 0 , L be a Kripke structure and ϕ a sentence. For a state w ∈ W , we say that ϕ holds at w in

K, denoted K, w |= ϕ, if w ∈ ϕ K (∅). K is a model of ϕ if there is a w ∈ W such that K, w |= ϕ.
Finally, ϕ is satisfiable if it has a model.

The Temporal Logics CTL * and CTL

The logic CTL * combines both branching-time and linear-time operators [START_REF] Emerson | Sometimes and not never revisited: On branching versus linear time[END_REF]. A path quantifier, either A ("for all paths") or E ("for some path"), can prefix an assertion composed of an arbitrary combination of the linear-time operators X ("next time"), and U ("until"). A positive normal form CTL * formula is a CTL * formula in which negations are applied only to atomic propositions. It can be obtained by pushing negations inward as far as possible, using De Morgan's laws and dualities of quantifiers and temporal connectives. For technical convenience, we use the linear-time operator U as a dual of the U operator, and write all CTL * formulas in a positive normal form. There are two types of formulas in CTL * : state formulas, whose satisfaction is related to a specific state, and path formulas, whose satisfaction is related to a specific path. Formally, let AP be a set of atomic proposition names. A CTL * state formula is either:

• true, false, p, or ¬p, for all p ∈ AP ;

• ϕ 1 ∧ ϕ 2 or ϕ 1 ∨ ϕ 2 , where ϕ 1 and ϕ 2 are CTL * state formulas;

• Aψ or Eψ, where ψ is a CTL * path formula.

A CTL * path formula is either:

• A CTL * state formula; • ψ 1 ∧ ψ 2 , ψ 1 ∨ ψ 2 , Xψ 1 , ψ 1 U ψ 2 , or ψ 1 U ψ 2 ,
where ψ 1 and ψ 2 are CTL * path formulas.

CTL * is the set of state formulas generated by the above rules. We use the following abbreviations in writing formulas:

• F ψ = trueU ψ ("eventually").

• Gψ = false U ψ ("always").

The logic CTL is a restricted subset of CTL * in which the temporal operators must be immediately preceded by a path quantifier. Formally, it is the subset of CTL * obtained by restricting the path formulas to be Xϕ 1 , ϕ 1 U ϕ 2 , or ϕ 1 U ϕ 2 , where ϕ 1 and ϕ 2 are CTL state formulas.

The closure cl(ϕ) of a CTL * (CTL) formula ϕ is the set of all CTL * (CTL) state sub-formulas of ϕ (including ϕ, but excluding true and false). We define the size |ϕ| of ϕ as the number of elements in cl(ϕ). Note that, even though the number of elements in the closure of a formula can be logarithmic in the length of the formula if there are multiple occurrences of identical sub-formulas, our definition of size is legitimate since it corresponds to the number of nodes in a reduced DAG representation of the formula.

The notation K, w |= ϕ indicates that a CTL * state formula ϕ holds at the state w of the Kripke structure K. Similarly, K, π |= ψ indicates that a CTL * path formula ψ holds on a path π of the Kripke structure K. When K is clear from the context, we write w |= ϕ and π |= ψ. Also, K |= ϕ iff K, w 0 |= ϕ. The relation |= is inductively defined as follows.

• For all w, we have w |= true and w |= false.

• w |= p for p ∈ AP iff p ∈ L(w).

• w |= ¬p for p ∈ AP iff p ∈ L(w).

• w |= ϕ 1 ∧ ϕ 2 iff w |= ϕ 1 and w |= ϕ 2 . • w |= ϕ 1 ∨ ϕ 2 iff w |= ϕ 1 or w |= ϕ 2 .
• w |= Aψ iff for every path π = w 0 , w 1 , . . ., with w 0 = w, we have π |= ψ.

• w |= Eψ iff there exists a path π = w 0 , w 1 , . . ., with w 0 = w, such that π |= ψ.

• π |= ϕ for a state formula ϕ, iff w 0 |= ϕ where π = w 0 , w 1 , . . .

• π |= ψ 1 ∧ ψ 2 iff π |= ψ 1 and π |= ψ 2 . • π |= ψ 1 ∨ ψ 2 iff π |= ψ 1 or π |= ψ 2 . • π |= Xψ iff π 1 |= ψ.
• π |= ψ 1 U ψ 2 iff there exists i ≥ 0 such that π i |= ψ 2 and for all 0 ≤ j < i, we have π j |= ψ 1 .

• π |= ψ 1 U ψ 2 iff for all i ≥ 0 such that π i |= ψ 2 , there exists 0 ≤ j < i such that π j |= ψ 1 .

Note that π |= ψ 1 U ψ 2 if and only if π |= (¬ψ 1 )U (¬ψ 2 ). That is, a path π satisfies ψ 1 U ψ 2 if ψ 2 holds everywhere along π (thus, the U does not reach its eventuality), or if the first occurrence of ¬ψ 2 is strictly preceded by an occurrence of ψ 1 (thus, ¬ψ 1 is falsified before the eventuality is reached). Another way to understand the U operator is to interpret ψ 1 U ψ 2 by "as long as ψ 1 is false, ψ 2 must be true".

Open Systems

An open system is a system that interacts with its environment and whose behavior depends on this interaction. We consider the case where the environment has imperfect information about the system, i.e., when the system has internal variables that are not visible to its environment. We describe such a system by a module M = AP, W s , W e , w 0 , R, L, ∼ = , where AP is a finite set of atomic propositions, W s is a set of system states, and W e is a set of environment states. We assume W s ∩ W e = ∅, and call W = W s ∪ W e the set of M's states. w 0 ∈ W is the initial state, R ⊆ W × W is a total transition relation, L : W → 2 AP is a labeling function that maps each state of M to the set of atomic propositions that hold in it, and ∼ = is an equivalence relation on W .

In order to present a unified definition that is general enough to handle both finite-state and infinite-state systems, we model the fact that the environment has imperfect information about the states of the system by an equivalence relation ∼ =. States that are indistinguishable by the environment, because the difference between them is kept invisible by the system, are equivalent according to ∼ =. We write [W ] for the set of equivalence classes of W under ∼ =. Since states in the same equivalence class are indistinguishable by the environment, from the environment's point of view, the states of the system are actually the equivalence classes themselves. The equivalence class [w] of w ∈ W , is called the visible part of w, since it is in a sense what the environment "sees" of w. We write vis(w) instead of [w], to emphasize this. Note that we can also do the converse. That is, given a function vis, whose domain is W , we can define the equivalence relation ∼ = by letting w ∼ = w ′ iff vis(w) = vis(w ′ ). We can then think of the range of vis as the set of the equivalence classes [W ] and associate [w] with the value vis(w).

A module M is closed if W e = ∅ (meaning that M does not interact with any environment) and open otherwise. Since the designation of a state as an environment state is obviously known to the environment, we require that for every w, w ′ ∈ W such that w ∼ = w ′ , we have that w ∈ W e iff w ′ ∈ W e . Also note that if w ∼ = w ′ , from the environment's point of view, the set of atomic propositions that currently hold in w may just as well be L(w ′ ). We therefore define the labeling, as seen by the environment, as a function visL : [W ] → 2 2 AP that maps the visible part of a state to a set of possible sets of atomic propositions:

visL([u]) = {L(w) : w ∈ W ∧ w ∼ = u}. If it is always the case that w ∼ = w ′ =⇒ L(w) = L(w ′
), we say that the atomic propositions are visible.

For (w, w ′ ) ∈ R, we say that w ′ is a successor of w. The requirement that R be total means that every state w has at least one successor. A computation of M is a sequence w 0 • w 1 • • • of states, such that for all i ≥ 0 we have (w i , w i+1 ) ∈ R. For each w ∈ W , we denote by succ(w) the (possibly empty) set of w's successors. When the module M is in a system state w s , then all successor states are possible next states. On the other hand, when M is in an environment state w e , the environment decides, based on the visible parts of each successor of w e , and of the history of the computation so far, to which of the successor states the computation can proceed, and to which it can not.

The set of all (maximal) computations of M starting from the initial state w 0 can be described by an AP -labeled W -tree T M , V M called a computation tree, which is obtained by unwinding M in the usual way.

Each node v = v 1 • • • v k of T M , V M describes the (partial) computation w 0 • v 1 • • • v k of M, with the root ε corresponding to w 0 . The children of v are exactly all nodes of the form v 1 • • • v k •w
, where w ranges over all the successors of v k in M. We extend the definition of the vis function to nodes in the natural way. Thus, the visible part of a node v is vis

(v) = vis(v 1 ) • • • vis(v k ).
The labeling V M of a node v depends on the state it corresponds to (its last state), i.e., V M (v) = L(last(v)). Also, if v corresponds to an environment state, we say that v is an environment node.

The problem of deciding, for a given temporal logic formula ϕ, over the set AP of atomic propositions, whether T M , V M satisfies ϕ is the usual model checking problem (formally denoted M |= ϕ) [START_REF] Clarke | Design and verification of synchronization skeletons using branching time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent programs in Cesar[END_REF]. In model checking, we only have to consider the computation tree T M , V M , since the module we want to check is closed and thus its behavior is not affected by the environment. On the other hand, whenever we consider an open module, T M , V M corresponds to a very specific environment: a maximal environment that never restricts the set of next states. Therefore, when we examine a branching-time specification ϕ w.r.t. an open module M, the formula ϕ should hold not only in T M , V M , but in all the trees obtained by pruning from T M , V M subtrees whose roots are children (successors) of environment nodes, in accordance with all possible environments. It is important to note that in the case of perfect information (i.e., ∼ = is actually the equality relation), every such pruning corresponds to some environment; however, in the case of imperfect information, only if the pruning is consistent with the partial information available to the environment, will the tree correspond to an actual environment. Formally, if two nodes v and v ′ are indistinguishable, i.e., if vis(v) = vis(v ′ ), then a tree in which the subtree rooted at v is pruned, but the one rooted at v ′ is not pruned, does not correspond to any environment, and should not be considered. As noted in [START_REF] Kupferman | Module checking revisited[END_REF], the fact that given a pruning of T M , V M , a finite automaton cannot decide if that pruning corresponds to an actual environment or not, is the main source of difficulty in dealing with module checking with imperfect information. Also note that the knowledge-based subset construction that is used to transform games of imperfect information into ones of perfect information (see for example [START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF]), is not applicable in this context, since in general there is no connection between the satisfiability of a branching time formula on the original structure and its satisfiability on the one obtained by the knowledge-based subset construction.

Recall that whenever M interacts with an environment ξ, its possible moves from environment states depends on the behavior of ξ. We can think of an environment to M as a strategy ξ : [W ] * → {⊤, ⊥} that maps a finite history s of a computation, as seen by the environment, to either ⊤ or ⊥, meaning that the environment respectively allows or disallows M to trace s. We say that the tree [W ] * , ξ maintains the strategy applied by ξ, and we call it a strategy tree. We denote by M ✁ ξ the AP -labeled W -tree induced by the composition of T M , V M with ξ; that is, the AP -labeled Wtree obtained by pruning from T M , V M subtrees according to ξ. Note that by the definition above, ξ may disable all the children of a node v. Since we usually do not want the environment to completely block the system, we require that at least one child of each node is enabled. In this case, we say that the composition M ✁ ξ is deadlock free.

To see the interaction of M with ξ, let v ∈ T M be an environment node, and v ′ ∈ T M be one of its children. The subtree rooted in v ′ is pruned iff ξ(vis(v ′ )) = ⊥. Every two nodes v 1 and v 2 that are indistinguishable according to ξ's imperfect information have vis(v 1 ) = vis(v 2 ). Also, recall that the designation of a state as an environment state is based only on the visible part of that state. Thus, if v 1 is a child of an environment node then so is v 2 , and either both subtrees with roots v 1 and v 2 are pruned, or both are not. Note that once ξ(v) = ⊥ for some v ∈ [W ] * , we can ignore ξ(v • t), for all t ∈ [W ] * . Indeed, once the environment disables the transition to a certain node v, it actually disables the transitions to all the nodes in the subtree with root v. We can now formally define the interaction of an open module with an environment with imperfect information. From now on, unless stated differently, we always refer to modules that are open, and environments with imperfect information. Given a module M, and a strategy tree [W ] * , ξ for an environment ξ, an AP -labeled W -tree T, V corresponds to M ✁ ξ iff the following hold:

• The root of T corresponds to w 0 .

• For v ∈ T with last(v) ∈ W s , we have child(T, v) = {v • w 1 , . . . , v • w n },
where succ(last(v)) = {w 1 , . . . , w n }.

• For v ∈ T with last(v) ∈ W e , there is a nonempty subset {w 1 , . . . , w k } of succ(last(v)) such that child(T, v) = {v•w 1 , . . . , v•w k }. Furthermore, for all w in {w 1 , . . . , w k } we have that ξ(vis(v • w)) = ⊤, while for all w in succ(last(v)) \ {w 1 , . . . , w k } we have that ξ(vis(x • w)) = ⊥.

• For every node v ∈ T , we have that

V (v) = L(last(v)).
For a module M and a temporal logic formula over the set AP , we say that M reactively satisfies ϕ, denoted M |= r ϕ, if M ✁ ξ satisfy ϕ, for every environment ξ for which M ✁ ξ is deadlock free. The problem of deciding whether M |= r ϕ is called module checking, and was first introduced and studied in [START_REF] Kupferman | Module checking[END_REF][START_REF] Kupferman | Module Checking[END_REF] for finite-state systems with perfect information. The problem was successively extended to imperfect information in [START_REF] Kupferman | Module checking revisited[END_REF]. It has been shown that the complexity of both problems is Exptime-complete2 for CTL, and 2Exptime-complete for CTL * .

Definition of the Problem

In this section, we extend the notion of module checking with imperfect information to infinite-state systems induced by Open Pushdown Systems (OPD). Definition 1. An OPD is a tuple S = AP, Q, q 0 , Γ, ♭, δ, µ, Env , where AP is a finite set of atomic propositions, Q is the set of ( control) states, and q 0 ∈ Q is an initial state. We assume that Q ⊆ 2 I∪H where I and H are disjoint finite sets of visible and invisible control variables, respectively. Γ is a finite pushdown store alphabet, ♭ ∈ Γ is the pushdown store bottom symbol, and we use Γ ♭ to denote Γ ∪ {♭}. We assume that Γ ⊆ 2 I Γ ∪H Γ where I Γ and H Γ are disjoint finite sets of visible and invisible pushdown store variables, respectively. δ

⊆ (Q × Γ ♭ ) × (Q × Γ * ♭ ) is a finite transition relation, and µ : Q × Γ ♭ → 2 AP is a labeling function. Env ⊆ Q × Γ ♭ is used to specify the set of environment configurations. The size |S| of S is |Q| + |Γ| + |δ|, with |δ| = ((p,γ),(q,β))∈δ |β|.
A configuration of S is a pair (q, α), where q is a control state and α ∈ Γ * •♭ is a pushdown store content. We write top(α) for the leftmost symbol of α and call it the top of the pushdown store α. The OPD moves according to the transition relation. Thus, ((p, γ), (q, β)) ∈ δ implies that if the OPD is in state p and the top of the pushdown store is γ, it can move to state q, pop γ and push β. We assume that if ♭ is popped it gets pushed right back, and that it only gets pushed in such cases. Thus, ♭ is always present at the bottom of the pushdown store, and nowhere else. Note that we make this assumption also about the various pushdown automata we use later. Also note that the possible moves of the system, the labeling function, and the designation of configurations as environment configurations, are all dependent only on the current control state and the top of the pushdown store.

For a control state q ∈ Q, the visible part of q is vis(q) = q ∩ I. For a pushdown store symbol γ ∈ Γ, if γ ⊆ H Γ and γ = ∅ we set vis(γ) = ε, otherwise we set vis(γ) = γ ∩ I Γ . By setting vis(γ) = ε whenever γ consists entirely of invisible variables, we allow the system to completely hide a push operation (obviously, a corresponding pop will also be invisible). When such a push occurs, the environment does not see the symbol ∅ being pushed, rather, it sees no push at all. This is necessary since in many applications what is actually pushed is immaterial, and the information to be revealed or hidden is only the depth of the pushdown store. The visible part of a pushdown store content s = γ 0 • • • γ n • ♭ is defined in the natural way:

vis(s) = vis(γ 0 ) • • • vis(γ n ) • ♭.
The visible part of a configuration (q, α), is thus vis((q, α)) = (vis(q), vis(α)). As for modules, the designation of a configuration of an OPD as an environment configuration is known to the environment. Thus, we require that for every two configurations (q, α) and (q ′ , α ′ ) such that vis(q, top(α)) = vis(q ′ , top(α ′ )), it holds that (q, top(α)) ∈ Env iff (q ′ , top(α ′ )) ∈ Env. Definition 2. An OPD S = AP, Q, q 0 , Γ, ♭, δ, µ, Env induces an infinitestate module M S = AP, W s , W e , w 0 , R, L, ∼ = , where:

• AP is a set of atomic propositions;

• W s ∪ W e = Q × Γ * • ♭ is the set of configurations;
• W e is the set of configurations (q, α) such that (q, top(α)) ∈ Env;

• w 0 = (q 0 , ♭) is the initial configuration;

• R is a transition relation, where ((q, γ • α), (q ′ , β)) ∈ R iff there exist ((q, γ), (q ′ , β ′ )) ∈ δ such that β = β ′ • α;

• L((q, α)) = µ(q, top(α)) for all (q, α) ∈ W ;

• For every w, w ′ ∈ W , we have that w ∼ = w ′ iff vis(w) = vis(w ′ ).

To describe the interaction of an OPD S with its environment, we consider the interaction of the environment with the induced module M S . Indeed, every environment ξ of S, can be represented by a strategy tree [W ] * , ξ , and the composition M S ✁ ξ of [W ] * , ξ with T M S , V M S describes all the computations of S allowed by the environment ξ. We can thus define the following problem.

Pushdown module checking problem with imperfect information: Given an OPD S, and a temporal logic formula3 ϕ, decide whether M S |= r ϕ. I.e., whether M S ✁ ξ satisfy ϕ, for every environment ξ for which M S ✁ ξ is deadlock free.

Note that starting with an OPD S having Env = ∅ (that is, the behavior of S is not affected by any environment) the induced module is closed. In this case, the problem we address becomes the classical pushdown model checking problem, and for CTL specifications it has been studied in [START_REF] Walukiewicz | Pushdown processes: Games and Model Checking[END_REF][START_REF] Walukiewicz | Model checking CTL properties of pushdown systems[END_REF]. Also, if the OPD is open (Env = ∅) but there is no invisible information (both H and H Γ are empty), the addressed problem is called pushdown module checking with perfect information, and for CTL and CTL * specifications it has been studied in [START_REF] Bozzelli | Pushdown module checking[END_REF].

Undecidability of the General Case

In this section, we study the pushdown module checking problem with imperfect information and show that it is undecidable already for the case of CTL specifications. In the next section, we show that undecidability relies on the system's ability to hide information about the pushdown store. Namely, we prove that if we start with an OPD with H Γ = ∅, the problem becomes decidable (even if H = ∅), and its complexity is the same as that of pushdown module checking with perfect information.

Undecidability of the pushdown module checking problem with imperfect information is obtained by a reduction from the universality problem of nondeterministic pushdown automata on finite words (PDA), which is undecidable [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF]. That is, given a PDA P, we build an OPD S and a CTL formula ϕ, such that the module induced by S reactively satisfies ϕ iff P is universal.

Our choice to do a reduction from the universality problem of PDA is not at all arbitrary. It is well known that checking for the universality of a nondeterministic automaton can be thought of as a game between a protagonist trying to prove that the automaton is not universal, and an antagonist which claims that it is universal. The universality game is played as follows. The protagonist chooses the first input letter, the antagonist responds with the first part of the run, the protagonist chooses the next input letter, the antagonist extends the run, and so on. The protagonist wins if the resulting run is rejecting, and the antagonist wins if it is accepting. Note that if the automaton is not universal then the protagonist has a winning strategy, namely, choosing the letters of a word not accepted by the automaton. However, since the automaton is nondeterministic, the converse is not true. That is, even if the automaton is universal, the antagonist may not have a winning strategy. Also note that (again due to nondeterminism) if the protagonist can see the moves of the antagonist, it may force the run to be rejecting even though the word it supplies can be accepted by the automaton. Hence, the game is sound but not complete. However, if the protagonist cannot see the moves of the antagonist the game becomes sound and complete. Deciding if the automaton is not universal can be reduced to deciding whether the protagonist has a winning strategy in the corresponding universality game with imperfect information. By casting the universality game of PDA to a special instance of the pushdown module checking problem with imperfect information, the latter is shown to be undecidable. Theorem 1. CTL pushdown module-checking with imperfect information is undecidable.

Proof. Given a PDA P, we build an OPD S and a CTL formula ϕ, such that the module induced by S reactively satisfies ϕ iff P is universal. Let P = Σ, Γ, Q, q 0 , ♭, ∆, F be a PDA on finite words, with an input alphabet Σ, a pushdown store alphabet Γ, a set Q of states, an initial state q 0 , a bottom of pushdown store symbol ♭, a transition function ∆ :

Q × Σ × Γ ♭ → 2 Q×Γ *
♭ , and a set of accepting states F ⊆ Q. We assume without loss of generality that P never gets stuck on any input.

The OPD S simulates all the runs of P on all words in Σ * . The states of S are pairs of a state in Q and a letter in Σ. Each transition of P, that reads a letter σ moves to a state q and does some pushdown store operation, is simulated in S by a transition that goes to the state (q, σ) and does the same pushdown store operation. In order to have in S infinite computations that simulate runs of P on finite words, we allow S, at any point, to end the simulation of a run by moving to one of two special states q acc and q rej , depending on whether the computation corresponds to an accepting or a rejecting run of P, respectively. Once in q acc or q rej , the computation stays there forever. The visible part of a configuration ((q, σ), α) of S, is just σ. Thus, looking at a computation of S that simulates a run of P on a word σ 1 • • • σ n , the environment can only see the letters σ 1 , . . . , σ n . It follows that the environment cannot distinguish between different computations of S that correspond to runs of P on the same word. This ensures that the environment can not disable some, but not all, of these computations. Note that a word w ∈ Σ * is accepted by P iff there is a computation in S, corresponding to a run of P on w, that visits the state q acc . The formula ϕ will check this condition. Formally, let P = Σ, Γ, Q, q 0 , ♭, ∆, F be a PDA on finite words. We build an OPD S = AP, Q ′ , q ′ 0 , Γ ′ , ♭, δ, µ, Env where,

• AP = Σ ∪ {♯, Acc}, where ♯ and Acc are new symbols not in Σ (nor in Q).

• I = Σ ∪ {♯}, and

H = Q ∪ {Acc}. The set of states Q ′ is {{q, σ} : q ∈ Q, σ ∈ Σ} ∪ {{♯}, {♯, Acc}}.
For simplicity, we will identify a set {q, σ} with the pair (q, σ), and use the aliases q acc = {♯, Acc} and q rej = {♯}.

• q ′ 0 = (q 0 , σ 0 ) where σ 0 is a letter arbitrarily chosen from Σ.

• I Γ = ∅ and H Γ = Γ. The pushdown store alphabet Γ ′ is formally the subset {{γ} : γ ∈ Γ} of 2 I Γ ∪H Γ . However, we can obviously simplify and set Γ ′ = Γ.

• δ is defined as follows. For all (p, σ) ∈ Q × Σ and γ ∈ Γ ♭ , we have that (((p, σ), γ), ((q, σ ′ ), β)) ∈ δ iff (q, β) ∈ ∆(p, σ ′ , γ). Also, (((p, σ), γ), (q acc , γ)) ∈ δ iff p ∈ F , and (((p, σ), γ), (q rej , γ)) ∈ δ iff p ∈ F . Finally, ((q, γ), (q, γ)) ∈ δ for q ∈ {q acc , q rej }.

• µ is defined as follows. For every (q, σ) ∈ Q×Σ and γ ∈ Γ ♭ we have that, µ((q, σ), γ) = {σ}. Also, µ(q acc , γ) = {♯, Acc} and µ(q rej , γ) = {♯}.

• Env = Q × Γ ♭ . That is, S has only environment configurations.

Let M S = AP, ∅, W, w 0 , R, L, ∼ = be the module induced by S. Observe that by our choice of visible control and pushdown store variables, the set of equivalence classes [W ] of the configurations of M S is {(σ, ♭) : σ ∈ Σ ∪ {♯}}. We can safely ignore the constant ♭ component of each pair, and think of environment strategies as full {⊤, ⊥}-labeled (Σ ∪ {♯})-trees. We claim that P is universal if and only if M S |= r ϕ, where ϕ = EG¬♯ ∨ EF Acc. It is easy to see that the sub-formula ϕ 1 = EG¬♯ is satisfied by the tree M S ⊳ ξ iff the strategy ξ has an infinite path π = v 1 • v 2 • • • such that for every i ≥ 0 we have that v i is labeled with ⊤, and last(v i ) = ♯. It is left to show that for all other strategies ξ, the tree M S ⊳ ξ satisfies the sub-formula ϕ 2 = EF Acc iff P is universal.

Given a word w = σ 1 • • • σ k ∈ Σ * , and a run r = (q 0 , ♭) • (q 1 , α 1 ) • • • (q k , α k ) of P on w, let τ = (q ′ 0 , ♭) • ((q 1 , σ 1 ), α 1 ) • • • ((q k , σ k ), α k ) be the finite computation of M S corresponding to r. The visible part of τ is vis(τ ) = (σ 0 , ♭) • (σ 1 , ♭) • • • (σ k , ♭). Thus, given a strategy ξ, we have that τ is associated with the node w in the strategy tree [W ] * , ξ (recall that (σ 0 , ♭) is associated with the root ε). It follows that all the nodes in T M S , V M S corresponding to runs of P on w are associated with the same node of the strategy tree. Hence, a strategy can either enable all computations corresponding to runs of P on w, or disable them all. Note that given a run r of P on w, with a corresponding finite computation τ = (q ′ 0 , ♭) • ((q 1 , σ 1 ), α 1 ) • • • ((q k , σ k ), α k ) of M S as above, the configuration (q acc , α k ) is a successor of ((q k , σ k ), α k ) iff r is an accepting run, and (q rej , α k ) is a successor of ((q k , σ k ), α k ) iff r is a rejecting run. Thus, τ can be extended to a path witnessing the satisfaction of ϕ 2 iff r is an accepting run of P on w.

For every word w = σ 1 . . . σ k ∈ Σ * there is a special strategy ξ w that enables exactly the computations in the module corresponding to all of P's runs on w. The strategy ξ w has all nodes on the path σ 1 • • • σ k • ♯ ω marked with ⊤ and all other nodes marked with ⊥. It is easy to see that M S ⊳ ξ w is deadlock free, that M S ⊳ ξ w |= ϕ 1 , and that w is accepted by P iff M S ⊳ ξ w |= ϕ 2 . Hence, to complete the proof, it is sufficient to show that if P is universal then for every other strategy ξ, for which M S ⊳ ξ has a node x whose label contains ♯, we have that M S ⊳ ξ |= ϕ 2 . Let x be such a node of minimal depth, and let τ be the father of x. Note that τ must be of the form τ = (q ′ 0 , ♭) • ((q 1 , σ 1 ), α 1 ) • • • ((q k , σ k ), α k ). Consider the word w = σ 1 • • • σ k . Since ξ cannot distinguish between computations corresponding to different runs of P on w, the tree M S ⊳ ξ must contain not only τ , but also the computations corresponding to all other runs (if such runs exist) of P on w. Thus, if P is universal,

M S ⊳ ξ contains a path π = τ ′ • (q acc , α ′ k ) ω , where τ ′ = (q ′ 0 , ♭) • ((q ′ 1 , σ ′ 1 ), α ′ 1 ) • • • ((q ′ k , σ ′ k ), α ′ k
) is a finite computation (maybe τ ) corresponding to an accepting run of P on w. Since the configuration (q acc , α ′ k ) is labeled with {♯, Acc}, the path π is a witness for the satisfaction of ϕ 2 .

It is easy to see that we can replace the OPD S used in the proof of Theorem 1 by an OPD S ′ with only one state. S ′ uses as pushdown store alphabet pairs of a control state and a pushdown store symbol of S, and can thus remember the current control state of S in its (invisible) top of pushdown store. This implies the following corollary to Theorem 1: Corollary 1. The pushdown module checking problem with imperfect information is undecidable also when the control states are completely visible.

A somewhat more surprising result is that the pushdown module checking problem remains undecidable even if the environment has full information, not only about about the control states, but also about which atomic propositions hold at each and every configuration of the system.

Theorem 2. The imperfect information pushdown module checking problem for CTL, with visible control states and atomic propositions, is undecidable.

Proof. Observe that almost all the atomic propositions of the OPD S used in the proof of Theorem 1 are visible. The only violation is that for every α, α ′ ∈ Γ * • ♭, we have that (q acc , α) ∼ = (q rej , α ′ ), but {♯, Acc} = L(q acc , α) = L(q rej , α ′ ) = {♯}. Since the formula used in the proof is ϕ = EG¬♯ ∨ EF Acc, keeping the environment in the dark as to whether only ♯ holds, or both ♯ and Acc hold, is crucial. Indeed, if we fully expose the atomic propositions, we would make legal the environment ξ that prunes only the computations corresponding to accepting runs of P, with the consequence that M S ⊳ ξ |= ϕ even in cases where P is universal. However, the environment's ability to prune is not only limited by the information visible to it, but also by the requirement that it does not completely block the system. With a slight modification to the construction of the OPD S used in the proof of Theorem 1, we can have visible atomic propositions, but reveal the difference between computations corresponding to accepting and rejecting runs only when it is too late for the environment to prune based on that difference. This is done by changing S in such a way that a simulation τ = (q ′ 0 , ♭) • ((q 1 , σ 1 ), α 1 ) • • • ((q k , σ k ), α k ) of an accepting run r of P is not ended by moving directly to the sink configuration (q acc , α k ). Instead, we temporarily move to the configuration (q rej , { √ } • α k ). The only possible move from (q rej , { √ } • α k ) is to the configuration (q acc , α k ).

Formally, we make the following modifications to S. We make the control variable Acc visible by setting I = Σ ∪ {♯, Acc}, and H = Q. We add a new invisible pushdown store variable √ , and derive from it a new pushdown store symbol { √ }. The definition of the labeling function µ remains the same, except that it now ranges over the extended pushdown store alphabet. Finally, we replace every transition of the form (((p, σ), γ), (q acc , γ)) with the transitions (((p, σ), γ), (q rej , { √ } • γ)) and ((q rej , { √ }), (q acc , ε)). Let τ and τ ′ be computations of S corresponding to a rejecting run and an accepting run (respectively) of P on the same word w. The key observation is that the first point of difference an environment ξ sees between the path π = τ • (q rej , α) ω and the path π

′ = τ ′ • (q rej , { √ } • α ′ ) • (q acc , α ′ ) ω , is at the nodes v = τ • (q rej , α) • (q rej , α) and v ′ = τ ′ • (q rej , { √ } • α ′ ) • (q acc , α ′ ).
But by now, it is too late for the environment to prune without creating a deadlock in M S ⊳ ξ. This is because v is the only successor of its father, and so is v ′ . Combining the above with Corollary 1 completes the proof.

Observe that the formula used in the proof of Theorems 1 and 2 is an existential formula. Hence, the problem is already undecidable for the existential fragment ECTL of CTL. Obviously, the problem remains undecidable for more expressive logics such as CTL * and µ-calculus.

Semi-Alternating Pushdown Tree Automata

In this section, we introduce semi-alternating pushdown tree automata, and prove their equivalence to nondeterministic Büchi tree automata. The results of this section are used in subsequent sections to solve the pushdown module checking problem with imperfect state information and visible pushdown store.

Alternating pushdown tree automata [START_REF] Ladner | Alternating pushdown and stack automata[END_REF][START_REF] Kupferman | Pushdown specifications[END_REF], are alternating tree automata, augmented with a pushdown store. Semi-alternating pushdown tree automata are obtained by restricting the universality with respect to the pushdown store. The formal definition of semi-alternating pushdown tree automata follows.

A semi-alternating pushdown tree automaton is a tuple A = Σ, D, Γ, Q, q 0 , ♭, δ, F where Σ is a finite input alphabet, D is a finite set of directions, Γ is a finite pushdown store alphabet, Q is a finite set of states, q 0 ∈ Q is the initial state, ♭ ∈ Γ is the pushdown store bottom symbol, and F is an acceptance condition, to be defined later. δ is a finite transition function

δ : Q × Σ × Γ ♭ → B + (D × Q × Γ * ♭ )
, where Γ ♭ = Γ ∪ {♭} as usual, and

B + (D × Q × Γ * ♭ )
is the set of all positive boolean combinations of triples (d, q, β), where d is a direction, q is a state, and β is a string of pushdown store symbols. We also allow the formulas true and false. We write S ∈ δ(p, σ, γ) to denote that S is a set of tuples (d, q, β) that satisfy δ(p, σ, γ). What makes the automaton semi-alternating is the requirement that for every d ∈ D, σ ∈ Σ, p, p ′ ∈ Q (possibly the same state), and γ ∈ Γ, if (d, q, β) appears in δ(p, σ, γ), and (d, q ′ , β ′ ) appears in δ(p ′ , σ, γ), then β = β ′ . That is, two copies of the automaton that read the same input, from two configurations that have the same top symbol of the pushdown store and proceed in the same direction, must push the same value into the pushdown store. In particular, it follows that in every run, two copies of the automaton that are reading the same node of an input tree have the same pushdown store content. Note that if we remove the semi-alternation requirement, the resulting automaton is simply an alternating pushdown tree automaton.

For example, having δ(q, σ, γ) = ((0, q 1 , β 1 ) ∨ (1, q 2 , β 2 )) ∧ (1, q 1 , β 2 ) means that when a copy of the automaton that is in a configuration where the current state is q, and the top of pushdown store is γ, reads a node in the input tree whose label is σ, it can proceed in one of two ways. In the first option, one copy proceeds in direction 0 to state q 1 , by replacing γ with β 1 , and one copy proceeds in direction 1 to state q 1 , by replacing γ with β 2 . In the second option, two copies proceed in direction 1, one to state q 1 and the other to state q 2 , and in both copies γ is replaced with β 2 . Hence, ∨ and ∧ in δ(q, σ, γ) represent, respectively, choice and concurrency. As a special case of semi-alternating pushdown tree automata, we consider nondeterministic pushdown tree automata where the concurrency feature is not allowed. That is, whenever the automaton visits a node x of the input tree, it sends to each successor (direction) of x at most one copy of itself. More formally, a nondeterministic pushdown tree automaton is a semi-alternating pushdown tree automaton in which δ is in disjunctive normal form, and in each conjunct each direction appears at most once.

A run of a semi-alternating pushdown tree automaton A on a Σ-labeled tree T, V , with T = D * , is a (D * × Q × Γ * • ♭)-labeled N-tree T r , r such that the root is labeled with (ε, q 0 , ♭) and the labels of each node and its successors satisfy the transition relation. Formally, a (D

* × Q × Γ * • ♭)-labeled tree T r , r is a run of A on T, V iff • r(ε) = (ε, q 0 , ♭), and
• for all x ∈ T r such that r(x) = (y, p, γ • α), there is an n ∈ N such that the successors of x are exactly x • 1, . . . x • n, and for all 1

≤ i ≤ n we have r(x • i) = (y • d i , p i , β i • α) for some {(d 1 , p 1 , β 1 ), . . . , (d n , p n , β n )} ∈ δ(p, V (y), γ).
As for tree automata without a pushdown store, a run T r , r is accepting iff all its infinite paths satisfy the acceptance condition. Note that here we are only interested in the Büchi and parity acceptance conditions. A parity winning condition F maps all states of the automaton to a finite set of colors C = {C min , . . . , C max } ⊂ N. Thus, F : W → C. For a path π, let maxC (π) be the maximal color that appears infinitely often along π. Then, π satisfies the parity condition F iff maxC (π) is even. The Büchi acceptance condition is a special case of the parity condition with only two colors, i.e., C = {1, 2}.

We denote the different classes of pushdown tree automata by preceding with "PD-" a three letter acronyms in {A, S, N} × {B, P} × {T}, where the first letter stands for the branching mode of the automaton (alternating, semi-alternating, or nondeterministic); the second letter stands for the acceptance-condition type (Büchi, or parity); and the third letter indicates that the automaton runs on trees. Thus, for example, a semi-alternating pushdown tree automaton with a parity acceptance condition is a PD-SPT, and a nondeterministic pushdown tree automaton with a Büchi acceptance condition is a PD-NBT.

Given a pushdown tree automaton A = Σ, D, Γ, Q, q 0 , ♭, δ, F , we define the size of A as |A| = |Q| + |δ|, where |δ| is the sum of the lengths of the satisfiable (i.e., not false) formulas that appear in δ(q, σ, γ) for some q, σ, and γ.

Translating PD-SPT to PD-NPT

As mentioned in Section 1, alternating pushdown automata are not equivalent to nondeterministic ones. However, as we show here, the limitations imposed on semi-alternating automata allow us to translate a PD-SPT to an equivalent PD-NPT. A key observation is that since a pushdown store operation performed by a semi-alternating automaton does not depend on the current (or next) control states, we can split the transition function of a PD-SPT into two functions: a state transition function δ Q , and a pushdown store update function δ Γ , as follows. Given a PD-

SPT A = Σ, D, Γ, Q, q 0 , ♭, δ, F , let δ Q : Q × Σ × Γ ♭ → B + (D × Q) be the projection of δ on B + (D × Q). That is, δ Q (q, σ
, γ) is obtained from δ(q, σ, γ) by replacing every element (d, q, β) that appears in δ(q, σ, γ) with (d, q). The pushdown store update function

δ Γ : Σ × Γ ♭ × D → Γ * ♭ , is a partial function; for every (p, σ, γ) ∈ Q × Σ × Γ ♭ and every (d, q, β) ∈ D × Q × Γ * ♭ , such that (d, q, β) appears in δ(p, σ, γ), we let δ Γ (σ, γ, d) = β. Since A is semi-alternating, δ Γ is well defined. Ob- serve that for every (p, σ, γ) ∈ Q × Σ × Γ ♭ we have that δ(p, σ, γ) can be obtained from δ Q (p, σ, γ) by replacing every (d, q) that appears in δ Q (p, σ, γ) with (d, q, δ Γ (σ, γ, d)).
Consider a Σ-labeled tree T, V , with T = D * . Note that for every node x ∈ T and every run of A on T, V , the pushdown store content of all the copies of A that visit x is the same, and only depends on x. We can thus define a function ∆ Γ : T → Γ * ♭ , giving for every node x its associated pushdown store content, as follows: (1) ∆ Γ (ε) = ♭, and (2) for all

x • d ∈ T we have ∆ Γ (x • d) = δ Γ (V (x), γ, d) • β, where ∆ Γ (x) = γ • β, and γ ∈ Γ ♭ .
Annotating input trees with pushdown store symbols enables us to simulate a PD-SPT by an APT running on the annotated version of an input tree. Given a Σ-labeled tree T, V , we define its Γ A -annotation to be the (Σ × Γ ♭ )-labeled tree T, U , obtained by letting U (x) = (V (x), top(∆ Γ (x))), for every x ∈ T . Lemma 1. Let A = Σ, D, Γ, Q, q 0 , ♭, δ, F be a PD-SPT. There is an APT Ã, such that A accepts T, V iff à accepts the Γ A -annotation of T, V .

Proof. Consider the APT à = Σ × Γ ♭ , D, Q, q 0 , δ, F , where δ(q, (σ, γ)) = δ Q (q, σ, γ). It is not hard to see that every run r = T r , r of A on T, V induces a corresponding run r ′ = T r , r ′ of à on the Γ A -annotation of T, V , and vice versa. The connection between r and r ′ being that for every x ∈ T r , we have that r(x) = (y, p, α) iff r ′ (x) = (y, p) and ∆ Γ (x) = α.

By [START_REF] Muller | Alternating automata on infinite trees[END_REF], every APT can be translated to an equivalent NPT. Hence, Lemma 1 implies that if A is a PD-SPT, then there is an NPT A ′ such that A accepts T, V iff A ′ accepts the Γ A -annotation of T, V . This allows us to translate A to an equivalent PD-NPT A ′′ (running on the same input trees as A). Given a Σ-labeled tree, A ′′ generates on the fly its Γ A -annotation and runs A ′ on the annotated tree. Formally, we have the following: Theorem 3. A PD-SPT A with n states and index k can be translated to an equivalent PD-NPT with (nk) O(nk) states, an O(nk) index, and a transition relation of size (nk) O(|D|nk) .

Proof. Let A = Σ, D, Γ, Q, q 0 , ♭, δ, F be a PD-SPT and à = Σ × Γ ♭ , D, Q, q 0 , δ, F be an APT derived from A by Lemma 1. By [START_REF] Muller | Alternating automata on infinite trees[END_REF], à has an equivalent NPT

A ′ = Σ × Γ ♭ , D, Q ′ , q ′ 0 , δ ′ , F ′ . Consider the PD-NPT A ′′ = Σ, D, Γ, Q ′ , q ′ 0 , ♭, δ ′′ , F ′ , where for every (p, σ, γ) ∈ Q ′ × Σ × Γ ♭ , we have that δ ′′ (p, σ, γ) is obtained from δ ′ (p, (σ, γ)) by replacing every (d, q) that appears in δ ′ (p, (σ, γ)), with (d, q, δ Γ (σ, γ, d)). Since A ′ is nondeterministic, so is A ′′ .
Given a Σ-labeled tree T, V , it is not hard to see that for every x ∈ T , the pushdown store of every copy of A ′′ that visits x contains exactly ∆ Γ (x). Hence, A ′′ accepts T, V iff A ′ accepts the Γ A -annotation of T, V , thus, by Lemma 1, iff A accepts T, V .

We now analyze the blow-up involved in the above construction. Looking at the automata transformations involved, we see that the only transformation that incurs a blow-up in the size of the automaton is the transformation of the APT Ã to the NPT A ′ . By [START_REF] Muller | Alternating automata on infinite trees[END_REF], if the APT Ã has n states and index k, and it runs over D * trees, the resulting NPT A ′ has (nk) O(nk) states, an O(nk) index, and a transition relation of size (nk) O(|D|nk) . We note that the runtime of the algorithm in [START_REF] Muller | Alternating automata on infinite trees[END_REF] is polynomial in the size of its input and output automata. We also wish to draw the reader's attention to the fact that the blow-up in the number of states of this translation is independent of the size of the transition relation of A.

By [START_REF] Kupferman | Pushdown specifications[END_REF], the emptiness of a PD-NPT can be decided in time exponential in the product of the number of states, the index, and the size of its transition relation. Together with Theorem 3, this gives us the following corollary: Corollary 2. The emptiness problem for a PD-SPT with n states and index k, running on D * trees, can be solved in time double-exponential in |D|nk.

Since the Büchi acceptance condition can be thought of as a parity condition with only two colors, Theorem 3 also yields a translation from PD-SBT to PD-NPT, and thus we also have the following corollary: Corollary 3. The emptiness problem for a PD-SBT with n states, running on D * trees, can be solved in time double-exponential in |D|n.

Translating PD-SBT to PD-NBT

As noted above, Theorem 3 also yields a translation from PD-SBT to PD-NPT, which, as it turns out, is good enough to obtain the required complexity results for our intended application in the context of CTL pushdown modulechecking. However, an alternative route is to use the much simpler and more direct translation of PD-SBT to PD-NBT presented below. In [START_REF] Miyano | Alternating finite automata on ω-words[END_REF] Miyano and Hayashi describe a translation of alternating Büchi automata on words to nondeterministic ones. In [START_REF] Kupferman | Safraless decision procedures[END_REF] the construction is adapted to the translation of alternating Büchi automata on trees to nondeterministic ones. Here, we further extend it to obtain a translation of PD-SBT to PD-NBT. Theorem 4. Let A be a PD-SBT with n states. There is a PD-NBT A ′ with 2 O(n) states, such that L(A ′ ) = L(A).

Proof. The automaton A ′ guesses a subset construction applied to a run of A. At a given node x of a run of A ′ , it keeps in its memory the set of configurations in which the various copies of A visit node x in the guessed run. Since A is semi-alternating, all copies of A that visit the same node x have the same pushdown store content, and thus, can all be remembered using one pushdown store and a set of states of A. In order to make sure that every infinite path visits states in F infinitely often, A ′ keeps track of states that "owe" a visit to F . The details of the construction are given below. Once we establish that indeed one pushdown store is enough to remember the all pushdown stores, of all the copies of A that visit the same node of the input tree, the correctness of the construction follows from the same arguments used in [START_REF] Miyano | Alternating finite automata on ω-words[END_REF][START_REF] Kupferman | Safraless decision procedures[END_REF].

Let A = Σ, D, Γ, Q, q 0 , ♭, δ, F . Then A ′ = Σ, D, Γ, 2 Q × 2 Q , {q 0 }, ∅ , ♭, δ ′ , 2 Q × {∅} .
To define δ ′ , we first need the following notation. For a set S ⊆ Q, a letter σ ∈ Σ, and a top of pushdown store symbol γ ∈ Γ, let sat(S, σ, γ) be the set of subsets of D × Q × Γ * ♭ that satisfy q∈S δ(q, σ, γ). Also, for two sets O ⊆ S ⊆ Q, a letter σ ∈ Σ, and a top of pushdown store symbol γ ∈ Γ, let pair sat(S, O, σ, γ) be such that S ′ , O ′ ∈ pair sat(S, O, σ, γ) iff S ′ ∈ sat(S, σ, γ), O ′ ⊆ S ′ , and O ′ ∈ sat(O, σ, γ). Finally, for a direction d ∈ D, we have S ′ d = {s : (d, s, β) ∈ S ′ for some β} and O ′ d = {o : (d, o, β) ∈ O ′ for some β}. Thus, S ′ d and O ′ d are, respectively, the collections of all states that appear in S ′ and O ′ along with the direction d. Since A is semi-alternating, for every two triplets (d, q, β) and (d, q ′ , β ′ ) in sat(S, σ, γ) having the same direction d, we have that β = β ′ . Thus, we can define store(d, σ, γ) = β. Now, δ ′ is defined, for all S, O ∈ 2 Q × 2 Q , σ ∈ Σ, and γ ∈ Γ, as follows.

• if O = ∅, then δ ′ ( S, O , σ, γ) = S ′ , O ′ ∈ pair sat(S, O, σ, γ) d∈D (d, S ′ d , O ′ d \F , store(d, σ, γ))
Thus, when reading σ, from a configuration with a top of pushdown store symbol γ, the automaton A ′ sends to a direction d ∈ D the set S ′ d of states that the different copies of A send to direction d in the guessed run. Each such S ′ d is paired with a subset O ′ d of S ′ d of the states that still "owe" a visit to F . The key observation is that since A is semialternating, all the copies that A sends to direction d replace γ with exactly the same pushdown store string, namely, with store(d, σ, γ). Hence, the pushdown stores of all the copies that A sends to direction d are identical, and A ′ can keep track of them all using the single stack of the copy it sent to direction d.

• if O = ∅, then δ ′ ( S, O , σ, γ) = S ′ , O ′ ∈ pair sat(S, O, σ, γ) d∈D (d, S ′ d , S ′ d \F , store(d, σ, γ))
Thus, when no state "owes" a visit to F we know that every path in the guessed run of A visited F one more time, and the requirement to visit F is reinforced.

So, we are done with the proof.

Module Checking with Visible Pushdown Store

In this section, we show that pushdown module checking with full information about the pushdown store content (H Γ = ∅), but not about the control states (when H = ∅), is decidable and 2Exptime-complete for CTL and propositional µ-calculus specifications, and is 3Exptime-complete for CTL * specifications.

The upper bounds follow by reducing this variant of the pushdown module checking problem to the emptiness problem of PD-SBT forCTL specifications, and to the emptiness problem of PD-SPT for CTL * and propositional µ-calculus specifications. The lower bounds follow from known results about perfect information pushdown module checking. In Section 6.1 we consider the simpler case of CTL specifications, while the other logics are treated in Section 6.2.

CTL Module Checking with Visible Pushdown Store

Theorem 5. For an OPD S with H Γ = ∅, and a CTL formula ϕ over S's atomic propositions. There is a PD-SBT A S,ϕ of size O(|S| • |ϕ|), such that L(A S,ϕ ) is exactly the set of strategies ξ such that M S ⊳ ξ is deadlock free and satisfies ϕ.

Proof. Essentially, the automaton A S,ϕ we build is an extension of the product automaton obtained in the alternating-automata theoretic approach for CTL module checking with imperfect information [START_REF] Kupferman | Module checking revisited[END_REF]. The extension we consider concerns the simulation of the pushdown store of the OPD, and its correctness follows using the same reasoning found in [START_REF] Kupferman | Module checking revisited[END_REF][START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF].

Let S = AP, Q, q 0 , Γ, ♭, δ, µ, Env be an OPD, let ϕ be a CTL formula in positive normal form, and let M S = AP, W s , W e , w 0 , R, L, ∼ = be the module induced by S. We build an automaton A S,ϕ that accepts {⊤, ⊥}-labeled trees corresponding to strategies ξ, whose composition with M S is deadlock free and satisfy ϕ. Intuitively, a run of A S,ϕ on an input strategy tree ξ, proceeds by simulating an unwinding of the module M S , pruned at each step according to the strategy ξ. Copies of the automaton simulating nodes in the computation tree of M S that are indistinguishable by the environment are sent to the same direction in the input tree. The resulting run tree of A S,ϕ on ξ is basically a replica of the composition M S ⊳ ξ, and the fact that it satisfies the formula ϕ is checked on the fly, by employing in A S,ϕ the usual alternating-automata approach for CTL model checking.

In the full computation tree of M S , the set of directions is G = {(q, β) : ((p, α), (q, β)) ∈ R for some p, α and β}. Since in S the pushdown store is completely visible to the environment, the set of directions of the input strategy trees is D = {(vis(q), β) : ((p, α), (q, β)) ∈ R for some p, α and β}. Finally, due to the fact that all copies of the automaton sent to direction (vis(q), β) push β into the pushdown store, the resulting automaton A S,ϕ is semi-alternating. Before we give the formal definition of A S,ϕ we need the following: for (p, γ • α) ∈ W , we define the set of successors of (p, γ • α) in M S , to be s(p, γ) = {(q, β) : ((p, γ), (q, β)) ∈ δ}. We now formally define A S,ϕ = {⊤, ⊥}, D, Γ, Q ′ , q ′ 0 , ♭, δ ′ , F , where

• Q ′ = (Q × (cl(ϕ) ∪ {p ⊤ }) × {∀, ∃} × {p e , p s }) ∪ {q ′ 0 }. • F = Q × U (ϕ)
× {∃, ∀} × {p e , p s }, where U (ϕ) is the set of all formulas of the form ∀ψ 1 U ψ 2 or ∃ψ 1 U ψ 2 in cl(ϕ).

• δ ′ : Q ′ × Σ × Γ ♭ → B + (D × Q ′ × Γ * ♭
) is defined as follows: In the rules below, for the sake of succinctness, we consider m ∈ {∃, ∀} × {p e , p s }, h ∈ AP ∪ {true, false}. Also, given a transition from ( p, ψ, m , ⊤, γ), we let p x = p e if (p, γ) ∈ Env, and p x = p s otherwise.

For all p ∈ Q, ψ 1 , ψ 2 ∈ cl(ϕ), ψ ∈ cl(ϕ) ∪ {p ⊤ }, and γ ∈ Γ ♭ , we have:

-δ ′ (q ′ 0 , ⊥, ♭) = false. -δ ′ (q ′ 0 , ⊤, ♭)= δ ′ ( q 0 , p ⊤ , ∃, p s , ⊤, ♭) ∧ δ ′ ( q 0 , ϕ, ∃, p s , ⊤, ♭).
δ ′ ( p, ψ, ∀, p e , ⊥, γ) = true, and δ ′ ( p, ψ, ∃, p e , ⊥, γ) = false.

δ ′ ( p, ψ, ∀, p s , ⊥, γ) = δ ′ ( p, ψ, ∀, p s , ⊤, γ), and

δ ′ ( p, ψ, ∃, p s , ⊥, γ) = δ ′ ( p, ψ, ∃, p s , ⊤, γ).
δ ′ ( p, p ⊤ , m , ⊤, γ) = (q,β)∈s(p,γ) (vis(q, β), q, p ⊤ , ∃, p x , β)).

-

δ ′ ( p, h, m , ⊤, γ) = true if h ∈ µ((p, γ)), or h = true. -δ ′ ( p, h, m , ⊤, γ) = false if h ∈ µ((p, γ)), or h = false. -δ ′ ( p, ¬h, m , ⊤, γ) = true if h ∈ µ((p, γ)), or h = false. -δ ′ ( p, ¬h, m , ⊤, γ) = false if h ∈ µ((p, γ)), or h = true. -δ ′ ( p, ψ 1 ∧ψ 2 , m , ⊤, γ) = δ ′ ( p, ψ 1 , m , ⊤, γ)∧δ ′ ( p, ψ 2 , m , ⊤, γ). -δ ′ ( p, ψ 1 ∨ψ 2 , m , ⊤, γ) = δ ′ ( p, ψ 1 , m , ⊤, γ)∨δ ′ ( p, ψ 2 , m , ⊤, γ).
concerns only successors of (p, γ • α) that are enabled, the mode of the new states is universal. The copies of A S,ϕ that check the composition with the strategy to be deadlock free guarantee that at least one successor of (p, γ • α) is enabled. As noted earlier, the enable/disable instructions of the strategy are ignored in every configuration (p, γ • α) that is a successor of a system configuration. Also note that since we assume that no configuration in M S has no successors, the conjunctions and disjunctions in δ ′ cannot be empty.

It is easy to that A S,ϕ has O(|S| •|ϕ|) states, and it is left to show that A S,ϕ is semi-alternating. It is sufficient to show that for every (t, β) ∈ D, σ ∈ Σ, p, p ′ ∈ Q ′ , and γ ∈ Γ, if ((t, β), p ′ , β ′ ) appears in δ ′ (p, σ, γ) then β = β ′ . To see that, notice that ((t, β), p ′ , β ′ ) appears in δ ′ (p, σ, γ) only if (q, β ′ ) ∈ s(p, γ, (t, β)), for some q ∈ Q. By the definition of s(p, γ, (t, β)) we must have that vis(q, β ′ ) = (t, β). Since the pushdown store is completely visible, we have that vis(q, β ′ ) = (vis(q), β ′ ), and we are done.

We now consider the complexity bound that follows from the above construction. Theorem 6. CTL pushdown module checking with imperfect information about the control states, but a visible pushdown store, is 2Exptime-complete.

Proof. The lower bound follows from the known bound for CTL pushdown module checking with perfect information [START_REF] Bozzelli | Pushdown module checking[END_REF]. For the upper bound, Theorem 5 implies that M S |= r ϕ iff the language of the automaton A S,¬ϕ is empty. Let M S = AP, W s , W e , w 0 , R, L, ∼ = be the module induced by S. Observe that the set of directions of the strategy trees that are the input of A S,¬ϕ is D = {(vis(q), β) : ((p, α), (q, β)) ∈ R for some p, q, α and β}, and it is bounded from above by |S|. By applying Corollary 3 to A S,¬ϕ we get the required result.

CTL * and µ-Calculus Module Checking with Visible Pushdown Store

Let us briefly recap the approach we have taken for solving the problem in the case of CTL, and discuss the changes required to adapt it to other specification logics. Given an OPD S, and a CTL formula ϕ, we build an automaton A S,ϕ that accepts {⊤, ⊥}-labeled trees corresponding to strategies ξ, whose composition with M S is deadlock-free and satisfies ϕ. Intuitively, a run of A S,ϕ on an input strategy tree ξ proceeds by simulating an unwinding of the module M S , pruned at each step according to the strategy ξ; copies of the automaton, which simulate nodes in the computation tree of M S that are indistinguishable by the environment, are sent to the same direction in the input tree. The resulting run tree of A S,ϕ on ξ is basically a replica of the composition M S ⊳ ξ, and the fact that it satisfies the formula ϕ is checked on the fly, by employing in A S,ϕ the classical alternating automaton (see [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF]) for model checking CTL.

When considering CTL * or the (propositional) µ-calculus 4 , adapting the construction we used for CTL basically amounts to replacing the embedded alternating automaton that does the on-the-fly model checking: instead of using an automaton that handles CTL, one uses an automaton that handles CTL * or µ-calculus (see [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF]). Since an alternating automaton that does µcalculus model checking is linear in the size of the formula, while one that does CTL * model checking is exponential in the size of the formula, the automaton A S,ϕ has O(|S| • |ϕ|) states in the case of µ-calculus, and O(|S| • 2 |ϕ| ) states in the case of CTL * . It is important to note that the acceptance condition of A S,ϕ is inherited from the embedded model checking automaton. Hence, unlike the case of CTL where a Büchi condition was enough, for the more expressive logics that we consider in this section we need the parity condition.

Theorem 7. Consider an OPD S with H Γ = ∅, and a CTL * or a propositional µ-calculus formula ϕ over S's atomic propositions. There is a PD-SPT A S,ϕ such that L(A S,ϕ ) is exactly the set of strategies ξ for which M S ⊳ ξ is deadlock-free and satisfies ϕ. Moreover,

• If ϕ is a propositional µ-calculus formula then A S,ϕ has O(|S| • |ϕ|)
states and an index O(|ϕ|).

• If ϕ is a CTL * formula then A S,ϕ has O(|S| • 2 |ϕ| ) states and an index 3.

Proof. We give the construction of A S,ϕ for the propositional µ-calculus.

The construction for CTL * is obtained by replacing (in this or the CTL construction) the embedded classical alternating-automata model checker with a CTL * one.

Let S = AP, Q, q 0 , Γ, ♭, δ, η, Env be an OPD, let ϕ be a µ-calculus formula (guarded5 , without free variables, and in positive normal form), and let M S = AP, W s , W e , w 0 , R, L, ∼ = be the module induced by S. We build an automaton A S,ϕ that accepts {⊤, ⊥}-labeled trees corresponding to strategies ξ, whose composition with M S is deadlock-free and satisfy ϕ. Intuitively, a run of A S,ϕ on an input strategy tree ξ, proceeds by simulating an unwinding of the module M S , pruned at each step according to the strategy ξ; copies of the automaton simulating nodes in the computation tree of M S that are indistinguishable by the environment are sent to the same direction in the input tree. The resulting run tree of A S,ϕ on ξ is essentially a replica of the composition M S ⊳ ξ, and the fact that it satisfies the formula ϕ is checked on the fly by employing in A S,ϕ the usual alternating-automata approach for µ-calculus model checking. In the full computation tree of M S , the set of directions is G = {(q, β) : ((p, α), (q, β)) ∈ R for some p, α and β}. Since in S the pushdown store is completely visible to the environment, the set of directions of the input strategy trees is D = {(vis(q), β) : ((p, α), (q, β)) ∈ R for some p, q, α and β}.

Finally, due to the fact that all copies of the automaton sent to direction (vis(q), β) push β into the pushdown store, the resulting automaton A S,ϕ is semi-alternating. As in [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF], we are going to use a function split to avoid the problem of having states with a component in cl(ϕ) that is a disjunction or a conjunction. Without the use of split, a run of the automaton may have no states that correspond to a fixpoint sub-formula of ϕ that is part of a conjunction or a disjunction, which makes it impossible to correctly define the acceptance condition.

We now formally define A S,ϕ = {⊤, ⊥}, D, Γ, Q ′ , q ′ 0 , ♭, δ ′ , F , where

• Q ′ = (Q × (cl(ϕ) ∪ {p ⊤ }) × {∀, ∃} × {p e , p s }) ∪ {q ′ 0 }.
States with the component p ⊤ are used to check that the composition of M S with the strategy is deadlock-free, while states with a component in cl(ϕ) check that this composition satisfies ϕ. The components p e and p s are used to flag that the currently simulated node, of the computation tree of M S , is a child of an environment or a system node, respectively. Clearly, the simulation should respect the strategy pruning specifications only if they correspond to children of environment nodes; that is, only if the current state q contains p e . Every state is either in an existential or a universal mode, as specified by the ∀ and ∃ components. When the automaton is in a universal state (q, ϕ, ∀, p e ) with a pushdown store content α, it accepts all strategies for which (q, α) in M S is either pruned or satisfies ϕ (where p ⊤ is satisfied iff the root of the strategy is labeled ⊤). When the automaton is in an existential state (q, ϕ, ∃, p e ) with a pushdown store content α, it accepts all strategies for which (q, α) in M S is not pruned and satisfies ϕ.

• δ ′ is a function δ ′ : Q ′ × Σ × Γ ♭ → B + (D × Q ′ × Γ * ♭ )
. Before giving the formal definition, we show an example. Consider, a transition from the configuration ( p, ∀Xψ, ∃, p e , γ • α), where (p, γ) ∈ Env. First, if the transition to (p, γ • α) is disabled (that is, the automaton reads ⊥), then, as the current mode is existential, the run is rejecting. If the transition to (p, γ • α) is enabled, then the successors of (p, γ • α) that are enabled should satisfy ψ. Note that all the successors of (p, γ • α) that are indistinguishable by the environment are sent by the automaton to the same direction v. This guarantees that either all these successors are enabled by the strategy (in case the letter to be read in direction v is ⊤) or all are disabled (in case the letter in direction v is ⊥). In addition, since the requirement to satisfy ψ concerns only successors of (p, γ • α) that are enabled, the mode of the new states is universal. The copies of A S,ϕ that check the composition with the strategy to be deadlock-free guarantee that at least one successor of (p, γ • α) is enabled. As noted earlier, the enable/disable instructions of the strategy are ignored in every configuration (p, γ • α) that is a successor of a system configuration. Also note that since we assume that no configuration in M S has no successors, the conjunctions and disjunctions in δ ′ cannot be empty. We now formally define the transition function δ ′ .

For (p, γ • α) ∈ W , we define the set of successors of (p, γ • α) in M S , to be s(p, γ) = {(q, β) : ((p, γ), (q, β)) ∈ δ}. The transition function

δ ′ : Q ′ × Σ × Γ ♭ → B + (D × Q ′ × Γ * ♭
) is defined as follows. In the rules below, for the sake of succinctness, we consider m ∈ {∃, ∀} × {p e , p s }, h ∈ AP ∪ {true, false}. Also, given a transition from ( p, ψ, m , ⊤, γ), we let p x = p e if (p, γ) ∈ Env, and p x = p s otherwise.

For all p ∈ Q, ψ 1 , ψ 2 ∈ cl(ϕ), ψ ∈ cl(ϕ) ∪ {p ⊤ }, and γ ∈ Γ ♭ , we have:

δ ′ (q ′ 0 , ⊥, ♭) = false δ ′ (q ′ 0 , ⊤, ♭)= δ ′ ( q 0 , p ⊤ , ∃, p s , ⊤, ♭) ∧ δ ′ ( q 0 , ϕ, ∃, p s , ⊤, ♭) -δ ′ ( p, ψ, ∀, p e , ⊥, γ) = true, and δ ′ ( p, ψ, ∃, p e , ⊥, γ) = false δ ′ ( p, ψ, ∀, p s , ⊥, γ) = δ ′ ( p, ψ, ∀, p s , ⊤, γ), and δ ′ ( p, ψ, ∃, p s , ⊥, γ) = δ ′ ( p, ψ, ∃, p s , ⊤, γ)

δ ′ ( p, p ⊤ , m , ⊤, γ) = ( (q,β)∈s(p,γ) (vis(q, β), q, p ⊤ , ∃, p x , β)) δ ′ ( p, AXψ 1 , m ,⊤, γ) = split( (q,β)∈s(p,γ) (vis(q, β), q, ψ 1 , ∀, p x , β))

-δ ′ ( p,
δ ′ ( p, EXψ 1 , m ,⊤, γ) = split( (q,β)∈s(p,γ) (vis(q, β), q, ψ 1 , ∃, p x , β))

δ ′ ( p, µy.ψ 1 (y), m ,⊤, γ) = split(δ ′ ( p, ψ 1 (µy.ψ 1 (y)), m ,⊤, γ))

δ ′ ( p, νy.ψ 1 (y), m ,⊤, γ) = split(δ ′ ( p, ψ 1 (νy.ψ 1 (y)), m ,⊤, γ))

The definition of the function split : B + (D×Q ′ ×Γ * ♭ ) → B + (D×Q ′ ×Γ * ♭ ) is a simple adaptation of the definition found in [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF]. For every d ∈ D, q ∈ Q, m ∈ {∃, ∀} × {p e , p s } and β ∈ Γ * ♭ we have the following:

- • It remains to define the acceptance condition F . Let d be the maximal alternation level of (greatest and lowest fixpoint) sub-formulas of ϕ.

For every 0 ≤ i ≤ d, denote by G i the set of all ν-formulas in cl(ϕ) of alternation depth i, and by B i the set of all µ-formulas in cl(ϕ) of alternation depth i. Now, F : Q ′ → {0..2d + 1}, where:

-For every u ∈ (Q×{p ⊤ }×{∀, ∃}×{p e , p s })∪{q ′ 0 } we have F (u) = 0.

-For every u ∈ (Q × B i × {∀, ∃} × {p e , p s }) we have F (u) = 2(di) + 1.

-For every u ∈ (Q × G i × {∀, ∃} × {p e , p s }) we have F (u) = 2(di).

Recall that, by the definition of PD-SPT, a path π of a run r is accepting iff the maximal color encountered infinitely many times along π is even. Hence, by our definition of F , such a color corresponds to the outermost fixpoint sub-formula that was visited infinitely often. Thus, the acceptance condition makes sure that the outermost fixpoint subformula that is visited infinitely often is a greatest fixpoint formula, and that all of its least fixpoint super-formulas are visited only finitely many times.

We now show that A S,ϕ is semi-alternating. It is sufficient to show that for every (t, β) ∈ D, σ ∈ Σ, p, p ′ ∈ Q ′ , and γ ∈ Γ, if ((t, β), p ′ , β ′ ) appears in δ ′ (p, σ, γ) then β = β ′ . To see that, notice that ((t, β), p ′ , β ′ ) appears in δ ′ (p, σ, γ) only if vis(q, β ′ ) = (t, β), for some q ∈ Q. Since by definition (because the pushdown store is completely visible) we have that vis(q, β ′ ) = (vis(q), β ′ ) we are done.

It is easy to see that in the construction above A S,ϕ has O(|S| • |ϕ|) states and an index O(|ϕ|). For CTL * , the embedded CTL * model checker is of size 2 O(|ϕ|) and its index is 3 [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF]. Hence, for CTL * , A S,ϕ has O(|S| • 2 |ϕ| ) states and its index is 3.

We now consider the complexity bounds that follow from the above construction.

Theorem 8. The pushdown module checking problem with imperfect information about the control states, but a visible pushdown store, is 2Exptimecomplete for propositional µ-calculus specifications, and 3Exptime-complete for CTL * specifications.

Proof. The lower bounds follows from the known bounds for pushdown module checking with perfect information (see [START_REF] Ferrante | Enriched µ-calculus pushdown module checking[END_REF] for propositional µ-calculus, and [6] forCTL * ). For the upper bound, Theorem 7 implies that M S |= r ϕ iff the language of the automaton A S,¬ϕ is empty. Let M S = AP, W s , W e , w 0 , R, L, ∼ = be the module induced by S. Recall that the size of the set of directions D (of the strategy trees that are the input of A S,¬ϕ ) is bounded from above by |S|. By Applying Corollary 2 to A S,¬ϕ we get the required results.

Discussion

Recall that in our setting, whenever we push a symbol consisting entirely of invisible variables, the environment does not see the push at all. One can think of a variant of the problem where the environment does see that a push occurred, but not what was pushed. Thus, the depth of the stack is always known to the environment. It is an open question whether this variant of the problem is decidable or not.

  h, m , ⊤, γ) = true if h ∈ η((p, γ)), or h = true δ ′ ( p, h, m , ⊤, γ) = false if h ∈ η((p, γ)), or h = false δ ′ ( p, ¬h, m , ⊤, γ) = true if h ∈ η((p, γ)), or h = false δ ′ ( p, ¬h, m , ⊤, γ) = false if h ∈ η((p, γ)), or h = true δ ′ ( p, ψ 1 ∧ ψ 2 , m ,⊤, γ) = split(δ ′ ( p, ψ 1 , m ,⊤, γ) ∧ δ ′ ( p, ψ 2 , m ,⊤, γ)) -δ ′ ( p, ψ 1 ∨ ψ 2 , m ,⊤, γ) = split(δ ′ ( p, ψ 1 , m ,⊤, γ) ∨ δ ′ ( p, ψ 2 , m ,⊤, γ))

-

  split(true) = true split(false) = false split(θ 1 ∨ θ 2 ) = split(θ 1 ) ∨ split(θ 2 ) split(θ 1 ∧ θ 2 ) = split(θ 1 ) ∧ split(θ 2 ) If ψ ∈ cl(ϕ)is of the form p, ¬p, AXψ ′ , EXψ ′ , µy.ψ ′ (y) or νy.ψ ′ (y), then split(d, p, ψ, m , β) = (d, p, ψ, m , β) split(d, p, ψ 1 ∨ψ 2 , m , β) = split(d, p, ψ 1 , m , β)∨split(d, p, ψ 2 , m , β) split(d, p, ψ 1 ∧ψ 2 , m , β) = split(d, p, ψ 1 , m , β)∧split(d, p, ψ 2 , m , β)

In the literature, the term incomplete information is sometimes used to refer to what we call imperfect information.

Although the complexity of the perfect and imperfect information cases coincide in the general case,[START_REF] Kupferman | Module Checking[END_REF][START_REF] Kupferman | Module checking revisited[END_REF] show that when the formula is constant the imperfect information case is exponentially harder.

The semantics of temporal logics such asCTL is usually defined with respect to infinite paths, so we assume M S has no configurations without successors. However, using a similar technique to the one used in[START_REF] Bozzelli | Pushdown module checking[END_REF] our results can be adapted to the situation where terminal configurations are also allowed.

Our construction can be extended in much the same way to the graded µ-calculus. The only subtle point involves handling the binary-encoded graded modalities without increasing the complexity with respect to the propositional µ-calculus. For more details see[START_REF] Aminof | mucalculus pushdown module checking with imperfect state information[END_REF].

The embedded µ-calculus model checking automaton requires that formulas be guarded. This guarantees that transitions involving fixpoint formulas are well defined (see[START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF]).

δ ′ ( p, ∀Xψ 1 , m , ⊤, γ) = ( (q,β)∈s(p,γ) (vis(q, β), q, ψ 1 , ∀, p x , β)).

δ ′ ( p, ∃Xψ 1 , m , ⊤, γ) = ( (q,β)∈s(p,γ) (vis(q, β), q, ψ 1 , ∃, p x , β)).

States with the component p ⊤ used to check that the composition of M S with the strategy is deadlock free, while states with a component in cl(ϕ) check that this composition satisfies ϕ. The components p e and p s are used to flag that a currently simulated node, of the computation tree of M S , is a child of an environment or a system node, respectively. Clearly, the simulation should respect the strategy pruning specifications only if they correspond to children of environment nodes; that is, only if the current state q contains p e . Every state is either in an existential or a universal mode, as specified by the ∀ and ∃ components. When the automaton is in a universal state (q, ϕ, ∀, p e ) with a pushdown store content α, it accepts all strategies for which (q, α) in M S is either pruned or satisfies ϕ (where p ⊤ is satisfied iff the root of the strategy is labeled ⊤). When the automaton is in an existential state (q, ϕ, ∃, p e ) with a pushdown store content α, it accepts all strategies for which (q, α) in M S is not pruned and satisfies ϕ.

To get a feeling of the transition rules, consider, for example, a transition from the configuration ( p, ∀Xψ, ∃, p e , γ • α), where (p, γ) ∈ Env. First, if the transition to (p, γ • α) is disabled (that is, the automaton reads ⊥), then, as the current mode is existential, the run is rejecting. If the transition to (p, γ • α) is enabled, then the successors of (p, γ • α) that are enabled should satisfy ψ. Note that all the successors of (p, γ • α) that are indistinguishable by the environment are sent by the automaton to the same direction v. This guarantees that either all these successors are enabled by the strategy (in case the letter to be read in direction v is ⊤) or all are disabled (in case the letter in direction v is ⊥). In addition, since the requirement to satisfy ψ