The PLTLSTR translation can be seen as a symbolic version of
PLTLSIM. The set of added temporal variables contains the purely
temporal subformulae
of the reward formulae in , to
which the modality is prepended (unless already there):
. By repeatedly applying
the equivalence
to any subformula in
, we can express its
current value, and hence that of reward formulae, as a function of the
current values of formulae in and state variables, as required by
the compact representation of the transition and reward models.
For our NMRDP example in Figure 3, the set of purely
temporal variables is
, and
is identical to
. Figure 6 shows some
of the ADDs forming part of the symbolic MDP produced by PLTLSTR:
the ADDs describing the dynamics of the temporal variables, i.e., the
ADDs describing the effects of the actions and on their
respective values, and the ADD describing the reward.
Figure 6:
ADDs Produced by PLTLSTR. prv (previously)
stands for
1. dynamics of
2. dynamics of
3. reward
As a more complex illustration, consider this example
[3] in which
We have that
and so the set of temporal variables
used is
Using the equivalences,
the reward can be decomposed and expressed by means of the
propositions and the temporal variables as follows:
As with PLTLSIM, the underlying MDP produced by PLTLSTR 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 dynamic analysis of rewards
contrast with PLTLMIN's static analysis [2] 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.