TEMPORAL REASONING WITH THE MODAL LOGIC-Z

This article presents a formal theory of concurrent actions that handl es the qualification, ramification, and frame problems. The theory is capable of temporal explanation, i.e., reasoning forward and backward. The approach uses the modal logic Z to extend the work of Lifschitz a nd Rabinov on miracle-based temporal reasoning. The advantages of mira cles for describing unknown actions are augmented with the ability to handle concurrent actions that can provide for the most economical exp lanation of state changes. For temporal explanation problems restricte d to finite domains, it has a worst-case exponential decision procedur e. The theory is as general as first-order logic in what it can expres s as preconditions and consequences of actions.