An Iterative Algorithm for Synthesizing Invariants

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.