Generalized planning: Synthesizing plans that work for multiple environments

We give a formal definition of generalized planning that is independent of any representation formalism. We assume that our generalized plans must work on a set of deterministic environments, which are essentially unrelated to each other. We prove that generalized planning for a finite set of environments is always decidable and EXPSPACE-complete. Our proof is constructive and gives us a sound, complete and complexity-wise optimal technique. We also consider infinite sets of environments, and show that generalized planning for the infinite "one-dimensional problems," known in the literature to be recursively enumerable when restricted to finite-state plans, is EXPSPACE-decidable without sequence functions, and solvable by generalized planning for finite sets.