On methodology of representing knowledge in dynamic domains

The main goal of this paper is to outline a methodology of programming in dynamic problem domains. The methodology is based on recent developments in theories of reasoning about action and change and in logic programming. The basic ideas of the approach are illustrated by discussion of the design of a program which verifies plans to control the Reaction Control System (RCS) of the Space Shuttle. We start with formalization of the RCS domain in an action description language. The resulting formalization A_RCS together with a candidate plan α and a goal G are given as an input to a logic program. This program verifies if G would be true after executing α in the current situation. A high degree of trust in the program's correctness was achieved by(a) the simplicity and transparency of our formalization, A_RCS, which made it possible for the users to informally verify its correctness;(b) a proof of correctness of the program with respect to A_RCS. This is an ongoing work under a contract with the United Space Alliance - the company primarily responsible for operating the Space Shuttle.