A logic of time, chance, and action for representing plans

This paper integrates logical and probabilistic approaches to the representation of planning problems by developing a first-order logic of time, chance, and action. We start by making explicit and precise commonsense notions about time, chance, and action central to the planning problem. We then develop a logic, the semantics of which incorporates these intuitive properties. The logical language integrates both modal and probabilistic constructs and allows quantification over time points, probability values, and domain individuals. Probability is treated as a sentential operator in the language, so it can be arbitrarily nested and combined with other logical operators. The language can represent the chance that facts hold and events occur at various times. It can represent the chance that actions and other events affect the future. The model of action distinguishes between action feasibility, executability, and effects. We present a proof theory for the logic and show how the logic can be used to describe actions in such a way that the action descriptions can be composed to infer properties of plans via the proof theory.