An Iterative Algorithm for Synthesizing Invariants

Published 30 July 2000

Jussi Rintanen

Citations79

TL;DR

A general algorithm for synthesizing state invariants that speed up automated planners and have other appli- cations in reasoning about change, and is strictly stronger than earlier algorithms combined.

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...

Keywords

Computer Science

Artificial IntelligenceFast planning through planning graph analysis

1,556 Citations1997Avrim Blum, Merrick L. Furst

A new approach to planning in STRIPS-like domains based on constructing and analyzing a compact structure the authors call a Planning Graph is introduced, and a new planner, Graphplan, is described that uses this paradigm.

IEEE Transactions on Computer-Aided Design of Integrated Circuits and SystemsSymbolic model checking for sequential circuit verification

552 Citations1994Jerry R. Burch, E. M. Clarke +3 more

The temporal logic model checking algorithm of Clarke, Emerson, and Sistla is modified to represent state graphs using binary decision diagrams (BDD's) and partitioned transition relations and is able to express a number of important liveness and fairness properties, which would otherwise not be expressible in CTL.

Journal of Artificial Intelligence ResearchThe Automatic Inference of State Invariants in TIM

195 Citations1998Maria Fox, Derek Long

A process by which state invariants can be extracted from the automatically inferred type structure of a domain is described, being developed for exploitation by STAN, a Graphplan based planner that employs state analysis techniques to enhance its performance.

View PDF

Lecture notes in computer sciencePowerful techniques for the automatic generation of invariants

114 Citations1996Saddek Bensalem, Yassine Lakhnech +1 more

A refined strengthening technique is presented that allows to avoid the problem of size-increase of the considered predicates which is the main drawback of the usual strengthening technique.

Inferring state constraints for domain-independent planning

114 Citations1998Alfonso Gerevini, Lenhart K. Schubert

Preliminary results on the effectiveness of adding computed state constraints and predicate domains to the specification of problems for SAT-based planners such as SATPLAN or MEDIC are shown.

A Planning Algorithm not based on Directional Search.

68 Citations1998Jussi Rintanen

A simple planning algorithm is discussed that reconstructs the planner in the background of the SAT/CSP approach to solve general-purpose satisfiability problems in STRIPS planning.

The role of domain-specific knowledge in the planning as satisfiability framework

67 Citations1998Henry Kautz, Bart Selman

This work presents a way to encode domain knowledge in a purely declarative, algorithm independent manner, and demonstrates that the same heuristic knowledge can be used by completely different search engines, one systematic, the other using greedy local search.

Fundamenta InformaticaeDeriving Invariants and Constraints from Action Theories

9 Citations1997Yan Zhang, Norman Foo

This paper proposes a persistence-based formalism of actions, and shows that the generation of action invariants is achieved from action specifications by reasoning about persistence, and investigates the generalization ofaction invariants into state constraints.