Towards the validation of high-level action descriptions from their low-level definitions

We address the problem of formally proving high-level effect descriptions of actions from low-level operational definitions. Both descriptions are expressed in a logic of actions and change, with extensions for characterizing continuous change, discontinuities, the distinction between true and estimated values of state variables, and the distinction between success and failure of an action. Both descriptions also require the use of nonmonotonicity in the logic in question. The transition from operational definition to effect description furthermore involves the creation of a closure with respect to the set of possible ways that the action can fail.

We outline, by means of an example, how these issues can be addressed as an extension of existing results on logics of actions and change.