An Iterative Algorithm for Synthesizing Invariants

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 contrast to earlier work, 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, the algorithm is not inherently restricted to invariants of particular syntactic forms.

Authors

• Jussi Rintanen Aalto University

Keywords

No keywords are indexed for this paper.