On the Computational Complexity of Stackelberg Planning and Meta-Operator Verification

Venue: icaps-conference_org_ICAPS_2024_Conference
Published: 2023-12-06 18:20:27

Abstract: Stackelberg planning is a two-player variant of classical planning,
in which one player tries to ``sabotage'' the other player in achieving its
goal. This yields a bi-objective planning problem, which appears to be
computationally more challenging than the single-player case. But is this
actually true? All investigations so far focused on practical aspects, i.e.,
algorithms, and applications like cyber-security or very recently
for meta-operator verification in classical planning. 
We close this gap by conducting the first theoretical complexity analysis
of Stackelberg planning. We show that in general Stackelberg planning is no
harder than classical planning. Under a polynomial plan-length restriction,
however, Stackelberg planning is a level higher up in the polynomial complexity
hierarchy, suggesting that compilations into classical planning come with an
exponential plan-length increase. In attempts to identify tractable fragments
exploitable, e.g., for Stackelberg planning heuristic design, we further study
its complexity under various planning task restrictions, showing that
Stackelberg planning remains intractable where classical planning is not.
We finally inspect the complexity of the meta-operator verification, which in
particular gives rise to a new interpretation as the dual problem of Stackelberg
plan existence.

Main paper: 
 : 
 vestigations so far focused on practical aspects, i.e., algorithms, and applications like cyber-security or very recently for meta-operator verification in classical planning. We close this gap by conducting the first theoretical complexity analysis of Stackelberg planning. We show that in general Stackelberg planning is no harder than classical planning. Under a polynomial plan-length restriction, however, Stackelberg planning is a level higher up in the polynomial complexity hierarchy, suggesting that compilations into classical planning come with an exponential plan-length increase. In attempts toStackelberg planning (Speicher et al. 2018a ) is a two-player variant of classical planning, where one player (the leader) tries to "sabotage" the other player (the follower). The leader moves first, committing to an action sequence, which subsequently the follower needs to complete to a plan. The leader's objective is maximizing the follower's optimal plan cost while minimizing her own cost. This type of planning is useful for real-world adversarial settings commonly found in the cyber-security domain (Speicher et al. 2018b; Di Tizio et al. 2023) . Leader-follower search (Speicher et al. 2018a) is the so far only algorithm paradigm proposed for solving such tasks. In essence, it boils down to a search in the leader state space, solving for every visited leader state the follower's associated classical planning task. Given that exponentially such follower tasks must be solved in the worst case, one might wonder whether Stackelberg planning is in fact computationally more difficult than classical variant.Past work on Stackelberg planning however so far focused on algorithmic improvements rather than studying this question (Torralba et al. 2021; Sauer et al. 2023) .To close this gap, we present the first theoretical investigation of Stackelberg planning's complexity. We show that Stackelberg planning remains PSPACE-complete in general. However, Stackelberg planning with polynomial plan-length bounds is Σ P 2 -complete, contrasting the NP-completeness of the corresponding classical planning problem (Bylander 1994) . Assuming that the polynomial hierarchy does not collapse, this suggests that compilations of Stackelberg planning into classical planning need to come with an exponential increase in plan length.The analysis of tractable fragments has shown to be an important source for the development of domain-independent heuristic in classical planning (e.g., Hoffmann and Nebel 2001; Domshlak, Hoffmann, and Katz 2015) . With the vision of establishing a basis for the development of leaderfollower search heuristics, we analyze the complexity of Stackelberg planning under various syntactic restrictions. An overview of our results is given in Tab. 1.Lastly, we explore a problem related to Stackelberg planning: meta-operator (Pham and Torralba 2023) verification. Meta-operators are action-sequence wild cards, which can be instantiated freely for every state satisfying the operator's precondition as long as operator's effects match. Pham and Torralba have cast verifying whether a given action is a valid meta-operator as a Stackelberg planning task. We show that meta-operator verification PSPACE-complete and Π P 2complete under a polynomial plan-length restriction. This gives rise to a new interpretation of the meta-operator verification as the dual problem of Stackelberg planning.Note to Reviewers: This is a short-paper version without proofs. All proofs are in the supplement, which we will publish. Alternatively, if you so desire, we can include all proofs into a long version of paper (see alternative attached).Classical Planning We assume STRIPS notation (Fikes and Nilsson 1971) . A planning task is a tuple Π = ⟨V, A, I, G⟩ consisting of a set of propositional state variables (or facts) V , a set of actions A, an initial state I ⊆ V , and a goal G ⊆ V . For p ∈ V , p and ¬p are called literals. A state s is a subset of V , with the interpretation that all state variables not in s do not hold in s. Each action a ∈ A has a precondition pre(a), a conjunction of literals, an add effect (also called positive effect) add(a) ⊆ V , a delete effect (neg- manner. The cost of π is the sum of costs of its actions. π is called an s-plan if π is applicable in s and G ⊆ s π . π is an optimal s-plan if c(π) is minimal among all s-plans. An (optimal) plan for Π is an (optimal) I-plan. If there is no I-plan, we say that Π is unsolvable. Two decision problem formulations of classical planning are considered in the literature.PLANSAT is the problem of given a planning task Π, deciding whether there exists any plan for Π. PLANMIN asks, given in addition a (binary-encoded) cost bound B, whether there is a plan π for Π with cost c(π) ≤ B. Both problems 100 are known to be PSPACE-complete (Bylander 1994) .Stackelberg Planning A Stackelberg planning task (Spe- icher et al. 2018a) is a tuple Π LF = ⟨V, A L , A F , I, G F ⟩,where the set of actions is partitioned into one for each player. A leader plan is an action sequenceπ L = ⟨a L 1 , . . . , a L n ⟩ ∈ (A L ) n that is applicable in I. π L in- duces the follower task Π F (π L ) = ⟨V, A F , I π L , G F ⟩.An (optimal) follower response to π L is an (optimal) plan for Π F (π L ). We denote by c F (π L ) the cost of the optimal follower response to π L , defining cF (π L ) = ∞ if Π F (π L ) is unsolvable. Leader plans are compared via a dominance order between cost pairs where ⟨c L 1 , c F 1 ⟩ weakly dominates ⟨c L 2 , c F 2 ⟩ (⟨c L 1 , c F 1 ⟩ ⊑ ⟨c L 2 , c F 2 ⟩), if c L 1 ≤ c L 2 and c F 1 ≥ c F 2 . ⟨c L 1 , c F 1 ⟩ (strictly) dominates ⟨c L 2 , c F 2 ⟩ (⟨c L 1 , c F 1 ⟩ ⊏ ⟨c L 2 , c F 2 ⟩), if ⟨c L 1 , c F 1 ⟩ ⊑ ⟨c L 2 , c F 2 ⟩ and 115 ⟨c L 1 , c F 1 ⟩ ̸ = ⟨c L 2 , c F 2 ⟩. To simplify notation, we write π L 1 ⊏ π L 2 if ⟨c(π L 1 ), c F (π L 1 )⟩ ⊏ ⟨c(π L 2 ), c F (π L 2 )⟩.A leader plan π L is optimal if it is not dominated by any leader plan. Previous works have considered algorithms for computing the set of all optimal solutions, called the Pareto frontier.We distinguish between two decision-theoretic formulations of Stackelberg planning, akin to classical planning: Definition 1 (STACKELSAT). Given Π LF , STACKELSAT is the problem of deciding whether there is a leader plan π L that makes Π F (π L ) unsolvable. Definition 2 (STACKELMIN). Given Π LF , and two binary-encoded numbers B L , B F ∈ N 0 . STACKELMIN is the problem of deciding whether there is a leader planπ L with ⟨c(π L ), c F (π L )⟩ ⊑ ⟨B L , B F ⟩.Interpreting the leader's objective as rendering the follower's objective infeasible, the first definition directly mirrors the PLANSAT plan-existence decision problem. Similarly, the second definition mirrors PLANMIN in looking for solutions matching a given quantitative cost bound. It is worth mentioning that both decision problems are implicitly looking for only a single point in the Pareto frontier, whereas previous practical works dealt with algorithms computing this frontier entirely. In terms of computational complexity, this difference is however unimportant. In particular, answering even just a single STACKELMIN question does in fact subsume the computation of the entire Pareto frontierif the answer is no, one necessarily had to compare the given bounds to every element in the Pareto frontier.As in classical planning, STACKELSAT can be easily (with polynomial overhead) reduced to STACKELMIN: Proposition 1. STACKELSAT is polynomially reducible to STACKELMIN.Given that Stackelberg planning is a proper generalization of classical planning, the Stackelberg decision problems are guaranteed to be at least as hard as the respective classical planning decision problem. By applying the same proof idea as the Immerman-Szelepcsényi theorem (Szelepcsényi 1987; Immerman 1988) , we can prove that it is also no harder than classical planning in the general case:Theorem 1. STACKELSAT is PSPACE-complete. Theorem 2. STACKELMIN is PSPACE-complete.In spite of these results, algorithms for Stackelberg planning are significantly more complicated than their classical planning counterparts. In particular, the results raise the question of whether it is possible to leverage directly the classical planning methods for solving Stackelberg tasks via compilation. Polynomial compilations necessarily exist as per the theorems, yet, it is interesting to investigate which "side-effects" these might need to have. For example, it is possible any such compilation will have exponentially longer plan, rendering this approach infeasible in practice. In order to investigate these questions, we turn to a more fine granular analysis by considering the complexity under various previously studied syntactic classes of planning tasks.For classical planning, it is commonly known that restricting the length of the plans to be polynomial in the size of the planning task description, makes the decision problems become NP-complete. Definition 3 (Polynomial Stackelberg Decision). Given Π LF with non-0 action costs, and two binary-encoded numbers B L , B F ∈ N 0 that are bounded by some polynomialp ∈ O(ℓ k ) for ℓ = |V | + |A L | + |A F |. STACKELPOLY is the problem of deciding whether there is a leader plan π L such that ⟨c(π L ), c F (π L )⟩ ⊑ ⟨B L , B F ⟩.We restrict the action cost to be strictly positive, ensuring that considering leader and follower plans with polynomial length is sufficient to answer the decision problem. STACK-ELPOLY is harder than the corresponding classical problem. Theorem 3. STACKELPOLY is Σ P 2 -complete. This result strongly suggests that a compilation of Stackelberg planning into classical planning is in general not possible without an exponential blow-up of some kind. Namely, suppose it were possible to compile any Stackelberg planning task into classical planning in a way so that the size as well as the length of the plans of the classical planning task can be related polynomially to the size of the Stackelberg task. Suppose the plans of the Stackelberg task are polynomially bounded. Since polynomial length plan existence for classical planning is NP-complete, this would, together with our result, imply that NP = Σ P 2 , thus collapsing the polynomial hierarchy (Arora and Barak 2007, Theorem 5.6 ). As this is unlikely given out current knowledge, we hence surmise that such polynomial compilations do not exist. Or in other words: we know that an exponential blow-up in the computation is not avoidable in all circumstances.Stackelberg Planning under Bylander's Syntactic Restrictions Bylander (1994) studied the complexity of classical planning under various syntactic restrictions, drawing a concise borderline between planning's tractability and infeasibility. Bylander distinguishes between different planning task classes based on the number of action preconditions and effects, and the existence of negative preconditions or effects. Table 1 provides an overview of the main classes. Here, we take up his analysis and show that even for the classes where classical planning is tractable, Stackelberg may not be. We consider STACKELSAT and STACKELMIN in this order. n is defined similarly. We omit m (n) if m = ∞ (n = ∞). We consider only cases where the classical-planning decision problems are in NP. Stackelberg planning is PSPACE-hard when classical planning is.Plan Existence Bylander (1994) has shown that PLANSAT is already NPcomplete for tasks with actions that even have just a single precondition and a single effect. Here we show that the corresponding Stackelberg decision problem is even one step 230 above in the polynomial hierarchy: Bylander (1994) has shown that PLANSAT is polynomial if only positive preconditions and only a single effect per action are allowed. Even under these restrictive conditions, 235 STACKELSAT however still remains intractable: Theorem 5. STACKELSAT + 1 is NP-complete. Stackelberg plan-existence however becomes easy, when forbidding preconditions throughout. While this class of tasks seems to be trivial at first glance, optimal Stackelberg 240 planning actually remains intractable as we show below. Theorem 6. STACKELSAT 0 is polynomial.Theorem 4. STACKELSAT 1 +1 is Σ P 2 -complete.As per Proposition 1, optimal planning is in general at least as hard as deciding plan existence. All intractability results 245 shown for STACKELSAT carry over to STACKELMIN. As in all classes analyzed in the previous section, the consideration of polynomially length-bounded plans is sufficient for hardness, Σ P 2 yields a sharp upper bound to the complexity of STACKELMIN, as per Theorem 3. In particular:250 Corrolary 1. STACKELMIN 1 +1 is Σ P 2 -complete.The results for STACKELSAT only provide a lower bound to the complexity of STACKELMIN. This lower bound may be strict as demonstrated by Thm. 7 and 8: Theorem 7. STACKELMIN +1 1 is Σ P 2 -complete.Theorem 8. STACKELMIN 0 2 is Σ P 2 -complete. Optimal Stackelberg planning remains intractable even when all actions have no preconditions and may have only at most one effect. Theorem 9. STACKELMIN 0 1 is NP-complete in general, but 260 polynomial when additionally assuming unit cost.Pham and Torralba (2023) have recently leveraged Stackelberg planning for synthesizing meta-operators in classical planning. Meta-operators, like macro-actions (Fikes and 265 Nilsson 1971) , are artificial actions that aggregate the effect of action sequences, therewith introducing shortcuts in statespace search. Formally, we are given a classical planning task Π and an action σ that is not in Π's action set. σ is a meta-operator for Π if, for every state s |= pre(σ) that is reachable from I, there exists a sequence π of Π's actions such that s σ = s π . Whether a given σ is a meta-operator can be verified by solving a Stackelberg planning task.Here, we consider the question whether using an expressive and computationally difficult formalism like Stackelberg planning is actually necessary. For this, we determine the computational complexity of meta-operator synthesis and compare it to that of Stackelberg planning, and based on this analysis point out an interesting connection. Definition 5 (Meta-Operator Verification). Given Π and a Theorem 10. METAOPVER is PSPACE-complete.In other words, meta-operator verification could as well be compiled directly into a classical rather than a Stackelberg planning task. But how difficult or effective would such a compilation be? To shed light on this question, we again turn to a length bounded version of the problem. Definition 6 (Polynomial Meta-Operator Verification). Given Π with non-0 action costs, a fresh action σ, and two binary-encoded numbers B P , B M ∈ N 0 that are bounded by some polynomial p ∈ O(ℓ k ) for ℓ = |V | + |A|. poly-METAOPVER is the problem of deciding whether for all states s |= pre(σ) reachable from I with a cost of at most B P , there exists π with c(π) ≤ B M and s π = s σ .The parameters B P and B M define the perimeter around the initial state respectively the reached state under which the meta-operator conditions are to be verified. As for Stackelberg planning, we require that the cost of all actions is strictly positive, which together with the cost bounds ensures that the radius of the perimeter is polynomially bounded.Polynomial meta-operator verification too is on the second level of the polynomial hierarchy. We again point out that, under the assumption that the polynomial hierarchy does not collapse, this result shows that all classicalplanning encodings of meta-operator verification generally need to come with an exponential explosion of some kind.Theorem 11. polyMETAOPVER is Π P 2 -complete. Note that polyMETAOPVER is therefore in the cocomplexity-class of polynomial Stackelberg plan-existence, i.e., they belong to co-classes on the same level of the polynomial hierarchy. This may not be surprising given that meta-operator verification can indeed be seen as the dual of Stackelberg plan existence: while the latter asks for the existence of a (leader) action sequence where all induced (follower) action sequences satisfy some property, metaoperator verification swaps the quantifiers.We want to point out that the duality between METAOPVER and STACKELSAT can be exploited further, showing analogous results for Bylander's (1994) task classes. Contrary to Stackelberg planning, however, the identification of tractable fragments is less useful for metaoperator verification due to the lack of the monotonicity invariance of the meta-operator condition. An action being a meta-operator in a task abstraction does not imply that the action is a meta-operator in the original task, and vice versa. We hence do not further explore this analysis here.Stackelberg planning is related to conformant and conditional planning, extensions of classical planning by state and/or action outcome uncertainty. Under the restriction to deterministic actions, both can be seen as a special case of Stackelberg planning using the leader-reachable states as an encoding of the initial belief. With this interpretation, STACKELSAT is false iff the conditional planning task is solvable. If the follower is restricted to use the same plan independent of the leader actions, we would have a model for conformant planning.In the general case, conditional planning under partial observability and with conditional effects is EXPSPACE complete (Rintanen 2004 ). Both conformant and conditional planning have been investigated under the restriction to only polynomially long plans, like we did here. Rintanen (1999) showed that polynomially-length-bounded conditional STRIPS planning Π P 2 complete, the co-result to our Thm. 3. His hardness proof uses a similar proof idea as ours, with technical differences owed to the different planning formalism. Bonet (2010) studied conditional planning with non-determinstic actions, proving that polynomially bounded plan existence for conditional plans with at most k branching points is Σ P 2k+k -complete. Stackelberg planning corresponds k = 1, the difference between determinism and non-determinism causing the Σ P 2 vs. Σ P 4 complexity results. For conformant planning, Baral, Kreinovich, and Trejo (2000) showed that plan existence is Σ 2 P -complete, if conditional effects are allowed. Turner (2002) considered conditional and conformant planning, but his formalism supported arbitrary boolean formulae as conditions, making length-1 plan existence already NP-complete.No prior work on conformant/conditional planning considered any of Bylander's syntactical restrictions. Further, Stackelberg planning differs from conditional/conformant planning in using a more complex compact description of the "relevant" states through reachability.Stackelberg planning remains PSPACE-complete like classical planning in general, but is Σ P 2 complete under a polynomial plan-length bound. Hence, unless the polynomial hierarchy collapses at its first level, it is not possible to compile Stackelberg planning into classical planning without exponential blow-up. We showed that Stackelberg planning remains intractable even under various syntactical restrictions. Lastly, we have proven similar results for meta-operator verification, showing that it is PSPACE-complete in general and Π P 2 -complete for the polynomial plan-length bounded case, implying the same type of results for it. 
 
 Appendix:  


Decision: The paper analyzes the theoretical complexity of Stackelberg planning. Since Stackelberg planning is a limited special case of FOND planning, the scope of the contribution is somewhat narrow (mostly interesting for those working on this fragment). The ideas behind the complexity proofs are mostly known from the more limited/more general formalism. This means that the work is not too original but it could also be considered as positive, because for many readers it makes it very easy to follow the proofs (it's definitively better than coming up with some obscure new proof idea just for the sake of originality). The reviewers are happy with the clarity of the paper but some of them oppose the presentation of Stackelberg planning as generalization of classical planning (as was done in earlier publications on the topic). Instead it should be viewed as a special case of FOND planning and general adversarial planning problems. The authors promise that they will change the presentation accordingly in the camera-ready version but from the rebuttal, the corresponding reviewers are not convinced that they will be able to do this properly.

Pros:
- clarifies the previously unknown theoretical complexity of Stackelberg planning
- sound and clearly written

Cons:
- limited scope
- relationship to FOND and general adversarial planning not properly discussed
- Results are not surprising and the proofs are similar to the ones from the related formalisms.
- Reviewers see opportunities for more direct/elegant proofs (exploiting the relation to the more special and more general formalisms).
- In one proof the authors refer to the Immerman-Szelepcsenyi theorem but none of the reviewers sees how this is relevant there.

Reviews: review: strength_weakness: strength_weakness: There are two main weaknesses: the novelty is limited due to the similarity to earlier results on contingent and adversarial planning, and the results are not clearly positioned w.r.t. earlier works. Specifically, Stackelberg planning is included in non-deterministic contingent planning, with a simple reduction. One could also say that as a narrow special case of contingent and adversarial planning this subclass is somewhat unusual and not very well motivated. A general weakness would of course be that "Stackelberg planning" as a concept seems a bit superfluous and unnecessary, because "adversarial planner" already fully covers it. Presumably many techniques useful for the former could benefit also the latter, at least if suitably generalized.

The paper should position "Stackelberg planning" in the bigger picture of non-deterministic and adversarial planning already in the abstract and introduction. Saying that it is a "variant of classical planning" is misleading, as classical planning is by definition single-agent, and, instead, Stackelberg is a special case of general (non-deterministic) contingent planning and adversarial planning problems. (Any form of planning could similarly and misleadingly be characterized as "a variant of classical planning"!)

Both alternating Turing machines and Turing machines with oracles are closely related to 2-player games, and the two main results, the PSPACE-completeness of the unlimited Stackelberg game and the SigmaP2-completeness when the game plays are polynomially long, and immediate through PSPACE=PSPACE^PSPACE and SigmaP2=NP^NP. One could trivially generalize these to three rounds, with the first and the third round with the same player, and obtain problems complete for PSPACE=PSPACE^PSPACE^PSPACE and NP^NP^NP=SigmaP3. And so on.

The proof techniques are in many cases similar/same as some of the earlier work, which reduces the novelty value.

There is a simple reduction from Stackelberg planning to contingent planning: Take the leader actions as is but with an additional precondition LEADER (these are all deterministic actions, so classical PDDL) and include an additional action that cedes control to the follower by setting LEADER false. The follower actions are represented by a single non-deterministic action, with the precondition (and (NOT LEADER) (NOT TERMINATE)), and effect (ONEOF e1 e2 ... en (TERMINATE)), where each ei is of the form (when P E) where P is the precondition and E is the effect of one of the follower actions. Here TERMINATE is an auxiliary variable that is initially FALSE. LEADER is initially TRUE.
So first a sequence of leader actions are taken, then control is ceded to the follower, and after that the single action for the follower is iterated arbitrarily many times.
The goal formula is (and TERMINATE (NOT G)), where G is the original goal.
Now an instance is in STACKELSAT if and only if the non-deterministic planning problem has a plan that reaches goals with certainty (with a "strong cyclic" plan): the leader can take any action sequence, and after that the non-deterministic action is iterated one or more times, and no matter when termination gets non-deterministically chosen, one has to be in a state that falsifies G.

The paper is quite technical, and although possible applications are hinted at, in the paper there are none. The paper would be far more interesting if the results were used in a convincing application that was thoroughly fleshed out.

On line 52, SigmaP2-completeness only implies that there is no guaranteed polynomial mapping from your problem with polynomial length restrictions to classical planning with polynomial length restrictions. Even if such mappings cannot always be polynomial, there are certainly cases where polynomiality is easily achieved. One example is when the follower can only take an action sequence with a constant bound, so that you could then reduce the follower to a new goal, and then use classical planning as is. Even without a constant bound on the follower's plans, backward chaining could under some syntactic or other restrictions generate a simple polynomial size goal. 

In lines 331-335 it is claimed that Conformant and Contingent planning are *special* *cases* of Stackelberg planning if actions are deterministic. First, conditional planning has never been seriously considered with full observability and deterministic actions only, so there is hardly any prior works that would be so restricted that they could be embedded in Stackelberg planning. One either has non-deterministic actions, or partial observability. Second, conformant planning even with deterministic actions is far harder than Stackelberg planning, and hence the innocent looking condition ""the follower is restricted to use the same plan independent of the leader actions" violates the basic assumptions of Stackelberg planning, and is hence highly misleading, as it in no way makes conformant planning a special case of Stackelberg planning.
In fact, Stackelberg planning can be easily embedded in FOND planning (contingent planning with full observability and non-deterministic actions), as pointed out earlier, and this embedding works both for STACKELSAT and STACKELOPT, contrarary to what the author claims in the rebuttal.

Please correct Sigma2P to SigmaP2 on line 357.

Line 360: Arbitrary Boolean formulas as preconditions does not change the complexity of contingent, conformant or classical planning. Please clarify what you refer to with "conditions".
questions: questions: Q1 Why do you say that Stackelberg planning is a "variant of classical planning"? Wouldn't it be far more accurate to say that it is a special case of contingent and game-theoretic planning problems? In adversarial 2-agent planning there are two agents that alternate with their moves. In your problem one agent makes multiple moves, and then the other agent makes multiple moves.

Q2 What do you mean by "Stackelberg planning differs from conditional/conformant planning in using a more complex compact description of the 'relevant' states through reachability"?
strength_weakness: strength_weakness: Since the paper's primary contribution is theorems describing the theoretical complexity results, I suggest that the proofs of essential theorems be included in the main paper.
questions: questions: -
strength_weakness: strength_weakness: I have one larger issue with the paper (novelty and connection to related work) and some more technical problems. The main problem is that Stackelberg planning is naturally seen as a simplification of FOND planning (almost any two-player game on graphs could be viewed as such) but this is never even acknowledged. Overall, I still recommend acceptance as a short paper, because it can be useful to have a concrete reference for the proofs and theorems, but I strongly recommend a revision to make it clearer that several of these results/proofs are related to previously studied and well-established concepts in planning.  

In more detail: 

Several of the proofs and results are adaptations/simplifications of canonical proofs in planning and theoretical computer science. This is OK, but this could be acknowledged more clearly. For example, alternating Turing Machines and representation of QBF are used over and over in planning results (some of which you cited), and making this connection would make the results much more straightforward, particularly in a dense short paper where any hint will help the reader. Moreover, Stackelbeg planning is just a simplified case of two-player games, but you never put it in this light. You always mention it as a somehow "practically harder" version of classical planning, but it is much more natural to think of it as a simplification of probabilistic/non-deterministic or adversarial planning -- which are never mentioned. In particular, I think the relation to non-deterministic planning *must* be discussed in the paper. Putting it forcefully, one can think of Stackelberg planning as a very simplified version of FOND planning. 

Talking about non-deterministic planning, the seminal paper by Littman [1997] gives one more example of the relation to previous work: Thm 1 and Thm 2 of his paper present ideas that are very similar to your proofs. The proofs can also be modified to show that Stackelberg planning is a simpler case of non-deterministic/probabilistic planning. We reduce Stackelberg planning to non-deterministic planning as follows: The new actions will be the leader actions plus two extra actions CHANGE-TURN and FOLLOWERS-ACTION. Add a propositional variable LEADERS-TURN to the precondition of all actions that were originally from the leader (and make LEADERS-TURN true in the initial state). Action CHANGE-TURN has precondition LEADERS-TURN, and effect (not LEADERS-TURN and FOLLOWERS-TURN). Action FOLLOWERS-ACTION has precondition (FOLLOWERS-TURNS and not TERMINATED), and a non-deterministic effect (oneof (not FOLLOWERS-TURN), E_1, E_2, ..., E_n) where E_i is is the conditional effect (when Pre_i Eff_i) where Pre_i and Eff_i are the precondition and effect of the i-th follower action. The goal is ((not LEADERS-TURN) and (not FOLLOWERS-TURN) and (not GOAL)), where GOAL is the original goal of the follower. The original Stackelberg task is only satisfiable if the non-deterministic task reaches the new goal with certainty. Note that the new goal represents that it is not the turn of any of the players (so in some sense they both "passed") but the original goal is still not reached. You can use the same idea for probabilistic planning using arbitrary non-zero probabilities for the effects.

A technical note: The proof of Theorem 1 must be rewritten. You mention using Immerman-Szelepcsenyi but it needs more details, and I believe you mixed the Immerman-Szelepcsenyi theorem with the Savitch theorem. The key here is that your algorithm guesses a plan for the leader, and then checks that no follower plan exists. In other words, the second step checks *unsolvability* instead of solvability. Alone, Savitch's algorithm in the second part (follower's plan) will give you nothing, because it can answer YES in poly-space (i.e., a plan exists), not NO (i.e., task is unsolvable). But here is where Immerman-Szelepcsenyi comes into play -- which shows that coPSPACE = PSPACE -- and you can indeed decide unsolvability in PSPACE.

Last, I was a bit confused by the discussion about meta-operators. The connection to Stackelberg planning is clear, but one key difference is that in METAOPVER \sigma is given. There is nothing analogous given to STACKELSAT. This difference should also be pointed out so it just not sound like it is direct to complement one for the other. Right now it reads as if METAOPVER is the complement of STACKELSAT, as UNSAT is the complement of SAT, for example.

Minor:
In the paper:
- You frequently use the word "compilation" instead of "reduction". I think in almost every case you want to say "reduction", which assumes that the solution sizes are polynomially preserved, while "compilation" does not.
- Starting from Thm 4, there is a mismatch in the numbering between the paper and the appendix.
- "As per Proposition 1, optimal planning is in general at least as hard as deciding plan existence" -> say "optimal *Stackelberg* planning", as this is not the case in general for other flavors of planning (e.g., deterministic planning using schematic actions and other fragments for which plan existence in EXPSPACE-complete or beyond)
-  "STACKELSAT is false" -> this should be rewritten
- "\Sigma^2_P" -> "\Sigma^P_2"
- Not sure what you mean by the last sentence of the related work section.

In the appendix:
- "alternating Turing Machine" -> "alternating *polynomial-time* Turing Machine"
- Theorem 4 does not exist.
- "Corrolary" -> "Corollary"
- In the proof of Thm 12, the notation for s^P[[\sigma]] used the wrong latex symbol.
questions: questions: I have no questions.