For the choice of the s,
Bacchus et al. [2] consider two
cases. In the simple case, which we call PLTLSIM, an MDP obeying
properties (1) and (2) is produced by simply labelling each e-state
with the set of all subformulae in
which are
true of the sequence leading to that e-state. This MDP is generated
forward, starting from the initial e-state labelled with and
with the set
of all subformulae which
are true of the sequence
. The successors of any
e-state labelled by NMRDP state and subformula set are
generated as follows: each of them is labelled by a successor of
in the NMRDP and by the set of subformulae
.
For instance, consider the NMRDP shown in Figure 3. The set
consists of a single reward
formula. The set
consists of all subformulae of this
reward formula, and their negations, that is
. The equivalent MDP produced by PLTLSIM is shown in
Figure 4.
Figure 3:
Another Simple NMRDP
|
Sylvie Thiebaux
2006-01-20