BRICS RS-96-54 I. Walukiewicz: Pushdown Processes: Games and Model Checking

BRICS

Basic Research in Computer Science

Pushdown Processes: Games and Model Checking

Igor Walukiewicz

BRICS Report Series RS-96-54 ISSN 0909-0878 December 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through World Wide Web and anonymous FTP:

http://www.brics.dk/
ftp://ftp.brics.dk/

This document in subdirectory RS/96/54/

Pushdown processes: games and model checking^{1}

Igor Walukiewicz

Institute of Informatics Warsaw University Banacha 2 02-097 Warsaw, POLAND e-mail: igw@mimuw.edu.pl

Abstract

Games given by transition graphs of pushdown processes are considered. It is shown that if there is a winning strategy in such a game then there is a winning strategy that is realized by a pushdown process. This fact turns out to be connected with the model checking problem for the pushdown automata and the propositional μ-calculus. It is show that this model checking problem is DEXPTIME-complete.

1 Introduction

Pushdown processes are, at least in this paper, just another name for a pushdown automata. The different name is used to underline the fact that we are mainly interested in the graph of configurations of a pushdown process and not in the language it recognises. This graph can be considered as a transition system. In general such a transition system may not be regular, i.e., may not be an unwinding of a finite transition system. Given a priority function mapping states of the automaton to natural numbers, such a transition system defines a two player parity game. In the game, moves of the players alternate. In a move, a player picks a state reachable by an edge from the current one. The result of a game is a finite or infinite path. The path is finite if one of the players cannot make a move; in this case the other player wins. If the path is infinite we find the smallest priority such that a state of this priority appears infinitely often on the path. Player I wins if this priority is even.

1

This work was done at Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

2This work was partially supported by Polish KBN grant No. 2 P301 009 06

Pushdown processes are a generalisation of regular process which correspond to finite automata or regular transition systems [6]. It is stated in [7] that the extra expressive power of pushdown processes may be of use for describing hierarchically structured systems, such as multi-level cashes, or wide area networks. Considering pushdown games is interesting at least for two reasons. First, as we will show here, there is a connection with model checking for pushdown processes and the μ-calculus. The second reason is the problem of synthesis of correct programs (see for example [14, 21]). The conditions of a game may be seen as a specification, and the two players as the program and environment respectively. In this approach the winning strategy is identified with a reactive program satisfying the specification. Hence it is important to know whether a strategy can be implemented as, for example, a regular or pushdown process.

The decidability of the model checking for pushdown processes and the propositional μ-calculus follows from [17]. An elementary model checking procedure for pushdown processes and alternation free fragment of the calculus was given in [3]. We are not aware of any such elementary decision procedure for the whole μ-calculus. The decidability result mentioned above as well as extensions of it (for example [8, 22]) deal with monadic second order logic and reduce the problem to the decidability of S2S formulas, hence give nonelementary algorithms.

Pushdown processes are a strict generalisation of processes from so called basic process algebra BPA (see [6] for a short survey). The processes from BPA can be considered as pushdown processes with only one state. If language recognition is concerned pushdown automata with one state can recognise the same languages as the general pushdown automata. This is not the case when configuration graph is considered. It was shown in [4] that there exists pushdown automaton which transition graph is not bisimilar to the transition graph of any BPA process. BPA is a subclass of process algebra (PA) [1]. For the other interesting subclass of PA, namely, basic parallel processes, the model checking is undecidable [12]. The question whether pushdown games have pushdown strategies was posed in [20]. The main results of this paper are the following.

• We show that for every pushdown game G: if there is a winning strategy in G then there is a pushdown winning strategy in G.

• We reduce a model checking problem for the pushdown process and the whole μ-calculus to the model checking problem for finite transition systems and the μ-calculus. The reduction gives a transition system of size O((k2^{cmn_{1}n_{2}})) where m is the number of states of the pushdown process, k the size of its stack alphabet, n_{1} is the size of the formula and n_{2} is the alternation depth of the original formula. The formula given by reduction is of size n_{2} and alternation depth n_{2}. In particular it turns out that the model checking problem for BPA and a fixed formula is polynomial.

• We show that there exists a formula α such that the model checking problem for a pushdown processes and this particular formula α is DEXPTIME-hard.

Let us mention that the restriction to parity games is not essential. One can use standard methods of translating Muller, Rabin or Streett conditions into parity conditions to obtain appropriate results for this kind of conditions.

The plan of the paper is as follows. We start with a preliminary section where we recall definitions of pushdown automata and the propositional μcalculus. In the following section we present some facts about games with parity conditions. In the next section we prove that if there is a winning strategy on a pushdown tree then there is one realized by a pushdown automaton. In the last section we consider the model checking problem.

Acknowledgement: I would like to thank Damian Niwinski for his helpful comments.

2 Preliminaries

2.1 Pushdown processes

The set of finite sequences over Σ is denoted Σ^{∗} and the set of finite nonempty sequences over Σ is denoted Σ^{+}. The empty sequence is denoted by ε. For s, s′ ∈ Σ^{∗} we let ss′ denote concatenation of the two sequences.

For a given finite set Σ_{s}, let Com(Σ_{s}) = {skip, pop} ∪ {push(z) : z ∈ Σ_{s}} be the set of stack commands over Σ_{s}. The command skip does nothing, the meaning of the remaining two commands is standard.

A pushdown automaton (over one letter alphabet) is a tuple:

A = ⟨Q, Σ_{s}, q_{0} ∈ Q, ⊥ ∈ Σ_{s}, δ : Q × Σ_{s} → P(Q × Com(Σ_{s}))⟩  (1)

where Q is a finite set of states and Σ_{s} a finite stack alphabet. State q_{0} is the initial state of the automaton and ⊥ is the initial stack symbol. A configuration of an automaton is a pair (s, q) with s ∈ Σ_{s}^{+} and q ∈ Q. The initial configuration is (⊥, q_{0}). We assume that ⊥ can be neither put nor removed from the stack. We will sometimes write (s, q) → (s′, q′) if the automaton in one step can go from the configuration (s, q) to (s′, q′). Let →^{+}, →^{∗} denote respectively the transitive closure of → and the reflexive and transitive closure of →.

We will use q to range over states and z to range over letters of the stack alphabet. Remark: In our definition of a pushdown automaton we have assumed that the automaton can put at most one symbol on the stack in one move. This is done only for convenience of the presentation. The main results also hold for the more general form of automata which can push many symbols on the stack in one move. Please note that we can simulate pushing more symbols on the stack by extending the alphabet and the set of states but the simulating automaton will be in general much bigger. This is because we are interested not in the language recognised by the automaton but in the tree of configurations it generates.

Definition 1 (Pushdown tree) A pushdown automaton A as in (1) defines a tree T_{A} ⊆ (Σ_{s}^{+} × Q)^{+} as follows:

• the root of the tree is (⊥, q_{0}),

• for every node (s_{0}, q_{0}), …, (s_{i}, q_{i}), if (s_{i}, q_{i}) → (s, q) then the node has a son (s_{0}, q_{0}), …, (s_{i}, q_{i}), (s, q).

We call (s_{i}, q_{i}) the label of the node (s_{0}, q_{0}), …, (s_{i}, q_{i}).

2.2 Propositional μ-calculus

Let Prop = {p_{1}, p_{2}, … } be a set of propositional constants and let Var = {X, Y, … } be a set of variables. Formulas of the μ-calculus over these sets can be defined by the following grammar:

F := Prop | ¬Prop | Var | F ∨ F | F ∧ F | ⟨ ⟩F | [ ]F | μVar.F |νVar.F

Note that we allow negations only before propositional constants. As we will be interested in closed formulas this is not a restriction. In the following, α, β, … will denote formulas.

Formulas are interpreted in transition systems of the form M = ⟨S, R, ρ⟩, where: S is a nonempty set of states, R ⊆ S × S is a binary relation on S and ρ : Prop → P(S) is a function assigning to each propositional constant a set of states where this constant holds.

For a given model M and an assignment V : Var → P(S), the set of states in which a formula φ is true, denoted ∥ φ ∥_{V}^{M}, is defined inductively as follows:

\begin{matrix}∥ p ∥_{V}^{M} = ρ(p)S & ∥ ¬p ∥_{V}^{M} = S − ρ(p) \\ ∥ X ∥_{V}^{M} = & Val(X) \\ ∥ α ∨ β ∥_{V}^{M} = & ∥ α ∥_{V}^{M} ∪ ∥ β ∥_{V}^{M} \\ ∥ α ∧ β ∥_{V}^{M} = & ∥ α ∥_{V}^{M} ∩ ∥ β ∥_{V}^{M} \\ ∥ ⟨ ⟩α ∥_{V}^{M} = & \{s : ∃s′.R(s, s′) ∧ s′ ∈ ∥ α ∥_{V}^{M}\} \\ ∥ [ ]α ∥_{V}^{M} = & \{s : ∀s′.R(s, s′) ⇒ s′ ∈ ∥ α ∥_{V}^{M}\} \\ ∥ μX.α(X) ∥_{V}^{M} = & ⋂\{S′ ⊆ S : ∥ α ∥_{V al[S′/X]}^{M} ⊆ S′\} \\ ∥ νX.α(X) ∥_{V}^{M} = & ⋃\{S′ ⊆ S : S′ ⊆ ∥ α ∥_{V al[S′/X]}^{M}\} \end{matrix}

here V [S′/X] is the valuation such that, V [S′/X](X) = S′ and V [S′/X](Y) = V (Y) for Y ≠ X. We shall write M, s, V ⊨ φ when s ∈ ∥ φ ∥_{V}^{M} and M, s ⊨ φ if M, s, V ⊨ φ for arbitrary V.

We will use the following well known equivalences. They define the negation of arbitrary closed formula.

¬⟨ ⟩α = [ ]¬α  ¬[ ]α = ⟨ ⟩¬α
¬μX.α(X) = νX.¬α(¬X)  ¬νX.α(X) = μX.¬α(¬X)  (2)

A model checking problem is to decide whether for a given model M, state s and formula α without free variables, the relation M, s ⊨ α holds. Here we will be interested in the case when M is a pushdown tree and s is the root of it.

3 Parity games and canonical strategies

In this section we recall the notion of parity games. We give an explicit description of winning strategies in parity games. We describe the set of winning positions by a fixpoint expression and derive a winning strategy from this expression using the concept of signatures. It turns out that this strategy is canonical in some sense.

The notion of signature was proposed by Streett and Emerson [19]. The proof of the existence of memoryless strategies in parity games was given independently by Mostowski [16] and by Emerson and Jutla [10]. Klarlund [13] proves a more general fact that a player has a memoryless winning strategy in a game if he has a winning strategy and his winning conditions are given as a Rabin condition.

Let G = ⟨V = V_{I} ∪ V_{II} , E ⊆ V × V, Ω : V → {1, …, n}⟩ be a bipartite graph with vertices labelled by priorities from {1, …, n}.

A game from some vertex v_{1} ∈ V_{I} is played as follows: first player I chooses a vertex v_{2} with E(v_{1}, v_{2}), then player II chooses a vertex v_{3} with E(v_{2}, v_{3}), and so on ad infinitum unless one of the players cannot make a move. If a player cannot make a move he looses. The result of an infinite play is an infinite path v_{1}, v_{2}, v_{3}, … This path is winning for player I if in the sequence Ω(v_{1}), Ω(v_{2}), Ω(v_{3}), … the smallest number appearing infinitely often is even. The play from vertices of V_{II} is defined similarly but this time player II starts.

A strategy σ for player I is a function assigning to every sequence of vertices v⃗ ending in a vertex from V_{I} a vertex σ(v⃗) ∈ V_{II} , such that, E(v, σ(v⃗)). A strategy is memoryless iff σ(v⃗) = σ(w⃗) whenever v⃗ and w⃗ end in the same vertex. A strategy is winning iff it guarantees a win for player I whenever he follows the strategy. Similarly we define a strategy for player II .

We will often consider strategies which are partial functions. To fit our definition one can assume that these are total functions which values for some elements don’t matter.

Our main goal is the following theorem:

Theorem 2 (Forgetful determinacy) Let G be a parity game. From every node of G one of the players has a forgetful winning strategy.

The idea of the proof is the following. First we define a set of nodes W_{I} of G by a special fixpoint formula. Having this formula, for every vertex in W_{I} we associate a signature which intuitively says how far is the vertex from something good. We use signatures to define a winning memoryless strategy for player I from vertices in W_{I} . Finally it turns out that the complement of W_{I} is defined by a formula of exactly the same shape as the one defining W_{I} . This gives us a memoryless winning strategy for player II from vertices not in W_{I} .

For the rest of this section let us fix a game graph:

G = ⟨V = V_{I} ∪ V_{II} , E, Ω : V → {1, …, n}⟩

In particular we assume that the range of Ω is {1, …, n} and that n is even. Clearly we can do so without a loss of generality. The graph G can be represented as a Kripke structure G = ⟨V, E, {I^{G}, 1^{G}, …, n^{G}}⟩, where: V is now considered to be a set of states; E defines an edge relation between states and {I , 1, …, n} are propositions. Proposition I^{G} denotes the set of vertices of player I , i.e., the set V_{I} . Each proposition i^{G} ∈ {1^{G}, …, n^{G}} denotes the set of nodes with priority i, i.e., the set {v : Ω(v) = i}.

Consider the formula:

φ_{I} (Z_{1}, …, Z_{n}) = (I ⇒ ⋀_{i∈{1,...,n}}(i ⇒ ⟨ ⟩Z_{i})) ∧ (¬I ⇒ ⋀_{i∈{1,...,n}}(i ⇒ [ ]Z_{i}))

We will be interested in the set:

W_{I} = ∥ μZ_{1}.νZ_{2}…. μZ_{n−1}.νZ_{n}.φ_{I} (Z_{1}, …, Z_{n}) ∥^{G}

(in the formula μ is used to close variables with odd indices and ν is used for even indices; n is even by our assumption).

Definition 3 When applied to n-tuples of ordinals symbols =, <, ≤ stand for corresponding relations in the lexicographical ordering. For every i ∈ {1, …, n} we use =_{i} to mean that both arguments are defined and when truncated to first i positions the two vectors are equal; similarly for <_{i} and ≤_{i}.

Definition 4 (Consistent signature assignment) A signature is a ntuple of ordinals. An assignment S of signatures to nodes from some set U ⊆ V will be called consistent if for every v ∈ U ∩ V_{I} there is a vertex w ∈ U with E(v, w) and such that:

S(w) ≤_{Ω(v)} S(v) and the inequality is strict if Ω(v) is odd.  (3)

similarly if v ∈ U ∩ V_{II} then for all vertices w with E(v, w) we have w ∈ U and the condition (3) holds.

We extend the syntax of the formulas by allowing constructions of the form μ^{τ}Z.α(Z), where τ is an ordinal and α(Z) is a formula from the extended syntax. The semantics is defined as follows:

∥ μ^{0}Z.α(Z) ∥_{V}^{M} = ∅ ∥ μ^{τ+1}Z.α(Z) ∥_{V}^{M} = ∥ α(Z) ∥_{V [∥μ^{τ} Z.α(Z)∥_{V}^{M}/Z]}^{M}
∥ μ^{τ}Z.α(Z) ∥_{V}^{M} = ⋃_{ρ<τ} ∥ μ^{ρ}Z.α(Z) ∥_{V}^{M} (τ a limit ordinal)

By Knaster-Tarski theorem ∥ μZ.α(Z) ∥_{V}^{M} = ⋃_{τ} ∥ μ^{τ}Z.α(Z) ∥_{V}^{M}.

Definition 5 (Canonical signatures) A canonical signature, Sig(v), of a vertex v ∈ V is the smallest in the lexicographical ordering sequence of ordinals (τ_{1}, …, τ_{n}) such that:

v ∈ ∥ φ_{I}(P_{1}, …, P_{n}) ∥^{G}

where:

P_{i} =μ^{τ_{i}}Z_{i}.νZ_{i+1} … νZ_{n}.φ_{I} (P_{1}, …, P_{i−1}, Z_{i}, …, Z_{n}) for i odd
P_{i} =νZ_{i}.μZ_{i+1} … νZ_{n}.φ_{I} (P_{1}, …, P_{i−1}, Z_{i}, …, Z_{n}) for i even

As for an even i the ordinal τ_{i} is not used, the definition implies that τ_{i} = 0 for every even i. We prefer to have this redundancy rather than to calculate right indices each time.

Fact 6 A vertex v belongs to W_{I} iff the canonical signature, Sig(v), is defined.

Proof Suppose v ∈ W_{I} . Let τ be an ordinal of a cardinality bigger than the cardinality of G. By Knaster-Tarski theorem we have:

W_{I} = ∥ μ^{τ}Z_{1}.νZ_{2} … μ^{τ}Z_{n−1}.νZ_{n}.φ_{I} (Z_{1}, …, Z_{n}) ∥^{G}

Hence (τ, …, τ) is an upper bound on the canonical signature for v. So the signature is defined.

Conversely, suppose Sig(v) is defined. For every ordinal ρ and every formula α(X) we have ∥ μ^{ρ}X.α(X) ∥^{G} ⊆ ∥ μX.α(X) ∥^{G}. Thus v ∈ W_{I} by monotonicity. □

Fact 7 The assignment v ↦ Sig(v) is a consistent signature assignment.

Proof We will consider only the case when v ∈ V_{I} . Let (τ_{1}, …, τ_{n}) be the canonical signature of v and let i = Ω(v). Let us assume that i is odd. The case when i is even is simpler.

By our assumptions we have v ∈ ∥ φ_{I} (P_{1}, …, P_{n}) ∥^{G}. Expanding the definition of φ_{I} we obtain: v ∈ ∥ ⟨ ⟩P_{i} ∥^{G}. Hence there is a vertex w ∈ ∥ P_{i} ∥^{G} with E(v, w).

P_{i} = μ^{τ_{i}}Z_{i}.νZ_{i+1} … νZ_{n}.φ_{I} (P_{1}, …, P_{i−1}, Z_{i}, …, Z_{n})

If τ_{i} is a limit ordinal then, by the definition of μ^{τ}, there is a successor ordinal ρ < τ_{i} such that:

w ∈ ∥ μ^{ρ}Z_{i}.νZ_{i+1} … νZ_{n}.φ_{I} (P_{1}, …, P_{i−1}, Z_{i}, …, Z_{n}) ∥^{G}

Once again referring to the definition of μ^{τ} we have:

w ∈ ∥ νZ_{i+1}.μZ_{i+2} … νZ_{n}.φ_{I} (P_{1}, …, P′_{i}, Z_{i+1}, …, Z_{n}) ∥^{G}

where P′_{i} = μ^{ρ−1}Z_{i}.νZ_{i+1} … νZ_{n}.φ_{I} (P_{1}, …, P_{i−1}, Z_{i}, …, Z_{n}). This shows that the canonical signature of w cannot be bigger than (τ_{1}, …, ρ − 1) on first i positions, for some ρ ≤ τ_{i}. Hence Sig(w) <_{i} Sig(v). □

Definition 8 (Canonical strategy) A canonical strategy is a strategy taking for each node v ∈ W_{I} ∩ V_{I} a son which has the smallest canonical signature.

Remark: Despite the name, canonical strategies may not be uniquely determined because a node may have many sons with the same signature.

The forgetful determinacy theorem follows from the next lemma.

Lemma 9 The canonical strategy is a winning memoryless strategy for player I from every node in W_{I} . From every node not in W_{I} player II has a memoryless winning strategy.

Proof Suppose v_{0} ∈ W_{I} . It should be clear that the canonical strategy is memoryless. We show that it is winning. Let P = v_{0}, v_{1}, … be a history of a play when player I uses the canonical strategy. To arrive at a contradiction assume that P is winning for player II . In other words, that the smallest priority appearing infinitely often on P is some odd number p.

Take an infinite sequence of positions j_{1} < j_{2} < … such that: no vertex after v_{j_{1}} has priority smaller than p, and Ω(v_{j_{k}}) = p for k = 1, … From Fact 7 we obtain that Sig(v_{j_{k+1}}) <_{p} Sig(v_{j_{k}}). This is a contradiction because the lexicographical ordering on sequences of ordinals of bounded length is a well ordering.

To show the second statement of the theorem we use some propositional logic. From equivalences (2), the complement of W_{I} is the set:

∥ νZ_{1}.μZ_{2}…. νZ_{n−1}.μZ_{n}.¬φ_{I} (¬Z_{1}, …, ¬Z_{n}) ∥^{G}

Using the propositional tautology

¬((p ⇒ q) ∧ (¬p ⇒ r)) ≡ ((p ⇒ ¬q) ∧ (¬p ⇒ ¬r))

we obtain

¬φ_{I} (¬Z_{1}, …, ¬Z_{n}) = (I ⇒ ⋁_{i∈{1,...,n}}(i ∧ [ ]Z_{i})) ∧ (¬I ⇒ ⋁_{i∈{1,...,n}}(i ∧ ⟨ ⟩Z_{i}))

Using the fact that in each vertex of G exactly one of the propositions 1, …, n holds, the formula above is equivalent to:

(I ⇒ ⋀_{i∈{1,...,n}}(i ⇒ [ ]Z_{i})) ∧ (¬I ⇒ ⋀_{i∈{1,...,n}}(i ⇒ ⟨ ⟩Z_{i}))

Consider the game G′ = ⟨V = V_{II} ∪ V_{I} , E, Ω′⟩ obtained from G by interchanging the vertices of player I and player II and letting Ω′(v) = Ω(v) + 1. It is easy to see that the strategy for player I in G′ translates to a strategy for player II in G and vice versa.

In the formulas above let us increase indices of the variables by one. Adding two dummy variables Z_{1}, Z_{n+2} we can see that in G′ the complement of W_{I} can be described by the formula:

μZ_{1}.νZ_{2} ….μZ_{n+1}.νZ_{n+2}.φ′_{I} (Z_{1}, …, Z_{n+2})

where

φ′_{I} (Z_{1}, …, Z_{n+2}) =

(I ⇒ ⋀_{i∈{2,...,n+1}}(i ⇒ ⟨ ⟩Z_{i})) ∧ (¬I ⇒ ⋀_{i∈{2,...,n+1}}(i ⇒ [ ]Z_{i}))

(observe that the variables Z_{1} and Z_{n+2} are not used). By the first statement of the theorem we know that in G′ there exists a memoryless winning strategy for player I from every node not in W_{I} . This strategy translates to a winning memoryless strategy for player II in G. □

Let us finish with a remark that points out an interesting property of canonical signatures. One can show that every strategy induces a consistent signature assignment and vice versa. Hence we can compare strategies by comparing signatures. The next fact implies that the canonical strategy is in some sense an optimal strategy.

Fact 10 The canonical signature assignment (v ↦ Sig(v)) is the least consistent signature assignment. In other words, for every consistent signature assignment S whenever for some node v, S(v) is defined then Sig(v) is defined and Sig(v) ≤ S(v).

Proof Assume conversely that there is a consistent signature assignment S for which the set of vertices {w : S(w) < Sig(w)} is not empty. Consider vertices from this set for which the difference is at the smallest possible position. Let v be one of such vertices for which S(v) is the smallest possible up to this position. More precisely v is a vertex such that for some i we have:

1. S(v) <_{i} Sig(v),

2. for every w, S(w) =_{i−1} Sig(w), 3. for every w, if S(w) <_{i} Sig(w) then S(v) ≤_{i} S(w).

Given a set of vertices Q we consider the formula:

νZ_{i+1} … μZ_{n−1}.νZ_{n}.φ_{I}(Q, …, Q, Z_{i+1}, …, Z_{n})

We abbreviate this formula by \overrightarrow{σZ}.ψ(Q, Z⃗). Observe that, by the definition, i must be odd.

Claim 10.1 Let u be a vertex and Q a set of vertices. If S(u) is defined and u ∉ ∥ \overrightarrow{σZ}.ψ(Q, Z⃗) ∥^{G} then, when player I uses S, player II can force the play into:

¬Q ∩ {w : S(w) <_{i} S(u)}  (4)

and the play visits only vertices of priority bigger than i before reaching this set.

Proof: If u ∉ ∥ \overrightarrow{σZ}.ψ(Q, Z⃗) ∥^{G} then:

u ∈ ∥ μZ_{i+1}.νZ_{i+2} … νZ_{n−1}.μZ_{n}.\overline{φ}_{I}(¬Q, …, ¬Q, Z_{i+1}, …, Z_{n}) ∥^{G} (5)

where

\overline{φ}_{I} (Z_{1}, …, Z_{n}) = (I ⇒ ⋀_{i∈\{1,...,n\}}(i ⇒ [ ]Z_{i})) ∧ (¬I ⇒ ⋀_{i∈\{1,...,n\}}(i ⇒ ⟨ ⟩Z_{i}))

Let \overline{Sig}(u) denote the signature of the formula in (5) in the node u.

Suppose Ω(u) > i. If u ∈ V_{I} then it is the turn of player I . He chooses a successor u′ of u with the smallest possible value of S. If u ∈ V_{II} then we let player II to choose a son u′ of u with the smallest possible value of \overline{Sig}. By consistency of S, in both cases we know that S(u′) ≤_{Ω(u)} S(u) and that S(u′) is strictly smaller if Ω(u) is odd. It is also easy to check that \overline{Sig}(u′) ≤_{Ω(u)} \overline{Sig}(u) and that \overline{Sig}(u′) is strictly smaller if Ω(u) is even.

We claim that after a finite number of steps as the one above, we must arrive to a vertex of priority not bigger than i. Suppose it is not the case then the above play is infinite. Let p > i be the smallest priority such that states with this priority appeared infinitely often during the play. This priority cannot be odd because, by consistency of S, it would mean that the prefix of length p of signatures given by S was decreased infinitely often and increased only finitely often. Similarly it cannot be even because then the prefix of length p of signatures given by \overline{Sig} would be decreased infinitely often and increased only finitely many times. A contradiction.

Hence the play eventually must reach a node w with Ω(w) ≤ i. From the way the play was constructed it follows that S(w) ≤_{i} S(u).

If w ∈ V_{I} then player I chooses w′ with the smallest possible value of S function. By consistency of S and the fact that i is odd we know that S(w′) <_{i} S(w) ≤_{i} S(u). Because w satisfies the formula (5) we get w′ ∈ ¬Q.

If w ∈ V_{II} then by consistency of S we know that for every w′ with E(w, w′) we have S(w′) <_{i} S(w). Because w satisfies the formula (5) we know that there exists a vertex w′ ∈ ¬Q with E(w, w′). □

We proceed with the proof of the fact. Recall that the vertex v was fixed at the beginning of the proof. It is a vertex from {u : S(u) <_{i} Sig(u)} that has the smallest S-signature up to position i.

We take Q = {w : Sig(w) <_{i} Sig(v) − (0, …, 1, …, 0)}, where the last vector has only one nonzero element on position i. We claim that v ∉ ∥ \overrightarrow{σZ}.ψ(Q, Z) ∥^{G} because otherwise v would have smaller signature. By Claim 10.1 we can find a node w ∈ ¬Q with S(w) <_{i} S(v). By the definition w ∈ ¬Q means Sig(w) ≥_{i} Sig(v) − (0, …, 1, …, 0). Hence S(w) <_{i} S(v) ≤_{i} Sig(v) − (0, …, 1, …, 0) ≤_{i} Sig(w). A contradiction with the choice of v.

□

4 Existence of pushdown strategies

Let A be a pushdown automaton as in (1). For simplicity of the presentation let us assume that the set Q of states of A is partitioned into two sets Q_{I} and Q_{II} . We also assume that transitions from states in Q_{I} lead only to states in Q_{II} and vice versa. More formally we require that for every q, q′, z, z′: whenever (push(z′), q′) or (pop, q′) is in δ(z, q) then: q ∈ Q_{I} iff q′ ∈ Q_{II} .

The automaton A defines a pushdown tree T_{A}. Together with a priority function Ω : Q → ℕ this defines a parity game.

Definition 11 (Pushdown game) An automaton A and a priority function Ω define the pushdown game G_{A} = ⟨V, E, Ω : V → {0, …, n}⟩ where ⟨V, E⟩ is a pushdown tree T_{A} and Ω(v) = Ω(q) for q the state in the label of v. A partition of V into V_{I} and V_{II} is defined by the partition of Q: v ∈ V_{I} iff the state occurring in the label of v belongs to Q_{I} .

Remark: From our assumption about partition of the states of A and assuming that the initial state belongs to Q_{II} we have that in the game G_{A} player II moves from the vertices on the even levels of T_{A} and player I moves from the vertices on odd levels. Observe that, as the game is played on a tree, a strategy can be identified with the subset of the game tree. An important point is what priority assignment functions we allow. We have chosen to allow only functions which are defined in terms of states of the automaton. This choice of the method of assigning priorities is motivated by the fact that we are interested in the winning conditions definable in S1S.

Next let us try to make it precise what we mean by a pushdown strategy. Such a strategy should be given by an automaton reading moves of player II and outputting moves for player I . In the infinity, if player II moved according to the rules then the obtained sequence of moves should determine a path of T_{A} which is winning for player I .

A move is an element of Q×Com(Σ_{s}), i.e., a pair consisting of a state of A and a stack command. A path of T_{A} determines a sequence of moves that the automaton made on this path. Other way around, a sequence of moves may determine a sequence of configurations, i.e., a path of T_{A}. Some sequences of moves do not determine paths because they contain invalid moves. Let us call valid, the sequences determining paths of T_{A}.

A strategy automaton is a deterministic automaton with input and output:

B = ⟨Q_{B}, Σ_{i}, Σ_{o}, Σ_{s,B}, q_{0}, ⊥, δ_{B} : Q_{B} × Σ_{s} × (Σ_{i} × {τ}) → Q_{B} × Com(Σ_{s}) × (Σ_{o} × {τ})⟩ (6)

where Q_{B} is a finite set of states; Σ_{i}, Σ_{o}, Σ_{s,B} are finite input, output and stack alphabets respectively. State q_{0} is the initial state and ⊥ is the initial stack symbol. If δ_{B}(q, z, a) = (q′, com, b) then in the state q with z on the top of the stack and a on the input tape, the automaton changes the state to q′, performs the stack command com, and outputs the symbol b. If a = τ then the automaton does not read the input (and does not move the input head). If b = τ, the automaton outputs nothing.

To be a strategy automaton, B should have the property that it should output one move of player I after reading one move of player II . Moreover it should output valid moves, i.e.: if m_{1}, …, m_{k} is a sequence of read moves, n_{1}, …, n_{k−1} is a sequence of output moves and m_{1}, n_{1}, …, m_{k−1}, n_{k−1}, m_{k} is a valid sequence of moves then B should output some move n_{k} such that m_{1}, n_{1}, …, m_{k}, n_{k} is a valid sequence. Finally, in the infinity, if the obtained sequence of moves is valid then it should determine a path of T_{A} that is winning for player I (see the definition on page 6).

We say that there is a pushdown strategy in G_{A} if there is a strategy automaton for A. Our goal in this section is the following theorem.

Theorem 12 If there is a winning strategy for player I in G_{A} then there is a winning pushdown strategy.

Let us now try to explain an idea of the construction of the strategy. First, we know that if there is a strategy for player I then there is a canonical strategy. This strategy depends only on the current configuration and consists of picking a configuration with the smallest possible signature. Unfortunately, a strategy automaton cannot know the current configuration as there are potentially infinitely many of them. Our strategy automaton, looking at its state and the top of its stack, will be able to tell what is currently on the top of the stack of A and what is the current state of A. It will also have some finite information about the rest of the stack of A as we try to describe now.

Let us look at a run of the automaton A. Suppose that in a configuration (s_{0}, q_{0}) one of the players performs (q, push(z)). Because the game is given by a pushdown automaton, the part of the game from the obtained configuration (sz, q) up to the nearest configurations where z is taken from the stack does not depend on s. What depends on s is the rest of the play when z is taken out from the stack and the current configuration becomes (s, q′) for some q′. Hence it should be enough if player I iinstead of knowing the whole s just knew which states he can reach when taking z from the stack. In general he will need a sequence of sets of states A⃗ = {A^{p}}_{p=1,...,n}, each set A^{p} containing the states that can be reached provided the smallest priority met between pushing and popping z is p.

The definition below formalises this intuition in the notion of subgame G(A⃗, z, θ, q). The additional parameter θ is used to capture the situation when some moves on the current level were already taken. In this case θ would be the smallest priority among states met when z was on the stack. Notation: We assume that {1, …, n} is the range of Ω. We use A⃗ to range over n element vectors of sets of states and θ to range over {1, …, n}. We also use z to range over stack symbols and q to range over states.

Definition 13 (Sub-game) For every quadruple A⃗, z, θ, q we define the game G(A⃗, z, θ, q) as follows. The arena of the game is a subtree of T_{A} starting from a node with the configuration (⊥z, q). Every node labelled with a configuration (⊥, q′), for some q′, is marked winning or loosing. We mark the node winning if q′ ∈ A^{min(p,θ)}, where p is the lowest priority of a state appearing on the path to the node (counting q but not q′). Otherwise we mark the node loosing. Whenever a play reaches a marked node then: player I wins if this node is marked winning otherwise player II is the winner. If a play is infinite: player I wins iff the obtained path is winning (as defined at the beginning of Section 3).

Remark: In our definition of the game we did not have the concept of marking but we allowed vertices with no sons, and had the rule that the player looses if he cannot make a move. Hence we can simulate marking of vertices with cutting the paths. We find the metaphor of markings more useful here.

Summarising, player I will have only partial information about the current configuration, namely: the current state, the current symbol on the top of the stack, the sets of states it is allowed to reach when popping this symbol and the lowest priority met from the time when this symbol was pushed on the stack. The size of this information is bounded. To accomplish his task of winning the sub-game he can try to use the canonical signatures.

Definition 14 (Signature, Hint) Suppose that player I has a winning strategy in a game G(A⃗, z, θ, q). Define Sig(A⃗, z, θ, q) to be the canonical signature of the root of the game.

If q ∈ Q_{I} then let v be a son of the root having the smallest signature (if there is more than one such son then fix one arbitrary). If v is labelled by (⊥, q′) then let Hint(A⃗, z, θ, q) = (q′, pop). If v is labelled (⊥z, q′) then let Hint(A⃗, z, θ, q) = (q′, skip). Otherwise v is labelled by (⊥zz′, q′) and let Hint(A⃗, z, θ, q) = (q′, push(z′)).

Finally, when a new push operation is performed, player I should calculate new sets of goal states just using the information he has at hand.

Definition 15 (Update function) Define Up(A⃗, z, θ, q) to be the sequence of sets A⃗_{1} = {A_{1}^{p}}_{p∈{1,...,n}}, where each A_{1}^{p} is the set of states q′ such that:

Sig(A⃗, z, min(Ω(q), p, θ), q′) ≤_{min(Ω(q),p)} Sig(A⃗, z, θ, q)

in the case min(Ω(q), p) is even and

Sig(A⃗, z, min(Ω(q), p, θ), q′) <_{min(Ω(q),p)} Sig(A⃗, z, θ, q)

otherwise.

Now we have all the components to define the strategy automaton.

Definition 16 (Strategy automaton) The strategy automaton B for G_{A} has the same set Q of states as A. Its input and output alphabets are the moves of A, i.e., Σ_{i} = Σ_{o} = Q × Com_{s}(Σ_{s}). Its stack alphabet Σ_{s,B} is P(Q)^{n} × Σ_{s} × {1, …, n}. Before defining the transition relation δ_{B} let us introduce an abbreviation. We introduce a new stack command repmin(θ′) which means: if on the top of the stack there is some triple A⃗zθ, replace it with A⃗zθ_{1}, where θ_{1} = min(θ, θ′). We also introduce a semicolon operation, so δ_{B}(q, A⃗zθ, a) = (q′, pop; repmin(θ′)) means that first A⃗zθ is removed from the stack, then possibly the third component of the triple currently at the top of the stack is changed and the new state becomes q′. Hence, if we had a configuration (sA⃗_{1}z_{1}θ_{1}A⃗zθ, q) then after this operation we obtain the configuration (sA⃗_{1}z_{1} min(θ_{1}, θ′), q′). Let us proceed with the definition of δ_{B}:

• If q ∈ Q_{I} then:

– δ_{B}(q, A⃗zθ, τ) = (q′, skip, “(q′, skip)”) if Hint(A⃗, z, q, θ) = (q′, skip).

– δ_{B}(q, A⃗zθ, τ) = (q′, pop; repmin(min(θ, Ω(q))), “(q′, pop)”) if Hint(A⃗, z, q, θ) = (q′, pop).

– δ_{B}(A⃗zθ, q, τ) = (q′, repmin(Ω(q)); push(A⃗′z′n), “(q′, push(z′))”) if Hint(A⃗, z, q, θ) = (q′, push(z′)) and A⃗′ = Up(A⃗, z, θ, q)

• If q ∈ Q_{II} then:

– δ_{B}(q, A⃗zθ, “(q′, skip)”) = (q′, skip, τ) if (q′, skip) ∈ δ_{A}(q, z)

– δ_{B}(q, A⃗zθ, “(q′, pop)”) = (q′, pop; repmin(min(θ, Ω(q))), τ) if (q′, pop) ∈ δ_{A}(q, z).

– δ_{B}(q, A⃗zθ, “(q′, push(z′))”) = (q′, repmin(Ω(q)); push(A⃗′z′n), τ) if (q′, push(z′)) ∈ δ_{A}(q, z) and A⃗′ = Up(A⃗, z, θ, q).

Lemma 17 Suppose that player I can win in G(A⃗, z, θ, q). If

δ_{B}(q, A⃗zθ, τ) = (q_{1}, repmin(Ω(q)); push(A⃗_{1}z′_{1}n), “(push(z′), q)”)

or

δ_{B}(q, A⃗zθ, “(q_{1}, push(z_{1}))”) = (q_{1}, repmin(Ω(q)); push(A⃗_{1}z_{1}n), τ)

then Sig(A⃗_{1}, z_{1}, n, q_{1}) ≤_{Ω(q)} Sig(A⃗, z, θ, q) and it is strictly smaller if Ω(q) is odd.

Proof Consider the games G = G(A⃗, z, θ, q) and G_{1} = G(A⃗_{1}, z_{1}, n, q_{1}). Define a function F : G_{1} → G by F((⊥s′, q′) … (⊥s′′, q′′)) = (⊥zs′, q′) … (⊥zs′′, q′′), i.e. to every configuration of the path we add z just after ⊥. It is an injective function respecting descendancy relation and priorities of nodes. This function assigns to the root of G_{1} the node v labelled (⊥zz_{1}, q_{1}). This node is a son of the root of G.

Let σ denote the canonical strategy in G. Because v ∈ σ we can use the function F to obtain a strategy σ_{1} = F^{−1}(σ) in G_{1}. We will show that this strategy is winning.

Let P be a result of a play in the game G_{1} when player I uses σ_{1}. If P is infinite then F(P) is a result of a play in G when player I uses σ. Hence P is winning for I . Suppose P is finite ending in some node w. The label of w is (⊥, q′) for some state q′. We will show that this node is marked winning. Let p be the minimum of priorities of states appearing on the path from v to F(w). According to Definition 13 the node is winning if q′ ∈ A⃗_{1}^{p}. By definition of the automaton B we know that A⃗_{1} = Up(A⃗, z, θ, q). Hence we have to show that:

Sig(A⃗, z, min(Ω(q), p, θ), q′) ≤_{min(Ω(q),p)} Sig(A⃗, z, θ, q)

Let us use the subscript G in Sig_{G}(v) to stress that this is the canonical signature in the game G.

Claim 17.1 Sig_{G}(F(w)) ≤_{min(Ω(q),p)} Sig(A⃗, z, θ, q) and it is strictly smaller if min(Ω(q), p) is odd.

Proof: As v is a son of the root of G on the path to F (w), by consistency of canonical signatures (Fact 7) Sig_{G}(F(w)) ≤_{p} Sig_{G}(v) and it is strictly smaller if p is odd. By the same fact we have Sig_{G}(v) ≤_{Ω(q)} Sig(A⃗, z, θ, q) and is strictly smaller if Ω(q) is odd. □

Claim 17.2 Sig_{G}(F(w)) = Sig_{G}(A⃗, z, min(Ω(q), p, θ), q′)

Proof: We show that the game G(A⃗, z, min(Ω(q), p, θ), q′) is isomorphic to the part of G issued from F(w). To see this, we have to check that a node is marked winning in G(A⃗, z, min(Ω(q), p, θ), q′) iff it is marked winning in G. Let q′′ be a state and u a node labelled by (⊥, q′′). Let also p′′ be the minimum of priorities of states that appeared between F(w) and u. The node u is marked winning in G iff q′′ ∈ A^{min(min(Ω(q),p,p′′),θ)}. It is marked winning in G(A⃗, z, min(Ω(q), p, θ), q′) iff q′′ ∈ A^{min(p′′,min(Ω(q),p,θ))}. □

Knowing that σ_{1} is winning in G_{1} we can define a signature assignment by S(w) = Sig(F(w)) for every w reachable in a play of G_{1} when player I uses σ_{1}. This is a consistent signature assignment, hence by Fact 10 we have that Sig(A⃗_{1}, z_{1}, θ_{1}, q_{1}) ≤ S(F^{−1}(v)). By consistency of S we have that S(F^{−1}(v)) ≤_{Ω(q)} Sig_{G}(A⃗, z, θ, q) and it is strictly smaller if Ω(q) is odd. □

Lemma 18 If a configuration (szA⃗θ, q) is reachable from the initial configuration then Sig(A⃗, z, θ, q) is defined.

Proof Induction on the length of the derivation with a help of Lemma 17. □

Lemma 19 Suppose that player I can win the game G_{A}. Let (szA⃗θ, q) be a configuration of B reachable from the initial one. Suppose also that on some finite input sequence w the automaton B goes from (szA⃗θ, q) to a configuration (szA⃗θ′, q′) and szA⃗ is always on the stack during this derivation. Let p be the minimum of the priorities of the states appearing in the derivation. We have:

1. θ′ = min(p, θ)

2. Sig(A⃗, z, θ′, q′) ≤_{p} Sig(A⃗, z, θ, q) and it is strictly smaller if p is odd (in particular both signatures are defined).

Proof The proof proceeds by induction the length of derivation. The case (sA⃗zθ, q) →^{a} (sA⃗zθ, q′) follows directly from the construction of the automaton.

Suppose:

(sA⃗zθ, q) →^{a} (sA⃗zθ′′A⃗_{1}z_{1}n, q_{1}) →^{u} (sA⃗zθ′′A⃗_{1}z_{1}θ′_{1}, q′_{1}) →^{b} (sA⃗zθ′, q′)

and A⃗_{1}z_{1} was not popped while reading the sequence u. By induction assumption, θ′_{1} is the minimum of priorities of states which appeared in the part of the derivation when there was sA⃗zθ′′A⃗_{1}z_{1} on the stack. Let p_{1} = min(θ′_{1}, Ω(q′_{1})). From Lemma 18 we know that the signature Sig(A⃗_{1}, z_{1}, θ′_{1}, q′_{1}) is defined. Hence q′ ∈ A_{1}^{p_{1}}. This, by definition, means:

Sig(A⃗, z, min(Ω(q), p, θ), q′) ≤_{min(Ω(q),p)} Sig(A⃗, z, θ, q)

and the inequality is strict if min(Ω(q), p) is odd. It is easy to see that θ′ = min(Ω(q), p, θ).

The remaining case is when (sA⃗zθ, q) →^{u} (sA⃗zθ_{1}, q_{1}) →^{v} (sAzθ′, q′). This follows directly from two applications of the induction assumption. □

Lemma 20 B is a strategy automaton.

Proof The automaton B is constructed in such a way that from the current configuration of B it is easy to extract the current configuration of A; it is enough to throw away A⃗ and θ components from the stack. We have also the property that whenever B read m_{1}, …, m_{i}, outputed n_{1}, …, n_{i} and m_{1}, n_{i}, …, m_{i} determines a path in T_{A} then m_{1}, n_{1}, …, m_{i}, n_{i} also determines a path in T_{A}. Moreover this path ends in a configuration of A which is extracted from the current configuration of B.

Now, assume conversely that B is not a strategy automaton. Let w_{i} = m_{1}, m_{2}, … be an input word on which B outputs w_{o} = n_{1}, n_{2}, … and the sequence m_{1}, n_{1}, … determines a loosing (for player I ) path in T_{A}.

Suppose that P is finite, i.e., B cannot make a move from some configuration. Say it is (szA⃗θ, q). If q ∈ Q_{II} then, by the definition of B, it means that the next move in the input sequence is invalid. Hence q ∈ Q_{I} . From Lemma 18 it follows that Sig(A⃗, z, θ, q) is defined. Hence Hint(A⃗, z, θ, q) is defined and B can make a move. A contradiction.

Suppose that P is infinite. This means that the smallest priority of a state appearing i.o. on the path determined by m_{1}, n_{1}, … is odd. Call it p. From what was said in the first paragraph, this means that p is the smallest priority of a state appearing i.o. in the run of B on w_{i}. Using these observations we will construct a sequence of strictly decreasing signatures. This will be a contradiction with the fact that the signatures are well ordered.

Let x_{0} be a position in the run such that: (i) after x_{0} no state with a priority smaller than p appears on the run, (ii) on the position x_{0} in the run there is a configuration (szA⃗θ, q) and for every position after x_{0} we have szA⃗ on the stack.

Suppose there is a position x_{1} after x_{0} with a configuration (szA⃗θ_{1}, q_{1}) and a state of the priority p occurs in a configuration between x_{0} and x_{1}. By Lemma 19 we have that Sig(A⃗, z, θ_{1}, q_{1}) <_{p} Sig(A⃗, z, θ, q). Next from x_{1} we can look for a position x_{2} with a configuration (szA⃗θ_{2}, q_{2}) such that a state of the priority p appears between x_{1} and x_{2}. This way we construct a sequence of positions x_{0}, x_{1}, …, x_{i}. Because the signatures decrease, this sequence must be finite. Hence form some position, say x_{i}, we will not be able find a bigger position with the required properties. As a state of priority p appears infinitely often on the run, there must be a position x_{i+1} after x_{i} with a configuration (szA⃗θ_{i}z′A⃗′n, q_{i+1}) such that (szA⃗θ_{i}z′A⃗′) is on the stack of every configuration after x_{i+1}. By Lemmas 17 and 19 we have Sig(A⃗′, z′, n, q_{i+1}) ≤_{p} Sig(A⃗, z, θ_{i}, q_{i}) and the inequality is strict if a state of priority p appeared between x_{i} and x_{i+1}. From x_{i+1} we can repeat exactly the same construction as from x_{0}. Repeating this reasoning infinitely often we obtain an infinite sequence of strictly decreasing signatures. A contradiction. □

Remark: The automaton B is exponentially larger than A. One can show that in general the strategy automaton must be exponentially larger, although it is not clear that the exponent must be O(n|Q|) as it is in the case of B. This situation is different from the situation for parity games on finite transition systems where no memory is need.

An example of a game that has only big strategies is the following. Player II starts by choosing a sequence of n symbols: 0 or 1. Then player II chooses a position i ∈ {1, …, n} and asks what symbol stands on this position. Player I has to answer correctly. Then Player II asks about another position and Player I wins if he answers correctly also this time. It is easy to see that the graph of such a game can be defined by a pushdown automaton of size O(n). Every strategy automaton must have the size O(2^{n}).

5 Model checking for pushdown trees

We consider a problem of checking whether a given pushdown tree satisfies a given formula of the propositional μ-calculus. We will reduce this problem to the problem of establishing existence of a winning strategy in a game on a pushdown tree. Next we will use results from the previous section to show how one can solve this later problem. Finally we will show the lower bound on the complexity of the model checking problem

5.1 Reduction to games

We will show how to reduce a model checking problem to a problem of establishing existence of a winning strategy in a game on a pushdown tree. Let us start with some technical definitions concerning μ-calculus formulas. These will facilitate the description of the reduction.

Definition 21 (Binding) We call a formula well named if every variable is bound at most once in the formula and free variables are distinct from bound variables. For a variable X bound in a well named formula φ there exists a unique subterm of φ of the form μX.β(X) or νX.β(X), from now on called the binding definition of X in φ and denoted D_{φ}(X). We call X a μ-variable when D_{φ}(X) = μX.β(X) for some β, otherwise we call X a ν-variable.

The function D_{φ} assigning to every bound variable its binding definition in φ will be called the binding function associated with φ.

Definition 22 (Dependency order) Given a formula φ we define the dependency order over the bound variables of φ, denoted ≤_{φ}, as the least partial order relation such that if X occurs free in D_{φ}(Y) then X ≤_{φ} Y. We will say that a bound variable Y depends on a bound variable X in φ when X ≤_{φ} Y.

Definition 23 (Fisher-Ladner closure) For a given formula α we denote by FL(α) (Fisher-Ladner closure) the set of subformulas of α (including α itself).

Let φ be a μ-calculus formula without free variables. Without a loss of generality we may assume that it is well named. Let X_{1}, …, X_{n} be some linearisation of the dependency order ≤_{φ}, i.e., if X_{i} ≤_{φ} X_{j} then i ≤ j. We will assume that the variables with even indices are ν-variables and the variables with odd indices are μ-variables. If it is not the case, we can add dummy variables to the list. This assumption is not essential but simplifies the presentation as the index immediately determines whether it is a μ or a ν-variable.

Let:

A = ⟨Q, Σ_{s}, q_{0} ∈ Q, ⊥ ∈ Σ_{s}, δ : Σ_{s} × Q → Com(Σ_{s}) × Q⟩

be a pushdown automaton as in (1).

In the previous section we have assumed that the states of the automaton defining a game are partitioned into Q_{I} and Q_{II} and transitions from states in one set lead to states in the other set. Here we will still assume the that the set of states is partitioned but it may now happen that a transition leads to a state from the same set. We can avoid this by adding some dummy states. The number of added states will be at most linear in the size of the automaton.

Now we define our target pushdown game. Consider the automaton:

C = ⟨Q × FL(φ), Σ_{s}, q_{0}, ⊥, δ_{C}⟩

where δ_{C} is defined as follows:

δ_{C}((q, α ∨ β), z) ={((q, α), skip), ((q, β), skip)}
δ_{C}((q, α ∧ β), z) ={((q, α), skip), ((q, β), skip)}
δ_{C}((q, μX.α(X)), z) =δ_{C}((q, νX.α(X)), z) = {((q, X), skip)}
δ_{C}((q, X), z) ={((q, α(X)), skip)} if D_{φ}(X) = σX.α(X)
((q′, α), push(z′)) ∈δ_{C}((q, ⟨ ⟩α), z) = δ_{C}(z, (q, [ ]α))
if δ(q, z) = (q′, push(z′))
((q′, α), push(z′)) ∈δ_{C}((q, ⟨ ⟩α), z) = δ_{C}((q, [ ]α), z)
if δ(q, z) = (q′, pop)

It remains to define in which nodes player I is to move and what is the priority of each state. Player I moves when the game is in a node which label contains a state: (q, α ∨ β), (q, μX.α(X)), (q, νX.α(X)), (q, X), or (q, ⟨ ⟩α); for some q ∈ Q and some formulas α, β. In the remaining nodes player II is to move. Priority function Ω is defined by: Ω((q, X_{i})) = i and Ω((q, α)) = n+1, for α not a variable and q ∈ Q.

Theorem 24 T_{A} ⊨ φ iff there is a winning strategy for player I in the game T_{C} with the priority function Ω.

For finite transition systems a very similar theorem was shown by Emerson, Jutla and Sistla in [9]. For left to right implication one can use signatures of φ. For right to left implication assume conversely and show that player II has a winning strategy. See for example [19] or [18] for similar arguments.

5.2 Establishing existence of winning strategies

Let A be a pushdown automaton as in (1) and let Ω : Q → {1, …, n} be an indexing function. These define the game on G_{A}. Here we are concerned with the problem: given A and Ω establish whether there exists a winning strategy for player I in G_{A}. We will reduce this problem to the problem of establishing existence of a winning strategy in a game on some finite graph. Let A and Ω be fixed for the rest of this subsection.

Definition 25 (Game M_{A}) Let M_{A} = ⟨V_{A}, →, Ω_{A}⟩ be a game on a finite graph defined as follows. For every A⃗, A⃗_{1}, z, z_{1}, θ, q, q_{1} and p ∈ {1, …, n} we have nodes:

Check(A⃗, z, θ, p, q)  Push(A⃗, z, θ, q)
Move((A⃗, z, θ, q), (?, z_{1}, q_{1})) Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1}))
Pop(q)  Err(q)

Here ‘?’ is a special symbol. We have the following transitions between the nodes:

Check(A⃗, z, θ, p, q) → Check(A⃗, z, θ, p, q′) if (q′, skip) ∈ δ(q, z) Check(A⃗, z, θ, p, q) → Pop(q′) if (q′, pop) ∈ δ(q, z) and q′ ∈ A^{min(Ω(q),θ)} Check(A⃗, z, θ, p, q) → Err(q′) if (q′, pop) ∈ δ(q, z) and q′ ∉ A^{min(Ω(q),θ)} Check(A⃗, z, θ, p, q) → Move((A⃗, z, θ, q), (?, z_{1}, q_{1}))

if (q_{1}, push(z_{1})) ∈ δ(q, z)

and exactly the same transitions from Push(A⃗, z, θ, q), moreover we have:

Move((A⃗, z, θ, q), (?, z_{1}, q_{1})) → Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})) Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})) → Push(A⃗_{1}, z_{1}, n, q_{1}) Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})) → Check(A⃗, z, min(θ, p), p, q′′)

if p ≤ Ω(q) and q′′ ∈ A_{1}^{p} The set V_{I} of nodes where Player I makes a move consists of nodes:

Check(A⃗, z, θ, p, q), Push(A⃗, z, θ, q), Move((A⃗, z_{1}, θ, q_{1}), (?, z_{2}, q_{2})) for q ∈ Q_{I} and arbitrary A⃗, z, z_{1}, z_{2}, θ, p, q_{1}, q_{2}

The set V_{II} of nodes where Player II makes a move consists of nodes:

Check(A⃗, z, θ, p, q), Push(A⃗, z, θ, q), Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})) for q ∈ Q_{II} and arbitrary A⃗, z, z_{1}, z_{2}, θ, p, q_{1}, q_{2}

Priority function Ω_{M} is defined by:

Ω_{M}(Check(A⃗, z, θ, p, q)) = p Ω_{M}(Push(A⃗, z, θ, q)) = Ω(q)
Ω_{M}(m) = n + 1 for all other nodes m of M_{A}

Player I wins in the game M_{A} if either:

• after finitely many steps player II cannot make a move or a node labelled Pop(q), for some q, is reached.

• the game is infinite and the infinite path P which is the result of the play is winning for I . Recall that this means that the minimal priority of states appearing infinitely often on P is even.

Theorem 26 Player I has a winning strategy in the game G_{A} iff he has a winning strategy in the game M_{A} from the node Check((∅, …, ∅), ⊥, n, n, q_{0}).

Proof First, let us consider the left to right implication. We define a strategy σ_{M} for player I on M_{A} as follows.

• if q ∈ Q_{I} , Sig(A⃗, z, θ, q) is defined and Hint(A⃗, z, θ, q) = (q_{1}, skip) then:

σ_{M}(Check(A⃗, z, θ, p, q)) = Check(A⃗, z, θ, p, q_{1})
σ_{M}(Push(A⃗, z, θ, q)) = Push(A⃗, z, θ, q_{1})

• if q ∈ Q_{I} , Sig(A⃗, z, θ, q) is defined and Hint(A⃗, z, θ, q) = (q_{1}, pop) then:

σ_{M}(Check(A⃗, z, θ, p, q)) = σ_{M}(Push(A⃗, z, θ, q)) = Pop(q_{1})

• If q ∈ Q_{I} , Sig(A⃗, z, θ, q) is defined and Hint(A⃗, z, θ, q) = (q_{1}, push(z_{1})) then:

σ_{M}(Check(A⃗, z, θ, p, q)) = σ_{M}(Push(A⃗, z, θ, q)) =

Move((A⃗, z, θ, q), (?, z_{1}, q_{1}))

• if q ∈ Q_{I} ∪ Q_{II} , Sig(A⃗, z, θ, q) is defined and A⃗_{1} = Up(A⃗, z, θ, q) then let:

σ_{M}(Move((A⃗, z, θ, q), (?, z_{1}, q_{1}))) = Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1}))

Let →_{σ_{M}} denote the subset of the transition relation of M_{A} defined by the strategy σ_{M}, i.e., →_{σ_{M}} = {(m, n) : if m ∈ V_{I} then σ_{M}(m) = n}∩ →. We will show that every path along →_{σ_{M}} is winning for player I .

The initial state of M_{A} is Check((∅, …, ∅), ⊥, n, n, q_{0}). From the assumption that player I can win in the game G_{A} it follows that Sig((∅, …, ∅), ⊥, n, q_{0}) is defined. Let us observe the following properties:

• There is always Pop(q_{1}) as required in the first clause of the definition of →_{σ_{M}}.

• There is no →_{σ_{M}} transition to Err(q_{1}), for any q_{1}.

• If Check(A⃗, z, θ, p, q) →_{σ_{M}} Check(A⃗, z, θ, q_{1}) then Sig(A⃗_{1}, z_{1}, n, q_{1}) ≤_{Ω(q)} Sig(A⃗, z, θ, q) and it is strictly smaller if Ω(q) is odd. Similarly for Push instead of Check.

• If Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})) →_{σ_{M}} Push(A⃗_{1}, z_{1}, n, q_{1}) then Sig(A⃗_{1}, z_{1}, n, q_{1}) ≤_{Ω(q)} Sig(A⃗, z, θ, q) and it is strictly smaller if Ω(q) is odd.

• If Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})) →_{σ_{M}} Check(A⃗, z, θ_{2}, p, q_{2}) then Sig(A⃗, z, θ_{2}, q_{2}) ≤_{p} Sig(A⃗, z, θ, q) and it is strictly smaller if p is odd.

A standard argument about the signatures shows that every path in M_{A} starting from the initial vertex and proceeding along →_{σ_{M}} transitions is winning for player I .

For the right to left implication assume that there is a winning strategy σ_{M} in M_{A}. We construct a strategy automaton C:

C = ⟨Q_{C}, Q × Com(Σ), Q × Com(Σ), S_{M}, q_{0}, Check((∅, …, ∅), ⊥, n, n, q_{0}), δ_{C}⟩ Where Q_{C} is some set of auxiliary states needed to “implement” the necessary behaviour of δ_{C} that we describe below. The automaton C will work in macro steps. Each step will begin and end in the state q_{0} ∈ Q_{C}. It will be also the case that at the beginning and end of each macro step there will be Check or Push node on the top of the stack.

Assume that m is the current symbol at the top of the stack. Assume also that m is of the form Check(A⃗, z, θ, p, q) or Push(A⃗, z, θ, q).

If q ∈ Q_{I} then for every transition m →_{σ_{M}} u we add to δ(q_{0}, m, τ) the following transitions:

• If u is Check(A⃗, z, θ, p, q′) or Push(A⃗, z, θ, q′) then replace m by u on the top of the stack and output “(q′, skip)”.

• If u is Pop(q′) then q′ ∈ A^{min(Ω(q),θ)}. Pop elements from the stack until a Push node is popped. The current top node of the stack becomes some Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})). Push the node Check(A⃗, z, min(θ, p), p, q′) where p = min(Ω(q′), θ_{1}, Ω(q)). Output “(q′, pop)”.

• If u is a Move((A⃗, z, θ, q), (?, z_{1}, q_{1})) node then there are nodes u′, u′′ such that u →_{σ_{M}} u′ →_{σ_{M}} u′′. Moreover u′ is Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})) and u′′ is Push(A⃗_{1}, z_{1}, n, q_{1}). Add to δ(q_{0}, m, τ) operations that push u′ and u′′ on the stack and output “(q_{1}, push(z_{1}))”

If q ∈ Q_{II} then for every transition m →_{σ_{M}} n we add the following transitions:

• If u is Check(A⃗, z, θ, p, q′) or Push(A⃗, z, θ, q′) then on input “(q′, skip)” replace m by u on the top of the stack. Do not produce any output.

• If u is Pop(q′) then q′ ∈ A^{min(Ω(q),θ)}. Start from δ(q_{0}, m, “(q′, Pop)”) an operation which pops elements from the stack until a Push node is popped. The current top node of the stack becomes some node Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})). Push the node Check(A⃗, z, min(θ, p), p, q′) where p = min(Ω(q′), θ_{1}, Ω(q)). Do not produce any output.

• If u is a Move((A⃗, z, θ, q), (?, z_{1}, q_{1})) node then there are nodes u′, u′′ such that u →_{σ_{M}} u′ →_{σ_{M}} u′′, where u′ is Move((A⃗, z, θ, q), (A⃗_{1}, z_{1}, q_{1})) and u′′ is Push(A⃗_{1}, z_{1}, n, q_{1}). Start from δ(q_{0}, m, “(q_{1}, Push(z_{1}))”) an operation that pushes u′ and u′′ on the stack. Do not produce any output.

After the end of the macro step we arrive back at the configuration when the state is q_{0} and the node on the top of the stack is either Push or Check node.

To see that C is a strategy automaton, one uses the following observation.

Observation 26.1 Let m_{1}, …, m_{i} be a sequence of moves of A. Suppose the automaton C on this sequence goes from a configuration (sm, q_{0}) to a configuration (s′m′, q_{0}) and outputs n_{1}, …, n_{i} in the process. If p is the smallest priority of a state appearing in m_{1}, n_{1}, …, m_{i}, n_{i} then the signature of m′ is not bigger on positions up to p than the signature of m; the first signature is strictly smaller if p is odd.

□

The size of the transition system M is O(k2^{cmn}) where k is the size of the stack alphabet, m is the number of states of A, n is the range of the priority function Ω and c is a constant. The task of establishing existence of a winning strategy in M is equivalent to checking satisfiability of the specific μ-calculus formula. Hence any model checking algorithm will solve the problem. Using currently known algorithms [11, 15] we obtain that the whole problem can be solved in time O((k2^{cmn})^{n}). This is the estimation only for the problem of establishing existence of a winning strategy. Putting it together with the reduction from the previous subsection we obtain:

Corollary 27 For a given automaton A with m states and k stack symbols and a formula φ of size n_{1} with alternation depth n_{2} there is an algorithm deciding in time O((k2^{cmn_{1}n_{2}})^{n_{2}}) whether φ holds in the root of the pushdown tree T_{A}.

5.3 The lower bound

Finally we show a deterministic exponential time lower bound on the model checking problem for pushdown automata and (non alternating) μ-calculus. It follows from a quite standard reduction by simulating alternating linear space bounded Turing machines. The simulating automaton is very similar to the one described by Chandra, Kozen and Stockmeyer in [5].

Let M be an alternating linear space bounded Turing machine. We will assume that M has only one tape and on the input of size n it uses at most n + 1 tape squares along any computation path. Let Q = Q_{∃} ∪ Q_{∀} be the set of states of M which is partitioned into existential and universal sates. Let Γ be a tape alphabet and let δ : Q × Γ → (Q × Γ × {left, right})^{2} be a transition function. A configuration of M is a string wqw′ where w, w′ ∈ Γ^{∗} and q ∈ Q, moreover ww′ is of length n + 1.

For a given machine M and a word w we construct a pushdown automaton A such that player I can reach a leaf in the game T_{A} iff w is accepted by M. Initially the automaton A pushes on the stack the sequence of n + 1 letters from Q ∪ Γ with exactly one letter from Q. Then the pushdown automaton arrives at an existential or universal state depending on whether the state q which was pushed on the stack was existential or universal. In this state pushdown automaton also remembers q and the letter a pushed on the stack just after q. It consults the transition function and chooses an element from the pair given by δ(q, a) or makes a universal branching to both elements. He puts this element on the stack and repeats the whole process of putting n+1 letters from Q∪Γ on the stack and deciding upon a next configuration. This cycle stops if in the latest sequence of n + 1 letters an accepting state was pushed on the stack. At this point the pushdown automaton goes to an universal state Check and on the stack we have a sequence:

c_{0}(q_{1}, a_{1}, d_{1})c_{1} … (q_{k}, a_{k}, d_{k})c_{k}

The universal branching of A is used to check whether it is a sequence of configurations of M provided for every i = 1, …, k, in the step i the move (q_{i}, a_{i}, d_{i}) was taken. Using universal choice the automaton goes to a state which checks whether c_{k} can be reached from c_{k−1} in the step (q_{k}, a_{k}, d_{k}) and it also goes to another state which just takes (q_{k}, a_{k}, d_{k})c_{k} from the stack and starts checking lower configurations. This is repeated until the first configuration is reached. The automaton then checks that this first configuration is of the form q_{0}wB^{i}, where B^{i} is a sequence of blanks of appropriate length. Please observe that checking that one configuration follows from the previous one can be done using universal branching in finite memory linear in the size of M. The automaton just checks each letter separately. It can do so as it can count to n + 5 in its finite control. If at some point one of the tests described above fails then the automaton enters into an infinite loop otherwise each of the tests stops in some final state. From this reduction we obtain.

Fact 28 There exists a formula α (without alternations) such that the problem “given a pushdown automaton A, is α satisfied in the root of T_{A}” is DEXPTIME-hard. (Formula α expresses the fact that player I can reach a final state.)

Remark:This argument does not work for BPA processes as they correspond to pushdown automata without states and we needed states in our reduction. Indeed looking and the complexity of our algorithm we can see that if the automaton has only one state and k stack symbols and the formula has size n_{1} and alternation depth n_{2} then we can solve the model checking problem in time O((k2^{n_{1}n_{2}})^{n_{2}}). Hence in polynomial time if n_{1}, n_{2} are fixed. In the case of alternation free formulas a similar complexity result was obtained in [2]. Remark: We conjecture that model checking is exponential also in the second parameter. That is, there exists a fixed pushdown process A such that the problem: “given a formula α, is α satisfied in the root of T_{A}” is DEXPTIME hard.

References

[1] J. Bergstra and J. Klop. Process theory based on bisimulation semantics. volume 354 of LNCS, 1988.

[2] O. Burkart and B. Steffen. Model checking for context-free processes. In CONCUR ’92, volume 630 of LNCS, pages 123–137, 1992.

[3] O. Burkart and B. Steffen. Pushdown processes: Parallel composition and model checking. In CONCUR ’94, volume 836 of LNCS, 1994.

[4] D. Caucal and Monfort. On the transition graphs of automata and grammars. In Graph-Theoretic Concepts in Computer Science, WG’90, volume 484 of LNCS, 1991.

[5] A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, 1981.

[6] S. Christiensen and H. Huttel. Deciding issues for infinite-state processes – a survey. Bulletin of EATCS, 51:156–166, October 1993.

[7] E. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In A Decade of Concurrency, volume 803 of LNCS, pages 124–175. Springer-Verlag, 1993.

[8] B. Courcelle. On the extension to infinite graphs of properties of finite ones. In preparation.

[9] E. A. Emerson, C. Jutla, and A. Sistla. On model-checking for fragments of μ-calculus. In CAV’93, volume 697 of LNCS, pages 385–396, 1993.

[10] E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy. In Proc. FOCS 91, 1991.

[11] E. A. Emerson and C. Lei. Efficient model checking in fragments of propositional mu-calculus. In First IEEE Symp. on Logic in Computer Science, pages 267–278, 1986.

[12] J. Esparza and A. Kiehn. On the model checking problem for branching time logics and basic parallel processes. In CAV ’95, volume 939 of LNCS, pages 353–366, 1995.

[13] N. Klarund. Progress measures, immediate determinacy and a subset construction for tree automata. In LICS ’92, pages 382–393, 1992.

[14] H. Lescow. On polynomial–size programs winning finite–state games. In CAV ’95, volume 939 of LNCS, pages 239–252, 1995.

[15] D. E. Long, A. Browne, E. M. Clarke, S. Jha, and W. R. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In CAV’94, volume 818 of LNCS, pages 338–350, 1994.

[16] A. W. Mostowski. Games with forbidden positions. Technical Report 78, University of Gdansk, 1991.

[17] D. Muller and P. Schupp. The theory of ends, pushdown automata and second-order logic. Theoretical Computer Science, 37:51–75, 1985.

[18] D. Niwiński and I. Walukiewicz. Games for μ-calculus. Theoretical Computer Science, 163:99–116, 1996.

[19] R. S. Streett and E. A. Emerson. An automata theoretic procedure for the propositional mu-calculus. Information and Computation, 81:249–264, 1989.

[20] W. Thomas. On the synthesis of strategies in infinite games. In STACS ’95, volume 900 of LNCS, pages 1–13, 1995.

[21] M. Y. Vardi. An automata-theoretic approach to fair realizability and synthesis. In CAV ’95, volume 939 of LNCS, pages 267–278, 1995.

[22] I. Walukiewicz. Monadic second order logic on tree-like structures. In STACS ’96, volume 1046 of LNCS, pages 401–414, 1996.

Recent Publications in the BRICS Report Series

RS-96-54 Igor Walukiewicz. Pushdown Processes: Games and Model Checking. December 1996. 31 pp. Appears in Alur and Henzinger, editors, 8th International Conference on Computer-Aided Veri�cation, CAV ’96 Proceedings, LNCS 1102, 1996, pages 62�74.

RS-96-53 Peter D. Mosses. Theory and Practice of Action Semantics. December 1996. 26 pp. Appears in Penczek and Szalas, editors, Mathematical Foundations of Computer Science: 21st International Symposium, MFCS ’96 Proceedings, LNCS 1113, 1996, pages 37�61.

RS-96-52 Claus Hintermeier, H� el� ene Kirchner, and Peter D. Mosses. Combining Algebraic and Set-Theoretic Speci�cations (Extended Version). December 1996. 26 pp. Appears in Haveraaen, Owe and Dahl, editors, Recent Trends in Data Type Speci�cation: 11th Workshop on Speci�cation of Abstract Data Types, joint with 8th COMPASS Workshop, Selected Papers, LNCS 1130, 1996, pages 255�274.

RS-96-51 Claus Hintermeier, H� el� ene Kirchner, and Peter D. Mosses. R^{n}- and G^{n}-Logics. December 1996. 19 pp. Appears in Gilles, Heering, Meinke and M� oller, editors, Higher-Order Algebra, Logic, and Term-Rewriting: 2nd International Workshop, HOA ’95 Proceedings, LNCS 1074, 1996, pages 90�108.

RS-96-50 Aleksandar Peke� c. Hypergraph Optimization Problems: Why is the Objective Function Linear? December 1996. 10 pp.

RS-96-49 Dan S. Andersen, Lars H. Pedersen, Hans H� uttel, and Josva Kleist. Objects, Types and Modal Logics. December 1996. 20 pp. To be presented at the 4th International Workshop on the Foundations of Object-Oriented, FOOL4, 1997.

RS-96-48 Aleksandar Peke� c. Scalings in Linear Programming: Necessary and Suf�cient Conditions for Invariance. December 1996. 28 pp.