A Weakest precondition semantics for conditional planning

In this paper we show an approach to conditional planning which is based on a particular three valued logic. Assignments and conditional formulae (built by means of the alternate operator as introduced in [7]) are used to represent uncertain situations. A model for actions in a conditional framework is defined by giving an execution function, which returns the updated situation after the execution, and an executability predicate. We also define a weakest precondition semantics in order to determine the least alternative situation in which a plan is executable and, after the execution, a required formula holds. The tools we introduced allow us to compile a plan in a macroaction, which is an abstraction of a plan, neglecting its internal decomposition. It is possible to prove that the use of macroactions is correct in a more complex plan.This work has been partially supported by Progetto Speciale “Pianificazione Automatica” under contract n. 93.006.27.CT07 of Italian National Research Council — C.N.R. and by 40% project “Algoritmi, Modelli di Calcolo e Strutture Informative” of M.U.R.S.T (18 citations in WOS)