An Iterative Algorithm for Synthesizing Invariants

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Planning and Scheduling

We present a general algorithm for synthesizing state invariants that speed up automated planners and have other applications in reasoning about change. Invariants are facts that hold in all states that are reachable from an initial state by the application of a number of operators. In comparison to earlier work on synthesizing invariants, we recognize the fact that establishing an invariant may require considering other invariants, and this in turn seems to require viewing synthesis of invariants as fixpoint computation. Also, our algorithm is not inherently restricted to invariants of particular syntactic forms.