In a seminal paper, Lin and Reiter introduced a model-theoretic definition for the progression of the initial knowledge base of a basic action theory. This definition comes with a strong negative result, namely that for certain kinds of action theories, first-order logic is not expressive enough to correctly characterize this form of progression, and second-order axioms are necessary. However, Lin and Reiter also considered an alternative definition for progression which is always first-order definable. They conjectured that this alternative definition is incorrect in the sense that the progressed theory is too weak and may sometimes lose information. This conjecture, and the status of first-order definable progression, has remained open since then. In this paper we present two significant results about this alternative definition of progression. First, we prove the Lin and Reiter conjecture by presenting a case where the progressed theory indeed does lose information. Second, we prove that the alternative definition is nonetheless correct for reasoning about a large class of sentences, including some that quantify over situations. In this case the alternative definition is a preferred option due to its simplicity and the fact that it is always first-order.

A great deal of research has addressed the problem of generating optimal plans, but these plans are of limited use in circumstances where noisy sensors, unanticipated exogenous actions, or imperfect models result in discrepancies between predicted and observed states of the world during plan execution. Such discrepancies bring into question the continued optimality of the plan being executed and, according to current-day practice, are resolved by aborting the plan and replanning, often unnecessarily. In this paper we address the problem of monitoring the continued optimality of a given plan at execution time, in the face of such discrepancies. While replanning cannot be avoided when critical aspects of the environment change, our objective is to avoid replanning unnecessarily. We address the problem by building on practical approaches to monitoring plan validity. We begin by formalizing plan validity in the situation calculus and characterizing common approaches to monitoring plan validity. We then generalize this characterization to the notion of plan optimality and propose an algorithm that verifies continued plan optimality. We have implemented our algorithm and tested it on simulated execution failures in well-known planning domains. Experimental results yield a significant speed-up in performance over the alternative of replanning, clearly demonstrating the merit of our approach.