Complexity Results for Fixing Classical Models Using LTL to Express Which Solutions Are (Un)Desired

Abstract

Model repair is the task of modifying a given planning model so that it satisfies a set of validity constraints. Prior frameworks encode constraints as finite sets of desired and undesired plans, which cannot capture properties of infinite sets of plans or patterns shared by all (non)solutions, thereby limiting their usefulness. We propose a unified formalism that subsumes prior approaches by incorporating validity constraints specified in Linear Temporal Logic over process traces (LTLp), thereby capturing temporal and structural properties of plans. We further present a comprehensive complexity analysis that begins with a highly restricted fragment of LTLp and progressively lifts restrictions, tracking how increasing expressivity impacts the complexity of model repair. This yields a complexity landscape ranging from NP through Sigma_2^p up to PSPACE. We also highlight connections between our framework and some well-studied problems, including planning with temporally extended goals (TEGs), model repair using desired and undesired plans, the model reconciliation explanation (MRE) problem, and counterfactual scenarios for automated planning.