Pod-Deployability in Kubernetes with Inter-Pod Affinity Constraints is PSPACE-Complete

Pod-Deployability in Kubernetes with Inter-Pod Affinity Constraints is PSPACE-Complete Saverio Giallorenzo Università di Bologna, Italy INRIA, Sophia-Antipolis, France

Jacopo Mauro University of Southern Denmark, Denmark

Gianluigi Zavattaro

arXiv:2608.19822v1 [cs.CC] 20 Aug 2026

Università di Bologna, Italy INRIA, Sophia-Antipolis, France

Abstract Kubernetes is the de-facto platform for container orchestration. Its scheduler combines resource capacities with label-based affinity and anti-affinity rules, and the interaction of these features can make the eventual placement of a pod. In this paper, we study the pod-deployability problem: given an initial cluster, a pod type, and a designated node, does some legal sequence of pod deployments and deletions cover the target pair? We give three complexity results. First, when dynamic constraints contain no affinity (anti-affinity is allowed), pod-deployability is decidable in polynomial time. Second, required affinity together with required anti-affinity makes the problem PSPACE-complete. Third, required affinity alone is already enough for PSPACE-completeness on a single node with one scalar capacity. The lower bounds encode, respectively, 1-safe Petri-net coverability and bounded black pebbling. These results isolate two independent sources of state-space complexity in Kubernetes scheduling: logical exclusion and resource-bounded prerequisite management. 2012 ACM Subject Classification Theory of computation → Problems, reductions and completeness; Computer systems organization → Cloud computing Keywords and phrases Kubernetes, scheduling, pod affinity, anti-affinity, coverability, PSPACE Digital Object Identifier 10.4230/LIPIcs.XXXX.2027.XX

© Saverio Giallorenzo, Jacopo Mauro, and Gianluigi Zavattaro; licensed under Creative Commons License CC-BY 4.0 XXXX. Editors: John Q. Open and Joan R. Access; Article No. XX; pp. XX:1–XX:23 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

XX:2

Kubernetes Pod-Deployability is PSPACE-Complete

1

Introduction

Kubernetes [18] is the de-facto standard platform for orchestrating containerized applications within a cluster of machines [3]—around 82% of container-using organizations worldwide adopt it and major cloud providers (like AWS, Google, and Azure) offer it as a managed service [5, 11]. Crucial terms in Kubernetes’ lingo are nodes and pods. The former are the machines participating in a cluster. Each node contributes computing resources, such as CPU and memory, and may carry labels describing properties such as its location, hardware, or security domain. Pods are the smallest unit managed by Kubernetes and a pod groups one or more containers placed on the same node and share runtime resources. At the heart of Kubernetes lies its scheduler. When the platform receives the command to deploy a given workload, it creates one or more pods with no assigned node, which triggers the scheduler to evaluate the cluster and select a suitable node for each one to run on. A node is suitable only if it satisfies all the pod’s hard scheduling constraints. These constraints include, among others, sufficient resource capacity, requirements on node labels, and relationships with pods that are already running. In particular, inter-pod affinity can require a pod to be placed close to other pods, while inter-pod anti-affinity can require separation from them— where “closeness” is determined by a topology domain, e.g., ranging from single nodes to whole availability zones. Although Kuberbetes evaluates each scheduling constraint locally at each pod placement, their combined effect over a sequence of pod deployments and deletions is not local. In this paper, we focus on the decidability and complexity of a basic question: can a pod of type t ever be deployed on node n? Answering this question is practically important, for instance, a positive answer may expose an unintended crossing of a security boundary—e.g., a pod processing private data might be deployable on a node belonging to a public or otherwise untrusted worker pool. We call this decision problem pod-deployability. Formally, we frame the problem as the coverability of a type-node coordinate and ask whether some reachable cluster configuration contains at least one instance of the target type-node. Contributions. We formalise the Kubernetes scheduling semantics (Section 2) and use it to give three main results that expose a sharp complexity boundary. 1. With anti-affinity and no capacities nor affinity, pod-deployability reduces to one feasibility check in the empty configuration and is decidable in time polynomial in the number of nodes and the total encoding length of the scheduling constraints (Section 4). 2. With affinity and anti-affinity and no capacities, pod-deployability is PSPACE-complete. The proof uses a four-phase protocol to simulate 1-safe Petri-net transitions (Section 5). 3. With affinity alone, pod-deployability is PSPACE-complete already for one node and one scalar capacity—reduction from black-pebbling under a matching space bound. (Section 6). 4. We mechanized all reductions and formally verified them in Lean, establishing a machinechecked correspondence between pod-deployability and the corresponding hardness sources. Structure of the paper. In Section 2, we formalize Kubernetes’ scheduler semantics. Then, we formulate pod-deployability as a coverability problem in Section 3, proving that it is in PSPACE. We study the polynomial fragment without affinity in Section 4 and present the two PSPACEcompleteness results in Sections 5 and 6. We discuss related work and conclude in Section 7. The appendix includes detailed proofs of all results and the encodings of the hardness proofs, which we formalised in Lean and make available at https://doi.org/10.5281/zenodo.22025656.

Disclosure of AI Usage. We used AI-based tools to assist in preparing this paper. Specifically, such tools helped refine the clarity and readability of the prose, and assisted in proving theorems and refactoring code within the Lean formalization. We reviewed and independently verified all AI-assisted output. We take full responsibility for the correctness of the results of the paper.

S. Giallorenzo, J. Mauro, and G. Zavattaro

2

XX:3

Kubernetes Scheduling Made Formal

We present Kubernetes and formalize its standard pod scheduling policy. Kubernetes is a container orchestration platform that manages applications deployed as collections of pods. A Kubernetes cluster consists of a set of worker nodes together with a control plane responsible for maintaining the desired cluster state. Among its components, the Kubernetes scheduler determines where newly created pods should run. When a pod is created without a node assignment, it remains pending until the scheduler selects a suitable node and records a binding [15, 17]. Scheduling proceeds conceptually in two main stages. During filtering, nodes that violate mandatory scheduling constraints are discarded. During scoring, the remaining nodes are ranked according to preferences such as resource usage or preferred affinity. After a binding is committed, the kubelet on the selected node starts and supervises the pod’s containers. Since this work is concerned with the feasibility of placements—rather than with the scheduler’s choice among feasible nodes—we model only hard scheduling constraints. Indeed, soft constraints affect which feasible node is preferred but cannot make an otherwise infeasible placement legal. We also abstract from implementation details such as scheduler concurrency, internal caches, transient API failures, preemption, and binding plugins. The resulting model retains the cluster information relevant to hard placement feasibility and represents successful scheduling nondeterministically: any node satisfying all hard constraints may be selected.

2.1

Pods, Nodes, and Cluster Configurations

We introduce the formal model alongside the Kubernetes objects that it represents. Let T , N , and R be finite sets of pod types, nodes, and resource dimensions, respectively. Let also LabelKey and LabelValue be a set of labels and corresponding values, respectively. A pod type represents the scheduling-relevant information shared by instances created from the same pod template. In particular, each t ∈ T has a label map λT (t) : LabelKey ⇀ LabelValue and a resource-request vector res(t) ∈ NR . Similarly, each node n ∈ N has a label map λN (n) : LabelKey ⇀ LabelValue and an allocatable capacity vector C(n) ∈ NR . The scheduler reasons about pod resource requests, and resources include dimensions like CPU and memory. We denote which pods instances run on which cluster nodes as σ : T ×N −→ N, where σ(t,n) is the number of running instances of type t on node n. Therefore, the total resources requested on a node n in configuration σ are X used(σ,n) = σ(t,n) res(t). t∈T

Consequently, placing an additional instance of type t on n respects the node’s capacity when used(σ,n)+res(t) ≤ C(n), with component-wise vector addition and comparison. We write 0 for the empty configuration, defined by 0(t,n) = 0 for every t ∈ T , n ∈ N . We further write σ + (t,n) for the configuration obtained by incrementing σ(t,n) by one, and σ−(t,n) for the corresponding decrement. Kubernetes uses labels and selectors to express relationships between pods. A selector s is a predicate over pod labels. We write JsK = {t ∈ T | λT (t) satisfies s}

XXXX 2027

XX:4

Kubernetes Pod-Deployability is PSPACE-Complete

for the set of pod types matched by s. Scheduling constraints can also refer to the topology of the cluster. Kubernetes represents topology through node labels. A topology key τ , e.g., the hostname or availability zone of a node, partitions the nodes according to the corresponding label value. For a node n, we define its topology domain with respect to τ by Dτ (n) = { m ∈ N | λN (m)(τ ) = λN (n)(τ ) }. Informally, we can view Dτ (n) as the n-induced domain under topology key τ . Thus, if τ denotes the hostname label, Dτ (n) typically contains only n, while if τ denotes a zone, Dτ (n) contains all the nodes in n’s zone. For well-formedness, we assume that all nodes have a value for every topology key, so that λN (m)(τ ) is always defined.

2.2

Static Constraints

Kubernetes enforces several hard constraints that determine whether a node is a valid candidate for a pod independently of the current cluster configuration: i) node affinity constraints use labels to restrict a pod to nodes satisfying specified label requirements (e.g., a pod may require a node labelled as belonging to a particular zone); ii) taints and tolerations allow nodes to repel pods that do not explicitly tolerate particular node conditions or administrative restrictions (e.g., a node reserved for a particular workload may be tainted so that only pods explicitly configured to tolerate that taint can be placed on it). We collect these configuration-independent checks into the predicate StaticOK(t,n). For a pod type t and a candidate node n, evaluating StaticOK(t,n) amounts to matching the label requirements and tolerations of t against the labels and taints of n, and takes time linear in the total number of these label requirements, tolerations, labels, and taints. Other Scheduling Constraints. While minimal, the combination of resource and pod-node constraints can capture additional ad-hoc constraints enforced by Kubernetes, for instance, the availability of persistent volumes and host network ports [16]. Regarding volumes, we can represent volume-related placement constraints by combining StaticOK(t, n) with resource capacities, which captures both compatibility requirements between a pod and the volumes available on a candidate node and quantitative restrictions, like the available storage or number of volume slots. Regarding network ports, we can model port-related placement constraints using resource capacities. In particular, we can capture a port as a distinct resource with unit capacity on each node, while a pod requesting that port consumes one unit of the corresponding resource. The capacity constraint then ensures that no two pods scheduled on the same node can claim the same port.

2.3

Inter-Pod Affinity and Anti-Affinity Constraints

Inter-pod affinity and anti-affinity constrain a pod according to the location of other pods. Required affinity permits a placement only when a pod matching a given selector (s) is already present in a specified topology domain (determined by τ ). Required anti-affinity has the opposite effect: it prevents the incoming pod from being placed in a domain containing a matching pod. We represent an affinity or anti-affinity term by a pair (s,τ ), where s is a pod selector and τ a topology key. For each pod type t, let A+ (t) and A− (t) denote its sets of required affinity and required anti-affinity terms, respectively. We define predicate present to determine whether a matching pod is present in a given n-induced, τ -determined domain presentσ (s,τ,n) ⇐⇒ ∃u ∈ JsK ∃m ∈ Dτ (n) : σ(u,m) > 0.

S. Giallorenzo, J. Mauro, and G. Zavattaro

XX:5

The required affinity and anti-affinity constraints of an incoming pod of type t on node n in configuration σ are satisfied when predicate AffinityOKσ (t,n) holds. required anti-affinity

z AffinityOKσ (t,n) ⇐⇒

^

required affinity

}| { ¬presentσ (s,τ,n)

(s,τ )∈A− (t)

z ∧

^

}| { presentσ (s,τ,n)

(s,τ )∈A+ (t) t∈JsK∨∃u,m:u∈JsK∧σ(u,m)>0 /

In particular, the definition captures the exception for self-affinity that avoids the bootstrap problem for scheduling self-affine pods, by allowing the first such pod to be scheduled when no matching pod is yet present in the cluster [14]. Formally, for an affinity term (s,τ ) such that the incoming type t itself matches the selector, i.e., t ∈ JsK, the term is not imposed when no pod matching s is present anywhere in the cluster. In this way, the first pod of a self-affine group can be scheduled despite the absence of an existing affinity witness. Once a pod matching s exists in the cluster, the exception no longer applies and the usual affinity condition is enforced: a matching pod must be present in the topology domain Dτ (n) of the candidate node. Thus, the cluster-wide test is used only to determine whether the self-affinity bootstrap exception applies, whereas presentσ (s,τ,n) enforces the ordinary topology-local affinity requirement.

2.4

Topology-Spread Constraints

Topology-spread constraints provide another mechanism for relating the placement of an incoming pod to the distribution of existing pods, and specify how to spread replicas across topology domains such as nodes, zones, or other administrator-defined domains. In particular, a topology-spread constraint restricts pod placement by rejecting candidate nodes that would cause exceeding the permitted skew between topology domains. We represent a hard topology-spread constraint by h = (s,τ,k,ℓ,E), where: s is the selector identifying the pods whose distribution is counted; τ is the topology key; k ≥ 1 is the maximum permitted skew; ℓ ≥ 1 is the minimum number of eligible topology domains; and E ⊆ N is the set of eligible nodes. For a topology value v, define X X countσ (s,τ,v,E) = σ(u,m). u∈JsK

m∈E λN (m)(τ )=v

This is the number of resident pods matching s in the eligible part of the τ -v topology domain. Given a topology-spread constraint h = (s,τ,k,ℓ,E), the skew calculation uses the minimum number of matching pods among eligible domains defined as follows:   min countσ (s,τ,v,E), if |{λN (n)(τ ) | n ∈ E}| ≥ ℓ, gminσ (h) = v∈{λN (n)(τ )|n∈E}  0, otherwise. Thus, when at least ℓ eligible domains exist, the global minimum is the minimum number of matching pods among them. When fewer than ℓ domains exist, Kubernetes treats the global minimum as zero. Whether the incoming pod contributes to the count depends on whether its type matches the selector. Define ( 1, t ∈ JsK, δ(t,s) = 0, t ∈ / JsK.

XXXX 2027

XX:6

Kubernetes Pod-Deployability is PSPACE-Complete

Placing a pod of type t on node n satisfies the topology-spread constraint h = (s,τ,k,ℓ,E) exactly when SpreadOK(h,t,n,σ) ⇐⇒ n ∈ E ∧countσ (s,τ,λN (n)(τ ),E)+δ(t,s)−gminσ (h) ≤ k. For example, suppose that two eligible zones a and b contain, respectively, two and one pods matching s, and that the maximum skew is k = 1. If the incoming pod also matches s, the global minimum is one. Placing the pod in a would produce 2+1−1 = 2 > 1 and is therefore rejected. Placing it in b, however, produces 1+1−1 = 1, which satisfies the constraint. For each pod type t, let Spread(t) denote its set of hard topology-spread constraints.

2.5

Hard Scheduling Feasibility

We can now combine the preceding Kubernetes constraints into a single predicate describing the filtering stage relevant to our analysis. ▶ Definition 1 (Feasible deployment). A pod of type t is feasible on node n in configuration σ if Hard(t,n,σ) holds, such that Hard(t,n,σ) ⇐⇒ used(σ,n)+res(t) ≤ C(n) ∧ StaticOK(t,n) ∧ AffinityOK(t,n,σ) ^ ∧ SpreadOK(h,t,n,σ). h∈Spread(t)

The four components of this predicate correspond to the aspects of hard Kubernetes scheduling represented by our model: resource capacity, static node compatibility, required inter-pod affinity and anti-affinity, and hard topology spread. We conclude with an observation that will be useful for investigating the complexity of the pod-deployability problem. Under the standard explicit representation of nodes, pod types, labels, resources, selectors, and scheduling constraints, evaluating Hard(t,n,σ) takes polynomial time in the size of the cluster representation. In fact, it is sufficient to check the component-wise inequality used(σ,n) + res(t) ≤ C(n), check StaticOK(t,n) that we consider encoded in the cluster representation, compute presentσ (s,τ,n) to check AffinityOK(t,n,σ) (in case of selfaffinity, we also check whether there is already a pod deployed), and checks n ∈ Eh for every encoded constraint h ∈ Spread(t). Note that comparison of binary-encoded integers (necessary to check resource bounds and spread constraints) is polynomial in their bit length, so capacities may be numerically exponential in the size of their encoding without affecting the polynomial bound.

2.6

Scheduling as a Transition System

The predicate in Definition 1 describes whether a single placement is legal. To reason about sequences of scheduling decisions, deployments, and deletions, we model the cluster as a transition system whose states are configurations. A successful scheduling operation adds one pod instance to one node. Since we abstract away the scoring stage that introduces only soft constraints, the choice among feasible nodes is nondeterministic: any node satisfying Hard may be selected. We also permit deletion of a running pod, which abstracts how pods may disappear from a Kubernetes cluster—at the level of our model, the precise operational cause for a deletion, like scale-downs, evictions, and terminations, is irrelevant.

S. Giallorenzo, J. Mauro, and G. Zavattaro

XX:7

The transition relation is generated by the following two rules: Hard(t,n,σ) Deploy σ −→ σ+(t,n)

σ(t,n) > 0 Delete. σ −→ σ−(t,n)

The Deploy rule abstracts filtering, selection, and successful binding. The rule states only that the placement is permitted by all hard constraints represented in the model. An important consequence of this semantics is that scheduling feasibility is not preserved under later deletions. Indeed, affinity and topology-spread constraints are evaluated at a pod’s Deployment and removing a pod can invalidate the condition that enabled the placement. Dually, scheduling unfeasibility does not persist under later deletions. For example, consider a single node with a resource capacity of two and three pod types a, b, and c, each requesting one unit of the resource. Suppose that b requires affinity to a, while c requires affinity to b. Starting from the empty configuration, the sequence 0 −→ {a} −→ {a,b} −→ {b} −→ {b,c} is legal: first deploy a, then use a as the affinity witness for b; delete a; and finally use b as the witness for c. At no point can all three pods coexist because the node has capacity two. Nevertheless, the temporary presence of a enables b, which remains after a is deleted and can subsequently enable c. Thus, the set of pods present in the final configuration does not contain all the intermediate witnesses needed to construct it. This distinction between currently satisfied constraints and constraints satisfied at deployment time is central to the reachability behavior of the model. In particular, this deploy-remove mechanism underlies the hardness proofs in Sections 5 and 6.

3

Pod-Deployability

In this section, we formulate the verification problem studied throughout the paper. We focus on the basic question of whether one pod type can ever be deployed on one designated node. This property is sufficient to express, for example, whether a sensitive workload may cross a placement boundary and run on an untrusted node. More elaborate properties could require several pods to be present simultaneously or could prescribe an entire final cluster configuration. We leave such variants aside and study the simplest node-specific deployment question, which already exhibits the complexity boundaries developed in the following sections. ▶ Definition 2 (Pod-deployability). Let σ0 be an initial configuration, t⋆ ∈ T a target pod type, and n⋆ ∈ N a target node. The target pod is deployable on n⋆ from σ0 if Deploy(σ0 ,t⋆ ,n⋆ ) holds, where Deploy(σ0 ,t⋆ ,n⋆ ) ⇐⇒ ∃σ : σ0 −→∗ σ∧σ(t⋆ ,n⋆ ) ≥ 1 where −→∗ is the reflexive and transitive closure of −→. Deployability asks whether this condition holds.

The decision problem Pod-

The definition requires only that the final configuration contains at least one instance of t⋆ on n⋆ . It imposes no condition on the other pods or nodes. Pod-deployability is therefore a coverability problem: the target specifies a lower bound on one coordinate of the configuration. Although an execution witnessing pod-deployability may be exponentially long, the problem can be solved in polynomial space whenever every configuration has a polynomial-size encoding. We make the required boundedness assumption explicit.

XXXX 2027

XX:8

Kubernetes Pod-Deployability is PSPACE-Complete

▶ Definition 3 (Capacity-bounded instance). An instance is capacity-bounded if, for every pod type t ∈ T and node n ∈ N , there exists a resource dimension r ∈ R such that res(t)(r) > 0. The capacity constraint gives the finite bound   C(n)(r) Bt,n = min r∈R res(t)(r) res(t)(r)>0

on the number of simultaneously running instances of type t on node n. This is a natural assumption for Kubernetes deployments. Every running pod consumes some finite node resource, even when its manifest omits explicit CPU or memory requests: it requires runtime and bookkeeping resources and is subject to node-level limits, such as the maximum number of pods supported by a node. The assumption does not bound how many instances may be created over the course of an execution. A controller may repeatedly create, delete, and recreate pods. It bounds only the number of instances represented in one configuration. The numerical value of Bt,n may be exponential in the input length, but its binary representation is polynomial in that length. This implies that a configuration can be stored in polynomial space. For each pair (t,n) ∈ T ×N , the capacity constraint implies 0 ≤ σ(t,n) ≤ Bt,n . We store σ(t,n) as a binary counter. This counter requires ⌈log2 (Bt,n +1)⌉ bits. Since capacities and requests are binary encoded, this number is polynomial in the input length. There are |T |·|N | counters, and therefore the complete configuration has a polynomial-size representation. The number of possible configurations is finite and bounded by YY K= (Bt,n +1). t∈T n∈N

Although K may be exponential, its binary length is polynomial in the input length. If a target configuration is reachable, then it is reachable by a path of length less than K that does not repeat any configuration. Hence, the deployability of a pod can be checked by a nondeterministic algorithm which guesses at most K transitions. Notice that this algorithm is in NPSPACE because it has to store the current configuration and the counter of the already guessed transitions. Thanks to Savitch’s theorem [12], stating that NPSPACE = PSPACE, we can conclude that Pod-Deployability is in PSPACE for capacity-bounded instances. ▶ Theorem 4 (Polynomial-space pod-deployability). Pod-Deployability for capacity-bounded instances is in PSPACE.

4

A Polynomial Fragment without Affinity

We now show that it is sufficient to remove affinity to obtain a fragment where PodDeployability can be solved in polynomial time. Formally, we focus on AAS be the fragment where pods do not declare affinity constraints, i.e., : A+ (t) = ∅ for every t ∈ T . Note that anti-affinity constraints are admitted, i.e., it is possible to have t ∈ T such that A− (t) ̸= ∅. The key property of AAS is that if a pod of type t is feasible on node n in a configuration σ, then it is feasible also in the empty configuration 0. According to Definition 1, t is feasible on node n in a configuration σ if StaticOK(t,n), V used(σ, n) + res(t) ≤ C(n), AffinityOK(t, n, σ), and h∈Spread(t) SpreadOK(h, t, n, σ). StaticOK(t,n) is independent of the current configuration. The inequation used(σ,n)+res(t) ≤ C(n) implies res(t) ≤ C(n), because used(σ,n) is a nonnegative vector. AffinityOK(t,n,0) holds because affinity requirements are not admitted and anti-affinity requirements are vacuously V satisfied in the empty configuration. Moreover, h∈Spread(t) SpreadOK(h, t, n, σ) implies

S. Giallorenzo, J. Mauro, and G. Zavattaro

XX:9

V

h∈Spread(t) SpreadOK(h,t,n,0) because for every topology-spread constraint h = (s,τ,k,ℓ,E), SpreadOK(h,t,n,σ) implies n ∈ E, gmin0 (h) = 0, and in the configuration 0 the spread inequality reduces to 0+δ(t,s)−0 ≤ k which holds because δ(t,s) ≤ 1 and k ≥ 1. This implies that a pod of type t is feasible on node n also in the empty configuration 0. The above key property of AAS allows us to check Deploy(σ0 ,t⋆ ,n⋆ ) simply by verifying whether node n⋆ already hosts a pod of type t⋆ in the initial configuration σ0 or Hard(t⋆ ,n⋆ ,0) holds. In fact, if the pod is deployed after a sequence of transitions we have that Hard(t⋆ ,n⋆ ,σ) holds for the configuration σ in which the pod is deployed; as observed above, this implies Hard(t⋆ ,n⋆ ,0). Conversely, if Hard(t⋆ ,n⋆ ,0) holds, from the initial configuration σ0 we can consider a sequence of delete transitions that remove all the pods, thus reaching the empty configuration 0, from which a pod of type t⋆ can be deployed on node n⋆ . The above verification procedure, i.e., check the initial configuration or Hard(t⋆ ,n⋆ ,0), takes polynomial time (see the discussion at the end of Section 2.5); hence Pod-Deployability in AAS can be verified in polynomial time.

▶ Theorem 5 (Polynomial affinity-free pod-deployability). Pod-Deployability in AAS is decidable in polynomial time.

5

PSPACE with Affinity and Anti-Affinity

We now isolate the expressive power of inter-pod affinity constraints. In this section, we consider a capacity-free fragment in which the only active scheduling constraints are required inter-pod affinity and anti-affinity. All resource requests are zero, all static node filters are true, and no topology-spread constraints are present. The reduction uses a single node, and therefore all affinity and anti-affinity terms use the hostname topology. We show that this fragment is already PSPACE-complete by encoding coverability of 1-safe Petri nets. We first recall the source problem, then present the encoding and its intuition and argue that it is polynomial. 1-safe Petri nets. A 1-safe net is a Petri net in which every reachable marking contains at most one token in each place. Formally, a 1-safe net is a tuple P = (P,T,Pre,Post,M0 ), where P and T are finite sets of places and transitions. For each transition a ∈ T , the sets Pre(a), Post(a) ⊆ P are its input and output places. The initial marking M0 ⊆ P indicates places that initially contain one token. In 1-safe nets, every reachable marking contains at most one token in each place and can therefore be identified with the set of places M ⊆ P containing a token. A transition a is enabled at M when Pre(a) ⊆ M. Firing a consumes the tokens in its input places a and produces tokens in its output places: M − → (M \Pre(a))∪Post(a). The source problem used in the reduction is goal coverability: given a 1-safe Petri net and a distinguished place g ∈ P , determine whether some reachable marking contains g. This problem is PSPACE-complete [4].1 Encoding. Let P = (P,T,Pre,Post,M0 ) be a 1-safe Petri net with distinguished goal place g. We construct a Kubernetes instance consisting of a single node. All pod types have zero resource requests. A token in a place p is represented by the presence of a pod carrying the label place = p. Several pod types may carry the same label place = p. For every transition a ∈ T , we partition the places involved in its firing into Consumed(a) (i.e., Pre(a)\Post(a)), Preserved(a) (i.e., Pre(a) ∩ Post(a)), and Produced(a) (i.e., Post(a) \ Pre(a)). Tokens in Consumed(a) are removed during the simulation of a, tokens in Preserved(a) remain present throughout, and tokens in Produced(a) are newly created.

1

Goal coverability is a simplified version, but with the same complexity, of the classical coverability problem for 1-safe Petri nets: coverability considers a set of target places instead of only one goal place.

XXXX 2027

XX:10

Kubernetes Pod-Deployability is PSPACE-Complete

The simulation is driven by a four-phase start-execute-end-ready protocol for each transition. A ready label marks a stable control state in which a new transition may be started. The initial configuration contains one initial ready pod and one initial token pod Ip for every p ∈ M0 . Both initial types require affinity to a fresh label ⊥ that no pod type carries, so they can be deleted but never redeployed. For every transition a, a start type Sa requires affinity to a ready pod and to a token pod for every p ∈ Pre(a), which is deployable when a is enabled. Its anti-affinity to the global start and end labels serializes protocols. Once Sa is deployed, the ready pod and the tokens in Consumed(a) are deleted; tokens in Preserved(a) are left untouched. An execute type Ea then requires affinity to Sa and anti-affinity to ready and to every consumed place, so it appears only after the consumed inputs have been removed. While Ea is present, an output-token type Pp,a for every p ∈ Produced(a) becomes deployable, so that it carries place = p and is anti-affine to place = p, ensuring at most one token per place. An end type Fa requires affinity to Ea and to every place in Post(a), certifying that all outputs are present. Finally, a ready type Ra requires affinity to Fa and anti-affinity to the start and execute labels, so it appears only after the management pods of the finished protocol have been deleted, and restores a stable configuration whose token projection is exactly (M \Pre(a))∪Post(a). A final subtlety is that Kubernetes permits arbitrary pod deletions, so a computation may lose tokens. This is not a problem: Petri-net enabling is monotone in the marking, so any execution interleaved with token losses can be lifted to a loss-free execution reaching a larger marking. Thus, if the goal place is marked by an execution with token losses, it will be marked also by the corresponding loss-free execution. The construction introduces a polynomial number of pod types and constraints: one initial token type per initially marked place, one output-token type for every transition-output-place pair, and a constant number of control types (start, execute, end, ready) per transition, plus one goal type. Labels and selectors use indices from P ∪T . The encoding function is therefore computable in time polynomial in the size of P. Finally, notice that although the fragment has no resource capacity, pod-deployability remains in PSPACE. Affinity and anti-affinity inspect only whether a matching pod is present; they do not inspect its exact multiplicity. Consequently, a configuration can be abstracted by its support supp(σ) = {(t,n) ∈ T ×N | σ(t,n) > 0}. Adding another instance of an already present type, or deleting one instance when another remains, does not change any affinity or anti-affinity guard. Multiplicities can therefore be saturated at one, and there are at most 2|T |·|N | support configurations. A nondeterministic algorithm stores the current support, guesses one deployment or deletion transition, checks its guards in polynomial time, and searches for at most this many configurations. The algorithm uses polynomial space, and hence pod-deployability belongs to NPSPACE = PSPACE by Savitch’s theorem [12]. ▶ Theorem 6 (Affinity and anti-affinity fragment). Pod-Deployability is PSPACE-complete when the only active scheduling constraints are required inter-pod affinity and required inter-pod anti-affinity. Hardness already holds for one node.

6

PSPACE with Affinity and One Capacity

The preceding section showed that required affinity and anti-affinity alone already yield PSPACE-completeness, without relying on resource capacities. We now consider a complementary fragment: anti-affinity is prohibited, and the only dynamic constraints are required inter-pod affinity and one scalar resource capacity. We can show that this fragment is also

S. Giallorenzo, J. Mauro, and G. Zavattaro

XX:11

PSPACE-complete, even if we can use a single node and unit resource requests. Thus, neither anti-affinity nor multiple resources, nodes, or topology domains are needed for the lower bound. We show that this fragment is already PSPACE-complete by encoding the bounded black pebbling game. We first recall the source problem, then present the encoding and its intuition and argue that it is polynomial. Bounded black pebbling game. Let G = (V,E) be a finite directed acyclic graph (DAG). For a vertex v ∈ V , let pred(v) = {u ∈ V | (u,v) ∈ E} be the set of its immediate predecessors. A pebble configuration is a set X ⊆ V such that a vertex belongs to X when it currently carries a pebble. The black-pebble game starts from the empty configuration. It permits the following moves. A pebble may be placed on an unpebbled vertex v when every immediate predecessor of v is currently pebbled: v ∈ / X and pred(v) ⊆ X. The resulting configuration is X ∪{v}. A pebble may be removed from any vertex v ∈ X. The resulting configuration is X \{v}. Source vertices have no predecessors and may therefore be pebbled at any time. Removing a predecessor does not remove pebbles that were placed using it; it may only prevent future placements until that predecessor is reconstructed. In the bounded game, every configuration must contain at most k pebbles. An instance of bounded black-pebble coverability consists of a DAG G = (V,E), a target vertex z ∈ V , and a bound k. The question is whether the empty configuration can reach some pebble configuration containing z, without ever using more than k pebbles. This problem is PSPACE-complete [7]. Encoding. Let (G,z,k) be a bounded black-pebble coverability instance, with G = (V,E). We construct a Kubernetes instance with a single node n and one scalar resource of capacity C(n) = k. For every vertex v ∈ V we introduce one pod type Pv that requests one unit of the resource and carries the unique label id = v. For every edge (u,v) ∈ E, the type Pv has one required pod-affinity term whose selector matches only id = u; hence, Pv can be deployed only while an instance of every predecessor type Pu with u ∈ pred(v) is running. Source types have no affinity terms and are deployable whenever one unit of capacity is free. The initial configuration is empty, and the pod-deployability target is (Pz ,n). The intuition is direct. The presence of an instance of Pv represents a pebble on v: deploying the first Pv instance is pebble placement, deleting its last instance is pebble removal, and the node capacity enforces the pebble bound. Required affinity expresses the predecessor prerequisite, and, because affinity is checked only at scheduling time, a pod may outlive the prerequisites that enabled it, mirroring that removing a predecessor does not remove pebbles placed using it. A final subtlety is that, in the absence of anti-affinity constraints, Kubernetes permits contemporaneous deployments of several instances of the pods of type Pv . This is not a problem: any sequence of pod deployments and deletions which deploys the target pod Pz , has a corresponding correct sequence obtained by removing the deployments of instances of already present Pv pods. The construction uses one node, one scalar capacity, one pod type per vertex, and one affinity term per edge, so its size is O(|V |+|E|+logk) and it is computable in polynomial time. Note that the produced instance is capacity-bounded hence pod-deployability is in PSPACE by Theorem 4. ▶ Theorem 7 (Affinity and One-capacity fragment). Pod-Deployability is PSPACE-complete for a capacity-bounded fragment when the only scheduling constraint is inter-pod required affinity. Hardness already holds for one node, one scalar resource and unit pod requests.

7

Related Work and Conclusion

Formal models of Kubernetes have previously been proposed for purposes other than reasoning about scheduling reachability. In particular, Turin et al. [19] develop a model of Kubernetes in Real-Time ABS to capture the resource-sensitive behaviour of containerized microservices and

XXXX 2027

XX:12

Kubernetes Pod-Deployability is PSPACE-Complete

predict CPU and memory consumption under different deployment scenarios. Their abstraction is aimed at resource modelling and performance prediction, rather than at formalizing the scheduler’s placement decisions and the constraints that determine whether a pod can be assigned to a node. More generally, existing work on Kubernetes formalization does not, to the best of our knowledge, study the computational complexity induced by the scheduler’s placement semantics. Our work takes a complementary perspective: we formalize the hard scheduling constraints that govern pod placement and their evolution under deployments and deletions, and study the resulting verification problem. To the best of our knowledge, this is the first formal analysis of Kubernetes pod-deployability and of its computational complexity. At first sight, anti-affinity appears to be the natural source of hardness: it is a negative test, since deployment is enabled by the absence of matching workloads. This intuition is consistent with classical computational models, in which adding zero or absence tests can substantially increase expressive power. For example, ordinary Petri-net coverability is EXPSPACE-hard [10], but it becomes undecidable in the presence of inhibitor arcs able to test the absence of tokens [9]. Our results show that negative tests do not imply a similar complexity jump in pod scheduling. On the other hand, required affinity, which is capable of checking the presence of selected pods, suffices for PSPACE-hardness already when combined with one scalar capacity. The work closest to ours is the analysis of APP and aAPP by De Palma et al. [6]. APP is a language for specifying scheduling policies for Function-as-a-Service platforms, and aAPP extends it with notions of affinity and anti-affinity similar to ours. Their reachability question— whether a function can be scheduled on a designated worker—is therefore closely related to poddeployability. They prove a linear-time bound for the anti-affinity-only fragment and PSPACEcompleteness for the full language containing both affinity and anti-affinity, using a reduction from propositional planning [2]. For the affinity-only fragment, however, they establish NPhardness but leave its exact complexity open. Our results sharpen and extend this picture in two directions. First, our formal language reflects Kubernetes placement and supports node-label restrictions, multidimensional resources, topology-aware affinity and anti-affinity, and hard topology-spread constraints. In particular, affinity is not restricted to the candidate node: a pod may require a matching witness anywhere in the node’s zone or in another labelled topology domain. Second, our lower bounds already hold for deliberately minimal fragments. The reduction from 1-safe Petri nets establishes PSPACE-hardness using only required affinity and anti-affinity, without capacities or spread constraints. More significantly, the bounded-pebbling reduction establishes PSPACE-hardness with required affinity alone, on a single node and with a single scalar capacity. Thus, for our scheduler model, it closes the affinity-only complexity gap identified for aAPP and shows that anti-affinity is not necessary for PSPACE-hardness. Pod-deployability naturally lends itself to a formulation as a coverability problem, since it asks whether some reachable configuration contains at least one instance of a target pod type on a designated node, without constraining the remainder of the cluster. Exact reachability would instead prescribe the complete target configuration, including the absence and multiplicity of every other pod type. This distinction parallels that between coverability and reachability in Petri nets, where the two problems may have substantially different complexities [4, 10]. An intermediate and practically relevant generalization is co-occurrence: can two designated pod types be simultaneously present on the same node? This is a coverability query over two type-node coordinates and corresponds closely to the co-occurrence property studied for aAPP scheduling policies by De Palma et al. [6]. Our lower bounds extend immediately to this problem by adding an unconstrained marker pod and asking whether it co-occurs with the original target. Moreover, the polynomial-space upper bound is preserved: capacity-bounded configurations still have polynomial-size representations, while the capacity-free affinity/anti-affinity fragment

S. Giallorenzo, J. Mauro, and G. Zavattaro

XX:13

can still be explored through its finite support abstraction. We therefore expect co-occurrence to be PSPACE-complete in both of our hard fragments. Exact configuration reachability deserves a separate analysis. When capacities bound every pod multiplicity, the configuration graph is finite and each state has a polynomial-size representation, so the same exploration argument gives a PSPACE upper bound. Without binding capacities, however, arbitrarily many instances of a zero-request pod type may be deployed on the same node. Our support abstraction identifies all positive multiplicities: configurations containing one, two, or one million instances of a type have the same support and satisfy the same affinity and anti-affinity constraints. This identification is sound for pod-deployability because that problem only asks whether at least one target instance is present. It is not sound for exact reachability, which must distinguish, for example, a target configuration containing exactly one instance from one containing two. Consequently, the finite support graph used in our PSPACE argument loses information needed by exact reachability. Whether these unbounded multiplicities can be handled by a different finite abstraction, and what complexity results, are left for future work. Our study also relates to the broader cluster-scheduling literature, which provides the architectural setting but generally asks different questions. Kubernetes descends from large-scale cluster managers such as Borg [20]. In this area, schedulers like Omega investigated shared-state optimistic scheduling [13], while Firmament formulated placement as a min-cost-flow problem [8]—Burns et al. [1] provide a detailed description of the lineage from Borg and Omega to Kubernetes. This line of work primarily concerns scheduler architecture, placement quality, usage, and scalability. Instead, we study the complexity of an existential verification question induced by Kubernetes’ hard filters. The Kubernetes documentation specifies the scheduling framework and the placement constraints abstracted by our semantics [17, 14]. Our model isolates the hard scheduling-time conditions relevant to pod-deployability and deliberately omits scoring, transient failures, preemption, and plugin-internal state. Conclusion. We introduced pod-deployability as the coverability problem of determining whether some legal sequence of deployments and deletions can place a pod of a given type on a designated node. Our results identify a sharp complexity boundary. Without affinity and without binding capacity, pod-deployability is decidable in polynomial time, even in the presence of anti-affinity and hard topology-spread constraints. With required affinity and anti-affinity it is PSPACE-complete even without capacities. Finally, with required affinity alone it remains PSPACE-complete on one node with one scalar capacity. Together, these results show that positive placement dependencies, rather than only negative exclusion tests, are sufficient to make long deployment and deletion histories computationally significant. For security-sensitive placement policies, inspecting each constraint in isolation is therefore insufficient: an unsafe placement may become feasible only after a long sequence of creations and deletions, even when it is absent from the current cluster state. At the same time, the polynomial fragment shows that efficient verification is possible when no positive prerequisite must be maintained. A natural direction for future work is to incorporate cluster autoscaling, allowing nodes to be dynamically added and removed. Because this yields an unbounded state space, it raises new questions about the decidability and complexity of pod-deployability.

References 1

Brendan Burns, Brian Grant, David Oppenheimer, Eric Brewer, and John Wilkes. Borg, omega, and kubernetes. Communications of the ACM, 59(5):50–57, 2016. doi:10.1145/2890784.

2

Tom Bylander. The computational complexity of propositional STRIPS planning. Artificial Intelligence, 69(1–2):165–204, 1994. doi:10.1016/0004-3702(94)90081-7.

XXXX 2027

XX:14

Kubernetes Pod-Deployability is PSPACE-Complete

3 4 5

6

7 8 9 10 11

12

13

14

15

16 17

18 19

20

Carmen Carrión. Kubernetes scheduling: Taxonomy, ongoing issues and challenges. ACM Computing Surveys, 55(7):1–37, 2023. doi:10.1145/3539606. Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147(1–2):117–136, 1995. doi:10.1016/0304-3975(94)00231-7. Cloud Native Computing Foundation. Kubernetes established as the de facto “operating system” for AI as production use hits 82%. https://www.cncf.io/announcements/2026/01/20/ kubernetes-established-as-the-de-facto-operating-system-for-ai-as-productionuse-hits-82/, January 2026. Accessed 2026-08-18. Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin, and Gianluigi Zavattaro. Reachability analysis of function-as-a-service scheduling policies. In Integrated Formal Methods – 20th International Conference, iFM 2025, Proceedings, volume 16194 of Lecture Notes in Computer Science, pages 226–247. Springer, 2026. doi:10.1007/978-3-032-10794-7_12. John R. Gilbert, Thomas Lengauer, and Robert E. Tarjan. The pebbling problem is complete in polynomial space. In STOC, pages 237–248, 1979. doi:10.1145/800135.804418. Ionel Gog, Malte Schwarzkopf, Adam Gleave, Robert N. M. Watson, and Steven Hand. Firmament: Fast, centralized cluster scheduling at scale. In OSDI, pages 99–115, 2016. Michel Hack. Petri net languages. Technical Report TR-159, MIT Laboratory for Computer Science, 1976. Richard J. Lipton. The reachability problem requires exponential space. Technical report, Department of Computer Science, Yale University, 1976. Mordor Intelligence. Kubernetes market size, share, trends 2031 report. https: //www.mordorintelligence.com/industry-reports/kubernetes-market, May 2026. Accessed 2026-08-18. Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2):177–192, 1970. doi:10.1016/S0022-0000(70)80006-X. Malte Schwarzkopf, Andy Konwinski, Michael Abd-El-Malek, and John Wilkes. Omega: Flexible, scalable schedulers for large compute clusters. In EuroSys, pages 351–364, 2013. doi:10.1145/2465351.2465386. The Kubernetes Authors. Assigning pods to nodes. Kubernetes Documentation. Accessed 4 August 2026. URL: https://kubernetes.io/docs/concepts/scheduling-eviction/assignpod-node/. The Kubernetes Authors. Kubernetes scheduler. Kubernetes Documentation. Accessed 4 August 2026. URL: https://kubernetes.io/docs/concepts/scheduling-eviction/kubescheduler/. The Kubernetes Authors. Scheduling configuration. Kubernetes Documentation. Accessed 4 August 2026. URL: https://kubernetes.io/docs/reference/scheduling/config/. The Kubernetes Authors. Scheduling framework. Kubernetes Documentation. Accessed 4 August 2026. URL: https://kubernetes.io/docs/concepts/scheduling-eviction/schedulingframework/. The Kubernetes Authors. Kubernetes documentation. https://kubernetes.io/docs/, 2026. Accessed: 2026-08-17. Gianluca Turin, Andrea Borgarelli, Simone Donetti, Ferruccio Damiani, Einar Broch Johnsen, and Silvia Lizeth Tapia Tarifa. Predicting resource consumption of kubernetes container systems using resource models. J. Syst. Softw., 203:111750, 2023. doi:10.1016/J.JSS.2023.111750. Abhishek Verma, Luis Pedrosa, Madhukar Korupolu, David Oppenheimer, Eric Tune, and John Wilkes. Large-scale cluster management at google with borg. In EuroSys, 2015. doi:10.1145/2741948.2741964.

S. Giallorenzo, J. Mauro, and G. Zavattaro

A

XX:15

Proofs of Pod-Deployability without affinity constraints

In this appendix, we give the full proof of Theorem 4, which states that Pod-Deployability is in PSPACE for capacity-bounded instances. We first show that every configuration of a capacity-bounded instance admits a polynomial-size representation (Lemma 8), then bound the number of distinct configurations and the length of shortest witnessing executions (Lemmas 9 and 10), and finally combine these facts in a nondeterministic polynomial-space decision procedure (Theorem 11). ▶ Lemma 8 (Polynomial-size configurations). For a capacity-bounded instance, every configuration σ can be stored in polynomial space. Proof. For each pair (t,n) ∈ T ×N , the capacity constraint implies 0 ≤ σ(t,n) ≤ Bt,n . We store σ(t,n) as a binary counter. This counter requires ⌈log2 (Bt,n +1)⌉ bits. Since capacities and requests are encoded in binary, this number is polynomial in the input length. There are |T | · |N | counters, and therefore the complete configuration has a polynomial-size representation. ◀ ▶ Lemma 9 (Finite configuration count). The number of possible configurations is finite and bounded by YY K= (Bt,n +1). t∈T n∈N

Although K may be exponential, its binary length is polynomial in the input length. Proof. Each counter σ(t,n) ranges over the Bt,n +1 values 0,...,Bt,n , so the product counts all configurations. Its binary length is XX ⌈log2 K⌉ ≤ ⌈log2 (Bt,n +1)⌉, t∈T n∈N

which is polynomial in the input length by Lemma 8.

◀

▶ Lemma 10 (Short witnessing paths). If a target configuration is reachable, then it is reachable by a path of length less than K that does not repeat any configuration. Proof. Take a shortest path from σ0 to a target configuration. If some configuration occurred twice, the cycle between its two occurrences could be removed, yielding a strictly shorter path; this contradicts minimality. Hence the path is simple. Since there are at most K distinct configurations by Lemma 9, a simple path has length strictly less than K. ◀ ▶ Theorem 11 (Polynomial-space pod-deployability). Pod-Deployability for capacitybounded instances is in PSPACE. Proof. Consider the following nondeterministic procedure. It stores the current configuration, initially σ0 , together with a binary step counter bounded by K. At every iteration, it first checks whether σ(t⋆ ,n⋆ ) ≥ 1. If so, it accepts. Otherwise, it nondeterministically chooses one of the following transitions:

XXXX 2027

XX:16

Kubernetes Pod-Deployability is PSPACE-Complete

choose t ∈ T and n ∈ N , verify Hard(t,n,σ), and replace σ by σ+(t,n); or choose t ∈ T and n ∈ N with σ(t,n) > 0, and replace σ by σ−(t,n). If no accepting configuration has been found after K transitions, the branch rejects. Each transition changes one binary counter by one. For the constraints of Section 2, resource sums, selector matching, affinity and anti-affinity tests, and topology-spread counts can all be computed by scanning the polynomially many counters, nodes, labels, and encoded constraints. Therefore the predicate Hard(t,n,σ) can be checked in polynomial space. The procedure stores only the current configuration, the step counter, and polynomially many auxiliary values, so it uses polynomial space. By Lemma 10, a target configuration is reachable exactly when it is reachable within K transitions, so the procedure accepts exactly the positive instances. Thus Pod-Deployability belongs to NPSPACE = PSPACE by Savitch’s theorem [12]. ◀

B

The Encoding of 1-Safe Petri Nets

In this appendix, we formalize the polynomial-time encoding function EPN used in Section 5 and prove its correctness: the goal place of a 1-safe Petri net is coverable if and only if the goal pod is deployable in the encoded instance. We use the following notation throughout this and the next appendix. For a label predicate L, write s[L] for the selector that matches exactly the pod types carrying label L. All affinity and anti-affinity terms use the hostname topology of the unique node; we therefore write only their selectors. Labels described as fresh are distinct from all other labels introduced by the construction. Let P = (P,T,Pre,Post,M0 ) be a 1-safe Petri net and let g ∈ P be its goal place. We identify a reachable marking with the set M ⊆ P of its marked places. A transition a ∈ T is enabled at M when Pre(a) ⊆ M , and its firing produces a(M ) = (M \Pre(a))∪Post(a). As recalled in Section 5, coverability of g is PSPACE-hard for 1-safe nets.

The encoding function. We define EPN (P,g) = (TP ,{n},σ0 ,(Gg ,n)). The result is a pod-deployability instance with one node n, zero resource requests, no capacity restriction, and only required affinity and required anti-affinity. The distinguished goal type Gg requires a token for place g and is the pod-deployability target. For every transition a ∈ T , partition its places into consumed, preserved, and produced: Consumed(a) = Pre(a)\Post(a), Preserved(a) = Pre(a)∩Post(a), Produced(a) = Post(a)\Pre(a). The set of pod types is TP = {Ip | p ∈ M0 } ∪ {Pp,a | a ∈ T, p ∈ Produced(a)} ∪ {Sa ,Ea ,Fa ,Ra | a ∈ T } ∪ {R0 ,Gg }. Here Ip is the initial token type for p, Pp,a is a token for p produced by transition a, and Sa ,Ea ,Fa ,Ra are the start, execute, end, and ready types of the protocol for a. The type R0 supplies the initial ready pod. Let ⊥ be a fresh label that no pod type carries. The labels and hard constraints generated by EPN are as follows; every unlisted affinity or anti-affinity set is empty. Initial token Ip . It carries place = p, requires affinity to s[⊥], and has anti-affinity to s[place = p]. Thus its initial instance can be deleted but the type can never be deployed again.

S. Giallorenzo, J. Mauro, and G. Zavattaro

XX:17

Initial ready type R0 . It carries ready, requires affinity to s[⊥], and has anti-affinity to s[ready]. It likewise cannot be recreated. Start type Sa . It carries start and start = a. Its affinity terms are {s[ready]}∪{s[place = p] | p ∈ Pre(a)}, and its anti-affinity terms are s[start] and s[end]. Execute type Ea . It carries execute and execute = a, requires affinity to s[start = a], and has anti-affinity to {s[ready],s[execute]}∪{s[place = p] | p ∈ Consumed(a)}. The absence test is imposed only on the consumed places; preserved places (self-loops) are left untouched. Produced-token type Pp,a . It carries place = p, requires affinity to s[execute = a], and has anti-affinity to s[place = p]. End type Fa . It carries end and end = a. It requires affinity to {s[execute = a]}∪{s[place = p] | p ∈ Post(a)}, and has anti-affinity to s[end]. Ready type Ra . It carries ready, requires affinity to s[end = a], and has anti-affinity to s[ready], s[start], and s[execute]. Goal type Gg . It carries the fresh label goal and has the single affinity term s[place = g]. Thus it is deployable exactly when a token for g is present. All types have zero resource requests and pass every static filter. The initial configuration is σ0 (Ip ,n) = 1

(p ∈ M0 ),

σ0 (R0 ,n) = 1,

and is zero elsewhere. Required resident anti-affinity ensures that at most one token carrying place = p, one ready pod, and one pod carrying each global control label can be present. For a Kubernetes configuration σ, define its token projection by πPN (σ) = {p ∈ P | some running pod in σ carries place = p}. A configuration is stable for M if its token projection is M , it contains exactly one ready pod, and it contains no start, execute, or end pod. Let ΦPN (M ) denote any such stable configuration. The choice of producer type for a token is irrelevant because all token types for the same place carry the same place label and the same uniqueness constraint. ▶ Theorem 12 (Polynomiality of the Petri-net encoding). The encoding function EPN is computable in time polynomial in the size of P. Proof. The encoding creates one node, one initial token type per initially marked place, one produced-token type per transition-produced-place pair, four control types per transition, one initial ready type, and one goal type. It contains one affinity term per preset or postset test and only a constant number of additional guards per type. Labels and selectors use indices from P ∪T , so the total size and the computation time are polynomial in |P |+|T |+|M0 |. ◀ ▶ Theorem 13 (PSPACE membership of the capacity-free fragment). Pod-deployability is in PSPACE when the only active scheduling constraints are required inter-pod affinity and required inter-pod anti-affinity, even without any capacity bound.

XXXX 2027

XX:18

Kubernetes Pod-Deployability is PSPACE-Complete

Proof. Affinity and anti-affinity inspect only whether a matching pod is present, not its exact multiplicity. Abstract a configuration by its support supp(σ) = {(t,n) | σ(t,n) > 0}. Adding another instance of an already present type satisfies no new affinity term, and deleting one instance while another remains changes no guard; hence multiplicities saturate at one. There are at most 2|T |·|N | supports. A nondeterministic algorithm a) stores the current support and a step counter bounded by this number, b) guesses one deployment or deletion, and c) checks its guards in polynomial time. The search uses polynomial space, so the problem is in NPSPACE = PSPACE by Savitch’s theorem [12]. ◀ a

→ M ′ in P, then every stable configuration for ▶ Lemma 14 (One firing is simulated). If M − M reaches a stable configuration for M ′ . Proof. Because a is enabled, Pre(a) ⊆ M . Hence the ready pod and the token pods for all places in Pre(a) witness the affinity terms of Sa . No start or end pod is present in a stable configuration, so its anti-affinity terms also hold and Sa can be deployed. Delete the ready pod and precisely the token pods for Consumed(a); the tokens for Preserved(a) remain. The start pod remains as a lock: its resident anti-affinity prevents every other start and every end. Now Ea is deployable. Its positive witness is Sa , and its negative tests certify that ready and every consumed input token have disappeared. Once Ea is present, deploy one Pp,a for every p ∈ Produced(a). Its execute affinity holds. Its place anti-affinity also holds: if p ∈ Produced(a) = Post(a)\Pre(a), 1-safety implies that p ∈ / M whenever a is enabled at a reachable marking. After all outputs exist, delete Sa and deploy Fa . The end affinities certify that Ea and every postset token are present: a preserved place is witnessed by the token kept throughout and a produced place by the newly deployed Pp,a . Delete Ea , then deploy Ra , witnessed by Fa . Finally delete Fa . The remaining configuration contains one ready pod, no control pod, and exactly the tokens (M \Pre(a))∪Post(a) = M ′ . It is therefore stable for M ′ . The sequence is illustrated in Figure 1. ◀ ∗

▶ Corollary 15 (Completeness of EPN ). If M0 − → M , then σ0 −→∗ ΦPN (M ). In particular, if g ∈ M , the encoded pod-deployability instance can deploy Gg . Proof. The initial configuration is stable for M0 . Apply Lemma 14 inductively to the firing sequence. ◀ Kubernetes also permits deletions not prescribed by the simulation. We use the following standard monotonicity argument to show that such losses cannot create a false positive. ▶ Lemma 16 (Lifting token losses). Suppose a sequence starting at M0 alternates Petri-net firings with arbitrary losses L 7→ L′ ⊆ L, and ends in Lf . Then P has a loss-free firing sequence from M0 to a reachable marking Mf ⊇ Lf . Proof. Maintain by induction a reachable loss-free marking M containing the current lossy marking L. Initially take M = L = M0 . A loss preserves the invariant without changing M . If a is enabled at L, then Pre(a) ⊆ L ⊆ M , so a is also enabled at M . Since M is reachable and the net is 1-safe, firing a is a legal safe firing. Moreover, (L\Pre(a))∪Post(a) ⊆ (M \Pre(a))∪Post(a). Taking the right-hand side as the new M preserves the invariant.

◀

S. Giallorenzo, J. Mauro, and G. Zavattaro

XX:19

Kubernetes protocol

R, Pp , Pq stable marking {p,q} Sa , Pp , Pq start: test the inputs delete R,Pp ,Pq Petri net

Sa , Ea execute: consumed inputs gone

p r q transition a

Ea , Pr produce every output delete Sa

Fa , P r end, then recreate R delete Ea ,Fa

R, Pr stable marking {r}

Figure 1 Encoding a Petri-net transition with Pre(a) = {p,q} and Post(a) = {r}. The displayed configurations suppress producer indices and transient deletion steps. The ready pod R separates completed protocol cycles.

▶ Lemma 17 (Protocol decomposition). Every Kubernetes execution generated by EPN is a concatenation of completed protocol intervals, followed by at most one unfinished interval. Each completed interval projects to one enabled Petri-net firing, possibly together with arbitrary token losses. An unfinished interval cannot start another protocol. Proof. A start pod requires ready. Once some Sa is deployed, its resident anti-affinity to s[start] excludes every other start pod. Moreover, ready must be deleted before Ea can appear. Execute requires the particular Sa and certifies, by anti-affinity, that all consumed preset tokens have been deleted. Thus reaching execute identifies an enabled transition a at the token projection observed when Sa was deployed. Produced-token types for a require Ea . An end pod requires all postset tokens and cannot appear while another end pod remains. Finally, a new ready pod requires Fa and cannot appear while a start or execute pod remains. A subsequent start is blocked until the end pod is also deleted. Consequently the only way to return to a stable control state is the ordered cycle ready ; Sa ; Ea ; {Pp,a : p ∈ Produced(a)} ; Fa ; Ra . Deleting a required control pod early makes completion impossible, because deleted control types cannot be recreated without an earlier phase. Such an execution is therefore an unfinished final interval and cannot enable a new start. Deletions of unrelated token pods are the only remaining deviations; they project exactly to token losses. ◀ ▶ Theorem 18 (Correctness of the Petri-net encoding). The goal place g is coverable from M0 in P if and only if the target (Gg ,n) is coverable in EPN (P,g). Proof. The forward implication is Corollary 15. For the reverse implication, consider the execution prefix ending immediately before the first deployment of Gg . Its affinity guard shows that this prefix contains a token for g. By Lemma 17, every completed protocol in the prefix

XXXX 2027

XX:20

Kubernetes Pod-Deployability is PSPACE-Complete

projects to a Petri firing, interspersed with possible token losses. If the goal token is already present after a completed interval, Lemma 16 yields a genuine loss-free execution whose final marking contains g. Otherwise the goal token is produced in the unique unfinished final interval. It must be an output Pg,a . Before it can appear, Sa was deployed while all preset tokens were present, the consumed tokens and ready were deleted, and Ea was deployed. Hence a was enabled in the lossy marking at the start of the interval. Append the abstract firing of a; its postset contains g. Applying Lemma 16 again yields a genuine Petri execution covering g. Thus no partial or lossy Kubernetes execution creates a false positive. ◀ Together with Theorems 12 and 13, Theorem 18 proves Theorem 6.

Lean formalization. The encoding and its correctness are mechanized in the Lean 4 library in lean_code and available at https://doi.org/10.5281/zenodo.22025656. The scheduler model (configurations, affinity and anti-affinity semantics, deployment and deletion steps, reachability, and pod-deployability) is defined in Scheduler.lean. One-safe Petri nets, their firing semantics, coverability, and the token-loss lifting lemma (Lemma 16) are formalized in PetriNet.lean and PetriNetEncoding.lean; the lossy step relation LossyNetStep combines an ordinary firing with an arbitrary token loss, and loss_lifting shows that every lossy abstract execution is simulated by a loss-free execution whose marking contains the lossy marking. The pod roles are an inductive type with constructors for initial tokens, produced tokens, start, execute, end, ready, and the goal; selectors such as tokenSelector, readySelector, and executeEqSelector implement the label predicates, and the functions affinity and antiAffinity give the concrete guards described above. The initial-only pods are blocked from redeployment by the affinity to the empty selector botSelector (s[⊥]), exactly as in the definition of EPN . Completeness (Corollary 15) is proved in PetriNetCompleteness.lean. The proof constructs the scheduler witness for one simulated firing as an explicit sequence of legal add and remove operations—deploy start, delete ready and the consumed inputs, deploy execute, deploy the produced outputs, delete start, deploy end, delete execute, deploy ready, delete end—and composes these sequences along the Petri firing sequence by induction, in stableConfig_transition_to_stableConfig and petri_covers_implies_goal_deployable. Soundness (reverse direction of Theorem 18) is proved in PetriNetCorrectness.lean. The proof first establishes that every reachable configuration satisfies a valid control combination (reachable_validControlCombination): each control role is globally unique, ready cannot coexist with execute, and start cannot coexist with end. It then splits every scheduler execution at its stable configurations using the inductively defined FirstStableTrace and SinceClosestStable decompositions, shows that every completed stable interval corresponds to one enabled Petri firing or to pure token loss (first_stable_reach_sound), and that the final interval producing the goal token requires an enabled transition whose postset contains the goal place (preset_present_at_closest_stable_before_output). Combining these with the loss-lifting lemma yields goal_deployable_implies_petri_covers. The main equivalence, petri_covers_iff_goal_deployable in PetriNetMainTheorem.lean, combines the two directions and corresponds exactly to Theorem 18.

S. Giallorenzo, J. Mauro, and G. Zavattaro

C

XX:21

The Encoding of Bounded Black Pebbling

In this appendix, we formalize the polynomial-time encoding function EPeb used in Section 6 and prove its correctness: the target vertex of a bounded black-pebble instance is coverable with at most k pebbles if and only if the target pod is deployable in the encoded instance. Let (G,z,k) be a bounded black-pebble coverability instance, where G = (V,E) is a DAG, z ∈ V , and k is the pebble bound. Write pred(v) = {u | (u,v) ∈ E}. A pebble position is a set X ⊆ V with |X| ≤ k. A move either removes any v ∈ X, or adds v ∈ / X when pred(v) ⊆ X and |X| < k.

The encoding function. Define EPeb (G,z,k) = ({Pv | v ∈ V },{n},0,(Pz ,n)). The unique node has one scalar resource r with capacity C(n)(r) = k. Every type Pv has unit request res(Pv )(r) = 1, carries the unique label id = v, and has required affinity terms A+ (Pv ) = {s[id = u] | u ∈ pred(v)}. All anti-affinity sets are empty and all static filters are true. Thus a source type has no affinity terms and can be deployed whenever capacity is available. The construction uses one type per vertex and one affinity term per edge. Define the canonical encoding of a pebble position X by ( 1, v ∈ X, ΦPeb (X)(Pv ,n) = 0, v ∈ / X, and project an arbitrary Kubernetes configuration to its support: πPeb (σ) = {v ∈ V | σ(Pv ,n) > 0}. Notice that |πPeb (σ)| ≤

P

v σ(Pv ,n) ≤ k.

▶ Theorem 19 (Polynomiality of the pebbling encoding). The encoding function EPeb is computable in time polynomial in the size of (G,z,k). Proof. The encoding creates one node, one scalar capacity, one pod type per vertex, and one affinity term per edge. Its size is O(|V |+|E|+logk), and it can be computed in the same time. ◀ ▶ Theorem 20 (PSPACE membership of the affinity-and-capacity fragment). Pod-deployability is in PSPACE for a fragment with one node, one scalar resource capacity, unit pod requests, and required inter-pod affinity only. Proof. A fragment where each pod type requires one unit of a unique available resource contains problem instances that are capacity-bounded (see Definition 3). Pod-deployability is then in PSPACE as a consequence of Theorem 11. ◀ ▶ Lemma 21 (Completeness of EPeb ). If the bounded pebble game moves from X to Y , then ΦPeb (X) −→ ΦPeb (Y ). Consequently, every bounded pebbling execution from ∅ has a corresponding Kubernetes execution from 0.

XXXX 2027

XX:22

Kubernetes Pod-Deployability is PSPACE-Complete

position X = {u,w} node n, capacity k = 3

u v

ΦPeb Pu

w

Pw

position X deploy Pv ; affinity to Pu ,Pw

w

ΦPeb

v u

Pu

Pw

Pv

position X ∪{v};

position X ∪{v} = {u,w,v} Figure 2 A pebble position and its canonical pod configuration. Since both predecessor pods are present and one capacity unit is free, deploying Pv implements the legal move X 7→ X ∪{v}.

Proof. Suppose first that Y = X ∪{v}. Legality of the pebble placement gives pred(v) ⊆ X and |X| < k. For every predecessor u, configuration ΦPeb (X) contains Pu , so every affinity term of Pv is satisfied. Its resource usage is |X|+1 ≤ k, so capacity also holds. Deploying Pv yields exactly ΦPeb (Y ), as illustrated in Figure 2. If Y = X \{v}, deleting the unique instance of Pv yields ΦPeb (Y ). Induction on the move sequence proves the second claim. ◀ Because the affinity-only language cannot forbid duplicate instances, the reverse direction must apply to noncanonical configurations as well. ▶ Lemma 22 (Support simulation). For every Kubernetes transition σ −→ σ ′ , exactly one of the following holds: 1. πPeb (σ ′ ) = πPeb (σ); or 2. πPeb (σ) −→ πPeb (σ ′ ) is a legal bounded pebble move. Proof. Consider a deployment of Pv . If Pv was already present, support does not change. Otherwise the support gains v. Every affinity term was checked before deployment, hence pred(v) ⊆ πPeb (σ). Moreover, capacity requires X σ(Pu ,n) < k. u∈V

Since support counts at most one vertex per running instance, |πPeb (σ)| < k. Adding v is therefore a legal bounded pebble move. Now consider deletion of one Pv . If another instance remains, support is unchanged. If the deleted pod was the last instance, support loses v, which is always a legal pebble-removal move. These cases exhaust the transition relation. ◀ ▶ Corollary 23 (Soundness of EPeb ). Every Kubernetes execution from 0 projects, after deleting support-preserving stuttering steps, to a legal bounded pebbling execution from ∅. Proof. Apply Lemma 22 to each transition. The projected initial support is empty, every non-stuttering projected step is a legal pebble move, and every projected support has size at most k. ◀ ▶ Theorem 24 (Correctness of the pebbling encoding). The target vertex z is coverable with at most k black pebbles if and only if (Pz ,n) is pod-deployable in EPeb (G,z,k).

S. Giallorenzo, J. Mauro, and G. Zavattaro

XX:23

Proof. If a bounded pebbling execution reaches X ∋ z, Lemma 21 produces a Kubernetes execution reaching ΦPeb (X), which contains Pz . Conversely, suppose a Kubernetes execution reaches σ with σ(Pz ,n) > 0. Then z ∈ πPeb (σ). By Corollary 23, this support is reachable by a bounded pebbling execution, after omitting stuttering steps. Hence that pebbling execution covers z. ◀ Together with Theorems 19 and 20, Theorem 24 proves Theorem 7.

Lean formalization. The pebbling encoding and its correctness are mechanized in the Lean 4 library in lean_code, availabile at https://doi.org/10.5281/zenodo.22025656. The bounded black-pebble game is defined in Pebbling.lean: a PebbleGame records the predecessor function, the target, and the bound; Step is the inductive legal-move relation (placement requires the predecessors to be present and spare capacity, removal is always legal), and Covers asks for a reachable position containing the target. The encoding is formalized in PebbleEncoding.lean. The scheduler specification spec gives each vertex pod a unit request, the node a capacity equal to the bound, and one affinity term predecessorTerm per edge; the initial configuration is empty. The canonical configuration of a position is canonical, and the support projection is support. Completeness (Lemma 21) is proved by pebbleStep_scheduler and pebbleRun_scheduler, which show that every legal pebble move is simulated by a scheduler transition between canonical configurations. Because affinity alone cannot forbid duplicate instances, soundness is proved for arbitrary configurations: schedulerStep_projects shows that every scheduler step either preserves the support (a stuttering step) or projects to a legal pebble move, and schedulerRun_projects lifts this to whole executions, also showing that the resource usage never exceeds the bound. The main equivalence, encoding_correct_and_complete, combines the two directions and corresponds to Theorem 24.

XXXX 2027

Related documents

• Processo de KDD para auxílio à reconfiguração de ambientes virtualizados#946274
• INTEGRATING ARTIFICIAL INTELLIGENCE WITH CLOUD-NATIVE ARCHITECTURES: DESIGN PATTERNS, CHALLENGES, AND FUTURE DIRECTIONS FOCUS: HOW AI MODELS ARE DEPLOYED IN SCALABLE CLOUD ENVIRONMENTS, INCLUDING MICROSERVICES, CONTAINERS, AND SERVERLESS SYSTEMS#15610
• INTEGRATING ARTIFICIAL INTELLIGENCE WITH CLOUD-NATIVE ARCHITECTURES: DESIGN PATTERNS, CHALLENGES, AND FUTURE DIRECTIONS FOCUS: HOW AI MODELS ARE DEPLOYED IN SCALABLE CLOUD ENVIRONMENTS, INCLUDING MICROSERVICES, CONTAINERS, AND SERVERLESS SYSTEMS#15609
• ConfigSpec: Profiling-Based Configuration Selection for Distributed Edge--Cloud Speculative LLM Serving#10329
• Interference-Aware Cross-Application Placement: A Multi-Objective Optimization Approach for Microservice Clusters#306984