Pod-Deployability in Kubernetes with Inter-Pod Affinity Constraints is PSPACE-Complete
Saverio Giallorenzo, Jacopo Mauro, Gianluigi Zavattaro
cs.CC
Aug 20, 2026 · v1
cs.DC
TL;DR
The polynomial-time result and both PSPACE-hardness reductions (from 1-safe Petri-net coverability and bounded black pebbling) are mechanized and verified in Lean 4, with a Zenodo artifact.
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.
Problem
Kubernetes schedules pods using resource capacities and label-based inter-pod affinity and anti-affinity rules. The question studied is pod-deployability: can some legal sequence of deployments and deletions place a given pod type on a designated node, for example across a security boundary?
Approach
The authors formalize the hard scheduling constraints of the Kubernetes scheduler as a transition system over cluster configurations and cast pod-deployability as a coverability problem. Lower bounds come from reductions from 1-safe Petri-net goal coverability and from bounded black-pebble coverability. The encodings and their correctness proofs are mechanized in a Lean 4 library.
Results
Without affinity (anti-affinity allowed), pod-deployability is decidable in polynomial time. Required affinity combined with anti-affinity makes it PSPACE-complete. Required affinity alone is already PSPACE-complete on a single node with one scalar capacity and unit resource requests.
