A More Expressive Behavioral Logic for Decision-Theoretic Planning

We examine the problem of compactly expressing models of non-Markovian reward decision processes (NMRDP). In the field of decision-theoretic planning NMRDPs are used whenever the agent's reward is determined by the history of visited states. Two different propositional linear temporal logics can be used to describe execution histories that are rewarding. Called PLTL and $FLTL, they are backward and forward looking logics respectively. In this paper we find both to be expressively weak and propose a change to $FLTL resulting in a much more expressive logic that we have called $* FLTL. The time complexities of $* FLTL and $FLTL related model checking operations performed in planning are the same.