\documentclass[11pt]{article}


\usepackage{theapa}
\usepackage{jair}
\usepackage{amssymb}
\usepackage{curves}
\usepackage{graphicx}
\usepackage{url}
\usepackage{algorithm}

\newcommand{\Omit}[1]{}

\newtheorem{definition}{Definition}
\newtheorem{proposition}{Proposition}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}
\newtheorem{property}{Property}

\newcommand{\theproof}[1]{{\bf Proof: } #1 \hspace*{\fill}$\Box$ \\ \mbox{}

}

\newcommand{\heads}{\mbox{heads}}


%temporal logic
\newcommand{\until}{\makebox[1em]{$\mathbin{\mbox{\sf U}}$}}
\newcommand{\always}{\mbox{$\Box$}}
\newcommand{\eventually}{\mbox{$\Diamond$}}
\newcommand{\balways}[1]{\mbox{$\Box_{#1}$}}
\newcommand{\beventually}[1]{\mbox{$\Diamond_{#1}$}}
\newcommand{\next}{\raisebox{0.6mm}{$\scriptstyle \bigcirc$}}
\newcommand{\reward}{\mathbin{\makebox[1em]{\sf R}}}
\newcommand{\dollar}{\mbox{\$}}
\newcommand{\valof}[2]{\mbox{$[\,#1\,]_{#2}$}}
\newcommand{\since}{\mathbin{\mbox{\sf S}}}
\newcommand{\last}{\circleddash}
\newcommand{\previously}{\makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}}
\newcommand{\alwaysPast}{\boxminus}
\newcommand{\xfltl}{\mbox{\dollar FLTL}}
\newcommand{\implies}{\rightarrow}
\newcommand{\xor}{\oplus}
\newcommand{\true}{\mbox{$\top$}}
\newcommand{\false}{\mbox{$\bot$}}
\newcommand{\tail}[1]{{\small\sf tail}(#1)}
\newcommand{\modelsb}[1]{\mbox{$\,\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize $#1$}}\:$}}
\newcommand{\notmodelsb}[1]{\mbox{$\,\not\models_{\!\!\!\raisebox{-0.7ex}{\scriptsize $#1$}}\:$}}
\newcommand{\restrict}[2]{\mbox{${#1}\Downarrow{#2}$}}

%MDPs 
\newcommand{\PP}{{\cal P}}
\newcommand{\RR}{{\cal R}}
\newcommand{\II}{{\cal I}}
\newcommand{\EE}{{\cal E}}
\newcommand{\FF}{{\cal F}}
\newcommand{\LL}{{\cal L}}
\newcommand{\T}{\Pr}
\newcommand{\TT}[2]{\Pr(#2,#1,\bullet)}
\newcommand{\TTT}[3]{\Pr(#2,#1,#3)}
\newcommand{\TP}{\Pr'}
\newcommand{\TTP}[2]{\Pr'(#2,#1,\bullet)}
\newcommand{\TTTP}[3]{\Pr'(#2,#1,#3)}


%CG: NMRDPP default strings for temporal operators.
\newcommand{\fut}{\until}
\newcommand{\fbx}{\always}
\newcommand{\fdi}{\eventually}
\newcommand{\nxt}{\next}
\newcommand{\snc}{\since}
\newcommand{\prv}{\last}

% functions
\newcommand{\E}{E}
\newcommand{\F}{F}
\newcommand{\Expect}{\makebox[1em]{$\mathbin{\mbox{\sf E}}$}}
\newcommand{\real}{\mbox{I$\!$R}}
\newcommand{\nat}{\mbox{I$\!$N}}
\newcommand{\wait}{\mbox{\sc null}}
\newcommand{\size}[1]{||#1||}
\newcommand{\kwd}[1]{\mbox{\sf #1\/}}
\newcommand{\Ind}[2]{\makebox[20pt][r]{#1.}~\hspace*{#2em}}
\newcommand{\Prog}{\mbox{Prog}}
\newcommand{\MProg}{\mbox{\em Prog}}
\newcommand{\Reg}{\mbox{Reg}}
\newcommand{\MReg}{\mbox{\em Reg}}
\newcommand{\SProg}{\mbox{R}\Prog}
\newcommand{\MSProg}{\mbox{{\em R}\MProg}}
\newcommand{\Rew}{\mbox{Rew}}
\newcommand{\MRew}{\mbox{\em Rew}}
\newcommand{\Sub}{\mbox{Sub}}
\newcommand{\MSub}{\mbox{\em Sub}}
\newcommand{\PTSub}{\mbox{PTSub}}
\newcommand{\MPTSub}{\mbox{\em PTSub}}
\newcommand{\NN}[1]{\overline{#1}}

%methods names
\newcommand{\pltlmin}{{\sc pltlmin}}
\newcommand{\pltlsimp}{{\sc pltlsim}}
\newcommand{\pltlstruct}{{\sc pltlstr}}
\newcommand{\pltlstrauto}{{\sc pltlstr(a)}}
\newcommand{\fltl}{{\sc fltl}}
\newcommand{\fltllao}{{\sc fltl}}

%problem names
\newcommand{\spuddlinear}{{\sc spudd-linear}}
\newcommand{\spuddexpon}{{\sc spudd-expon}}
\newcommand{\balls}{{\sc on/off}}
\newcommand{\complete}{{\sc complete}}

\jairheading{25}{2006}{17-74}{12/04}{01/06}
\ShortHeadings{Decision-Theoretic Planning with non-Markovian Rewards}{Thi\'ebaux, Gretton, Slaney, Price \& Kabanza}
\firstpageno{17}


\newcommand{\nmrdpp}{{\sc nmrdpp}}
\newcommand{\mdpsim}{{\sc mdpsim}}
\newcommand{\mtbdd}{{\sc mtbdd}}

\newcommand{\nega}{---}
\newcommand{\none}{}
\begin{document}

\title{Decision-Theoretic Planning with non-Markovian Rewards}


\author{\name Sylvie Thi\'ebaux
  \email Sylvie.Thiebaux@anu.edu.au\\
  \name Charles Gretton
  \email Charles.Gretton@anu.edu.au\\
  \name John Slaney
  \email John.Slaney@anu.edu.au\\
  \name David Price
  \email David.Price@anu.edu.au\\
  \addr National ICT Australia \&\\ 
  The Australian National University\\
  Canberra, ACT 0200, Australia\\~\\  
  \name Froduald Kabanza
  \email kabanza@usherbrooke.ca\\
  \addr D\'epartement d'Informatique\\
  Universit\'e de Sherbrooke\\
  Sherbrooke, Qu\'ebec J1K 2R1, Canada}


\maketitle

\begin{abstract}
A decision process in which rewards depend on history rather than
merely on the current state is called a decision process with
non-Markovian rewards (NMRDP).  In decision-theoretic planning, where
many desirable behaviours are more naturally expressed as properties
of execution sequences rather than as properties of states, NMRDPs
form a more natural model than the commonly adopted fully Markovian
decision process (MDP) model.  While the more tractable solution
methods developed for MDPs do not directly apply in the presence of
non-Markovian rewards, a number of solution methods for NMRDPs have
been proposed in the literature. These all exploit a compact
specification of the non-Markovian reward function in temporal logic,
to automatically translate the NMRDP into an equivalent MDP which is
solved using efficient MDP solution methods.
%
This paper presents \nmrdpp (Non-Markovian Reward Decision Process
Planner), a software platform for the development
and experimentation of methods for decision-theoretic planning with
non-Markovian rewards. The current version of \nmrdpp\ implements,
under a single interface, a family of methods based on existing as
well as new approaches which we describe in detail. These include
dynamic programming, heuristic search, and structured
methods.  Using \nmrdpp, we compare the methods and identify certain
problem features that affect their performance.
%
\nmrdpp's treatment of non-Markovian rewards is inspired by the
treatment of domain-specific search control knowledge in the TLPlan
planner, which it incorporates as a special case.  In the First
International Probabilistic Planning Competition, \nmrdpp\ was able to
compete and perform well in both the domain-independent and hand-coded
tracks, using search control knowledge in the latter.
\end{abstract}

\newpage

\section{Introduction}
\label{sec:intro}

\subsection{The Problem}

Markov decision processes (MDPs) are now widely accepted as the
preferred model for decision-theoretic planning problems
\cite{boutilier:etal:99}. The fundamental assumption behind the MDP
formulation is that not only the system dynamics but also the reward
function are {\em Markovian}. Therefore, all information needed to
determine the reward at a given state must be encoded in the state
itself.

This requirement is not always easy to meet for planning problems, as
many desirable behaviours are naturally expressed as properties of
execution {\em sequences} \cite<see
e.g.,>{drummond:89,haddawy:hanks:92,bacchus:kabanza:98,pistore:traverso:01}.
Typical cases include rewards for the maintenance of some property,
for the periodic achievement of some goal, for the achievement of a
goal within a given number of steps of the request being made, or even
simply for the very first achievement of a goal which becomes
irrelevant afterwards.

For instance, consider a health care robot which assists ederly or
disabled people by achieving simple goals such as reminding them to do
important tasks (e.g. taking a pill), entertaining them, checking or
transporting objects for them (e.g. checking the stove's temperature
or bringing coffee), escorting them, or searching (e.g. for glasses or
for the nurse) \shortcite{cesta:etal:03}. In this domain, we might
want to reward the robot for making sure a given patient takes his
pill exactly once every 8 hours (and penalise it if it fails to
prevent the patient from doing this more than once within this time
frame!), we may reward it for repeatedly visiting all rooms in the
ward in a given order and reporting any problem it detects, it may
also receive a reward once for each patient's request answered within
the appropriate time-frame, etc.
%
Another example is the elevator control domain
\cite{koehler:schuster:00}, in which an elevator must get passengers
from their origin to their destination as efficiently as possible,
while attempting to satisfying a range of other conditions such as
providing priority services to critical customers. In this domain,
some trajectories of the elevator are more desirable than others,
which makes it natural to encode the problem by assigning rewards to
those trajectories.


 A decision process in which rewards depend on
the sequence of states passed through rather than merely on the
current state is called a decision process with {\em non-Markovian
  rewards} (NMRDP) \cite{bacchus:etal:96}.
A difficulty with NMRDPs is that the most efficient MDP solution
methods do not directly apply to them. The traditional way to
circumvent this problem is to formulate the NMRDP as an equivalent
MDP, whose states result from augmenting those of the original NMRDP
with extra information capturing enough history to make the reward
Markovian. Hand crafting such an MDP can however be very difficult in
general. This is exacerbated by the fact that the size of the MDP
impacts the effectiveness of many solution methods. Therefore,
there has been interest in automating the translation into an MDP,
starting from a natural specification of non-Markovian rewards and of
the system's dynamics \cite{bacchus:etal:96,bacchus:etal:97}. This is
the problem we focus on.

\subsection{Existing Approaches}

When solving NMRDPs in this setting, the central issue is to define a
non-Markovian reward specification language and a translation into an
MDP {\em adapted} to the class of MDP solution methods and
representations we would like to use for the type of problems at hand.
More precisely, there is a tradeoff between the effort spent in the
translation, e.g.\ in producing a {\em small} equivalent MDP without
many irrelevant history distinctions, and the effort required to solve
it. Appropriate resolution of this tradeoff depends on the type of
representations and solution methods envisioned for the MDP.  For
instance, {\em structured}\ representations and solution methods which
have some ability to ignore irrelevant information may cope with a
crude translation, while {\em state-based}\ (flat) representations and
methods will require a more sophisticated translation producing an MDP
as small as feasible.


Both the two previous proposals within this line of research rely on
past linear temporal logic (PLTL) formulae to specify the behaviours
to be rewarded \cite{bacchus:etal:96,bacchus:etal:97}. A nice feature
of PLTL is that it yields a straightforward semantics of non-Markovian
rewards, and lends itself to a range of translations from the crudest
to the finest. The two proposals adopt very different translations
adapted to two very different types of solution methods and
representations. The first \cite{bacchus:etal:96} targets classical
state-based solution methods such as policy iteration \cite{howard:60}
which generate {\em complete} policies at the cost of enumerating all
states in the entire MDP. Consequently, it adopts an expensive
translation which attempts to produce a {\em minimal}\ MDP. By
contrast, the second translation \cite{bacchus:etal:97}\ is very
efficient but crude, and targets structured solution methods and
representations \cite<see
e.g.,>{hoey:etal:99,boutilier:etal:00,feng:hansen:02}, which do not
require explicit state enumeration.


\subsection{A New Approach}

The first contribution of this paper is to provide a language and a
translation adapted to another class of solution methods which have
proven quite effective in dealing with large MDPs, namely {\em
anytime} state-based heuristic search methods such as LAO*
\cite{hansen:zilberstein:01}, LRTDP \cite{bonet:geffner:03}, and
ancestors \cite{barto:etal:95,dean:etal:95,thiebaux:etal:95}.  These
methods typically start with a compact representation of the MDP based
on probabilistic planning operators, and search forward from an
initial state, constructing new states by expanding the envelope of
the policy as time permits. They may produce an approximate and even
incomplete policy, but explicitly construct and explore only a
fraction of the MDP. Neither of the two previous proposals is
well-suited to such solution methods, the first because the cost of
the translation (most of which is performed prior to the solution
phase) annihilates the benefits of anytime algorithms, and the second
because the size of the MDP obtained is an obstacle to the
applicability of state-based methods.  Since here both the cost of the
translation and the size of the MDP it results in will severely impact
on the quality of the policy obtainable by the deadline, we need an
appropriate resolution of the tradeoff between the two.

Our approach has the following main features.  The translation is
entirely embedded in the anytime solution method, to which full
control is given as to which parts of the MDP will be explicitly
constructed and explored.  While the MDP obtained is not minimal, it
is of the minimal size achievable without stepping outside of the
anytime framework, i.e., without enumerating parts of the state space
that the solution method would not necessarily explore.  We formalise
this relaxed notion of minimality, which we call {\em blind
minimality}\ in reference to the fact that it does not require any
lookahead (beyond the fringe). This is appropriate in the context of anytime
state-based solution methods, where we want the minimal MDP achievable
without expensive pre-processing.
  


When the rewarding behaviours are specified in PLTL, there does not
appear to be a way of achieving a relaxed notion of minimality as
powerful as blind minimality without a prohibitive translation.
Therefore instead of PLTL, we adopt a variant of {\em future} linear
temporal logic (FLTL) as our specification language, which we extend
to handle rewards. While the language has a more complex semantics
than PLTL, it enables a natural translation into a blind-minimal MDP
by simple {\em progression} of the reward formulae.  Moreover, search
control knowledge expressed in FLTL \cite{bacchus:kabanza:00}\ fits
particularly nicely in this framework, and can be used to dramatically
reduce the fraction of the search space explored by the solution
method.

\subsection{A New System}

Our second contribution is \nmrdpp, the first reported implementation
of NMRDP solution methods. \nmrdpp\ is designed as a software platform
for their development and experimentation under a common interface.
Given a description of the actions in a domain, \nmrdpp\ lets the user
play with and compare various encoding styles for non-Markovian
rewards and search control knowledge, various translations of the
resulting NMRDP into MDP, and various MDP solution methods.  While
solving the problem, it can be made to record a range of statistics
about the space and time behaviour of the algorithms.  It also
supports the graphical display of the MDPs and policies generated.

While \nmrdpp's primary interest is in the treatment of non-Markovian
rewards, it is also a competitive platform for decision-theoretic
planning with purely Markovian rewards. In the First International
Probabilistic Planning Competition, \nmrdpp\ was able to enrol in both
the domain-independent and hand-coded tracks, attempting all problems
featuring in the contest. Thanks to its use of search
control-knowledge, it scored a second place in the hand-coded track
which featured probabilistic variants of blocks world and logistics
problems.  More surprisingly, it also scored second in the
domain-independent subtrack consisting of all problems that were {\em
not} taken from the blocks world and logistic domains.  Most of these
latter problems had not been released to the participants prior to the
competition.


\subsection{A New Experimental Analysis}

Our third contribution is an experimental analysis of the factors that
affect the performance of NMRDP solution methods.  Using \nmrdpp, we
compared their behaviours under the influence of parameters such as
the structure and degree of uncertainty in the dynamics, the type of
rewards and the syntax used to described them, reachability of the
conditions tracked, and relevance of rewards to the optimal policy.
We were able to identify a number of general trends in the behaviours
of the methods and provide advice concerning which are best suited in
certain circumstances. Our experiments also lead us to rule out one of
the methods as systematically underperforming, and to identify issues
with the claim of minimality made by one of the PLTL approaches.


\subsection{Organisation of the Paper}

The paper is organised as follows. Section~\ref{sec:background}\
begins with background material on MDPs, NMRDPs, and existing
approaches.  Section~\ref{sec:new}\ describes our new approach and
Section~\ref{sec:nmrdpp}\ presents \nmrdpp.
Sections~\ref{sec:experiments}\ and~\ref{sec:concrete}\ report our
experimental analysis of the various approaches.
Section~\ref{sec:competition}\ explains how we used \nmrdpp\ in the
competition.  Section~\ref{sec:conclusion}\ concludes with remarks
about related and future work.  Appendix~\ref{app:proofs}\ gives the
proofs of the theorems. Most of the material presented is compiled
from a series of recent conference and workshop papers
\cite{thiebaux:etal:02,thiebaux:etal:02:mochart,gretton:etal:03,gretton:etal:03:icaps}. Details
of the logic we use to represent rewards may be found in our 2005
paper \cite{slaney:05}.

\section{Background}
\label{sec:background}


\subsection{MDPs, NMRDPs, Equivalence}

We start with some notation and definitions. Given a finite set $S$ of
states, we write $S^*$ for the set of finite sequences of states over
$S$, and $S^\omega$ for the set of possibly infinite state sequences.
Where `$\Gamma$' stands for a possibly infinite state sequence in
$S^\omega$ and $i$ is a natural number, by `$\Gamma_i$' we mean the
state of index $i$ in $\Gamma$, by `$\Gamma(i)$' we mean the prefix
$\langle \Gamma_0, \ldots, \Gamma_i \rangle \in S^{*}$ of $\Gamma$.
$\Gamma;\Gamma'$ denotes the concatenation of $\Gamma\in S^*$ and
$\Gamma' \in S^\omega$.



\subsubsection{MDPs}

A Markov decision process of the type we consider is a 5-tuple
$\langle S,s_0,A,\T,R\rangle$, where $S$ is a finite set of fully
observable states, $s_{0}\in S$ is the initial state, $A$ is a finite
set of actions ($A(s)$ denotes the subset of actions applicable in
$s\in S$), $\{\TT{a}{s} \mid s\!\in\!S, a\!\in\!A(s)\}$ is a family of
probability distributions over $S$, such that $\TTT{a}{s}{s'}$ is the
probability of being in state $s'$ after performing action $a$ in
state $s$, and $R: S \mapsto \real$ is a reward function such that
$R(s)$ is the immediate reward for being in state $s$.  It is well
known that such an MDP can be compactly represented using dynamic
Bayesian networks \cite{dean:kanazawa:89,boutilier:etal:99}\ or
probabilistic extensions of traditional planning languages
\cite<see e.g.,>{kushmerick:etal:95,thiebaux:etal:95,younes:littman:04}.

A stationary policy for an MDP is a function $\pi : S \mapsto A$, such
that $\pi(s)\in A(s)$ is the action to be executed in state $s$.  The
value $V_\pi$ of the policy at $s_0$, which we seek to maximise, is
the sum of the expected future rewards over an infinite horizon,
discounted by how far into the future they occur:
\[
V_\pi(s_0) = \lim_{n\rightarrow\infty} \Expect \bigg{[} 
\sum_{i=0}^{n} \beta^{i} R(\Gamma_i) \mid \pi, \Gamma_{0} = s_{0} \bigg{]}
\]
where $0 \leq \beta < 1$ is the discount factor controlling the
contribution of distant rewards. 

\subsubsection{NMRDPs}

A decision process with non-Markovian rewards is identical to an MDP
except that the domain of the reward function is $S^{*}$. The idea is
that if the process has passed through state sequence $\Gamma(i)$ up
to stage $i$, then the reward $R(\Gamma(i))$ is received at stage
$i$. Figure~\ref{fig:NMRDP}\ gives an example. Like the reward
function, a policy for an NMRDP depends on history, and is a mapping
from $S^{*}$ to $A$. As before, the value of policy $\pi$ is the
expectation of the discounted cumulative reward over an infinite
horizon:
\[
V_{\pi}(s_{0}) = \lim_{n\rightarrow\infty} \Expect \bigg{[} 
\sum_{i=0}^{n} \beta^{i} R(\Gamma(i)) \mid \pi, \Gamma_{0} = s_{0} \bigg{]}
\]

For a decision process $D=\langle S,s_0,A,\T,R\rangle$ and a state $s\in
S$, we let $\widetilde{D}(s)$ stand for the set of state sequences rooted at
$s$ that are {\em feasible} under the actions in $D$, that is:
$\widetilde{D}(s) = \{ \Gamma\in S^\omega \mid \Gamma_0 = s
\mbox{~and~}\forall i~\exists a \in A(\Gamma_i)~~
\TTT{a}{\Gamma_{i}}{\Gamma_{i+1}} > 0 \}$. Note that the definition of
$\widetilde{D}(s)$ does not depend on $R$ and therefore applies
to both MDPs and NMRDPs.

\setlength{\unitlength}{5.5mm}
\newcommand{\astate}[2]{\put(#1){\bigcircle{1}}
                        \put(#1){\makebox(0,0){#2}}}

\begin{figure}[t]
\centering
\begin{picture}(0,8)(0,-4)
%
\put(-8.4,0){\begin{picture}(0,0)(0,0)
\astate{0,3}{{\footnotesize $s_0$}}
\astate{0,-1}{{\footnotesize $s_1$}}
%
\put(0,-0.5){\vector(0,1){3}}
\put(-0.3,1){\makebox(0,0){{\footnotesize $d$}}}
\put(0.5,1){\makebox(0,0){{\footnotesize 1.0}}}
%
\put(0.354,2.646){\line(1,-1){0.646}}
\put(-0.25,0.75){\arc(1.25,1.25){-110}} \put(0.48,-0.87){\vector(-4,-3){0}}
\put(2.81,2.75){\line(0,1){0.5}}
\put(1.75,2.75){\arc(-0.75,-0.75){135}}
\put(1.75,3.25){\arc(-0.75,0.75){-135}}
\put(1,4){\vector(-1,-1){0.646}}
\put(-1,2.5){\makebox(0,0){{\footnotesize $a$}}}
\put(-2,0.5){\makebox(0,0){{\footnotesize 0.1}}}
\put(-2.5,1.5){\makebox(0,0){{\footnotesize 0.9}}}
%
\put(-0.354,2.646){\line(-1,-1){0.646}}
\put(0.25,0.75){\arc(-1.25,1.25){110}} \put(-0.48,-0.87){\vector(4,-3){0}}
\put(-2.81,2.75){\line(0,1){0.5}}
\put(-1.75,2.75){\arc(0.75,-0.75){-135}}
\put(-1.75,3.25){\arc(0.75,0.75){135}}
\put(-1,4){\vector(1,-1){0.646}}
\put(1,2.5){\makebox(0,0){{\footnotesize $b$}}}
\put(2,0.5){\makebox(0,0){{\footnotesize 0.5}}}
\put(2.5,1.5){\makebox(0,0){{\footnotesize 0.5}}}
%
\put(-0.354,-1.354){\line(-1,-1){0.646}}
\put(1,-2){\vector(-1,1){0.646}}
\put(-0.5,-3.2125){\line(1,0){1}}
\put(-0.5,-2.5){\arc(-0.5,0.5){135}}
\put(0.5,-2.5){\arc(0.5,0.5){-135}}
\put(-1,-1.5){\makebox(0,0){{\footnotesize $c$}}}
\put(0,-2.8){\makebox(0,0){{\footnotesize 1.0}}}
\end{picture}}
%
\put(-0.8,4){
\parbox[t]{0.52\textwidth}{\footnotesize
  In the initial state $s_0$, $p$ is false and two actions are possible: $a$
  causes a transition to $s_1$ with probability 0.1, and no change with
  probability 0.9, while for $b$ the transition probabilities are 0.5. In
  state $s_1$, $p$ is true, and actions $c$ and $d$ (``stay'' and ``go'') lead
  to $s_1$ and $s_0$ respectively with probability 1.

  A reward is received the first time $p$ is true, but not
  subsequently. That is, the rewarded state sequences are:\\
  \hspace*{2em} $\langle s_0,s_1 \rangle$ \\
  \hspace*{2em} $\langle s_0,s_0,s_1 \rangle$ \\
  \hspace*{2em} $\langle s_0,s_0,s_0,s_1 \rangle$ \\
  \hspace*{2em} $\langle s_0,s_0,s_0,s_0,s_1 \rangle$
  \hspace*{1em} etc.
%
}}
\end{picture}

\caption{\label{fig:NMRDP}A Simple NMRDP}
\end{figure}

\subsubsection{Equivalence}

The clever algorithms developed to solve MDPs cannot be directly
applied to NMRDPs. One way of dealing with this problem is to
translate the NMRDP into an equivalent MDP with an expanded state
space \cite{bacchus:etal:96}. The expanded states in this MDP
(\emph{e-states}, for short) augment the states of the NMRDP by
encoding additional information sufficient to make the reward
history-independent. For instance, if we only want to reward the very
first achievement of goal $g$ in an NMRDP, the states of an equivalent
MDP would carry one extra bit of information recording whether $g$ has
already been true.  An e-state can be seen as labelled by a state of
the NMRDP (via the function $\tau$ in Definition~\ref{def:equivalent}
below) and by history information. The dynamics of NMRDPs being
Markovian, the actions and their probabilistic effects in the MDP are
exactly those of the NMRDP. The following definition, adapted from
that given by Bacchus et al.\ \citeyear{bacchus:etal:96},
makes this concept of equivalent MDP precise. Figure~\ref{fig:XMDP}\
gives an example.


\begin{definition}
\label{def:equivalent}
MDP $D'\!\!=\!\!\langle S',s'_{0},A',\TP\!,R'\rangle$ is equivalent
to NMRDP $D=\langle S,s_{0},A,\T,R\rangle$ if there
exists a mapping $\tau : S' \mapsto S$ such that:\footnote{Technically, the definition allows the sets of actions
$A$ and $A'$ to be different, but any action in which they differ must be
inapplicable in reachable states in the NMRDP and in all e-states in
the equivalent MDP.  For all practical purposes, $A$ and $A'$ can be seen as
identical.}\\[-4ex]\mbox{}
\begin{enumerate}
\item $\tau(s'_{0}) = s_{0}.$\\[-1ex]\mbox{}
\item For all $s' \in S'$, $A'(s')= A(\tau(s'))$.\\[-1ex]\mbox{}
\item For all $s_1,s_2\in S$, if there is
$a\in A(s_1)$ such that $\TTT{a}{s_1}{s_2} > 0$, then for all
$s_1'\in S'$ such that $\tau(s_1')= s_1$, there exists a
unique $s_2' \in S'$, $\tau(s'_2) = s_2$, such that for
all $a'\in A'(s'_1)$,
$\TTTP{a'}{s'_1}{s'_2}\!=\!\TTT{a'}{s_1}{s_2}$.\\[-1ex]\mbox{}
\item For any feasible state sequence $\Gamma \in \widetilde{D}(s_0)$
and $\Gamma' \in \widetilde{D}'(s'_0)$ such that $\tau(\Gamma'_{i}) =
\Gamma_{i}$ for all $i$, we have: $R'(\Gamma'_{i}) = R(\Gamma(i))$ for
all $i$.\\[-1ex]\mbox{}
\end{enumerate}
\end{definition}
Items 1--3 ensure that there is a bijection between feasible state
sequences in the NMRDP and feasible e-state sequences in the MDP.
Therefore, a stationary policy for the MDP can be reinterpreted as a
non-stationary policy for the NMRDP. Furthermore, item 4 ensures that
the two policies have identical values, and that consequently, solving
an NMRDP optimally reduces to producing an equivalent MDP and solving
it optimally \cite{bacchus:etal:96}:
\begin{proposition}
  Let $D$ be an NMRDP, $D'$ an equivalent MDP for it, and $\pi'$ a policy for
  $D'$. Let $\pi$ be the function defined on the sequence prefixes
  $\Gamma(i)\in \widetilde{D}(s_{0})$ by $\pi(\Gamma(i)) = \pi'(\Gamma'_i)$, where
  for all $j\leq i~\tau(\Gamma'_{j})=\Gamma_{j}$. Then $\pi$ is a policy for
  $D$ such that $V_{\pi}(s_0) = V_{\pi'}(s'_0)$.
\end{proposition}


\begin{figure}[t]
\centering
\begin{picture}(0,9.5)(0,-4.5)
%
\put(2,-1){\begin{picture}(0,0)(0,0)
\astate{3,0}{{\footnotesize $s'_0$}}
\astate{-1,0}{{\footnotesize $s'_1$}}
%
\put(2.646,0.354){\line(-1,1){0.646}}
\put(0.75,-0.25){\arc(1.25,1.25){110}} \put(-0.87,0.48){\vector(-3,-4){0}}
\put(2.75,2.81){\line(1,0){0.5}}
\put(2.75,1.75){\arc(-0.75,-0.75){-135}}
\put(3.25,1.75){\arc(0.75,-0.75){135}}
\put(4,1){\vector(-1,-1){0.646}}
\put(2.5,-1){\makebox(0,0){{\footnotesize $a$}}}
\put(0.5,-2){\makebox(0,0){{\footnotesize 0.1}}}
\put(1.5,-2.5){\makebox(0,0){{\footnotesize 0.9}}}
%
\put(2.646,-0.354){\line(-1,-1){0.646}}
\put(0.75,0.25){\arc(1.25,-1.25){-110}} \put(-0.87,-0.48){\vector(-3,4){0}}
\put(2.75,-2.81){\line(1,0){0.5}}
\put(2.75,-1.75){\arc(-0.75,0.75){135}}
\put(3.25,-1.75){\arc(0.75,0.75){-135}}
\put(4,-1){\vector(-1,1){0.646}}
\put(2.5,1){\makebox(0,0){{\footnotesize $b$}}}
\put(0.5,2){\makebox(0,0){{\footnotesize 0.5}}}
\put(1.5,2.5){\makebox(0,0){{\footnotesize 0.5}}}
%
\put(-1.5,0){\vector(-1,0){3.5}}
\put(-2,-0.3){\makebox(0,0){{\footnotesize $c$}}}
\put(-1.3,1.5){\makebox(0,0){{\footnotesize $d$}}}
%
\end{picture}}
%

\put(-1.25,4){\oval(4.5,2)[t]}
\put(-3.5,4){\vector(0,-1){0.5}}
\put(1,-0.5){\line(0,1){4.5}}

%
\put(-3.5,0){\begin{picture}(0,0)(0,0)
\astate{0,3}{{\footnotesize $s'_2$}}
\astate{0,-1}{{\footnotesize $s'_3$}}
%
\put(0,-0.5){\vector(0,1){3}}
\put(-0.3,1){\makebox(0,0){{\footnotesize $d$}}}
\put(0.5,1){\makebox(0,0){{\footnotesize 1.0}}}
%
\put(0.354,2.646){\line(1,-1){0.646}}
\put(-0.25,0.75){\arc(1.25,1.25){-110}} \put(0.48,-0.87){\vector(-4,-3){0}}
\put(2.81,2.75){\line(0,1){0.5}}
\put(1.75,2.75){\arc(-0.75,-0.75){135}}
\put(1.75,3.25){\arc(-0.75,0.75){-135}}
\put(1,4){\vector(-1,-1){0.646}}
\put(-1,2.5){\makebox(0,0){{\footnotesize $a$}}}
\put(-2,0.5){\makebox(0,0){{\footnotesize 0.1}}}
\put(-2.5,1.5){\makebox(0,0){{\footnotesize 0.9}}}
%
\put(-0.354,2.646){\line(-1,-1){0.646}}
\put(0.25,0.75){\arc(-1.25,1.25){110}} \put(-0.48,-0.87){\vector(4,-3){0}}
\put(-2.81,2.75){\line(0,1){0.5}}
\put(-1.75,2.75){\arc(0.75,-0.75){-135}}
\put(-1.75,3.25){\arc(0.75,0.75){135}}
\put(-1,4){\vector(1,-1){0.646}}
\put(1,2.5){\makebox(0,0){{\footnotesize $b$}}}
\put(2,0.5){\makebox(0,0){{\footnotesize 0.5}}}
\put(2.5,1.5){\makebox(0,0){{\footnotesize 0.5}}}
%
\put(-0.354,-1.354){\line(-1,-1){0.646}}
\put(1,-2){\vector(-1,1){0.646}}
\put(-0.5,-3.2125){\line(1,0){1}}
\put(-0.5,-2.5){\arc(-0.5,0.5){135}}
\put(0.5,-2.5){\arc(0.5,0.5){-135}}
\put(-1.2,-1.8){\makebox(0,0){{\footnotesize $c$}}}
\put(0,-2.8){\makebox(0,0){{\footnotesize 1.0}}}
%
\end{picture}}
%
\end{picture}
%

\caption{\label{fig:XMDP}An MDP Equivalent to the NMRDP in Figure
  \ref{fig:NMRDP}. $\tau(s'_0) = \tau(s'_2) = s_0$. $\tau(s'_1) = \tau(s'_3)
  = s_1$. The initial state is $s'_0$. State $s'_1$ is rewarded; the other
  states are not.}
\end{figure}


\subsection{Existing Approaches}
\label{subsec:previous}
Both existing approaches to NMRDPs
\cite{bacchus:etal:96,bacchus:etal:97}\ use a temporal logic of the
past (PLTL) to compactly represent non-Markovian rewards and
exploit this compact representation to translate the NMRDP into an MDP
amenable to off-the-shelf solution methods. However, they target
different classes of MDP representations and 
solution methods, and consequently, adopt
different styles of translations.

Bacchus et al.\ \citeyear{bacchus:etal:96}\ target state-based MDP
representations. The equivalent MDP is first generated entirely -- this
involves the enumeration of all e-states and all transitions between
them.  Then, it is solved using traditional dynamic programming
methods such as value or policy iteration. Because these methods are
extremely sensitive to the number of states, attention is paid to
producing a minimal equivalent MDP (with the least number of states).
A first simple translation which we call \pltlsimp\ produces a large
MDP which can be post-processed for minimisation before being solved.
Another, which we call \pltlmin, directly results in a minimal MDP,
but relies on an expensive pre-processing phase.

The second approach \cite{bacchus:etal:97}, which we call \pltlstruct,
targets structured MDP representations: the transition model,
policies, reward and value functions are represented in a compact
form, e.g. as trees or algebraic decision diagrams (ADDs)
\cite{hoey:etal:99,boutilier:etal:00}. For instance, the probability
of a given proposition (state variable) being true after the execution
of an action is specified by a tree 
whose internal nodes are labelled with the state variables on
whose previous values the given variable depends, whose arcs are
labelled by the possible previous values ($\true$ or $\false$) of
these variables, and whose leaves are labelled with
probabilities.   The translation amounts to augmenting the structured
MDP with new {\em temporal}
variables tracking the relevant properties of state sequences,
together with the compact representation of (1) their
dynamics, e.g.\ as trees over the previous values of relevant
variables, and (2) of the non-Markovian reward function in terms of
the variables' current values. Then, structured solution methods such
as structured policy iteration or the SPUDD algorithm are run on the
resulting structured MDP. Neither the translation nor the solution
methods explicitly enumerates the states.

We now review these approaches in some detail.
The reader is referred to the respective papers for additional
information.

\subsubsection{Representing Rewards with PLTL}
The syntax of PLTL, the language chosen to represent rewarding
behaviours, is that of propositional logic, augmented with the
operators $\last$ (previously) and $\since$ (since)
\cite<see>{emerson:90}. Whereas a classical propositional logic formula
denotes a set of states (a subset of $S$), a PLTL formula denotes a
set of finite {\em sequences} of states (a subset of $S^*$). A formula
without temporal modality expresses a property that must be true of
the current state, i.e., the last state of the finite sequence.
$\last f$ specifies that $f$ holds in the previous state (the state
one before the last).  $f_1 \since f_2$, requires $f_2$ to have been
true at some point in the sequence, and, unless that point is the present,
$f_1$ to have held ever since. More formally, the modelling relation 
$\models$ stating whether a formula $f$ holds of a finite sequence 
$\Gamma(i)$ is defined recursively as follows:
%
\begin{itemize}
\item $\Gamma(i) \models p$ iff $p\in\Gamma_i$, for $p\in {\cal P}$, the set
of atomic propositions
\item $\Gamma(i) \models \neg f$ iff $\Gamma(i)\not\models f$
\item $\Gamma(i) \models f_1 \wedge f_2$ iff $\Gamma(i) \models f_1$ 
and $\Gamma(i) \models f_2$
\item $\Gamma(i) \models \last f$ iff $i > 0$ and $\Gamma(i-1)
\models f$
\item $\Gamma(i) \models f_1 \since f_2$ iff $\exists
j \leq i, \Gamma(j) \models f_2$ and $\forall k, j<k\leq i,
\Gamma(k) \models f_1$
\end{itemize}
%
From $\since$, one can define the useful operators $\previously f
\equiv \true \since f$ meaning that $f$ has been true at some point,
and $\alwaysPast f \equiv \neg\previously\neg f$ meaning that $f$ has
always been true. E.g, $g \wedge \neg\last\previously g$ denotes the
set of finite sequences ending in a state where $g$ is true for the
first time in the sequence. Other useful abbreviation are $\last^k$
($k$ times ago), for $k$ iterations of the $\last$ modality,
$\previously_k f$ for $\vee_{i=1}^{k} \last^i f$ ($f$ was true at some
of the $k$ last steps), and $\alwaysPast_k f$ for $\wedge_{i=1}^{k}
\last^i f$ ($f$ was true at all the $k$ last steps).

Non-Markovian reward functions are described with a set of pairs $(f_i
: r_i)$ where $f_i$ is a PLTL reward formula and $r_i$ is a real, with
the semantics that the reward assigned to a sequence in $S^*$ is the
sum of the $r_i$'s for which that sequence is a model of $f_i$. Below,
we let $\F$ denote the set of reward formulae $f_i$ in the description
of the reward function. Bacchus et al.\ \citeyear{bacchus:etal:96}\
give a list of behaviours which it might be useful to reward, together
with their expression in PLTL.  For instance, where $f$ is an
atemporal formula, $(f: r)$ rewards with $r$ units the achievement of
$f$ whenever it happens. This is a Markovian reward. In contrast
$(\previously f : r)$ rewards every state following (and including)
the achievement of $f$, while $(f \wedge \neg\last\previously f: r)$
only rewards the first occurrence of $f$.  $(f \wedge \alwaysPast_k
\neg f: r)$ rewards the occurrence of $f$ at most once every $k$
steps. $(\last^n \neg \last \false: r)$ rewards the $n^{\mbox{th}}$
state, independently of its properties.  $(\last^2 f_1 \wedge \last
f_2 \wedge f_3 :r)$ rewards the occurrence of $f_1$ immediately
followed by $f_2$ and then $f_3$.  In reactive planning, so-called
{\em response} formulae which describe that the achievement of $f$ is
triggered by a condition (or command) $c$ are particularly useful.
These can be written as $(f \wedge \previously c: r)$ if every state
in which $f$ is true following the first issue of the command is to be
rewarded. Alternatively, they can be written as $(f \wedge \last (\neg
f \since c) : r)$ if only the first occurrence of $f$ is to be
rewarded after each command. It is common to only reward the
achievement $f$ within $k$ steps of the trigger; we write for example
$(f \wedge \previously_k c : r)$ to reward all such states in which
$f$ holds.


From a theoretical point of view, it is known
\cite{lichtenstein:etal:85} that the behaviours representable in PLTL
are exactly those corresponding to star-free regular languages. Non
star-free behaviours such as $(pp)*$ (reward an even number of states
all containing $p$) are therefore not representable. Nor, of course,
are non-regular behaviours such as $p^nq^n$ (e.g.\ reward taking equal
numbers of steps to the left and right). We shall not speculate here
on how severe a restriction this is for the purposes of planning.


\subsubsection{Principles Behind the Translations}

All three translations into an MDP (\pltlsimp, \pltlmin, and
\pltlstruct) rely on the equivalence $\mbox{$f_1 \since f_2$} \equiv
f_2 \vee (f_1 \wedge \last(f_1 \since f_2))$, with which we can
decompose temporal modalities into a requirement about the last state
$\Gamma_i$ of a sequence $\Gamma(i)$, and a requirement about the
prefix $\Gamma(i-1)$ of the sequence. More precisely, given state $s$
and a formula $f$, one can compute in\footnote{The size $\size{f}$ of
a reward formula is measured as its length and the size $\size{F}$ of
a set of reward formulae $F$ is measured as the sum of the lengths of
the formulae in $F$.}  ${\cal O}(\size{f})$ a new formula $\Reg(f,s)$
called the regression of $f$ through $s$.  Regression has the property
that, for $i>0$, $f$ is true of a finite sequence $\Gamma(i)$ ending
with $\Gamma_i =s$ iff $\Reg(f,s)$ is true of the prefix
$\Gamma(i-1)$. That is, $\Reg(f,s)$ represents what must have been
true previously for $f$ to be true now. $\Reg$ is defined as follows:
%
\begin{itemize}
\item $\Reg(p,s) = \true$ iff $p\in s$ and $\false$ otherwise, 
for $p\in {\cal P}$
\item $\Reg(\neg f,s)= \neg\Reg(f,s)$
\item $\Reg(f_1 \wedge f_2,s) = \Reg(f_1,s) \wedge \Reg(f_2,s)$
\item $\Reg(\last f,s) = f$
\item $\Reg(f_1 \since f_2,s) = \Reg(f_2,s) \vee (\Reg(f_1,s)
\wedge (f_1 \since f_2))$
\end{itemize}
%
For instance, take a state $s$ in which $p$ holds and $q$ does not,
and take $f = (\last \neg q) \wedge (p \since q)$, meaning that $q$
must have been false 1 step ago, but that it must have held at some
point in the past and that $p$ must have held since $q$ last did.
$\Reg(f,s) = \neg q \wedge (p \since q)$, that is, for $f$ to hold
now, then at the previous stage, $q$ had to be false and the $p \since
q$ requirement still had to hold. When $p$ and $q$ are both false in
$s$, then $\Reg(f,s) = \false$, indicating that $f$ cannot be
satisfied, regardless of what came earlier in the sequence.

For notational convenience, where $X$ is a set of
formulae we write $\NN{X}$ for $X \cup \{\neg x \mid x \in X\}$.
Now the translations exploit the PLTL representation of rewards as
follows.  Each expanded state (e-state)
in the generated MDP can be seen as labelled
with a set $\Psi \subseteq \NN{\Sub(F)}$ of subformulae of the reward
formulae in $F$ (and their negations). The
subformulae in $\Psi$ must be (1) true of the paths leading to the
e-state, and (2) sufficient to determine the current truth of all
reward formulae in $F$, as this is needed to compute the current
reward. Ideally the $\Psi$s should also be (3) small enough to enable
just that, i.e. they should not contain subformulae which draw history
distinctions that are irrelevant to determining the reward at one
point or another. Note however that in the worst-case, the number of
distinctions needed, even in the minimal equivalent MDP, may be
exponential in $\size{F}$. This happens for instance with the formula
$\last^k f$, which requires $k$ additional bits of information
memorising the truth of $f$ over the last $k$ steps.

\subsubsection{\pltlsimp}

For the choice of the $\Psi$s, 
Bacchus et al.\ \citeyear{bacchus:etal:96}\ consider two
cases. In the simple case, which we call \pltlsimp, an MDP obeying
properties (1) and (2) is produced by simply labelling each e-state
with the set of {\em all}\ subformulae in $\NN{\Sub(F)}$ which are
true of the sequence leading to that e-state.  This MDP is generated
forward, starting from the initial e-state labelled with $s_0$ and
with the set $\Psi_0 \subseteq \NN{\Sub(F)}$ of all subformulae which
are true of the sequence $\langle s_0 \rangle$.  The successors of any
e-state labelled by NMRDP state $s$ and subformula set $\Psi$ are
generated as follows: each of them is labelled by a successor $s'$ of
$s$ in the \mbox{NMRDP} and by the set of subformulae $\{\psi' \in
\NN{\Sub(F)} \mid \Psi \models \Reg(\psi',s')\}$.

For instance, consider the NMRDP shown in Figure~\ref{fig:pq}.  The set
$F = \{q \wedge \last\last p\}$ consists of a single reward
formula. The set $\NN{\Sub(F)}$ consists of all subformulae of this
reward formula, and their negations, that is $\NN{\Sub(F)}=
\{p,q,\last p, \last\last p, q \wedge \last\last p, \neg p, \neg q,
\neg \last p, \neg \last \last p, \neg (q \wedge \last \last
p)\}$. The equivalent MDP produced by \pltlsimp\ is shown in
Figure~\ref{fig:pqpltlsim}.

\begin{figure}
\centering
\parbox{0.5\textwidth}
{\includegraphics[height=0.18\textheight]{figures/pq}}
\parbox[c]{0.4\textwidth}{\footnotesize
In the initial state, both $p$ and $q$ are false.  When $p$ is false,
action $a$ independently sets $p$ and $q$ to true with probability
0.8. When both $p$ and $q$ are false, action $b$ sets $q$ to true with
probability 0.8. Both actions have no effect otherwise. A reward is
obtained whenever $q \wedge \last\last p$. The optimal policy is to
apply $b$ until $q$ gets produced, making sure to avoid the state on
the left-hand side, then to apply $a$ until $p$ gets produced, and
then to apply $a$ or $b$ indifferently forever.  }
\caption{\label{fig:pq}Another Simple NMRDP}
\end{figure}

\subsubsection{\pltlmin}

Unfortunately, the MDPs produced by \pltlsimp\ are far from
minimal. Although they could be postprocessed for minimisation before
invoking the MDP solution method, the above expansion may still
constitute a serious bottleneck. Therefore, 
Bacchus et al.\ \citeyear{bacchus:etal:96}\
consider a more complex two-phase translation, which we call
\pltlmin, capable of producing an MDP also satisfying property
(3). Here, a preprocessing phase iterates over all states in $S$, and
computes, for each state $s$, a set $l(s)$ of subformulae, where the
function $l$ is the solution of the fixpoint equation
$l(s) = F \cup \{\Reg(\psi',s') \mid \psi' \in l(s'), \mbox{$s'$ is a
  successor of $s$}\}$.  Only subformulae in $\NN{l(s)}$ will be
candidates for inclusion in the sets labelling the respective e-states
labelled with $s$. That is, the subsequent expansion phase will be as
above, but taking $\Psi_0 \subseteq \NN{l(s_0)}$ and $\psi' \subseteq
\NN{l(s')}$ instead of $\Psi_0 \subseteq \NN{\Sub(F)}$ and $\psi'
\subseteq \NN{\Sub(F)}$. As the subformulae in $l(s)$ are exactly
those that are relevant to the way feasible execution sequences
starting from e-states labelled with $s$ are rewarded, this leads the
expansion phase to produce a minimal equivalent MDP.

Figure~\ref{fig:pqpltlmin}\ shows the equivalent MDP produced by
\pltlmin\ for the NMRDP example in Figure~\ref{fig:pq}, together with
the function $l$ from which the labels are built. Observe how this MDP
is smaller than the \pltlsimp\ MDP: once we reach the state on the
left-hand side in which $p$ is true and $q$ is false, there is no
point in tracking the values of subformulae, because $q$ cannot become
true and so the reward formula cannot either. This is reflected by the
fact that $l(\{p\})$ only contains the reward formula.

In the worst case, computing $l$ requires a space, and a number of
iterations through $S$, exponential in $\size{F}$. Hence the question
arises of whether the gain during the expansion phase is worth the
extra complexity of the preprocessing phase. This is one of the
questions our experimental analysis in Section~\ref{sec:experiments}\
will try to answer.

\begin{figure}[p]
\centering
\parbox{0.55\textwidth}
{\includegraphics[height=0.4\textheight]{figures/pqpltlsim}}
\parbox[c]{0.4\textwidth}{\footnotesize

The following subformulae in $\NN{\Sub(F)}$ label the e-states:\\
$f_1: p$\\
$f_2: q$\\
$f_3: \last p$\\
$f_4: \last \last p$\\
$f_5: q \wedge \last\last p$\\
$f_6: \neg p$\\
$f_7: \neg q$\\
$f_8: \neg \last p$\\
$f_9: \neg \last \last p$\\
$f_{10}: \neg (q \wedge \last\last p)$
}
\caption{\label{fig:pqpltlsim}Equivalent MDP Produced by \pltlsimp}
\end{figure}


\begin{figure}[p]
\centering
\parbox{0.55\textwidth}
{\includegraphics[height=0.4\textheight]{figures/pqpltlmin}}
\parbox[c]{0.4\textwidth}{\footnotesize

The function $l$ is given by:\\
$l(\{\}) = \{q \wedge \last\last p, \last p, p\}$\\
$l(\{p\}) = \{q \wedge \last\last p\}$\\
$l(\{q\}) = \{q \wedge \last\last p, \last p, p\}$\\
$l(\{p,q\}) =  \{q \wedge \last\last p, \last p, p\}$\\[2ex]
The following formulae label the e-states:\\
$f_1: q \wedge \last\last p$\\
$f_2: \last p$\\
$f_3: p$\\
$f_4: \neg(q \wedge \last\last p$)\\
$f_5: \neg\last p$\\
$f_6: \neg p$\\
}
\caption{\label{fig:pqpltlmin}Equivalent MDP Produced by \pltlmin}
\end{figure}


\subsubsection{\pltlstruct}

The \pltlstruct\ translation can be seen as a symbolic version of
\pltlsimp. The set $T$ of added temporal variables contains the purely
temporal subformulae $\PTSub(F)$ of the reward formulae in $F$, \ to
which the $\last$ modality is prepended (unless already there): $T =
\{ \last \psi \mid \psi \in \PTSub(F), \psi \neq \last \psi'\} \cup
\{\last \psi \mid \last\psi \in \PTSub(F)\}$. By repeatedly applying
the equivalence $f_1 \since f_2 \equiv f_2 \vee (f_1 \wedge \last(f_1
\since f_2))$ to any subformula in $\PTSub(F)$, we can express its
current value, and hence that of reward formulae, as a function of the
current values of formulae in $T$ and state variables, as required by
the compact representation of the transition and reward models.

For our NMRDP example in Figure~\ref{fig:pq}, the set of purely
temporal variables is $\PTSub(F) = \{\last p,\last\last p\}$, and $T$
is identical to $\PTSub(F)$. Figure~\ref{fig:pqpltlstruct}\ shows some
of the ADDs forming part of the symbolic MDP produced by \pltlstruct:
the ADDs describing the dynamics of the temporal variables, i.e., the
ADDs describing the effects of the actions $a$ and $b$ on their
respective values, and the ADD describing the reward.

\begin{figure}
\centering
\begin{tabular}{ccc}
{\includegraphics[height=0.12\textheight]{figures/pqpltlstructprvp}} &
{\includegraphics[height=0.12\textheight]{figures/pqpltlstructprvprvp}} &
{\includegraphics[height=0.2\textheight]{figures/pqpltlstructreward}}\\
1. dynamics of $\last p$ &
2. dynamics of $\last\last p$ &
3. reward
\end{tabular}
\caption{\label{fig:pqpltlstruct}ADDs Produced by \pltlstruct. prv (previously)
stands for $\last$}
\end{figure}

As a more complex illustration, consider this example
\cite{bacchus:etal:97}\ in which 
\[F = \{\previously(p \since\ (q \vee
\last r))\} \equiv  \{\top \since\ (p \since\ (q \vee \last r))\}\]
We have that 
\[\PTSub(F) = \{ \top \since\ (p \since\ (q \vee \last r)),
p \since\ (q \vee \last r), \last r\}\] and so the set of temporal variables
used is 
\[T = \{ t_1: \last(\top \since\ (p \since (q \vee \last r))), t_2:
\last (p \since\ (q \vee \last r)), t3: \last r\}\] 
Using the equivalences,
the reward can be decomposed and expressed by means of the
propositions $p,q$ and the temporal variables $t_1, t_2, t_3$ as follows:
\[
\begin{array}{ll}
\top \since\ (p \since\ (q \vee \last r)) & \equiv\\
(p \since\ (q \vee \last r)) \vee \last (\top \since\ (p \since\ (q \vee \last r)))& \equiv\\
(q \vee \last r) \vee (p \wedge \last (p \since\ (q \vee \last r))) \vee t_1 & \equiv\\
 (q \vee t_3) \vee (p \wedge t_2) \vee t_1
\end{array}
\]


As with \pltlsimp, the underlying MDP produced by \pltlstruct\ is far
from minimal -- the encoded history features do not even vary from one
state to the next.  However, size is not as problematic as with
state-based approaches, because structured solution methods do not
enumerate states and are able to dynamically ignore some of the
variables that become irrelevant during policy construction. For
instance, when solving the MDP, they may be able to determine that
some temporal variables have become irrelevant because the situation
they track, although possible in principle, is too costly to be
realised under a good policy. This {\em dynamic}\ analysis of rewards
contrast with \pltlmin's {\em static} analysis \cite{bacchus:etal:96}\
which must encode enough history to determine the reward at all
reachable future states under any policy.

One question that arises is that of the circumstances under which this
analysis of irrelevance by structured solution methods, especially the
dynamic aspects, is really effective. This is another question our
experimental analysis will try to address.

\section{\fltl: A Forward-Looking Approach}
\label{sec:new}

As noted in Section \ref{sec:intro} above, the two key issues facing
approaches to NMRDPs are how to specify the reward functions compactly
and how to exploit this compact representation to automatically
translate an NMRDP into an equivalent MDP amenable to the chosen
solution method. Accordingly, our goals are to provide a reward
function specification language and a translation that are adapted to
anytime state-based solution methods. After a brief reminder of the
relevant features of these methods, we consider these two goals in
turn. We describe the syntax and semantics of the language, the notion
of formula progression for the language which will form the basis of
our translation, the translation itself, its properties, and its
embedding into the solution method. We call our approach \fltl.  We
finish the section with a discussion of the features that distinguish
\fltl\ from existing approaches.

\subsection{Anytime State-Based Solution Methods}

The main drawback of traditional dynamic programming algorithms such
as policy iteration \cite{howard:60}\ is that they explicitly
enumerate all states that are reachable from $s_{0}$ in the entire
MDP. There has been interest in other state-based solution methods,
which may produce incomplete policies, but only enumerate a fraction
of the states that policy iteration requires.

Let $\E(\pi)$ denote the {\em envelope} of policy $\pi$, that is the
set of states that are reachable (with a non-zero probability) from
the initial state $s_{0}$ under the policy. If $\pi$ is defined at all
$s \in \E(\pi)$, we say that the policy is {\em complete}, and that it
is incomplete otherwise.  The set of states in $\E(\pi)$ at which
$\pi$ is undefined is called the {\em fringe} of the policy.  The
fringe states are taken to be absorbing, and their value is heuristic.
%
A common feature of anytime state-based algorithms is that they perform a
forward search, starting from $s_{0}$ and repeatedly expanding the
envelope of the current policy one step forward by adding one or more
fringe states.  When provided with admissible heuristic values for the
fringe states, they eventually converge to the optimal policy without
necessarily needing to explore the entire state space.  In fact, since
planning operators are used to compactly represent the state space,
they may not even need to {\em construct} more than a small subset of
the MDP before returning the optimal policy.  When interrupted before
convergence, they return a possibly incomplete but often useful
policy.

These methods include the envelope expansion algorithm
\cite{dean:etal:95}, which deploys policy iteration on judiciously
chosen larger and larger envelopes, using each successive policy to
seed the calculation of the next.  The more recent LAO$^{*}$ algorithm
\cite{hansen:zilberstein:01}\ which combines dynamic programming with
heuristic search can be viewed as a clever implementation of a
particular case of the envelope expansion algorithm, where fringe
states are given admissible heuristic values, where policy iteration
is run up to convergence between envelope expansions, and where the
clever implementation only runs policy iteration on the states whose
optimal value can actually be affected when a new fringe state is
added to the envelope.  Another example is a backtracking forward
search in the space of (possibly incomplete) policies rooted at
$s_{0}$ \cite{thiebaux:etal:95}, which is performed until interrupted,
at which point the best policy found so far is returned.  Real-time
dynamic programming (RTDP) \cite{barto:etal:95} is another popular
anytime algorithm which is to MDPs what learning real-time A$^{*}$
\cite{korf:90}\ is to deterministic domains, and which has asymptotic
convergence guarantees. The RTDP envelope is made up of sample paths
which are visited with a frequency determined by the current greedy
policy and the transition probabilities in the domain.  RTDP can be
run on-line, off-line for a given number of steps or until
interrupted.  A variant called LRTDP \cite{bonet:geffner:03}\
incorporates mechanisms that focus the search on states whose value
has not yet converged, resulting in convergence speed up and finite
time convergence guarantees.

The \fltl\ translation we are about to present targets these anytime
algorithms, although it could also be used with more
traditional methods such as value and policy iteration.

\subsection{Language and Semantics}
\label{subsec:semantics}

Compactly representing non-Markovian reward functions reduces to
compactly representing the behaviours of interest, where by
\emph{behaviour} we mean a set of finite sequences of states (a subset
of $S^{*}$), e.g.\ the $\{\langle s_0,s_1\rangle, \langle
s_0,s_0,s_1\rangle, \langle s_0,s_0,s_0,s_1\rangle \ldots\}$ in
Figure~\ref{fig:NMRDP}.  Recall that the reward is issued at the end
of any prefix $\Gamma(i)$ in that set. Once behaviours are compactly
represented, it is straightforward to represent non-Markovian reward
functions as mappings from behaviours to real numbers -- we shall
defer looking at this until Section~\ref{subsec:rfs}.

To represent behaviours compactly, we adopt a version of future linear
temporal logic (FLTL) \cite<see>{emerson:90}, augmented with a
propositional constant `\dollar', intended to be read `The behaviour
we want to reward has just happened' or `The reward is received
now'. The language \xfltl\ begins with a set of basic propositions
$\PP$ giving rise to literals:
$$
\LL ::= \PP \;|\; \neg \PP \;|\; \true \;|\; \false
\;|\; \dollar
$$
where $\true$ and $\false$ stand for `true' and `false', respectively.
The connectives are classical $\wedge$ and $\vee$, and the temporal
modalities \next\ (next) and \until\ (\emph{weak} until), giving
formulae: 
$$
\FF ::= \LL \;|\; \FF \wedge \FF \;|\; \FF
\vee \FF \;|\; \next \FF \;|\; \FF \until \FF
$$
Our `until' is weak: $f_1 \until f_2$ means $f_{1}$ will be true from
now on until $f_{2}$ is, if ever. Unlike the more commonly used strong
`until', this does not imply that $f_2$ will eventually be true. It
allows us to define the useful operator \always\ (always): $\always f
\equiv f \until \false$ ($f$ will always be true from now on). We also
adopt the notations $\next^{k} f$ for $k$ iterations of the $\next$
modality (f will be true in exactly $k$ steps), $\beventually{k} f$
for $\bigvee_{i=1}^{k} \next^i f$ (f will be true within the next $k$
steps), and $\balways{k} f$ for $\bigwedge_{i=1}^{k} \next^{i} f$ ($f$
will be true throughout the next $k$ steps).

Although negation officially occurs only in literals, i.e., the
formulae are in negation normal form (NNF), we allow ourselves to
write formulae involving it in the usual way, provided that they have
an equivalent in NNF. Not every formula has such an equivalent,
because there is no such literal as $\neg\dollar$ and because
eventualities (`f will be true some time') are not expressible. These
restrictions are deliberate.  If we were to use our notation and logic
to \emph{theorise} about the allocation of rewards, we would indeed
need the means to say when rewards are not received or to express
features such as liveness (`always, there will be a reward
eventually'), but in fact we are using them only as a mechanism for
ensuring that rewards are given where they should be, and for this
restricted purpose eventualities and the negated dollar are not
needed. In fact, including them would create technical difficulties in
relating formulae to the behaviours they represent.

The semantics of this language is similar to that of FLTL, with an
important difference: because the interpretation of the constant
$\dollar$ depends on the behaviour $B$ we want to reward (whatever
that is), the modelling relation $\models$ must be indexed by $B$. We
therefore write $(\Gamma,i)\modelsb{B} f$ to mean that formula $f$
holds at the $i$-th stage of an arbitrary sequence $\Gamma\in
S^{\omega}$, relative to behaviour $B$. Defining $\modelsb{B}$ is the
first step in our description of the semantics:

\begin{trivlist}
%
\item $(\Gamma,i)\modelsb{B} \dollar$ iff $\Gamma(i)\in B$
%
\item $(\Gamma,i)\modelsb{B} \true$
%
\item $(\Gamma,i)\notmodelsb{B} \false$
%
\item $(\Gamma,i)\modelsb{B} p$, for $p\in\PP$, iff $p\in\Gamma_i$
%
\item $(\Gamma,i)\modelsb{B} \neg p$, for $p\in\PP$, iff $p\not\in\Gamma_i$
%
\item $(\Gamma,i)\modelsb{B} f_1 \wedge f_2\; \mbox{ iff } \; (\Gamma,i)
  \modelsb{B} f_1 \mbox{ and } (\Gamma,i)\modelsb{B} f_2$
%
\item $(\Gamma,i)\modelsb{B} f_1 \vee f_2\; \mbox{ iff } \; (\Gamma,i)
  \modelsb{B} f_1 \mbox{ or } (\Gamma,i)\modelsb{B} f_2$
%
\item $(\Gamma,i)\modelsb{B} \next f\; \mbox{ iff } \;
(\Gamma,i+1)\modelsb{B} f$
%
\item $(\Gamma,i)\modelsb{B} f_1 \until f_2\; \mbox{ iff } \; \forall k\geq i
\mbox{ if } (\forall j, i\leq j\leq k \; (\Gamma,j)\notmodelsb{B} f_2$)
$\mbox{ then } (\Gamma,k)\modelsb{B} f_1$
\end{trivlist}
%
Note that except for subscript $B$ and for the first rule, this is
just the standard FLTL semantics, and that therefore \dollar-free
formulae keep their FLTL meaning. As with FLTL, we say $\Gamma
\modelsb{B} f$ iff $(\Gamma,0)\modelsb{B} f$, and $\modelsb{B} f$ iff
$\Gamma \modelsb{B} f$ for all $\Gamma\in S^{\omega}$.

The modelling relation $\modelsb{B}$ can be seen as specifying when a
formula holds, on which reading it takes $B$ as input. Our next and
final step is to use the $\modelsb{B}$ relation to define, for a
formula $f$, the behaviour $B_f$ that it represents, and for this we
must rather {\em assume} that $f$ holds, and then {\em solve} for $B$.
For instance, let $f$ be $\always (p \implies \dollar)$, i.e., we get
rewarded every time $p$ is true. We would like $B_f$ to be the set of
all finite sequences ending with a state containing $p$. For an
arbitrary $f$, we take $B_f$ to be the set of prefixes that
\emph{have} to be rewarded if $f$ is to hold in all sequences:
\begin{definition}
\label{def:Bf}
$B_f \;\equiv\; \bigcap\{B \mid \modelsb{B} f\}$
\end{definition}
%
To understand Definition~\ref{def:Bf}, recall that $B$ contains
prefixes at the end of which we get a reward and \dollar\ evaluates to
true.  Since $f$ is supposed to describe the way rewards will be
received in an \emph{arbitrary} sequence, we are interested in
behaviours $B$ which make \dollar\ true in such a way as to make $f$
hold without imposing constraints on the evolution of the world.
However, there may be many behaviours with this property, so we take
their intersection,%
\footnote{
%
  If there is no $B$ such that $\modelsb{B} f$, which is the case for
  any \dollar-free $f$ which is not a logical theorem, then $B_f$ is
  $\bigcap\emptyset$ -- i.e.\ $S^*$ following normal set-theoretic
  conventions. This limiting case does no harm, since \dollar-free
  formulae do not describe the attribution of rewards.}
%
ensuring that $B_f$ will only reward a prefix if it has to because
that prefix is in \emph{every} behaviour satisfying $f$.  In all but
pathological cases (see Section~\ref{subsec:normal}), this makes $B_f$
coincide with the (set-inclusion) minimal behaviour $B$ such that
$\modelsb{B} f$. The reason for this `stingy' semantics, making
rewards minimal, is that $f$ does not actually say that rewards are
allocated to more prefixes than are required for its truth. For
instance, $\always(p \implies \dollar)$ \emph{says} only that a reward
is given every time $p$ is true, even though a more generous
distribution of rewards would be \emph{consistent} with it.

\subsection{Examples}
\label{subsec:examples}


It is intuitively clear that many behaviours can be specified by means
of \xfltl\ formulae. While there is no simple way in general to
translate between past and future tense expressions,%
%
\footnote{It is an open question whether the set of representable
  behaviours is the same for \xfltl\ as for PLTL, that is
star-free regular languages. Even if the
behaviours were the same, there is little hope that a practical
translation from one to the other exists.}
%
all of the examples used to illustrate PLTL in
Section~\ref{subsec:previous}\ above are expressible naturally in
\xfltl, as follows. 

The classical goal formula $g$ saying that a goal $p$ is rewarded
whenever it happens is easily expressed: $\always(p \rightarrow
\dollar)$.  As already noted, $B_g$ is the set of finite sequences of
states such that $p$ holds in the last state. If we only care that $p$
is achieved once and get rewarded at each state from then on, we write
$\always(p \implies \always \dollar)$. The behaviour that this formula
represents is the set of finite state sequences having at least one
state in which $p$ holds. By contrast, the formula $\neg p \until (p
\wedge \dollar)$ stipulates only that the first occurrence of $p$ is
rewarded (i.e.\ it specifies the behaviour in Figure \ref{fig:NMRDP}).
To reward the occurrence of $p$ at most once every $k$ steps, we write
$\always((\next^{k+1} p \wedge \balways{k} \neg p) \implies
\next^{k+1} \dollar)$.

For response formulae, where the achievement of $p$ is triggered by
the command $c$, we write $\always(c \implies \next\always(p \implies
\dollar))$ to reward every state in which $p$ is true following the
first issue of the command. To reward only the first occurrence $p$
after each command, we write $\always(c\implies \next (\neg p \until
(p \wedge \dollar)))$. As for bounded variants for which we only
reward goal achievement within $k$ steps of the trigger command, we
write for example $\always(c \implies \balways{k}(p \implies
\dollar))$ to reward all such states in which $p$ holds.

It is also worth noting how to express simple behaviours involving
past tense operators. To stipulate a reward if $p$ has always been
true, we write $\dollar \until \neg p$. To say that we are rewarded if
$p$ has been true since $q$ was, we write $\always(q \implies (\dollar
\until \neg p))$.

Finally, we often find it useful to reward the holding of $p$ until
the occurrence of $q$. The neatest expression for this is $\neg q
\until ((\neg p \wedge \neg q) \vee (q \wedge \dollar))$.


\subsection{Reward Normality}
\label{subsec:normal}

\xfltl\ is therefore quite expressive. Unfortunately, it is rather
\emph{too} expressive, in that it contains formulae which describe
``unnatural'' allocations of rewards. For instance, they may make
rewards depend on future behaviours rather than on the past, or they
may leave open a choice as to which of several behaviours is to
be rewarded.%
%
\footnote{These difficulties are inherent in the use of linear-time
  formalisms in contexts where the principle of directionality must be
  enforced. They are shared for instance by formalisms developed for
  reasoning about actions such as the Event Calculus and LTL action
  theories \cite<see e.g.,>{calvanese:etal:02}.}
%
An example of dependence on the future is \mbox{$\next p \implies \dollar$}, which
stipulates a reward \emph{now} if $p$ is going to hold \emph{next}.
We call such formula {\it reward-unstable}. What a reward-stable $f$
amounts to is that whether a particular prefix needs to be rewarded in
order to make $f$ true does not depend on the future of the sequence.
An example of an open choice of which behavior to reward
is \mbox{$\always(p \implies \dollar) \vee
  \always(\neg p \implies \dollar)$} which says we should
\emph{either} reward all achievements of the goal $p$ \emph{or} reward
achievements of $\neg p$ but does not determine which. We call such
formula {\it reward-indeterminate}. What a reward-determinate $f$
amounts to is that the set of behaviours modelling $f$, i.e. $\{B \mid
\modelsb{B} f\}$, has a unique minimum. If it does not, $B_f$ is
insufficient (too small) to make $f$ true.


In investigating \xfltl\ \cite{slaney:05}, 
we examine the notions of reward-stability and
reward-determinacy in depth, and motivate the claim that formulae that
are both reward-stable and reward-determinate -- we call them
\emph{reward-normal} -- are precisely those that capture the notion of
``no funny business''.  This is the intuition that we ask the reader
to note, as it will be needed in the rest of the paper.  Just for
reference then, we define:
\begin{definition}
  $f$ is \emph{reward-normal}\ iff for every $\Gamma \in S^{\omega}$
  and every $B \subseteq S^{*}$, $\Gamma \modelsb{B} f$ iff for every
  $i$, if $\Gamma(i) \in B_f$ then $\Gamma(i) \in B$.
\end{definition}
The property of reward-normality is decidable
  \cite{slaney:05}. In Appendix \ref{app:normal}\ we give some
  simple syntactic constructions guaranteed to result in reward-normal
  formulae.
While reward-abnormal formulae may be interesting, for present
purposes we restrict attention to reward-normal ones. Indeed, we
stipulate as part of our method that only reward-normal formulae
should be used to represent behaviours.
Naturally, all formulae in Section~\ref{subsec:examples}\ are normal.


\subsection{\xfltl\ Formula Progression}

Having defined a language to represent behaviours to be rewarded, we
now turn to the problem of computing, given a reward formula, a
minimum allocation of rewards to states actually encountered in an
execution sequence, in such a way as to satisfy the formula. Because
we ultimately wish to use anytime solution methods which generate
state sequences incrementally via forward search, this computation is
best done on the fly, while the sequence is being generated. We
therefore devise an incremental algorithm based on a model-checking
technique normally used to check whether a state sequence is a model
of an FLTL formula \cite{bacchus:kabanza:98}.  This technique is known
as formula {\em progression} because it `progresses' or `pushes' the
formula through the sequence.

Our progression technique is shown in Algorithm~\ref{alg:progression}.
In essence, it computes the modelling relation $\modelsb{B}$ given in
Section~\ref{subsec:semantics}. However,unlike the definition of
$\modelsb{B}$, it is designed to be useful when states in the sequence
become available one at a time, in that it defers the evaluation of
the part of the formula that refers to the future to the point where
the next state becomes available. Let $s$ be a state, say $\Gamma_i$,
the last state of the sequence prefix $\Gamma(i)$ that has been
generated so far, and let $b$ be a boolean true iff $\Gamma(i)$ is in
the behaviour $B$ to be rewarded. Let the $\xfltl$ formula $f$
describe the allocation of rewards over all possible futures. Then the
progression of $f$ through $s$ given $b$, written $\Prog(b,s,f)$, is a
new formula which will describe the allocation of rewards over all
possible futures of the \emph{next} state, given that we have just
passed through $s$. Crucially, the function $\Prog$ is Markovian,
depending only on the current state and the single boolean value $b$.
Note that $\Prog$ is computable in linear time in the length of $f$,
and that for \dollar-free formulae, it collapses to FLTL formula
progression \cite{bacchus:kabanza:98}, regardless of the value of $b$.
We assume that \Prog\ incorporates the usual simplification for
sentential constants $\false$ and $\true$: $f \wedge \false$
simplifies to $\false$, $f \wedge \true$ simplifies to $f$, etc.


\begin{algorithm}
\caption{\label{alg:progression}\$FLTL Progression}
\begin{tabular}{l@{~~~}l@{~~~}l}
$\Prog(\mbox{true},s,\dollar)$ & = & $\true$\\
$\Prog(\mbox{false},s,\dollar)$ & = & $\false$\\
$\Prog(b,s,\true)$ & = & $\true$\\
$\Prog(b,s,\false)$ & = & $\false$\\
$\Prog(b,s,p)$ & = & $\true$ iff $p\in s$ and $\false$ otherwise\\
$\Prog(b,s,\neg p)$ &= & $\true$ iff $p\not\in s$ and $\false$ otherwise\\
$\Prog(b,s,f_1 \wedge f_2)$ & = & $\Prog(b,s,f_1) \wedge \Prog(b,s,f_2)$\\
$\Prog(b,s,f_1 \vee f_2)$ & = &  $\Prog(b,s,f_1) \vee \Prog(b,s,f_2)$\\
$\Prog(b,s,\next f)$  & = & $f$\\
$\Prog(b,s,f_{1} \until f_{2})$ & = & $\Prog(b,s,f_{2})$ $\vee
(\Prog(b,s,f_{1}) \wedge f_{1} \until f_{2})$ \\[1ex]
$\Rew(s,f)$ & = & true iff $\Prog(\mbox{false},s,f)=\false$\\
$\dollar\Prog(s,f)$ & = & $\Prog(\Rew(s,f),s,f)$
\end{tabular}
\end{algorithm}


The fundamental property of $\Prog$ is the following. Where
$b \Leftrightarrow (\Gamma(i) \in B)$:
\begin{property} 
\label{prop:fundamental}
$(\Gamma,i) \modelsb{B} f$ iff $(\Gamma,i+1) \modelsb{B} \MProg(b,
\Gamma_i,f)$
\end{property}
\theproof{
See Appendix \ref{app:proofs}.}

Like $\modelsb{B}$, the function $\Prog$ seems to require $B$ (or at
least $b$) as input, but of course when progression is applied in
practice we only have $f$ and one new state at a time of $\Gamma$, and
what we really want to do is {\em compute} the appropriate $B$, namely
that represented by $f$.  So, similarly as in
Section~\ref{subsec:semantics}, we now turn to the second step, which
is to use $\Prog$ to decide on the fly whether a newly generated
sequence prefix $\Gamma(i)$ is in $B_f$ and so should be allocated a
reward.  This is the purpose of the functions $\dollar\Prog$ and
$\Rew$, also given in Algorithm~\ref{alg:progression}.  Given $\Gamma$
and $f$, the function $\dollar\Prog$ in
Algorithm~\ref{alg:progression}\ defines an infinite sequence of
formulae $\langle f_0, f_1, \ldots \rangle$ in the obvious way:
\begin{tabbing}
MM \= stuff \kill
\> $f_0 = f$ \\
\> $f_{i+1} = \dollar\Prog(\Gamma_i,f_i)$
\end{tabbing}
To decide whether a prefix $\Gamma(i)$ of $\Gamma$ is to be rewarded,
$\Rew$ first tries progressing the formula $f_i$ through $\Gamma_i$
with the boolean flag set to `false'. If that gives a consistent
result, we need not reward the prefix and we continue without
rewarding $\Gamma(i)$, but if the result is $\false$ then we know that
$\Gamma(i)$ must be rewarded in order for $\Gamma$ to satisfy $f$. In
that case, to obtain $f_{i+1}$ we must progress $f_i$ through
$\Gamma_i$ again, this time with the boolean flag set to the value
`true'. To sum up, the behaviour corresponding to $f$ is $\{\Gamma(i)|
\Rew(\Gamma_i,f_i)\}$.


To illustrate the behaviour of \xfltl\ progression, consider the
formula $f = \neg p \until (p \wedge \dollar)$ stating that a reward
will be received the first time $p$ is true.  Let $s$ be a state in
which $p$ holds, then $\Prog(\mbox{false},s,f) = \bot \vee (\bot
\wedge \neg p \until (p \wedge \dollar)) \equiv \bot$. Therefore,
since the formula has progressed to $\bot$,
$\Rew(s,f)$ is true and a reward is received.
$\dollar\Prog(s,f) = \Prog(\mbox{true},s,f) = \top \vee (\bot \wedge
\neg p \until (p \wedge \dollar)) \equiv \top$, so the reward formula
fades away and will not affect subsequent progression steps.  If, on
the other hand, $p$ is false in $s$, then $\Prog(\mbox{false},s,f) =
\bot \vee (\top \wedge \neg p \until (p \wedge \dollar)) \equiv \neg p
\until (p \wedge \dollar))$.  Therefore, since the formula has not
progressed to $\bot$,  $\Rew(s,f)$ is false and no reward is received.
$\dollar\Prog(s,f) =
\Prog(\mbox{false},s,f) = \neg p \until (p \wedge \dollar)$, so the
reward formula persists as is for subsequent progression steps.


The following theorem states that under weak assumptions, rewards are
correctly allocated by progression: \vspace*{-0.25ex}
%
\begin{theorem}
\label{thm:prog:ok}
%
Let $f$ be reward-normal, and let $\langle f_0, f_1, \ldots \rangle$
be the result of progressing it through the successive states of a
sequence $\Gamma$ using the function $\dollar\MProg$. 
Then, provided no $f_i$ is 
$\false$, for all $i$ $\MRew(\Gamma_i,f_i)$ iff $\Gamma(i)\in B_{f}$.
\end{theorem}
%
\theproof{See Appendix \ref{app:proofs}}

\noindent
The premise of the theorem is that $f$ never progresses to
$\false$. Indeed if $f_i = \false$ for some $i$, it means that even
rewarding $\Gamma(i)$ does not suffice to make $f$ true, so something
must have gone wrong: at some earlier stage, the boolean $\Rew$ was
made false where it should have been made true. The usual explanation
is that the original $f$ was not reward-normal. For instance $\next p
\implies \dollar$, which is reward unstable, progresses to $\false$ in
the next state if p is true there: regardless of $\Gamma_0$, $f_0 =
\next p \implies \dollar = \next \neg p \vee \dollar$,
$\Rew(\Gamma_0,f_0) = \mbox{false}$, and $f_{1} = \neg p$, so if
$p\in\Gamma_1$ then $f_{2} = \false$. However, other (admittedly
bizarre) possibilities exist: for example, although $\next p \implies
\dollar$ is reward-unstable, its substitution instance
$\next\next\true\implies \dollar$, which also progresses to $\false$
in a few steps, is logically equivalent to $\dollar$ and is
reward-normal.

If the progression method were to deliver the correct minimal behaviour
in all cases (even in all reward-normal cases) it would have to
backtrack on the choice of values for the boolean flags. In the
interest of efficiency, we choose not to allow backtracking. Instead,
our algorithm raises an exception whenever a reward formula progresses
to \false, and informs the user of the sequence which caused the
problem.  The onus is thus placed on the domain modeller to select
sensible reward formulae so as to avoid possible progression to \false.
It should be noted that in the worst case, detecting reward-normality
cannot be easier than the decision problem for \xfltl\ so it is not to
be expected that there will be a simple syntactic criterion for
reward-normality.
In practice, however, commonsense precautions such as avoiding making
rewards depend explicitly on future tense expressions suffice to keep
things normal in all routine cases. For a generous class of
syntactically recognisable reward-normal formulae, see Appendix
\ref{app:normal}.

\subsection{Reward Functions}
\label{subsec:rfs}

With the language defined so far, we are able to compactly represent
behaviours. The extension to a non-Markovian reward function is
straightforward. We represent such a function by a set%
%
\footnote{Strictly speaking, a multiset, but for convenience we
  represent it as a set, with the rewards for multiple occurrences of
  the same formula in the multiset summed.}
%
$\phi \subseteq \xfltl\ \times \real$ of formulae associated with real
valued rewards.  We call $\phi$ a {\em reward function specification}.
Where formula $f$ is associated with reward $r$ in $\phi$, we write
`$(f:r) \in \phi$'.  The rewards are assumed to be independent and
additive, so that the reward function $R_{\phi}$ represented by $\phi$
is given by:
%
\begin{definition}
\label{def:rfs}
$ {\displaystyle R_{\phi}(\Gamma(i)) = \sum_{(f:r) \in \phi} \{r\mid
  \Gamma(i) \in B_{f}\}}$
\end{definition}
%
E.g, if $\phi$ is $\{\neg p \until (p \wedge \dollar) : 5.2,
\always(q\implies \always \dollar) : 7.3\}$, we get a reward of 5.2
the first time that $p$ holds, a reward of $7.3$ from the first time
that $q$ holds onwards, a reward of $12.5$ when both conditions are
met, and 0 otherwise.

Again, we can progress a reward function specification $\phi$ to
compute the reward at all stages i of $\Gamma$. As before,
progression defines a sequence $\langle \phi_{0}, \phi_{1},
\ldots\rangle$ of reward function specifications, with $\phi_{i+1} =
\SProg(\Gamma_i,\phi_{i})$, where $\SProg$ is the function that
applies \Prog\ to all formulae in a reward function specification:
\[\SProg(s,\phi) = \{(\Prog(s,f):r) \mid (f:r) \in \phi\}\]
%
Then, the total reward received at stage $i$ is simply the sum of
the real-valued rewards granted by the progression function to the
behaviours represented by the formulae in $\phi_i$:
\[
\sum_{(f:r) \in \phi_{i}} \{r \mid \Rew(\Gamma_{i},f)\}
\]
%
By proceeding that way, we get the expected analog of 
Theorem~\ref{thm:prog:ok}, which states 
progression correctly computes non-Markovian reward functions:
\begin{theorem}
  Let $\phi$ be a reward-normal%
%
  \footnote{We extend the definition of reward-normality to reward
    specification functions in the obvious way, by requiring that all
    reward formulae involved be reward normal.}
%
  reward function specification, and let $\langle \phi_{0},\phi_{1}
  \ldots\rangle$ be the result of progressing it through the
  successive states of a sequence $\Gamma$ using the function
  $\MSProg$. Then, provided $(\false\!:\!r)\!\not\in\!\phi_i$ for any
  $i$, then ${\displaystyle \sum_{(f:r) \in \phi_{i}} \{r \mid
    \MRew(\Gamma_{i},f)\} = R_{\phi}(\Gamma(i))}$.
\end{theorem}
\theproof{
Immediate from Theorem~\ref{thm:prog:ok}.}


\subsection{Translation Into MDP}
\label{subsec:translation}
We now exploit the compact representation of a non-Markovian reward
function as a reward function specification to translate an NMRDP into
an equivalent MDP amenable to state-based anytime solution methods.
Recall from Section~\ref{sec:background}\ that each e-state in the MDP
is labelled by a state of the NMRDP and by history information
sufficient to determine the immediate reward. In the case of a compact
representation as a reward function specification $\phi_0$, this
additional information can be summarised by the progression of
$\phi_0$ through the sequence of states passed through.  So an e-state
will be of the form $\langle s, \phi\rangle$, where $s \in S$ is a
state, and $\phi \subseteq \xfltl\times\real$ is a reward function
specification (obtained by progression). Two e-states $\langle s,\phi
\rangle$ and $\langle t,\psi \rangle$ are equal if $s=t$, the
immediate rewards are the same, and the results of progressing $\phi$
and $\psi$ through $s$ are semantically equivalent.%
%
\footnote{Care is needed over the notion of `semantic equivalence'.
  Because rewards are additive, determining equivalence may involve
  arithmetic as well as theorem proving. For example, the reward
  function specification $\{(p \rightarrow \dollar:3),
  (q \rightarrow \dollar:2)\}$ is equivalent to $\{((p
  \wedge q) \rightarrow \dollar:5), ((p \wedge \neg q)
  \rightarrow \dollar:3), ((\neg p \wedge q) \rightarrow
  \dollar:2)\}$ although there is no one-one correspondence between
  the formulae in the two sets.}


\begin{definition}
\label{def:translation}
Let $D = \langle S,s_{0},A,\T,R\rangle$ be an NMRDP, and $\phi_{0}$ be a
reward function specification representing $R$ (i.e., $R_{\phi_0} = R$, see
Definition~\ref{def:rfs}).
We translate $D$ into the MDP $D'=\langle S',s'_{0},A',\TP,R'\rangle$
defined as follows:
\begin{enumerate}
\item $S' \subseteq S\times 2^{\xfltl\ \times \real}$\\[-3ex]
\item $s'_{0} = \langle s_{0},\phi_0 \rangle$\\[-3ex]
\item $A'(\langle s,\phi \rangle) = A(s)$\\[-3ex]
\item If $a\in A'(\langle s, \phi\rangle)$, then $\TTTP{a}{\langle
s,\phi\rangle}{\langle s', \phi'\rangle} =$
$\left\{ \begin{array}{ll}
  \TTT{a}{s}{s'} & \mbox{if~} \phi' = \MSProg(s,\phi)\\ 0 &
   \mbox{otherwise}
\end{array} \right.$\\
If $a\not\in A'(\langle s, \phi\rangle)$, then $\TTP{a}{\langle
s,\phi\rangle}$ is undefined\\[-3ex]
\item $R'(\langle s,\phi\rangle) = {\displaystyle \sum_{(f:r) \in \phi}
\{r \mid \MRew(s,f)\}}$
\item For all $s' \in S'$, $s'$ is reachable under $A'$ from $s'_0$.
\end{enumerate}
\end{definition}
%
Item 1 says that the e-states are labelled by a state and a reward
function specification. Item 2 says that the initial e-state is
labelled with the initial state and with the original reward function
specification. Item 3 says that an action is applicable in an e-state
if it is applicable in the state labelling it. Item 4 explains how
successor e-states and their probabilities are computed. Given an
action $a$ applicable in an e-state $\langle s,\phi\rangle$, each
successor e-state will be labelled by a successor state $s'$ of $s$ via
$a$ in the NMRDP and by the progression of $\phi$ through $s$. The
probability of that e-state is $\TTT{a}{s}{s'}$ as in the NMRDP. Note
that the cost of computing $\TP$ is linear in that of computing $\T$
and in the sum of the lengths of the formulae in $\phi$. Item 5 has
been motivated before (see Section~\ref{subsec:rfs}). Finally, since
items 1--5 leave open the choice of many MDPs differing only in the
unreachable states they contain, item 6 excludes all such irrelevant
extensions. 
%
It is easy to show that this translation leads to an equivalent MDP,
as defined in Definition~\ref{def:equivalent}. Obviously, the function 
$\tau$ required for Definition\ref{def:equivalent} is given by 
$\tau(\langle s,\phi\rangle) = s$, and then
the proof is a matter of checking conditions.

In our practical implementation, the labelling is one step ahead of
that in the definition: we label the initial e-state with
$\SProg(s_0,\phi_0)$ and compute the current reward and the current
reward specification label by progression of predecessor reward
specifications through the current state rather than through the
predecessor states.  As will be apparent below, this has the potential
to reduce the number of states in the generated MDP.

Figure~\ref{fig:pqfltl}\ shows the equivalent MDP produced for the
\xfltl\ version of our NMRDP example in Figure~\ref{fig:pq}. 
Recall that for this example, the PLTL reward formula was 
$q \wedge \last\last p$. In
\xfltl, the allocation of rewards is described by $\always ((p \wedge
\next\next q) \implies \next \next \dollar)$. The figure also shows the
relevant formulae labelling the e-states, obtained by
progression of this reward formula. Note that without progressing one step
ahead, there would be 3 e-states with state $\{p\}$ on the
left-hand side, labelled with $\{f_1\}$, $\{f_1,f_2\}$, and $\{f_1,f_2,f_3\}$,
respectively.

\begin{figure}[t]
\centering
\parbox{0.55\textwidth}
{\includegraphics[height=0.4\textheight]{figures/pqfltl}}
\parbox[c]{0.4\textwidth}{\footnotesize

The following formulae label the e-states:\\
$f_1: \always((p \wedge \next\next q) \implies \next\next \dollar)$\\
$f_2: \next q \implies \next \dollar$\\
$f_3: q \implies \dollar$\\
}
\caption{\label{fig:pqfltl}Equivalent MDP Produced by \fltl}
\end{figure}


\subsection{Blind Minimality}


The size of the MDP obtained, i.e. the number of e-states it contains is a
key issue for us, as it has to be amenable to state-based solution methods.
Ideally, we would like the MDP to be of minimal size.  However, we do
not know of a method building the {\it minimal} equivalent MDP 
incrementally, adding parts as required by the solution method. 
And since in the worst case even the minimal equivalent MDP 
can be larger than the NMRDP by a factor exponential in the length 
of the reward formulae \cite{bacchus:etal:96}, constructing it 
entirely would nullify the interest of anytime solution methods.

However, as we now explain, Definition~\ref{def:translation}\ leads to
an equivalent MDP exhibiting a relaxed notion of minimality, and which
is amenable to incremental construction. By inspection, we may observe
that wherever an e-state $\langle s, \phi\rangle$ has a successor
$\langle s',\phi'\rangle$ via action $a$, this means that in order to
succeed in rewarding the behaviours described in $\phi$ by means of
execution sequences that start by going from $s$ to $s'$ via $a$, it
is necessary that the future starting with $s'$ succeeds in rewarding
the behaviours described in $\phi'$. If $\langle s, \phi\rangle$ is in
the minimal equivalent MDP, and if there really are such execution
sequences succeeding in rewarding the behaviours described in $\phi$,
then $\langle s', \phi' \rangle$ must also be in the minimal MDP. That
is, construction by progression can only introduce e-states which are
{\it a priori} needed. Note that an e-state that is {\it a priori}
needed may not \emph{really} be needed: there may in fact be no
execution sequence using the available actions that exhibits a given
behaviour. For instance, consider the response formula $\always (p
\implies (\next^{k}q \implies \next^{k}\dollar))$, i.e., every time
trigger $p$ is true, we will be rewarded $k$ steps later provided $q$
is true then. Obviously, whether $p$ is true at some stage affects the
way future states should be rewarded. However, if the transition
relation happens to have the property that $k$ steps from a state
satisfying $p$, no state satisfying $q$ can be reached, then \emph{a
  posteriori} $p$ is irrelevant, and there was no need to label
e-states differently according to whether $p$ was true or not --
observe an occurrence of this in the example in Figure~\ref{fig:pqfltl}, and
how this leads \fltl\ to produce an extra state at
the bottom left of the Figure. To
detect such cases, we would have to look perhaps quite deep into
feasible futures, which we cannot do while constructing the e-states
on the fly. Hence the relaxed notion which we call {\em blind
  minimality} does not always coincide with absolute minimality.


We now formalise the difference between true and blind minimality. For
this purpose, it is convenient to define some functions $\rho$ and
$\mu$ mapping e-states $e$ to functions from $S^*$ to $\real$
intuitively assigning rewards to sequences in the NMRDP starting from
$\tau(e)$. Recall from Definition \ref{def:equivalent} that $\tau$
maps each e-state of the MDP to the underlying NMRDP state.
\begin{definition}
  \label{def:rho}
Let $D$ be an NMRDP. Let $S'$ be the set of e-states in an equivalent
MDP $D'$ for $D$. Let $e$ be any reachable e-state in $S'$. Let
$\Gamma'(i)$ be a sequence of e-states in $\widetilde{D'}(s'_0)$ such
that $\Gamma'(i) = e$. Let $\Gamma(i)$ be the corresponding sequence
in $\widetilde{D}(s_0)$ obtained under $\tau$ in the sense that, for
each $j \leq i$, $\Gamma(j) = \tau(\Gamma'_j)$. Then for any $\Delta
\in S^*$, we define
  $$
  \rho(e): \Delta \mapsto \left\{\begin{array}{ll}
      R(\Gamma(i-1);\Delta) & \mbox{if $\Delta_0 = \Gamma_i$} \\
      0 & \mbox{otherwise}
  \end{array}\right.
  $$
  and
  $$
  \mu(e): \Delta \mapsto \left\{\begin{array}{ll}
      R(\Gamma(i-1);\Delta) & \mbox{if $\Delta \in \widetilde{D}(\Gamma_i)$} \\
      0 & \mbox{otherwise}
  \end{array}\right.
  $$
  For any unreachable e-state $e$, we define both $\rho(e)(\Delta)$
  and $\mu(e)(\Delta)$ to be 0 for all $\Delta$.
\end{definition}
Note carefully the difference between $\rho$ and $\mu$. The former
describes the rewards assigned to \emph{all} continuations of a given
state sequence, while the latter confines rewards to \emph{feasible}
continuations. Note also that $\rho$ and $\mu$ are well-defined
despite the indeterminacy in the choice of $\Gamma'(i)$, since by
clause 4 of Definition \ref{def:equivalent}, all such choices lead to
the same values for $R$. 
%
\begin{theorem}
\label{thm:minimal}
Let $S'$ be the set of e-states in an equivalent MDP $D'$ for
$D=\langle S,s_0,A,\T,R\rangle$. $D'$ is minimal iff every e-state in
$S'$ is reachable and $S'$ contains no two distinct e-states $s'_1$
and $s'_2$ with $\tau(s'_1) = \tau(s'_2)$ and $\mu(s'_1) = \mu(s'_2)$.
\end{theorem}
%
\theproof{ See Appendix \ref{app:proofs}.}
%
\noindent
Blind minimality is similar, except that, since there is no looking ahead, no
distinction can be drawn between feasible trajectories and others in the
future of $s$:
%
\begin{definition}
\label{def:blindminimal}
Let $S'$ be the set of e-states in an equivalent MDP $D'$ for
$D=\langle S,s_0,A,\T,R\rangle$. $D'$ is \emph{blind minimal} iff
every e-state in $S'$ is reachable and $S'$ contains no two distinct
e-states $s'_1$ and $s'_2$ with $\tau(s'_1) = \tau(s'_2)$ and
$\rho(s'_1) = \rho(s'_2)$.
\end{definition}

\begin{theorem}
\label{thm:blindminimal}
  Let $D'$ be the translation of $D$ as in
  Definition~\ref{def:translation}. $D'$ is a blind minimal
  equivalent MDP for $D$.
\end{theorem}
\theproof{
See Appendix \ref{app:proofs}.}

The size difference between the blind-minimal and minimal MDPs will
depend on the precise interaction between rewards and dynamics for the
problem at hand, making theoretical analyses difficult and
experimental results rather anecdotal. However, our experiments in
Section~\ref{sec:experiments}\ and~\ref{sec:concrete}\ will show that
from a computation time point of view, it is often preferable to work
with the blind-minimal MDP than to invest in the overhead of computing
the truly minimal one.

Finally, recall that syntactically different but semantically
equivalent reward function specifications define the same
e-state. Therefore, neither minimality nor blind minimality can be
achieved in general without an equivalence check at least as complex
as theorem proving for LTL. In pratical implementations, we avoid
theorem proving in favour of embedding (fast) formula simplification
in our progression and regression algorithms. This means that in
principle we only approximate minimality and blind minimality, but
this appears to be enough for practical purposes.


\subsection{Embedded Solution/Construction}

Blind minimality is essentially the best achievable with anytime
state-based solution methods which typically extend their envelope one
step forward without looking deeper into the future. Our translation
into a blind-minimal MDP can be trivially embedded in any of these
solution methods. This results in an `on-line construction' of the
MDP: the method entirely drives the construction of those parts of the
MDP which it feels the need to explore, and leave the others
implicit. If time is short, a suboptimal or even incomplete policy may
be returned, but only a fraction of the state and expanded state
spaces might be constructed. Note that the solution method should
raise an exception as soon as one of the reward formulae progresses to
$\false$, i.e., as soon as an expanded state $\langle s, \phi\rangle$
is built such that $(\false:r) \in \phi$, since this acts as a
detector of unsuitable reward function specifications.

To the extent enabled by blind minimality, our approach allows for a
dynamic analysis of the reward formulae, much as in \pltlstruct\
\cite{bacchus:etal:97}. Indeed, only the execution sequences feasible
under a particular policy actually explored by the solution method
contribute to the analysis of rewards for that policy. Specifically,
the reward formulae generated by progression for a given policy are
determined by the prefixes of the execution sequences feasible under
this policy. This dynamic analysis is particularly useful, since
relevance of reward formulae to particular policies (e.g. the optimal
policy) cannot be detected a priori.

The forward-chaining planner TLPlan \cite{bacchus:kabanza:00}\
introduced the idea of using FLTL to specify domain-specific {\em
search control knowledge} and formula progression to prune unpromising
sequential plans (plans violating this knowledge) from deterministic
search spaces. This has been shown to provide enormous time gains,
leading TLPlan to win the 2002 planning competition hand-tailored
track.  Because our approach is based on progression, it provides an
elegant way to exploit search control knowledge, yet in the context of
decision-theoretic planning. Here this results in a dramatic reduction
of the fraction of the MDP to be constructed and explored, and
therefore in substantially better policies by the deadline.

We achieve this as follows.  We specify, via a \dollar-free formula
$c_0$, properties which we know must be verified by paths feasible
under {\em promising} policies. Then we simply progress $c_0$
alongside the reward function specification, making e-states triples
$\langle s,\phi,c \rangle$ where $c$ is a \dollar-free formula
obtained by progression.  To prevent the solution method from applying an
action that leads to the control knowledge being violated, the action
applicability condition (item 3 in Definition~\ref{def:translation})
becomes: $a \in A'(\langle s,\phi,c\rangle)$ iff $a\in A(s)$ and
$c\neq \false$ (the other changes are straightforward). For instance,
the effect of the control knowledge formula $\always(p\implies \next
q)$ is to remove from consideration any feasible path in which $p$ is
not followed by $q$. This is detected as soon as violation occurs,
when the formula progresses to $\false$.  Although this paper focuses
on non-Markovian rewards rather than dynamics, it should be noted that
\dollar-free formulae can also be used to express non-Markovian
constraints on the system's dynamics, which can be incorporated in our
approach exactly as we do for the control knowledge.


\subsection{Discussion}
\label{subsec:discussion}

Existing approaches \cite{bacchus:etal:96,bacchus:etal:97} advocate
the use of PLTL over a finite past to specify non-Markovian
rewards. In the PLTL style of specification, we describe the past
conditions under which we get rewarded now, while with \xfltl\ we
describe the conditions on the present and future under which future
states will be rewarded. While the behaviours and rewards may be the
same in each scheme, the naturalness of thinking in one style or the
other depends on the case. Letting the kids have a strawberry dessert
because they have been good all day fits naturally into a
past-oriented account of rewards, whereas promising that they may
watch a movie if they tidy their room (indeed, making sense of the
whole notion of promising) goes more naturally with \xfltl. One
advantage of the PLTL formulation is that it trivially enforces the
principle that present rewards do not depend on future states. In
\xfltl, this responsibility is placed on the domain modeller.  The
best we can offer is an exception mechanism to recognise mistakes when
their effects appear, or syntactic restrictions.  On the other hand,
the greater expressive power of \xfltl\ opens the possibility of
considering a richer class of decision processes, e.g. with
uncertainty as to which rewards are received (the dessert or the
movie) and when (some time next week, before it rains).

At any rate, we believe that \xfltl\ is better suited than PLTL to
solving NMRDPs using anytime state-based solution methods.  While the
\pltlsimp\ translation could be easily embedded in such a solution
method, it loses the structure of the original formulae when
considering subformulae individually. Consequently, the expanded state
space easily becomes exponentially bigger than the blind-minimal one.
This is problematic with the solution methods we consider, because
size severely affects their performance in solution quality.  The
pre-processing phase of \pltlmin\ uses PLTL formula regression to find
sets of subformulae as potential labels for possible predecessor
states, so that the subsequent generation phase builds an MDP
representing all and only the histories which make a difference to the
way actually feasible execution sequences should be rewarded. Not only
does this recover the structure of the original formula, but in the best
case, the MDP produced is exponentially smaller than the blind-minimal
one. However, the prohibitive cost of the pre-processing phase makes
it unsuitable for anytime solution methods. We do not consider that
any method based on PLTL and regression will achieve a meaningful
relaxed notion of minimality without a costly pre-processing
phase. \fltl\ is an approach based on \xfltl\ and progression which
does precisely that, letting the solution method resolve the tradeoff
between quality and cost in a principled way intermediate between the
two extreme suggestions above.

The structured representation and solution methods targeted by Bacchus
et al.\ \citeyear{bacchus:etal:97}\ differ from the anytime
state-based solution methods \fltl\ primarily aims at, in particular
in that they do not require explicit state enumeration at all.  Here,
non-minimality is not as problematic as with the state-based
approaches. In virtue of the size of the MDP produced, the
\pltlstruct\ translation is, as \pltlsimp, clearly unsuitable to
anytime state-based methods.\footnote{It would be interesting, on the
other hand, to use \pltlstruct\ in conjunction with symbolic versions
of such methods, e.g. Symbolic LAO* \cite{feng:hansen:02}\ or Symbolic
RTDP \cite{feng:etal:03}.}  In another sense, too, \fltl\ represents a
middle way, combining the advantages conferred by state-based and
structured approaches, e.g. by \pltlmin\ on one side, and \pltlstruct\
on the other.  From the former \fltl\ inherits a meaningful notion of
minimality. As with the latter, approximate solution methods can be
used and can perform a restricted dynamic analysis of the reward
formulae. In particular, formula progression enables even state-based
methods to exploit some of the structure in `\xfltl\ space'.  However,
the gap between blind and true minimality indicates that progression
alone is insufficient to always fully exploit that structure. There is
a hope that \pltlstruct\ is able to take advantage of the full
structure of the reward function, but also a possibility that it will
fail to exploit even as much structure as \fltl, as efficiently.  An
empirical comparison of the three approaches is needed to answer this
question and identify the domain features favoring one over the other.



\section{NMRDPP}
\label{sec:nmrdpp}

The first step towards a decent comparison of the different approaches
is to have a framework that includes them all. The Non-Markovian
Reward Decision Process Planner, \nmrdpp, is a platform for the
development and experimentation of approaches to NMRDPs. 
it provides an implementation of the approaches we have described in a common
framework, within a single system, and with a common input language.
\nmrdpp\ is available on-line, see
\url{http://rsise.anu.edu.au/~charlesg/nmrdpp}. It is worth noting that
Bacchus et al.\ \citeyear{bacchus:etal:96,bacchus:etal:97}\
do not report any implementation of their approaches.

\subsection{Input language}

The input language enables the specification of actions, initial
states, rewards, and search control-knowledge. The format for the
action specification is essentially the same as in the SPUDD system
\cite{hoey:etal:99}.  The reward specification is one or more
formulae, each associated with a name and a real number. These
formulae are in either PLTL or \xfltl.  Control knowledge is given in
the same language as that chosen for the reward. Control knowledge
formulae will have to be verified by any sequence of states feasible
under the generated policies. Initial states are simply specified as
part of the control knowledge or as explicit assignments to
propositions.

For instance, consider a simple example consisting of a coin showing
either heads or tails ($\neg \heads$). There are two actions that can
be performed.  The flip action changes the coin to show heads or tails
with a 50\% probability.  The tilt action changes it with 10\%
probability, otherwise leaving it as it is. The initial state is
tails. We get a reward of 5.0 for the very first head (this is written
$\heads \wedge \neg \last \previously \heads$ in PLTL) and a reward of
1.0 each time we achieve the sequence heads, heads, tails ($\last^{2}
\heads \wedge \last \heads \wedge \neg \heads$ in PLTL).  In our input
language, this NMRDP is described as shown in Figure~\ref{fig:input}.

\begin{figure}
\begin{verbatim}
action flip
   heads (0.5)
endaction

action tilt
   heads (heads (0.9) (0.1))
endaction

heads = ff
[first, 5.0]? heads and ~prv (pdi heads)
[seq, 1.0]? (prv^2 heads) and (prv heads) and ~heads
\end{verbatim}
\vspace*{-2ex}
\caption{\label{fig:input}Input for the Coin Example. {\tt prv}\
(previously) stands for $\last$ and\\ {\tt pdi}\ (past diamond) stands
for \previously.}
\vspace*{-2ex}
\end{figure}

\begin{figure}
\centering
{\small
\hspace*{-1ex}\begin{tabular}{ll}
{\tt > loadWorld('coin')} & load coin NMRDP\\
{\tt > preprocess('sPltl')}     & \pltlstruct\ preprocessing\\
{\tt > startCPUtimer}\\
{\tt > spudd(0.99, 0.0001)}     & solve MDP with SPUDD$(\beta,\epsilon)$\\
{\tt > stopCPUtimer}          \\
{\tt > readCPUtimer}            & report solving time\\ 
{\tt 1.22000}\\
{\tt > iterationCount}        & report number of iterations\\
{\tt 1277}\\
{\tt > displayDot(valueToDot)} & display ADD of value function\\
\multicolumn{2}{l}{\includegraphics[height=0.17\textheight]{figures/value}}\\
{\tt > displayDot(policyToDot)} & display policy\\
\multicolumn{2}{l}{\includegraphics[height=0.1\textheight]{figures/policy}}\\
{\tt > preprocess('mPltl')}   & \pltlmin\ preprocessing\\
{\tt > expand}                & completely expand MDP\\
{\tt > domainStateSize}       & report MDP size\\
{\tt 6}\\
{\tt > printDomain ("") | 'show-domain.rb'}    & display postcript rendering of MDP\\
\multicolumn{2}{l}{\includegraphics[height=0.28\textheight]{figures/domain}}\\
{\tt > valIt(0.99, 0.0001)}   & solve MDP with VI$(\beta,\epsilon)$\\
{\tt > iterationCount}        & report number of iterations\\
{\tt 1277}\\
{\tt > getPolicy}             & output policy (textual)\\
{\tt ...}
\end{tabular}
}
\caption{\label{fig:session}Sample Session}
\vspace*{-2ex}
\end{figure}


\subsection{Common framework}
The common framework underlying \nmrdpp\ takes advantage of the fact
that NMRDP solution methods can, in general, be divided into the
distinct phases of preprocessing, expansion, and solving. 
The first two
are optional. 

For \pltlsimp, {\em preprocessing}\ simply computes the set
$\NN{\Sub(F)}$ of subformulae of the reward formulae. For \pltlmin, it
also includes computing the labels $l(s)$ for each state $s$.  For
\pltlstruct, preprocessing involves computing the set $T$ of temporal
variables as well as the ADDs for their dynamics and for the
rewards. \fltl\ does not require any preprocessing.

{\em Expansion} is the optional generation of the entire equivalent
MDP prior to solving. Whether or not off-line expansion is sensible
depends on the MDP solution method used. If state-based value or
policy iteration is used, then the MDP needs to be expanded
anyway. If, on the other hand, an anytime search algorithm or
structured method is used, it is definitely a bad idea. In our
experiments, we often used expansion solely for the purpose of
measuring the size of the generated MDP.

{\em Solving} the MDP can be done using a number of
methods. Currently, \nmrdpp\ provides implementations of classical
dynamic programming methods, namely state-based value and policy
iteration \cite{howard:60}, of heuristic search methods: state-based
LAO* \cite{hansen:zilberstein:01} using either value or policy
iteration as a subroutine, and of one structured method, namely SPUDD
\cite{hoey:etal:99}. Prime candidates for future developments are
(L)RTDP \cite{bonet:geffner:03}, symbolic LAO* \cite{feng:hansen:02},
and symbolic RTDP \cite{feng:etal:03}.

\subsection{Approaches covered}

Altogether, the various types of preprocessing, the choice of whether
to expand, and the MDP solution methods, give rise to quite a number
of NMRDP approaches, including, but not limited to those previously
mentioned (see e.g. \pltlstrauto\ below). Not {\it all} combinations
are possible. E.g., state-based processing variants are incompatible
with structured solution methods (the converse is possible in
principle, however).  Also, there is at present no structured form of
preprocessing for \xfltl\ formulae.

\pltlstrauto\ is an example of an interesting variant of \pltlstruct,
which we obtain by considering additional preprocessing, whereby the
state space is explored (without explicitly enumerating it) to produce
a BDD representation of the e-states reachable from the start
state. This is done by starting with a BDD representing the start
e-state, and repeatedly applying each action. Non-zero probabilities
are converted to ones and the result ``or-ed'' with the last
result. When no action adds any reachable e-states to this BDD, we can
be sure it represents the reachable e-state space. This is then used
as additional control knowledge to restrict the search. It should be
noted that without this phase \pltlstruct\ makes no assumptions about
the start state, and thus is left at a possible disadvantage.  Similar
structured reachability analysis techniques have been used in the
symbolic implementation of LAO* \cite{feng:hansen:02}.  However, an
important aspect of what we do here is that temporal variables are
also included in the BDD.

\subsection{The \nmrdpp\ System}

\nmrdpp\ is controlled by a command language, which is read either
from a file or interactively. The command language provides commands
for the different phases (preprocessing, expansion, solution) of the
methods, commands to inspect the resulting policy and value functions,
e.g. with rendering via DOT~\cite{graphviz:02}, as well as supporting
commands for timing and memory usage. A sample session, where the coin
NMRDP is successively solved with \pltlstruct\ and \pltlmin\ is shown
in Figure~\ref{fig:session}.

\nmrdpp\ is implemented in C++, and makes use of a number of
supporting libraries. In particular, it relies heavily on the CUDD
package for manipulating ADDs \cite{somenzi:01}: action specification
trees are converted into and stored as ADDs by the system, and
moreover the structured algorithms rely heavily on CUDD for ADD
computations.  The state-based algorithms make use of the MTL -- Matrix
Template Library for matrix operations. MTL takes advantage of modern
processor features such as MMX and SSE and provides efficient sparse
matrix operations. We believe that our implementations of MDP solution
methods are comparable with the state of the art.  For instance, we
found that our implementation of SPUDD is comparable in performance
(within a factor of 2) to the reference implementation
\cite{hoey:etal:99}.  On the other hand, we believe that data
structures used for regression and progression of temporal formulae
could be optimised.



\section{Experimental Analysis}
\label{sec:experiments}

We are faced with three substantially different approaches that are
not easy to compare, as their performance will depend on domain
features as varied as the structure in the transition model, the type,
syntax, and length of the temporal reward formula, the presence of
rewards unreachable or irrelevant to the optimal policy, the
availability of good heuristics and control-knowledge, etc, and on the
interactions between these factors.  In this section, we report an
experimental investigation into the influence of some of these factors
and try to answer the questions raised previously:\footnote{Here is an
executive summary of the answers for the executive reader. 1. no,
2. yes, 3. yes, 4.  \pltlstruct\ and \fltl, 5. \pltlsimp, 6. yes,
7. yes and no, respectively, 8. yes, 9. no and yes, respectively.}
\begin{enumerate}
\item is the dynamics of the domain the predominant factor affecting 
performance?
\item is the type of reward a major factor?
\item is the syntax used to describe rewards a major factor?
\item is there an overall best method?
\item is there an overall worst method?
\item does the preprocessing phase of \pltlmin\ pay, compared to \pltlsimp?
\item does the simplicity of the \fltl\ translation compensate for
blind-minimality, or does the benefit of true minimality outweigh the
cost of \pltlmin\ preprocessing?
\item are the dynamic analyses of rewards in \pltlstruct\ and \fltl\
effective?
\item is one of these analyses more powerful, or are they rather
complementary?
\end{enumerate}
In some cases but not all, we were able to identify systematic
patterns. The results in this section were obtained using a
Pentium4 2.6GHz GNU/Linux 2.4.20 machine with 500MB of ram. 

\subsection{Preliminary Remarks}

Clearly, \fltl\ and \pltlstrauto\ have great potential for exploiting
domain-specific heuristics and control-knowledge; \pltlmin\ less
so. To avoid obscuring the results, we therefore refrained from
incorporating these features in the experiments. When running LAO*,
the heuristic value of a state was the crudest possible (the sum of
all reward values in the problem). Performance results should be
interpreted in this light -- they do not necessarily reflect the
practical abilities of the methods that are able to exploit these
features.

We begin with some general observations. One question raised above was
whether the gain during the PLTL expansion phase is worth the
expensive preprocessing performed by \pltlmin, i.e.\ whether \pltlmin\
typically outperforms \pltlsimp. We can definitively answer this
question: up to pathological exceptions, preprocessing pays. We found
that expansion was the bottleneck, and that post-hoc minimisation of
the MDP produced by \pltlsimp\ did not help much. \pltlsimp\ is
therefore of little or no practical interest, and we decided not to
report results on its performance, as it is often an order of
magnitude worse than that of \pltlmin.
%
Unsurprisingly, we also found that \pltlstruct\ would typically scale
to larger state spaces, inevitably leading it to outperform
state-based methods. However, this effect is not uniform: structured
solution methods sometimes impose excessive memory requirements which
makes them uncompetitive in certain cases, for example where
$\prv^nf$, for large $n$, features as a reward formula.

\subsection{Domains}

Experiments were performed on four hand-coded domains (propositions +
dynamics) and on random domains.  Each hand-coded domain has $n$
propositions $p_i$, and a dynamics which makes every state possible
and eventually reachable from the initial state in which all
propositions are false.  The first two such domains, \spuddlinear\ and
\spuddexpon\, were discussed by Hoey et al.\ \citeyear{hoey:etal:99}; 
the two others are our own.

The intention of \spuddlinear\ was to take advantage of the best case
behaviour of SPUDD. For each proposition $p_i$, it has an action $a_i$
which sets $p_i$ to true and all propositions $p_j$, $1 \leq j < i$ to
false.  \spuddexpon, was used by Hoey et al.\ \citeyear{hoey:etal:99}\
to demonstrate the worst case behaviour of SPUDD.  For each
proposition $p_i$, it has an action $a_i$ which sets $p_i$ to true
only when all propositions $p_j$, $1 \leq j < i$ are true (and sets
$p_i$ to false otherwise), and sets the latter propositions to false.
The third domain, called \balls, has one ``turn-on'' and one
``turn-off'' \ action per proposition. The ``turn-on-$p_i$'' action
only probabilistically succeeds in setting $p_i$ to true when $p_i$
was false.  The turn-off action is similar. The fourth domain, called
\complete, is a fully connected reflexive domain. For each proposition
$p_i$ there is an action $a_i$ which sets $p_i$ to true with
probability $i/(n+1)$ (and to false otherwise) and $p_j$, $j\neq i$ to
true or false with probability 0.5. Note that $a_i$ can cause a
transition to any of the $2^n$ states.

Random domains of size $n$ also involve $n$ propositions. The method
for generating their dynamics is detailed in
appendix~\ref{app:random}.  Let us just summarise by saying that we
are able to generate random dynamics exhibiting a given degree of
``structure'' and a given degree of uncertainty.  Lack of structure
essentially measures the bushiness of the internal part of the ADDs
representing the actions, and uncertainty measures the bushiness of
their leaves.


\subsection{Influence of Dynamics}

The interaction between dynamics and reward certainly affects the
performance of the different approaches, though not so strikingly as
other factors such as the reward type (see below). We found that under
the same reward scheme, varying the degree of structure or uncertainty
did not generally change the relative success of the different
approaches.  For instance, Figures~\ref{fig:structure}\
and~\ref{fig:uncertainty}\ show the average run time of the methods as
a function of the degree of structure, resp.\ degree of uncertainty,
for random problems of size $n=6$ and reward $\last^{n} \neg
\last\true$ (the state encountered at stage $n$ is rewarded,
regardless of its properties\footnote{ $\nxt^{n}\dollar$ in \xfltl}).
Run-time increases slightly with both degrees, but there is no
significant change in relative performance.  These are typical of the
graphs we obtain for other rewards.

Clearly, counterexamples to this observation exist. These are most
notable in cases of extreme dynamics, for instance with the
\spuddexpon\ domain. Although for small values of $n$, such as $n=6$,
\pltlstruct\ approaches are faster than the others in handling the
reward $\last^{n} \neg \last\true$ for virtually any type of dynamics
we encountered, they perform very poorly with that reward on
\spuddexpon.  This is explained by the fact that only a small fraction
of \spuddexpon\ states are reachable in the first $n$ steps. After $n$
steps, \fltl\ immediately recognises that reward is of no consequence,
because the formula has progressed to $\true$.  \pltlmin\ discovers
this fact only after expensive preprocessing. \pltlstruct, on the
other hand, remains concerned by the prospect of reward, just as
\pltlsimp\ would.

\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/structure}
\caption{\label{fig:structure}Changing the Degree of Structure}
\end{figure}
%
\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/uncertainty}
\caption{\label{fig:uncertainty}Changing the Degree of Uncertainty}
\end{figure}


\subsection{Influence of Reward Types}

The type of reward appears to have a stronger influence on performance
than dynamics. This is unsurprising, as the reward type significantly
affects the size of the generated MDP: certain rewards only make the
size of the minimal equivalent MDP increase by a constant number of
states or a constant factor, while others make it increase by a factor
exponential in the length of the formula. Table~\ref{table:size}\
illustrates this. The third column reports the size of the minimal
equivalent MDP induced by the formulae on the left hand
side.\footnote{The figures are not necessarily valid for
non-completely connected NMRDPs. Unfortunately, even for completely
connected domains, there does not appear to be a much cheaper way to
determine the MDP size than to generate it and count states.}

A legitimate question is whether there is a direct correlation between
size increase and (in)appropriateness of the different methods. For
instance, we might expect the state-based methods to do particularly
well in conjunction with reward types inducing a small MDP and
otherwise badly in comparison with structured methods. Interestingly,
this is not always the case. For instance, in Table~\ref{table:size}\
whose last two columns report the fastest and slowest methods over the
range of hand-coded domains where $1 \leq n \leq 12$, the first row
contradicts that expectation. Moreover, although \pltlstruct\ is
fastest in the last row, for larger values of $n$ (not represented in
the table), it aborts through lack of memory, unlike the other
methods.

\begin{table}[t]
\centering
{\small
\begin{tabular}{|l|l|l|l|l|}
\hline
type & formula & size & fastest & slowest\\ \hline
first time all $p_i$s & $(\wedge_{i=1}^{n} p_i) \wedge (\neg\last\previously \wedge_{i=1}^{n} p_i)$ & ${\cal O}(1)\size{S}$ & \pltlstrauto & \pltlmin\\
$p_i$s in sequence from start state & $(\wedge_{i=1}^{n}\last^{i} p_i) \wedge \last^{n} \neg \last \true$ & ${\cal O}(n)\size{S}$ & \fltl & \pltlstruct\\
two consecutive $p_i$s & $\vee_{i=1}^{n-1} (\last p_i \wedge p_{i+1})$ & ${\cal O}(n^{k})\size{S}$ & \pltlstruct & \fltl\\
all $p_i$s $n$ times ago & $\last^{n} \wedge_{i=1}^{n} p_i$ & ${\cal O}(2^n)\size{S}$ & \pltlstruct & \pltlmin\\ \hline
\end{tabular}
}
\caption{\label{table:size}Influence of Reward Type on MDP Size and Method Performance}
\end{table}

\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/syntax}
\caption{\label{fig:syntax}Changing the Syntax}
\end{figure}



The most obvious observations arising out of these experiments is that
\pltlstruct\ is nearly always the fastest -- until it runs out of
memory.  Perhaps the most interesting results are those in the second
row, which expose the inability of methods based on PLTL to deal with
rewards specified as long sequences of events.  In converting the
reward formula to a set of subformulae, they lose information about
the order of events, which then has to be recovered laboriously by
reasoning. \xfltl\ progression in contrast takes the events one at a
time, preserving the relevant structure at each step.  Further
experimentation led us to observe that all PLTL based algorithms
perform poorly where reward is specified using formulae of the form
$\prv^k f$, $\previously_{k} f$, and $\alwaysPast_{k}f$ ($f$ has been
true $k$ steps ago, within the last $k$ steps, or at all of the last
$k$ steps).


\subsection{Influence of Syntax}

Unsurprisingly, we find that the syntax used to express rewards, which
affects the length of the formula, has a major influence on the run
time. A typical example of this effect is captured in
Figure~\ref{fig:syntax}.  This graph demonstrates how re-expressing
$\mbox{\emph{prvOut}}\equiv\prv^n (\wedge_{i=1}^{n} p_i)$ as
$\mbox{\emph{prvIn}}\equiv\wedge_{i=1}^{n} \prv^n p_i$, thereby
creating $n$ times more temporal subformulae, alters the running time
of all PLTL methods. \fltl\ is affected too as \xfltl\ progression
requires two iterations through the reward formula. The graph
represents the averages of the running times over all the methods, for
the \complete\ domain.


\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/multiplesize}
\caption{\label{fig:multiplesize}Effect of Multiple Rewards on MDP size}
\end{figure}
%
\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/multipletime}
\caption{\label{fig:multipletime}Effect of Multiple Rewards on Run Time}
\end{figure}




Our most serious concern in relation to the PLTL approaches is their
handling of reward specifications containing multiple reward elements.
Most notably we found that \pltlmin\ does not necessarily produce the
minimal equivalent MDP in this situation. To demonstrate, we consider
the set of reward formulae $\{f_1,f_2, \ldots, f_n\}$, each
associated with the same real value $r$. Given this, PLTL approaches
will distinguish unnecessarily between past behaviours which lead to
identical future rewards. This may occur when the reward at an e-state
is determined by the truth value of $f_1 \vee f_2$. This formula
does not necessarily require e-states that distinguish between the
cases in which $\{f_1 \equiv \top, f_2 \equiv \bot\}$ and
$\{f_1 \equiv \bot, f_2 \equiv \top\}$ hold; however, given the
above specification, \pltlmin\ makes this distinction. For
example, taking $f_i = \prv p_i$, Figure~\ref{fig:multiplesize}\
shows that \fltl\ leads to an MDP whose size is at most 3 times that
of the NMRDP. In contrast, the relative size of the MDP produced by
\pltlmin\ is linear in $n$, the number of rewards and
propositions. These results are obtained with all hand-coded domains
except \spuddexpon. Figure~\ref{fig:multipletime}\ shows the run-times
as a function of $n$ for \complete. \fltl\ dominates and is only
overtaken by \pltlstruct(A)\ for large values of $n$, when the MDP
becomes too large for explicit exploration to be practical.  To obtain
the minimal equivalent MDP using \pltlmin, a bloated reward
specification of the form $\{(\prv \vee_{i=1}^{n} (p_i
\wedge_{j=1,j\neq i}^{n} \neg p_j) : r), \ldots, (\prv \wedge_{i=1}^{n}
p_i : n*r)\}$ is necessary, which, by virtue of its exponential length,
is not an adequate solution.




\subsection{Influence of Reachability}

All approaches claim to have some ability to ignore variables which
are irrelevant because the condition they track is
unreachable:\footnote{Here we sometimes speak of conditions and goals
being `reachable' or `achievable' rather than `feasible', although
they may be temporally extended. This is to keep in line with
conventional vocabulary as in the phrase `reachability analysis'.}
\pltlmin\ detects them through preprocessing, \pltlstruct\ exploits
the ability of structured solution methods to ignore them, and \fltl\
ignores them when progression never exposes them.  However, given that
the mechanisms for avoiding irrelevance are so different, we expect
corresponding differences in their effects.  On experimental
investigation, we found that the differences in performance are best
illustrated by looking at response formulae, which assert that if a
trigger condition $c$ is reached then a reward will be received upon
achievement of the goal $g$ in, resp.\ within, $k$ steps. In PLTL,
this is written $g \wedge \prv^{k} c$, resp.\ $g \wedge
\previously_{k}c$, and in \xfltl, $\fbx (c \implies \nxt^k (g \implies
\$))$, resp.\ $\fbx (c \implies \always_k(g \implies \$))$


When the {\em goal} is unreachable, PLTL approaches perform
well. As it is always false, the goal $g$ does not lead to behavioural
distinctions. On the other hand, while constructing the MDP, \fltl\
considers the successive progressions of $\nxt^k g$ without being able
to detect that it is unreachable until it actually fails to
happen. This is exactly what the blindness of blind minimality amounts
to.  Figure~\ref{fig:unachievablegoal}\ illustrates the difference in
performance as a function of the number $n$ of propositions involved
in the \spuddlinear\ domain, when the reward is of the form $g \wedge
\prv^{n} c$, with $g$ unreachable.

\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/unachievablegoal}
\caption{\label{fig:unachievablegoal}Response Formula with Unachievable Goal}
\end{figure}
%
\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/unachievablecondition}
\caption{\label{fig:unachievablecondition}Response Formula with Unachievable Trigger}
\end{figure}



\fltl\ shines when the {\em trigger} is unreachable. Since $c$ never
happens, the formula will always progress to itself, and the goal,
however complicated, is never tracked in the generated MDP. In this
situation PLTL approaches still consider $\last^{k} c$ and its
subformulae, only to discover, after expensive preprocessing for
\pltlmin, after reachability analysis for \pltlstrauto, and never for
\pltlstruct, that these are irrelevant.  This is illustrated in
Figure~\ref{fig:unachievablecondition}, again with \spuddlinear\ and a
reward of the form $g \wedge \prv^{n} c$, with $c$ unreachable.

\subsection{Dynamic Irrelevance}

Earlier we claimed that one advantage of \pltlstruct\ and \fltl\ over
\pltlmin\ and \pltlsimp\ is that the former perform a dynamic analysis
of rewards capable of detecting irrelevance of variables to particular
policies, e.g.\ to the optimal policy.  Our experiments confirm this
claim. However, as for reachability, whether the goal or the
triggering condition in a response formula becomes irrelevant plays an
important role in determining whether a \pltlstruct\ or \fltl\
approach should be taken: \pltlstruct\ is able to dynamically ignore
the goal, while \fltl\ is able to dynamically ignore the trigger.

This is illustrated in Figures~\ref{fig:unrewardinggoal}\
and~\ref{fig:unrewardingcondition}. In both figures, the domain
considered is \balls\ with $n=6$ propositions, the response formula is
$g \wedge \prv^{n} c$ as before, here with both $g$ and $c$
achievable.  This response formula is assigned a fixed reward.  To
study the effect of dynamic irrelevance of the goal, in
Figure~\ref{fig:unrewardinggoal}, achievement of $\neg g$ is rewarded
by the value $r$ (i.e. we have $(\neg g : r)$ in PLTL). In
Figure~\ref{fig:unrewardingcondition}, on the other hand, we study the
effect of dynamic irrelevance of the trigger and achievement of $\neg
c$ is rewarded by the value $r$. Both figures show the runtime of the
methods as $r$ increases.


Achieving the goal, resp. the trigger, is made less attractive as $r$
increases up to the point where the response formula becomes
irrelevant under the optimal policy. When this happens, the run-time
of \pltlstruct\, resp. \fltl, exhibits an abrupt but durable
improvement.  The figures show that \fltl\ is able to pick up
irrelevance of the trigger, while \pltlstruct\ is able to exploit
irrelevance of the goal. As expected, \pltlmin\ whose analysis is
static does not pick up either and performs consistently badly.  Note
that in both figures, \pltlstruct\ progressively takes longer to
compute as $r$ increases because value iteration requires additional
iterations to converge.

\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/unrewardinggoal}
\caption{\label{fig:unrewardinggoal}Response Formula with Unrewarding Goal}
\end{figure}
%
\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/unrewardingcondition}
\caption{\label{fig:unrewardingcondition}Response Formula with Unrewarding Trigger}
\end{figure}


\subsection{Summary}

In our experiments with artificial domains, we found \pltlstruct\ and
\fltl\ preferable to state-based PLTL approaches in most cases.  If
one insists on using the latter, we strongly recommend preprocessing.
\fltl\ is the technique of choice when the reward requires tracking a
long sequence of events or when the desired behaviour is composed of
many elements with identical rewards.  For response formulae, we
advise the use of \pltlstruct\ if the probability of reaching the goal
is low or achieving the goal is very costly, and conversely, we advise
the use of \fltl\ if the probability of reaching the triggering
condition is low or if reaching it is very costly.  In all cases,
attention should be paid to the syntax of the reward formulae and in
particular to minimising its length. Indeed, as could be expected, we
found the syntax of the formulae and the type of non-Markovian reward
they encode to be a predominant factor in determining the difficulty
of the problem, much more so than the features of the Markovian
dynamics of the domain.

\section{A Concrete Example}
\label{sec:concrete}
Our experiments have so far focused on artificial
problems and have aimed at characterising the strengths and weaknesses
of the various approaches. We now look at a concrete example
in order to give a sense of the size of more interesting problems that 
these techniques can solve. 
%
Our example is derived from the Miconic elevator classical planning
benchmark \cite{koehler:schuster:00}.  An elevator must get a number
of passengers from their {\em origin} floor to their {\em
destination}. Initially, the elevator is {\em at} some arbitrary floor
and no passenger is {\em served} nor has {\em boarded} the
elevator. In our version of the problem, there is one single action
which causes the elevator to {\em service} a given floor, with the
effect that the unserved passengers whose origin is the serviced floor
board the elevator, while the boarded passengers whose destination is
the serviced floor unboard and become served. The task is to plan the
elevator movement so that all passengers are eventually
served.\footnote{We have experimented with stochastic variants of
Miconic where passengers have some small probability of desembarking
at the wrong floor.  However, we find it more useful to present
results for the deterministic version since it is closer to the
Miconic deterministic planning benchmark and since, as we have shown
before, rewards have a far more crucial impact than dynamics on the
relative performance of the methods.}

There are two variants of Miconic. In the `simple' variant, a reward
is received each time a passenger becomes served.  In the `hard'
variant, the elevator also attempts to provide a range of priority
services to passengers with special requirements: many passengers will
prefer travelling in a single direction (either up or down) to their
destination, certain passengers might be offered non-stop travel to
their destination, and finally, passengers with disabilities or young
children should be supervised inside the elevator by some other
passenger (the supervisor) assigned to them. Here we omit the
VIP and conflicting group services present in the original hard
Miconic problem, as the reward formulae for those do not create
additional difficulties.


Our formulation of the problem makes use of the same propositions as
the PDDL description of Miconic used in the 2000 International
Planning Competition: dynamic propositions record the floor the
elevator is currently at and whether passengers are served or boarded,
and static propositions record the origin and destination floors of
passengers, as well as the categories (non-stop, direct-travel,
supervisor, supervised) the passengers fall in.  However, our
formulation differs from the PDDL description in two interesting
ways. Firstly, since we use {\em rewards} instead of goals, we are
able to find a preferred solution even when all goals cannot
simultaneously be satisfied. Secondly, because priority services are
naturally described in terms of {\em non-Markovian} rewards, we are
able to use the same action description for both the simple and hard
versions, whereas the PDDL description of hard miconic requires
additional actions (up, down) and complex preconditions to monitor the
satisfaction of priority service constraints.
%
The reward schemes for Miconic can be encapsulated through four
different types of reward formula.

\begin{enumerate}

\item In the simple variant, a reward is received the first time each passenger
$P_i$ is served:

{\small 
\begin{tabular}{ll}
{\bf PLTL:} &  $ServedP_i \wedge \last \alwaysPast \neg ServedP_i$\\
~\\
{\bf \xfltl:} &  $\neg ServedP_i \until (ServedP_i \wedge \dollar)$
\end{tabular}
}

\item Next, a reward is received each time a non-stop passenger $P_i$ is
served in one step after boarding the elevator:

{\small 
\begin{tabular}{ll}
{\bf PLTL:} &  $NonStopP_i \wedge \last\last \neg BoardedP_i \wedge \last\last \neg ServedP_i
\wedge ServedP_i$\\
~\\
{\bf \xfltl:} & $\always ((NonStopP_i \wedge \neg BoardedP_i \wedge \neg ServedP_i
\wedge \next\next ServedP_i) \implies \next\next\dollar)$
\end{tabular}
}

\item Then, a reward is received each time a supervised passenger
$P_i$ is served while having been accompanied at all times inside the
elevator by his supervisor\footnote{To understand the \xfltl\ formula,
observe that we get a reward iff $(BoardedP_i \wedge SupervisedP_i)
\implies (BoardedP_j \wedge SupervisorP_jP_i)$ holds until $ServedP_i$
becomes true, and recall that the formula $\neg q \until ((\neg p
\wedge \neg q) \vee (q \wedge \dollar))$ rewards the holding of $p$
until the occurrence of $q$.} $P_j$:

{\small
\begin{tabular}{ll}
{\bf PLTL:}  & 
$SupervisedP_i \wedge SupervisorP_jP_i \wedge ServedP_i \wedge$\\
& $\last\alwaysPast\neg ServedP_i \wedge \alwaysPast(BoardedP_i \implies BoardedP_j)$
\end{tabular}

~\\
\begin{tabular}{ll@{}l}
{\bf \xfltl:} & 
$\neg ServedP_i \until$ & $((BoardedP_i \wedge SupervisedP_i \wedge
                        \neg(BoardedP_j \wedge SupervisorP_jP_i) \wedge$\\
                        &&$~\neg ServedP_i) \vee
                         (ServededP_i \wedge \dollar))$
\end{tabular}
}


\item Finally, reward is received each time a direct travel passenger $P_i$
is served while having travelled only in one direction since boarding, e.g., in the case of going up:

{\small
\begin{tabular}{ll}
{\bf PLTL:}  &
$DirectP_i \wedge ServedP_i \wedge \last \neg ServedP_i \wedge$\\
& $((\bigvee_j \bigvee_{k > j} (AtFloor_k \wedge \last AtFloor_j))\since 
(BoardedP_i \wedge \last\neg BoardedP_i))$
\end{tabular}

~\\
\begin{tabular}{ll@{}l}
{\bf \xfltl:} & 
$\always((DirectP_i \wedge BoardedP_i) \implies (\neg ServedP_i \until$ & 
$((\neg (\bigvee_j \bigvee_{k > i} AtFloor_j \wedge \next AtFloor_k) \wedge$\\
                                                            &&$~\neg ServedP_i) \vee
                                                            (servedP_i \wedge \dollar))))$
\end{tabular}
}
and similarly in the case of going down.

\end{enumerate}


Experiments in this section were run on a Dual Pentium4 3.4GHz
GNU/Linux 2.6.11 machine with 1GB of ram.  We first experimented with
the simple variant, giving a reward of 50 each time a passenger is
first served. Figure~\ref{fig:miconicsimple:time}\ shows the CPU time
taken by the various approaches to solve random problems with an
increasing number $n$ of floors and passengers, and
Figure~\ref{fig:miconicsimple:space}\ shows the number of states
expanded when doing so. Each data point corresponds to just one random
problem. To be fair with the structured approach, we ran \pltlstrauto\
which is able to exploit reachability from the start state. A first
observation is that although \pltlstrauto\ does best for small values
of $n$, it quickly runs out of memory. \pltlstrauto\ and \pltlsimp\
both need to track formulae of the form $\prv \alwaysPast\neg
ServedP_i$ while \pltlsimp\ does not, and we conjecture that this is
why they run out of memory earlier.  A second observation is that
attempts at PLTL minimisation do not pay very much here. While
\pltlmin\ has reduced memory because it tracks fewer subformulae, the
size of the MDP it produces is identical to the size of the \pltlsimp\
MDP and larger than that of the \fltl\ MDP.  This size increase is due
to the fact that PLTL approaches label differently e-states in which
the same passengers are served, depending on who has just become
served (for those passengers, the reward formula is true at the
e-state). In contrast, our \fltl\ implementation with progression one step
ahead labels all these e-states with the reward formulae relevant
to the passengers that still need to be served, the other formulae
having progressed to $\top$. The gain in number of expanded states
materialises into run time gains, resulting in \fltl\ eventually
taking the lead.

\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/miconicsimpletime} 
\caption{\label{fig:miconicsimple:time}Simple Miconic - Run Time}
\end{figure}
%
\begin{figure}
\centering
\includegraphics[width=0.65\textwidth]{figures/miconicsimplespace}
\caption{\label{fig:miconicsimple:space}Simple Miconic - Number of Expanded States}
\end{figure}


\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/miconicheuristictime} 
\caption{\label{fig:miconicheuristic:time}Effect of a Simple Heuristic on Run Time}
\end{figure}
%
\begin{figure}
\centering
\includegraphics[width=0.65\textwidth]{figures/miconicheuristicspace}
\caption{\label{fig:miconicheuristic:space}Effect of a Simple Heuristic on the Number of Expanded States}
\end{figure}


\begin{figure}[t]
\centering
\includegraphics[width=0.65\textwidth]{figures/miconichardtime} 
\caption{\label{fig:miconichard:time}Hard Miconic - Run Time}
\end{figure}
%
\begin{figure}
\centering
\includegraphics[width=0.65\textwidth]{figures/miconichardspace}
\caption{\label{fig:miconichard:space}Hard Miconic - Number of Expanded States}
\end{figure}


Our second experiment illustrates the benefits of using an even
extremely simple admissible heuristic in conjunction with \fltl. Our
heuristic is applicable to discounted stochastic shortest path
problems, and discounts rewards by the shortest time in the future in
which they are possible.  Here it simply amounts to assigning a fringe
state to a value of 50 times the number of still unserved passengers
(discounted once), and results in avoiding floors at which no
passenger is waiting and which are not the destination of a boarded
passenger.  Figures~\ref{fig:miconicheuristic:time}\ and
\ref{fig:miconicheuristic:space}\ compare the run time and number of
states expanded by \fltl\ when used in conjunction with value
iteration (valIt) to when it is used in conjunction with an LAO*
search informed by the above heuristic (LAO(h)). Uninformed LAO*
(LAO*(u), i.e.\ LAO* with a heuristic of $50*n$ at each node) is also included
as a reference point to show the overhead induced by heuristic
search. As can be seen from the graphs, the heuristic search generates
significantly fewer states and this eventually pays in terms of run
time.


In our final experiment, we considered the hard variant, giving a
reward of 50 as before for service (1), a reward of 2 for non-stop
travel (2), a reward of 5 for appropriate supervision (3), and a
reward of 10 for direct travel (2).  Regardless of the number $n$ of
floors and passengers, problems only feature a single non-stop
traveller, a third of passengers require supervision, and only half
the passengers care about traveling direct. CPU time and number of
states expanded are shown in Figures~\ref{fig:miconichard:time}\
and~\ref{fig:miconichard:space}, respectively.  As in the simple case,
\pltlsimp\ and \pltlstruct\ quickly run out of memory. Formulae of
type (2) and (3) create too many additional variables to track
for these approaches, and the problem does not seem to exhibit 
enough structure to help \pltlstruct.
\fltl\ remains the fastest. Here, this does not seem to be so much due to
the size of the generated MDP which is just slightly below that of the
\pltlmin\ MDP, but rather to the overhead incurred by
minimisation. Another observation arising from this experiment is that
only very small instances can be handled in comparison to the
classical planning version of the problem solved by state of the art
optimal classical planners. For example, at the 2000 International
Planning Competition, the {\sc PropPlan} planner \cite{fourman:00}\
optimally solved instances of hard Miconic with 20 passengers and 40 floors 
in about 1000 seconds on a much less powerful machine.



\section{\nmrdpp\ in the Probabilistic Planning Competition}
\label{sec:competition}

We now report on the behaviour of \nmrdpp\ in the probabilistic track
of the 4th International Planning Competition (IPC-4).
Since the competition did not feature non-Markovian rewards,
our original motivation in taking part was to further
compare the  solution methods implemented in \nmrdpp\
in a {\em Markovian}\ setting. This objective largely
underestimated the challenges raised by merely getting a planner ready
for a competition, especially when that competition is the first of its kind.
In the end, we decided that successfully preparing \nmrdpp\
to attempt all problems in the competition using {\em one}\ solution
method (and possibly search control knowledge), would be an 
honorable result.

The most crucial problem we encountered was the translation of PPDDL
\cite{younes:littman:04}, the probabilistic variant of PDDL used as
input language for the competition, into \nmrdpp's \ ADD-based input
language. While translating PPDDL into ADDs is possible in theory,
devising a translation which is practical enough for the need of the
competition (small number of variables, small, quickly generated, and
easily manipulable ADDs) is another matter. \mtbdd, the translator
kindly made available to participants by the competition organisers,
was not always able to achieve the required efficiency. At other
times, the translation was quick but \nmrdpp\ was unable to use the
generated ADDs efficiently. Consequently, we implemented a state-based
translator on top of the PDDL parser as a backup, and opted for a
state-based solution method since it did not rely on ADDs and could
operate with both translators.

The version of \nmrdpp\ entered in the competition did the following:
\begin{enumerate}
\item Attempt to get a translation into ADDs using \mtbdd, and
if that proves infeasible, abort it and rely on the state-based
translator instead.
\item Run \fltl\ expansion of the state space, taking search control
knowledge into account when available. Break after 10mn if not complete.
\item Run value iteration to convergence. Failing to achieve
any useful result (e.g. because expansion was not complete enough to
even reach a goal state), go back to step 2.
\item Run as many of the 30 trials as possible in the remaining
time,\footnote{On each given problem, planners had 15mn to run whatever
computation they saw as appropriate (including parsing,
pre-processing, and policy generation if any), and execute 30 trial
runs of the generated policy from an initial state to a goal state.}\
following the generated policy where defined, and falling back on the
non-deterministic search control policy when available.
\end{enumerate}
With Step 1 we were trying to maximise the instances in which the
original ADD-based \nmrdpp\ version could be run intact. In Step
3, it was decided not to use LAO* because when run with no good
heuristic, it often incurs a significant 
overhead compared to value iteration.

The problems featured in the competition can be classified into
goal-based or reward-based problems. In goal-based problems, a
(positive) reward is only received when a goal state is reached.  In
reward-based problems, action performance may also incur a (usually
negative) reward. Another orthogonal distinction can be made between
problems from domains that were not communicated in advance to the
participants and those from domains that were. The latter
consisted of variants of blocks world and logistics (or box world)
problems, and gave the participating planners 
an opportunity to exploit knowledge of the domain,
much as in the hand-coded deterministic planning track.

We decided to enroll \nmrdpp\ in a control-knowledge mode and in a
domain-independent mode. The only difference between the two modes is
that the first uses FLTL search control knowledge written for the
known domains as additional input. Our main concern in writing the
control knowledge was to achieve a reasonable compromise between the
size and effectiveness of the formulae. For the blocks world domain,
in which the two actions pickup-from and putdown-to had a 25\% chance
of dropping the block onto the table, the control knowledge we used
encoded a variant of the well-known GN1 near-optimal strategy for
deterministic blocks world planning \cite{slaney:thiebaux:01}:
whenever possible, try putting a clear block in its goal position,
otherwise put an arbitrary clear block on the table. Because blocks
get dropped on the table whenever an action fails, and because the
success probabilities and rewards are identical across actions,
optimal policies for the problem are essentially made up of optimal
sequences of actions for the deterministic blocks world and there was
little need for a more sophisticated strategy.\footnote{More
sophisticated near-optimal strategies for deterministic blocks world
exist \cite<see>{slaney:thiebaux:01}, but are much more complex to
encode and might have caused time performance problems.}  In the colored
blocks world domain, where several blocks can share the same color and
the goal only refers to the color of the blocks, the control knowledge
selected an arbitrary goal state of the non-colored blocks world
consistent with the colored goal specification, and then used the same
strategy as for the non-colored blocks world. The performance of this
strategy depends entirely on the goal-state selected and can therefore
be arbitrarily bad.

Logistics problems from IPC-2 distinguish between airports and
other locations within a city; trucks can drive between any two
locations in a city and planes can fly between any two airports.  In
contrast, the box world only features cities, some of which have an
airport, some of which are only accessible by truck. A priori, the map
of the truck and plane connections is arbitrary.  The goal is to get
packages from their city of origin to their city of
destination. Moving by truck has a 20\% chance of resulting in reaching
one of the three cities closest to the departure city rather than the
intended one.  The size of the box world search space turned out to be
quite challenging for \nmrdpp. Therefore, when writing search control
knowledge, we gave up any optimality consideration and favored maximal
pruning. We were helped by the fact that the box world generator
produces problems with the following structure. Cities are divided
into clusters, all of which are composed of at least one airport city.
Furthermore each cluster has at least one hamiltonian circuit which
trucks can follow.  The control knowledge we used forced all planes
but one, and all trucks but one in each cluster to be idle. In each
cluster, the truck allowed to move could only attempt driving along
the chosen hamiltonian circuit, picking up and dropping parcels as it
went.


\begin{table}[p]
{\footnotesize
\begin{tabular}{|l|l|l|} \hline
Part. & Description & Reference\\ \hline
C  & symbolic LAO* & \cite{feng:hansen:02}\\
E* & first-order heuristic search in the fluent calculus & \cite{karabaev:skvortsova:05}\\
G1 & \nmrdpp\ without control knowledge & this paper\\
G2* & \nmrdpp\ with control knowledge & this paper\\
J1* & interpreter of hand written classy policies & \shortcite{fern:etal:04}\\
J2* & learns classy policies from random walks & \shortcite{fern:etal:04}\\
J3 & version of {\sc ff} replanning upon failure & \cite{hoffmann:nebel:01}\\
P & m{\sc gpt}: {\sc lrtdp} with automatically extracted heuristics & \cite{bonet:geffner:05}\\
Q & {\sc ProbaProp}: conformant probabilistic planner & \shortcite{onder:etal:06}\\
R & structured reachability analysis and structured PI & \cite{teichteilkonigsbuch:fabiani:05}\\
\hline
\end{tabular}
}
\caption{\label{table:participants}Competition Participants. Domain-specific planners are starred}
\end{table}

\begin{table}[p]
{\footnotesize
\begin{tabular}{|l|r@{~~}r@{~~}r@{~~~~~}c@{~~~~~}r@{}r|rrrr|r|} \cline{1-11}
          \multicolumn{1}{|c|}{dom} &
          \multicolumn{3}{c}{bw-c-nr} & 
          \multicolumn{1}{c}{bw-nc-nr} &
          \multicolumn{2}{c|}{bx-nr} &
          \multicolumn{1}{c}{expl-bw} &
          \multicolumn{1}{c}{hanoise} &
          \multicolumn{1}{c}{zeno} &
          \multicolumn{1}{c|}{tire-nr} \\ \cline{1-12}
          \multicolumn{1}{|c|}{prob} &
          \multicolumn{1}{c@{~~}}{5} & 
          \multicolumn{1}{c@{~~}}{8} & 
          \multicolumn{1}{c@{~~~~}}{11} &  
          \multicolumn{1}{c@{~~~~}}{8} &  
          \multicolumn{1}{c@{}}{5-10} & 
          \multicolumn{1}{c|}{10-10} & 
          \multicolumn{1}{c}{11} &
          \multicolumn{1}{c}{5-3} &
          \multicolumn{1}{c}{1-2-3-7} &
          \multicolumn{1}{c|}{30-4} &
          \multicolumn{1}{c|}{total}\\ \hline
{\bf     G2}* & {\bf 100} & {\bf 100} & {\bf 100} & {\bf 100} & {\bf 100} & {\bf 100} & \none & \none & \none & \none & {\bf 600}\\ 
     J1* & 100 & 100 & 100 & 100 & 100 & 100 & \none & \none & \none & \none & 600\\ 
     J2* & 100 & 100 & 100 & 100 & 100 &  67 & \none & \none & \none & \none & 567\\ 
      E* & 100 & 100 & 100 & 100 & \none & \none & \none & \none & \none & \none & 400\\ \hline

     J3 & 100 & 100 & 100 & 100 & 100 & 100 & 9 &  \nega & \nega   &  23  & 632 \\ 
{\bf G1}&     &     &     &     &     &     & \nega & {\bf 50} & {\bf 100} & {\bf 30}  & {\bf 180} \\ 
      R &     &     &     &   3 &     &     &   & 57 &  90 &  30 &  177 \\ 
      P &     &     &     &     &     &     &   &    & 100 &  53  & 153 \\ 
      C &     &     &     &     &     &     &   &    & 100 & ?  & $\geq$ 100 \\ 
      Q &     &     &     &     &     &     &   &    &   3 &  23  &  26 \\ \hline
\end{tabular}
}
\caption{\label{table:compgoal}Results for Goal-Based Problems.
Domain-specific planners are starred. Entries are the percentage of
runs in which the goal was reached.  A blank indicates that the
planner was unable to attempt the problem. A \nega\ indicates that the
planner attempted the problem but was never able to achieve the
goal. A ? indicates that the result is unavailable (due to
a bug in the evaluation software, a couple of the results initially announced
were found to be invalid).}
\vspace*{-1ex}
\end{table}

\begin{table}[p]
{\footnotesize
\begin{tabular}{|l|r@{~~}r@{~~}r@{~~~~~}c@{~~}r@{~~}r@{~~}r@{~~}r@{~~}r@{~~~~~}r@{}r@{}r|rr|r|} \cline{1-15}
          \multicolumn{1}{|c|}{dom} &
          \multicolumn{3}{c}{bw-c-r} & 
          \multicolumn{6}{c}{bw-nc-r} &
          \multicolumn{3}{c|}{bx-r} &
          \multicolumn{1}{c}{file} &
          \multicolumn{1}{c|}{tire-r} \\ \cline{1-16}
          \multicolumn{1}{|c|}{prob} &
          \multicolumn{1}{c@{~~}}{5} & 
          \multicolumn{1}{c@{~~}}{8} & 
          \multicolumn{1}{c@{~~~~}}{11} &   
          \multicolumn{1}{c@{~~}}{5} & 
          \multicolumn{1}{c@{~~}}{8} & 
          \multicolumn{1}{c@{~~}}{11} &   
          \multicolumn{1}{c@{~~}}{15} & 
          \multicolumn{1}{c@{~~}}{18} & 
          \multicolumn{1}{c@{~~~~}}{21} &   
          \multicolumn{1}{c@{}}{5-10} & 
          \multicolumn{1}{c@{}}{10-10} & 
          \multicolumn{1}{c|}{10-15} & 
          \multicolumn{1}{c}{30-4} &
          \multicolumn{1}{c|}{30-4} &
          \multicolumn{1}{c|}{total}\\ \hline
     J1* & 497 & 487 & 481 & 494 & 489 & 480 & 470 & 462 & 458 & 419 & 317   & 129   & \none & \none & 5183\\
{\bf G2}*& {\bf 495} &  {\bf 486} &  {\bf 480} & {\bf 495} & {\bf 490} &  {\bf 480}  & {\bf 468} & {\bf 352} & {\bf 286} & {\bf 438} & {\bf 376} &  {\bf \nega} & {\bf \none} & {\bf \none} & 4846\\
      E* & 496 & 492 & 486 & 495 & 490 &    &    &   &    & \none & \none   & \none   & \none & \none & 2459\\ 
     J2* & 497 & 486 & 482 & 495 & 490 & 480 & 468 & \nega & 455 & 376 & \nega & \nega & \none & \none & 4229\\ \hline

     J3 & 496 & 487 & 482 & 494 & 490 & 481 & \nega & \nega   & 459 & 425 &  346  &  279  &  36 & \nega & 4475\\ 
      P &     &     &     & 494 & 488 & 466 & 397 &     &     & 184 & \nega &       &  58 & \nega & 2087\\ 
      C &     &     &     & 495 &     &     &     &     &     &     &       &       &     & ?  &  $\geq$ 495\\ 
{\bf G1}&     &     &     & {\bf 495} &     &     &     &     &     &       &       &     &{\bf \nega} & {\bf \nega} &  {\bf 495}\\
      R &     &     &     & 494 &     &     &     &     &     &     &       &       &     &     &  494\\ 
      Q &     &     &     & 180 &     &     &     &     &     &     &       &       &     &  11 &  191\\ 
 
\hline

\end{tabular}
}
\caption{\label{table:compreward}Results for Reward-Based Problems.
Domain-specific planners are starred.  Entries are the average reward
achieved over the 30 runs.  A blank indicates that the planner was
unable to attempt the problem. A \nega\ indicates that the planner
attempted the problem but did not achieve a strictly positive reward.
A ? indicates that the result is unavailable.}
\vspace*{-2ex}
\end{table}

The planners participating in the competition are shown in
Table~\ref{table:participants}. Planners 
E, G2, J1, and J2 are domain-specific: either they are
tuned for blocks and box worlds, or they use domain-specific search
control knowledge, or learn from examples. The other participating
planners are domain-independent.

Tables~\ref{table:compgoal}\ and~\ref{table:compreward}\ show the
results of the competition, which we extracted from the competition
overview paper \cite{younes:etal:05}\ and from the competition web
site \url{http://www.cs.rutgers.edu/~mlittman/topics/ipc04-pt/}.  The
first of those tables concerns goal-based problems and the second the
reward-based problems. The entries in the tables represent the
goal-achievement percentage or average reward achieved by the various
planner versions (left-column) on the various problems (top two
rows). Planners in the top part of the tables are domain-specific.
Problems from the known domains lie on the left-hand side of the
tables.  The colored blocks world problems are {\sf bw-c-nr}
(goal-based version) and {\sf bw-c-r} (reward version) with 5, 8, and
11 blocks. The non-colored blocks world problems are {\sf bw-nc-nr}
(goal-based version) with 8 blocks, and {\sf bw-nc-r} (reward-based
version) with 5, 8, 11, 15, 18, and 21 blocks. The box world problems
are {\sf bx-nr} (goal-based) and {\sf bx-r} (reward-based), with 5 or
10 cities and 10 or 15 boxes. Problems from the unknown domains lie on
the right hand side of the tables. They comprise: {\sf expl-bw}, an
exploding version of the 11 block blocks world problem in which
putting down a block may destroy the object it is put on, {\sf zeno},
a probabilistic variant of a zeno travel domain problem from the IPC-3
with 1 plane, 2 persons, 3 cities and 7 fuel levels, {\sf hanoise}, a
probabilistic variant of the tower of hanoi problem with 5 disks and 3
rods, {\sf file}, a problem of putting 30 files in 5 randomly chosen
folders, and {\sf tire}, a variant a the tire world problem with 30
cities and spare tires at 4 of them, where the tire may go flat while
driving.

Our planner \nmrdpp\ in its G1 or G2 version, was able to attempt all
problems, achieving a strictly positive reward in all but 4 of them.
Not even {\sc ff} (J3), the competition overall winner, was able to
successfully attempt that many problems. \nmrdpp\ performed
particularly well on goal-based problems, achieving the goal in 100\%
of the runs except in {\sf expl-bw}, {\sf hanoise}, and {\sf tire-nr}
(note that for these three problems, the goal achievement probability
of the optimal policy does not exceed 65\%). No other planner
outperformed \nmrdpp\ on that scale.  As pointed out before, {\sc ff}\
behaves well on the probabilistic version of blocks and box world
because the optimal policies are very close to those for the
deterministic problem -- Hoffmann \citeyear{hoffmann:02}\ analyses
the reasons why the {\sc ff}\ heuristic works well for traditional
planning benchmarks such as blocks world and logistics. On the other
hand, {\sc ff}\ is unable to solve the unknown problems which have a
different structure and require more substantial probabilistic
reasoning, although these problems are easily solved by a number of
participating planners.  As expected, there is a large discrepancy
between the version of \nmrdpp\ allowed to use search control (G2) and
the domain-independent version (G1). While the latter performs okay
with the unknown goal-based domains, it is not able to solve any of
the known ones. In fact, to except for {\sc ff}, none of the
participating domain-independent planners were able to solve these
problems.


In the reward-based case, \nmrdpp\ with control knoweldge behaves well
on the known problems. Only the human-encoded policies (J1) performed
better. Without control knowledge \nmrdpp\ is unable to scale on those
problems, while other participants such as {\sc ff}\ and m{\sc gpt}\
are. Furthermore \nmrdpp\ appears to perform poorly on the two unknown
problems.  In both cases, this might be due to the fact that it fails
to generate an optimal policy: suboptimal policies easily have a high
negative score in these domains \cite<see>{younes:etal:05}.  For {\sf
r-tire}, we know that \nmrdpp\ did indeed generate a suboptimal
policy. Additionally, it could be that \nmrdpp\ was unlucky with the
sampling-based policy evaluation process: in {\sf tire-r} in
particular, there was a high variance between the costs of various
trajectories in the optimal policy.

Alltogether, the competition results suggest that control knowledge is
likely to be essential when solving larger problems (Markovian or not)
with \nmrdpp, and that, as has been observed with deterministic
planners, approaches making use of control knowledge are quite
powerful.


\section{Conclusion, Related, and Future Work}
\label{sec:conclusion}

In this paper, we have examined the problem of solving decision
processes with non-Markovian rewards. We have described existing
approaches which exploit a compact representation of the reward
function to automatically translate the NMRDP into an equivalent
process amenable to MDP solution methods. The computational model
underlying this framework can be traced back to work on the
relationship between linear temporal logic and automata in the areas
of automated verification and model-checking
\cite{vardi:03,wolper:87}. While remaining in this framework, we
have proposed a new representation of non-Markovian reward functions
and a translation into MDPs aimed at making the best possible use of
state-based anytime heuristic search as the solution method. Our
representation extends future linear temporal logic to express
rewards. Our translation has the effect of embedding model-checking in
the solution method. It results in an MDP of the minimal size
achievable without stepping outside the anytime framework, and
consequently in better policies by the deadline. We have described
\nmrdpp, a software platform that implements such approaches under a
common interface, and which proved a useful tool in their experimental
analysis. Both the system and the analysis are the first of their
kind.  We were able to identify a number of general trends in the
behaviours of the methods and to provide advice as to which are the
best suited to certain circumstances. For obvious reasons, our
analysis has focused on artificial domains. Additional work should
examine a wider range of domains of more practical interest, to
see what form these results take in that context. Ultimately,
we would like our analysis to help \nmrdpp\ automatically select
the most appropriate method. Unfortunately,
because of the difficulty of translating between PLTL and \xfltl,
it is likely that \nmrdpp\ would still have to maintain both a
PLTL and a \xfltl\ version of the reward formulae.

A detailed comparison of our approach to solving NMRDPs with existing
methods \cite{bacchus:etal:96,bacchus:etal:97}\ 
can be found in Sections~\ref{subsec:discussion}\
and~\ref{sec:experiments}. Two important aspects of future work would
help take the comparison further.  One is to settle the question of
the appropriateness of our translation to structured solution methods.
Symbolic implementations of the solution methods we consider, e.g.
symbolic LAO* \cite{feng:hansen:02}, as well as formula progression in
the context of symbolic state representations
\cite{pistore:traverso:01}\ could be investigated for that
purpose. The other is to take advantage of the greater expressive
power of \xfltl\ to consider a richer class of decision processes, for
instance with uncertainty as to which rewards are received and when.
Many extensions of the language are possible: adding eventualities,
unrestricted negation, first-class reward propositions, quantitative
time, etc. Of course, dealing with them via progression without
backtracking is another matter.

We should investigate the precise relationship between our line of
work and recent work on planning for temporally extended goals in
non-deterministic domains. Of particular interest are `weak'
temporally extended goals such as those expressible in the Eagle
language \shortcite{dallago:etal:02}, and temporally extended goals
expressible in $\pi$-CTL* \cite{baral:zhao:04}.  Eagle enables the
expression of attempted reachability and maintenance goals of the form
``try-reach $p$'' and ``try-maintain $p$'', which add to the goals
``do-reach $p$'' and ``do-maintain $p$'' already expressible in
CTL. The idea is that the generated policy should make every attempt
at satisfying proposition $p$. Furthermore, Eagle includes recovery
goals of the form ``$g_1$ fail $g_2$'', meaning that goal $g_2$ must
be achieved whenever goal $g_1$ fails, and cyclic goals of the form
``repeat $g$'', meaning that $g$ should be achieved cyclically until
it fails.  The semantics of these goals is given in terms of variants
of B\"uchi tree automata with preferred transitions.  Dal Lago et al.\
\citeyear{dallago:etal:02}\ present a planning algorithm based on
symbolic model-checking which generates policies achieving those
goals.  Baral and Zhao \citeyear{baral:zhao:04}\ describe $\pi$-CTL*,
an alternative framework for expressing a subset of Eagle goals and a
variety of others. $\pi$-CTL* is a variant of CTL* which allows for
formulae involving two types of path quantifiers: quantifiers tied to
the paths feasible under the generated policy, as is usual, but also
quantifiers more generally tied to the paths feasible under any of the
domain actions.  Baral and Zhao \citeyear{baral:zhao:04}\ do not
present any planning algorithm.  It would be very interesting to know
whether Eagle and $\pi$-CTL* goals can be encoded as non-Markovian
rewards in our framework. An immediate consequence would be that
\nmrdpp\ could be used to plan for them.  More generally, we would
like to examine the respective merits of non-deterministic planning
for temporally extended goals and decision-theoretic planning with
non-Markovian rewards.

In the pure probabilistic setting (no rewards), recent related
research includes work on planning and controller synthesis for
probabilistic temporally extended goals expressible in probabilistic
temporal logics such as CSL or PCTL
\shortcite{younes:simmons:04,baier:etal:04}.  These logics enable
expressing statements about the probability of the policy satisfying a
given temporal goal exceeding a given threshold. For instance, Younes
and Simmons \citeyear{younes:simmons:04}\ describe a very general
probabilistic planning framework, involving concurrency, continuous
time, and temporally extended goals, rich enough to model generalised
semi-Markov processes. The solution algorithms are not directly
comparable to those presented here.


Another exciting future work area is the investigation of temporal
logic formalisms for specifying heuristic functions for NMRDPs or more
generally for search problems with temporally extended goals.  Good
heuristics are important to some of the solution methods we are
targeting, and surely their value ought to depend on history. The
methods we have described could be applicable to the description and
processing of such heuristics. Related to this is the problem of
extending search control knowledge to {\em fully}\ operate under the
presence of temporally extended goals, rewards, and stochastic
actions.  A first issue is that branching or probabilistic logics such
as CTL or PCTL variants should be preferred to FLTL when describing
search control knowledge, because when stochastic actions are
involved, search control often needs to refer to {\it some}\ of the
possible futures and even to their probabilities.\footnote{We would
{\em not} argue, on the other hand, that CTL is necessary for
representing non-Markovian {\em rewards}.}  Another major problem is
that the GOALP modality, which is the key to the specification of
reusable search control knowledge is interpreted with respect to a
fixed reachability goal\footnote{Where $f$ is an atemporal formula,
GOALP($f$) is true iff $f$ is true of all goal states.}
\cite{bacchus:kabanza:00}, and as such, is not applicable to domains
with temporally extended goals, let alone
rewards. Kabanza and Thi\'ebaux \citeyear{kabanza:thiebaux:05}\ 
present a first approach to
search control in the presence of temporally extended goals in
deterministic domains, but much remains to be done for a system like
\nmrdpp\ to be able to support a meaningful extension of GOALP.

Finally, let us mention that related work in the area of databases
uses a similar approach to \pltlstruct\ to extend a database with
auxiliary relations containing sufficient information to check
temporal integrity constraints \cite{chomicki:95}. The issues are
somewhat different from those raised by NMRDPs: as there is only ever
one sequence of databases, what matters is more the size of these
auxiliary relations than avoiding making redundant distinctions.


\section*{Acknowledgements}
Many thanks to Fahiem Bacchus, Rajeev Gor\'e, Marco Pistore, Ron van
der Meyden, Moshe Vardi, and Lenore Zuck for useful discussions and
comments, as well as to the anonymous reviewers and to David Smith for
their thorough reading of the paper and their excellent suggestions.
Sylvie Thi\'ebaux, Charles Gretton, John Slaney, and David Price thank
National ICT Australia for its support. NICTA is funded through the
Australian Government's {\em Backing Australia's Ability} initiative,
in part through the Australian Research Council. Froduald Kabanza is
supported by the Canadian Natural Sciences and Engineering Research
Council (NSERC).

\appendix

\section{A Class of Reward-Normal Formulae}
\label{app:normal}

The existing decision procedure \cite{slaney:05}\ for determining
whether a formula is reward-normal is guaranteed to terminate
finitely, but involves the construction and comparison of automata and
is rather intricate in practice. It is therefore useful to give a
simple syntactic characterisation of a set of constructors for
obtaining reward-normal formulae even though not all such formulae are
so constructible.

We say that a formula is \emph{material} iff it contains no $\dollar$
and no temporal operators -- that is, the material formulae are the
boolean combinations of atoms.

We consider four operations on behaviours representable by formulae of
\xfltl. Firstly, a behaviour may be delayed for a specified number of
timesteps. Secondly, it may be made conditional on a material trigger.
Thirdly, it may be started repeatedly until a material termination
condition is met. Fourthly, two behaviours may be combined to form
their union. These operations are easily realised syntactically by
corresponding operations on formulae. Where $m$ is any material
formula:
\begin{eqnarray*}
     \mbox{{\sf delay}}[f]       & = & \next f         \\
     \mbox{{\sf cond}}[m,f]      & = & m \rightarrow f \\
     \mbox{{\sf loop}}[m,f]      & = & f \until m      \\
     \mbox{{\sf union}}[f_1,f_2] & = & f_1 \wedge f_2
\end{eqnarray*}
We have shown \cite{slaney:05}\ that the set of reward-normal formulae
is closed under {\sf delay}, {\sf cond} (for any material $m$), {\sf
  loop} (for any material $m$) and {\sf union}, and also that the
closure of $\{\dollar\}$ under these operations represents a class of
behaviours closed under intersection and concatenation as well as
union.

Many familiar reward-normal formulae are obtainable from $\dollar$ by
applying the four operations. For example, $\always(p \rightarrow
\dollar)$ is $\mbox{{\sf loop}}[\false,\mbox{{\sf cond}}[p,\dollar]]$.
Sometimes a paraphrase is necessary. For example, $\always((p \wedge
\next q) \rightarrow \next \dollar)$ is not of the required form
because of the $\next$ in the antecedent of the conditional, but the
equivalent $\always(p \rightarrow \next(q \rightarrow \dollar))$ is
$\mbox{{\sf loop}}[\false,\mbox{{\sf cond}}[p,\mbox{{\sf
    delay}}[\mbox{{\sf cond}}[q,\dollar]]]]$. Other cases are not so
easy. An example is the formula $\neg p \until (p \wedge \dollar)$
which stipulates a reward the first time $p$ happens and which is not
at all of the form suggested. To capture the same behaviour using the
above operations requires a formula like $(p \rightarrow \dollar)
\wedge (\next(p \rightarrow \dollar) \until p)$.

\section{Proofs of Theorems}
\label{app:proofs}

{\bf Property \ref{prop:fundamental}} Where $b \Leftrightarrow
(\Gamma(i) \in B)$, $(\Gamma,i) \modelsb{B} f$ iff $(\Gamma,i+1)
\modelsb{B} \Prog(b, \Gamma_i,f)$.

\medskip\noindent
\theproof{ Induction on the structure of $f$. There are several base
  cases, all fairly trivial. If $f=\true$ or $f=\false$ there is
  nothing to prove, as these progress to themselves and hold
  everywhere and nowhere respectively. If $f = p$ then if $f$ holds in
  $\Gamma_i$ then it progresses to $\true$ which holds in
  $\Gamma_{i+1}$ while if $f$ does not hold in $\Gamma_i$ then it
  progresses to $\false$ which does not hold in $\Gamma_{i+1}$. The
  case $f = \neg p$ is similar. In the last base case, $f = \dollar$.
  Then the following are equivalent: \\
  \hspace*{1.5em} $(\Gamma,i) \modelsb{B} f$ \\
  \hspace*{1.5em} $\Gamma(i) \in B$ \\
  \hspace*{1.5em} $b$ \\
  \hspace*{1.5em} $\Prog(b,\Gamma_i,f) = \true$ \\
  \hspace*{1.5em} $(\Gamma,i+1) \modelsb{B} \Prog(b, \Gamma_i,f)$
  
  \medskip\noindent
  Induction case 1: $f = g \wedge h$. The following are equivalent: \\
  \hspace*{1.5em} $(\Gamma,i) \modelsb{B} f$ \\
  \hspace*{1.5em} $(\Gamma,i) \modelsb{B} g$ and $(\Gamma,i) \modelsb{B} h$ \\
  \hspace*{1.5em} $(\Gamma,i+1) \modelsb{B} \Prog(b, \Gamma_i,g)$ and
  $(\Gamma,i+1) \modelsb{B} \Prog(b, \Gamma_i,h)$ (by induction
  hypothesis) \\
  \hspace*{1.5em} $(\Gamma,i+1) \modelsb{B} \Prog(b, \Gamma_i,g) \wedge
  \Prog(b, \Gamma_i,h)$ \\
  \hspace*{1.5em} $(\Gamma,i+1) \modelsb{B} \Prog(b, \Gamma_i,f)$

  \medskip\noindent
  Induction case 2: $f = g \vee h$. Analogous to case 1.

  \medskip\noindent
  Induction case 3: $f = \next g$. Trivial by inspection of the definitions.
  
  \medskip\noindent
  Induction case 4: $f = g \until h$. Then $f$ is logically equivalent
  to $h \vee (g \wedge \next(g \until h)$ which by cases 1, 2 and 3 holds at
  stage $i$ of $\Gamma$ for behaviour $B$ iff $\Prog(b, \Gamma_i, f)$
  holds at stage i+1.
}

\bigskip\noindent
{\bf Theorem \ref{thm:prog:ok}} \ 
%
{\it Let $f$ be reward-normal, and let $\langle f_0, f_1, \ldots
  \rangle$ be the result of progressing it through the successive
  states of a sequence $\Gamma$. Then, provided no $f_i$ is $\false$,
  for all $i$ $\MRew(\Gamma_i,f_i)$ iff $\Gamma(i)\in B_{f}$.}
  
  \medskip\noindent \theproof{ First, by the definition of
    reward-normality, if $f$ is reward-normal then $\Gamma \modelsb{B}
    f$ iff for all $i$, if $\Gamma(i) \in B_f$ then $\Gamma(i) \in B$.
    Next, if $\Gamma \modelsb{B} f$ then progressing $f$ through
    $\Gamma$ according to $B$ (that is, letting each $b_i$ be true iff
    $\Gamma(i) \in B$) cannot lead to a contradiction because by
    Property \ref{prop:fundamental}, progression is truth-preserving.

    It remains, then, to show that if $\Gamma \notmodelsb{B} f$ then
    progressing $f$ through $\Gamma$ according to $B$ must lead
    eventually to $\false$. The proof
    of this is by induction on the structure of $f$ and as usual the
    base case in which $f$ is a literal (an atom, a negated atom or
    $\true$, $\false$ or $\dollar$) is trivial.

    Case $f = g \wedge h$. Suppose $\Gamma \notmodelsb{B} f$. Then
    either $\Gamma \notmodelsb{B} g$ or $\Gamma \notmodelsb{B} h$, so
    by the induction hypothesis either $g$ or $h$ progresses
    eventually to $\false$, and hence so does their conjunction.

    Case $f = g \vee h$. Suppose $\Gamma \notmodelsb{B} f$. Then both
    $\Gamma \notmodelsb{B} g$ and $\Gamma \notmodelsb{B} h$, so by the
    induction hypothesis each of $g$ and $h$ progresses eventually to
    $\false$. Suppose without loss of generality that $g$ does not
    progress to $\false$ before $h$ does. Then at some point $g$ has
    progressed to some formula $g'$ and $f$ has progressed to $g' \vee
    \false$ which simplifies to $g'$. Since $g'$ also progresses to
    $\false$ eventually, so does $f$.

    Case $f = \next g$. Suppose $\Gamma \notmodelsb{B} f$. Let $\Gamma
    = \Gamma_0;\Delta$ and let $B' = \{\gamma| \Gamma_0;\gamma \in
    B\}$. Then $\Delta \notmodelsb{B'} g$, so by the induction
    hypothesis $g$ progressed through $\Delta$ according to $B'$
    eventually reaches $\false$. But The progression of $f$ through
    $\Gamma$ according to $B$ is exactly the same after the first
    step, so that too leads to $\false$.

    Case $f = g \until h$. Suppose $\Gamma \notmodelsb{B} f$. Then
    there is some $j$ such that $(\Gamma,j) \notmodelsb{B} g$ and for
    all $i \leq j$, $(\Gamma,i) \notmodelsb{B} h$. We proceed by
    induction on $j$. In the base case $j=0$, and both $\Gamma
    \notmodelsb{B} g$ and $\Gamma \notmodelsb{B} h$ whence by the main
    induction hypothesis both $g$ and $h$ will eventually progress to
    $\false$. Thus $h \vee (g \wedge f')$ progresses eventually to
    $\false$ for any $f'$, and in particular for $f' = \next f$,
    establishing the base case. For the induction case, suppose
    $\Gamma \modelsb{B} g$ (and of course $\Gamma \notmodelsb{B} h$).
    Since $f$ is equivalent to $h \vee (g \wedge \next f)$ and $\Gamma
    \notmodelsb{B} f$, $\Gamma \notmodelsb{B} h$ and $\Gamma
    \modelsb{B} g$, clearly $\Gamma \notmodelsb{B} \next f$.  Where
    $\Delta$ and $B'$ are as in the previous case, therefore, $\Delta
    \notmodelsb{B'} f$ and the failure occurs at stage $j-1$ of
    $\Delta$.  Therefore the hypothesis of the induction on $j$
    applies, and $f$ progressed through $\Delta$ according to $B'$
    goes eventually to $\false$, and so $f$ progressed through
    $\Gamma$ according to $B$ goes similarly to $\false$.}

\bigskip\noindent
{\bf Theorem \ref{thm:minimal}} \ 
%
{\it Let $S'$ be the set of e-states in an equivalent MDP $D'$ for
  $D=\langle S,s_0,A,\T,R\rangle$. $D'$ is minimal iff every e-state
  in $S'$ is reachable and $S'$ contains no two distinct e-states
  $s'_1$ and $s'_2$ with $\tau(s'_1) = \tau(s'_2)$ and $\mu(s'_1) =
  \mu(s'_2)$.}
  
\medskip\noindent
%
\theproof{Proof is by construction of the canonical equivalent MDP
  $D^c$. Let the set of finite prefixes of state sequences in
  $\widetilde{D}(s_0)$ be partitioned into equivalence classes, where
  ${\Gamma}1(i) \equiv {\Gamma}2(j)$ iff ${\Gamma}1_i = {\Gamma}2_j$
  and for all $\Delta\in S^*$ such that ${\Gamma}1(i);\Delta \in
  \widetilde{D}(s_0)$, $R({\Gamma}1(i);\Delta) =
  R({\Gamma}2(j);\Delta)$. Let $[\Gamma(i)]$ denote the equivalence
  class of $\Gamma(i)$. Let ${\cal E}$ be the set of these equivalence
  classes. Let ${\cal A}$ be the function that takes each
  $[\Gamma(i)]$ in ${\cal E}$ to $A(\Gamma_i)$. For each $\Gamma(i)$
  and $\Delta(j)$ and for each $a \in {\cal A}([\Gamma(i)])$, let
  ${\cal T}( [\Gamma(i)],a,[\Delta(j)] )$ be $\TTT{a}{\Gamma_i}{s}$ if
  $[\Delta(j)] = [\Gamma(i);\langle s \rangle]$. Otherwise let ${\cal
    T}( [\Gamma(i)],a,[\Delta(j)] ) = 0$. Let ${\cal R}([\Gamma(i)])$
  be $R(\Gamma(i))$. Then note the following four facts:
\begin{enumerate}
\item Each of the functions $A$, $T$ and $R$ is well-defined.
\item $D^c = \langle {\cal E}, [\langle s_0 \rangle], {\cal A}, {\cal
    T}, {\cal R} \rangle$ is an equivalent MDP for $D$ with
  $\tau([\Gamma(i)])=\Gamma_i$.
\item For any equivalent MDP $D''$ of $D$ there is a mapping from a
  subset of the states of $D''$ onto $\cal E$.
\item $D'$ satisfies the condition that every e-state in $S'$ is
  reachable and $S'$ contains no two distinct e-states $s'_1$ and
  $s'_2$ with $\tau(s'_1) = \tau(s'_2)$ and $\mu(s'_1) = \mu(s'_2)$
  iff $D^c$ is isomorphic to $D'$.
\end{enumerate}

What fact 1 above amounts to is that if $\Gamma{1}(i) \equiv
\Gamma{2}(j)$ then it does not matter which of the two sequences is
used to define ${\cal A}$, ${\cal T}$ and ${\cal R}$ of their
equivalence class. In the cases of ${\cal A}$ and ${\cal T}$ this is
simply that $\Gamma{1}_i = \Gamma{2}_j$. In the case of ${\cal R}$, it
is the special case $\Delta = \langle \Gamma{1}_i \rangle$ of the
equality of rewards over extensions.

Fact 2 is a matter of checking that the four conditions of Definition
\ref{def:equivalent} hold. Of these, conditions 1 ($\tau([s_0]) =
s_{0}$) and 2 (${\cal A}([\Gamma(i)])= A(\Gamma_i)$) hold trivially by
the construction. Condition 4 says that for any feasible state
sequence $\Gamma \in \widetilde{D}(s_0)$, we have ${\cal
  R}([\Gamma(i)]) = R(\Gamma(i))$ for all $i$. This also is given in
the construction.  Condition 3 states:
\begin{quote}
  For all $s_1,s_2\in S$, if there is $a\in A(s_1)$ such that
  $\TTT{a}{s_1}{s_2} > 0$, then for all $\Gamma(i) \in
  \widetilde{D}(s_0)$ such that $\Gamma_i = s_1$, there exists a
  unique $[\Delta(j)] \in {\cal E}$, $\Delta_j = s_2$, such that for
  all $a \in {\cal A}([\Gamma(i)])$, ${\cal
    T}([\Gamma(i)],a,[\Delta[j]]) = \TTT{a}{s_1}{s_2}$.
\end{quote}
Suppose $\TTT{\alpha}{s_1}{s_2} > 0$, $\Gamma(i) \in
\widetilde{D}(s_0)$ and $\Gamma_i = s_1$. Then the required
$\Delta(j)$ is $\Gamma(i);\langle s_2 \rangle$, and of course ${\cal
  A}([\Gamma(i)]) = A(\Gamma_i)$, so the required condition reads:
\begin{quote}
  $[\Gamma(i);\langle s_2 \rangle]$ is the unique element $X$ of
  ${\cal E}$ with $\tau(X) = s_2$ such that for all $a \in
  A(\Gamma_i)$, ${\cal T}( [\Gamma(i)],a,X ) = \TTT{a}{s_1}{s_2}$.
\end{quote}
To establish existence, we need that if $a \in A(\Gamma_i)$ then
${\cal T} ( [ \Gamma(i) ],a, [\Gamma(i);\langle s_2 \rangle] ) =
\TTT{a}{\Gamma_i}{s_2}$, which is immediate from the definition of
$\cal T$ above. To establish uniqueness, suppose that $\tau(X) = s_2$
and ${\cal T}( [\Gamma(i)],a,X ) = \TTT{a}{s_1}{s_2}$ for all actions
$a \in A(\Gamma_i)$. Since $\TTT{\alpha}{s_1}{s_2} > 0$, the
transition probability from $[\Gamma(i)]$ to $X$ is nonzero for some
action, so by the definition of $\cal T$, $X$ can only be
$[\Gamma(i);\langle s_2 \rangle]$.

Fact 3 is readily observed. Let $M$ be any equivalent MDP for $D$. For
any states $s_1$ and $s_2$ of $D$, and any state $X$ of $M$ such that
$\tau(X) = s_1$ there is at most one state $Y$ of $M$ with $\tau(Y) =
s_2$ such that some action $a \in A(s_1)$ gives a nonzero probability
of transition from $X$ to $Y$. This follows from the uniqueness part
of condition 3 of Definition \ref{def:equivalent} together with the
fact that the transition function is a probability distribution (sums
to 1). Therefore for any given finite state sequence $\Gamma(i)$ there
is at most one state of $M$ reached from the start state of $M$ by
following $\Gamma(i)$. Therefore $M$ induces an equivalence relation
$\approx_M$ on $S^*$: $\Gamma(i) \approx_M \Delta(j)$ iff they lead to
the same state of $M$ (the sequences which are not feasible in $M$ may
all be regarded as equivalent under $\approx_M$). Each reachable state
of $M$ has associated with it a nonempty equivalence class of finite
sequences of states of $D$. Working through the definitions, we may
observe that $\approx_M$ is a sub-relation of $\equiv$ (if $\Gamma(i)
\approx_M \Delta(j)$ then $\Gamma(i) \equiv \Delta(j)$). Hence the
function that takes the equivalence class under $\approx_M$ of each
feasible sequence $\Gamma(i)$ to $[\Gamma(i)]$ induces a mapping $h$
(an epimorphism in fact) from the reachable subset of states of $M$
onto $\cal E$.

To establish Fact 4, it must be shown that in the case of $D'$ the
mapping can be reversed, or that each equivalence class $[\Gamma(i)]$
in $D^c$ corresponds to exactly one element of $D'$. Suppose not (for
contradiction). Then there exist sequences $\Gamma{1}(i)$ and
$\Gamma{2}(j)$ in $\widetilde{D}(s_0)$ such that $\Gamma{1}(i) \equiv
\Gamma{2}(j)$ but on following the two sequences from $s_0'$ we arrive
at two different elements $s'_1$ and $s'_2$ of $D'$ with $\tau(s'_1) =
\Gamma{1}_i = \Gamma{2}_j = \tau(s'_2)$ but with $\mu(s'_1) \neq
\mu(s'_2)$.  Therefore there exists a sequence $\Delta(k) \in
\widetilde{D}(s)$ such that $R(\Gamma{1}(i-1);\Delta(k)) \neq
R(\Gamma{2}(j-1);\Delta(k))$. But this contradicts the condition for
$\Gamma{1}(i) \equiv \Gamma{2}(j)$.  }

Theorem \ref{thm:minimal} follows immediately from facts 1--4.


\bigskip\noindent
{\bf Theorem \ref{thm:blindminimal}} \ 
%
  {\it Let $D'$ be the translation of $D$ as in
  Definition~\ref{def:translation}. $D'$ is a blind minimal
  equivalent MDP for $D$.}
  
\medskip\noindent
%
\theproof{Reachability of all the e-states is obvious, as they are
  constructed only when reached. Each e-state is a pair $\langle s,
  \phi \rangle$ where $s$ is a state of $D$ and $\phi$ is a reward
  function specification. In fact, $s = \tau(\langle s, \phi \rangle)$
  and $\phi$ determines a distribution of rewards over all
  continuations of the sequences that reach $\langle s, \phi \rangle$.
  That is, for all $\Delta$ in $S^*$ such that $\Delta_0 = s$, the
  reward for $\Delta$ is $\sum_{(f:r) \in \phi} \{r\mid \Delta \in
  B_{f}\}$. If $D'$ is not blind minimal, then there exist distinct
  e-states $\langle s, \phi \rangle$ and $\langle s, \phi' \rangle$
  for which this sum is the same for all $\Delta$. But this makes
  $\phi$ and $\phi'$ semantically equivalent, contradicting the
  supposition that they are distinct.


}

\section{Random Problem Domains}
\label{app:random}
Random problem domains are produced by first creating a random action
specification defining the domain dynamics.  Some of the experiments
we conducted\footnote{None of those are included in this paper,
however.}\ also involved producing, in a second step, a random reward
specification that had desired properties in relation to the generated
dynamics.

The random generation of the domain dynamics takes as parameters the
number $n$ of propositions in the domain and the number of actions to be
produced, and starts by assigning some effects to each action such
that each proposition is affected by exactly one action.  For example,
if we have 5 actions and 14 propositions, the first 4 actions may
affect 3 propositions each, the 5th one only 2, and the affected 
propositions are all different. Once each action has
some initial effects, we continue to add more effects one at a time,
until a sufficient proportion of the state space is reachable -- see
``proportion reachable'' parameter below. 
Each additional effect is generated by picking up a random action
and a random proposition, and producing a random decision
diagram according to the ``uncertainty'' and ``structure'' parameters
below:

\begin{description}
\item{The Uncertainty}
parameter is the probability of a non zero/one
value as a leaf node.  An uncertainty of 1 will result in all leaf
nodes having random values from a uniform distribution.  An uncertainty
of 0 will result in all leaf nodes having values 0 or 1 with an equal
probability.

\item{The Structure (or influence)}
parameter is the probability of a decision diagram
containing  a particular proposition.  So an influence of 1 will
result in all decision diagrams including all 
propositions (and very unlikely to have significant structure), 
while 0 will result in decision diagrams that 
do not depend on the values of propositions.

\item{The Proportion Reachable} parameter is a lower bound on the
proportion of the entire $2 ^ n$ state space that is reachable from
the start state.  The algorithm adds behaviour until this lower bound
is reached.  A value of 1 will result in the algorithm running until
the actions are sufficient to allow the entire state space to be
reachable.

\end{description}

A reward specification can be produced with regard to the generated
dynamics such that a specified number of the rewards are reachable and
a specified number are unreachable.  First, a decision diagram is
produced to represent which states are reachable and which are not,
given the domain dynamics.  Next, a random path is taken from the root
of this decision diagram to a true terminal if we are generating an
attainable reward, or a false terminal if we are producing an
unattainable reward.  The propositions encountered on this path, both
negated and not, form a conjunction that is the reward formula.  This process
is repeated until the desired number of reachable and unreachable
rewards are obtained.

\bibliography{thiebaux06a} \bibliographystyle{theapa}




\end{document}
