Nonmarkovian control in dynamical systems and planning
Alfredo Gabaldon Royval · 2005
Building on Reiter's situation calculus Basic Action Theories, we consider generalizations that allow more flexible reasoning about the evolution of a dynamical system. First, we introduce nonMarkovian basic action theories, which generalize Reiter's action theories by allowing the axiomatization of a nonMarkovian system. By a nonMarkovian system we mean a system whose dynamics are such that the effects of actions on fluents and the preconditions of the actions are not necessarily fully determined by the current state of the system, but may also depend on the full system history. Furthermore, we generalize Reiter's regression operator, the main reasoning mechanism associated with Basic Action Theories, so that it can be utilized with nonMarkovian theories and, in general, with a class of situation calculus formulas that allow quantification over situation variables under some restrictions. Second, we introduce an operator for transforming nonMarkovian theories into Markovian basic action theories, which allows taking advantage of previous theoretical and implementation results applicable to formalisms that make the Markov assumption or that are inherently Markovian, such as state-based approaches. Third, we present two simple solutions to the qualification problem in presence of dynamic constraints: one resulting in a nonMarkovian action theory, and another one in a Markovian theory obtained by applying our transformation. Finally, we consider the problem of planning with declarative search control in the style of the TLPlan system. We introduce a procedure for obtaining precondition control from linear temporal logic search control formulas and prove that the preconditions obtained through this procedure prune a plan prefix if and only if the TLPlan system's progression algorithm eliminates the plan prefix. This procedure together with our transformation from nonMarkovian to Markovian theories provide a mechanism for computing precondition control, i.e., for compiling declarative search control into action preconditions.