Plans often change due to changes in the situation or our understanding of the situation. Sometimes, a feasible plan may not even exist, and identifying such infeasibilities is useful to determine when requirements need adjustment. Common planning approaches focus on efficient one-shot planning in feasible cases rather than updating domains or detecting infeasibility. We propose a Petri net reachability relaxation to enable robust invariant synthesis, efficient goal-unreachability detection, and helpful infeasibility explanations. We further leverage incremental constraint solvers to support goal and constraint updates. Empirically, compared to baselines, our system produces a comparable number of invariants, detects up to 2 times more infeasibilities, performs competitively in one-shot planning, and outperforms in sequential plan updates in the tested domains.

翻译：由于情境变化或对情境理解的改变，规划方案常需调整。有时甚至不存在可行方案，识别此类不可行性有助于确定何时需要调整需求。传统规划方法主要关注可行情况下的高效单次规划，而非领域更新或不可行性检测。本文提出一种Petri网可达性松弛方法，可实现鲁棒的约束不变式生成、高效的目标不可达检测以及具有解释力的不可行性分析。我们进一步利用增量约束求解器以支持目标与约束的实时更新。实验表明：相较于基线方法，本系统生成的约束不变式数量相当，检测到的不可行情况提升至2倍，在单次规划任务中表现相当，并在测试领域的序贯规划更新中展现出更优性能。