An Iterative Algorithm for Synthesizing Invariants

Abstract

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. Introduction For a given transition system, for example expressed as an initial state and a set of operators, invariants are facts that hold in all of its reachable states, or more precisely, they are true in the initial state, and their truth is preserved by the application of every operator (which is why they are called invariants.) Invariants can be applied in many kinds of planning algorit...