Influence of Reachability

All approaches claim to have some ability to ignore variables which are irrelevant because the condition they track is unreachable:¹³PLTLMIN detects them through preprocessing, PLTLSTR 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 \circleddash ^{k} c$, resp. $g \wedge \makebox[8pt][c]{\makebox[0pt][c]{$\Diamond$}\makebox[0pt][c]{\raisebox{0.5pt}{-}}}_{k}c$, and in $FLTL, $\mbox{$\Box$}(c \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}^k (g \rightarrow \$))$, resp. $\mbox{$\Box$}(c \rightarrow \mbox{$\Box$}_k(g \rightarrow \$))$ When the 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 $\raisebox{0.6mm}{$\scriptstyle \bigcirc$}^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 15 illustrates the difference in performance as a function of the number $n$ of propositions involved in the SPUDD-LINEAR domain, when the reward is of the form $g \wedge \circleddash ^{n} c$, with $g$ unreachable.

Figure 15: Response Formula with Unachievable Goal

Figure 16: Response Formula with Unachievable Trigger

FLTL shines when the 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 $\circleddash ^{k} c$ and its subformulae, only to discover, after expensive preprocessing for PLTLMIN, after reachability analysis for PLTLSTR(A), and never for PLTLSTR, that these are irrelevant. This is illustrated in Figure 16, again with SPUDD-LINEAR and a reward of the form $g \wedge \circleddash ^{n} c$, with $c$ unreachable.