Jussi Rintanen, Albert-Ludwigs-Universität Freiburg
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.