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. PLTLSTR(A) below). Not 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 $FLTL formulae. PLTLSTR(A) is an example of an interesting variant of PLTLSTR, 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 PLTLSTR 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* [21]. However, an important aspect of what we do here is that temporal variables are also included in the BDD.