State-Based Discovery and Verification of Propositional Planning Invariants
Lenhart K. Schubert, Proshanto Mukherji · UR Research (University of Rochester) · 2005
Planning invariants are formulae that are true in every reachable state of a planning world. We describe a novel approach to the problem of discovering such invariants in propositional form---by analyzing only a set of reachable states of the planning domain, and not its operators. Our system works by exploiting perceived patterns of propositional covariance across the set of states: It hypothesizes that strongly-defined patterns represent features of the planning world. We demonstrate that, in practice, our system overwhelmingly produces correct invariants. Moreover, we compare it with a well-known system from the literature that uses complete operator descriptions, and show that it discovers a comparable number of invariants, and moreover, does so hundreds or thousands of times faster. We also show how an existing operator-based invariant finder can be used to verify the correctness of the invariants we find, should operator information be available. We show that such hybrid systems can efficiently produce verifiably true invariants.