Examples

It is intuitively clear that many behaviours can be specified by means of $FLTL formulae. While there is no simple way in general to translate between past and future tense expressions,⁴all of the examples used to illustrate PLTL in Section 2.2 above are expressible naturally in $FLTL, as follows. The classical goal formula $g$ saying that a goal $p$ is rewarded whenever it happens is easily expressed: $\mbox{$\Box$}(p \rightarrow \mbox{\$})$. 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 $\mbox{$\Box$}(p \rightarrow \mbox{$\Box$}\mbox{\$})$. 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 \makebox[1em]{$\mathbin{\mbox{\sf U}}$}(p \wedge \mbox{\$})$ stipulates only that the first occurrence of $p$ is rewarded (i.e. it specifies the behaviour in Figure 1). To reward the occurrence of $p$ at most once every $k$ steps, we write $\mbox{$\Box$}((\raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{k+1} p \wedge \mbox{$... ...\neg p) \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}^{k+1} \mbox{\$})$. For response formulae, where the achievement of $p$ is triggered by the command $c$, we write $\mbox{$\Box$}(c \rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}\mbox{$\Box$}(p \rightarrow \mbox{\$}))$ 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 $\mbox{$\Box$}(c\rightarrow \raisebox{0.6mm}{$\scriptstyle \bigcirc$}(\neg p \makebox[1em]{$\mathbin{\mbox{\sf U}}$} (p \wedge \mbox{\$})))$. As for bounded variants for which we only reward goal achievement within $k$ steps of the trigger command, we write for example $\mbox{$\Box$}(c \rightarrow \mbox{$\Box_{k}$}(p \rightarrow \mbox{\$}))$ 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 $\mbox{\$}\makebox[1em]{$\mathbin{\mbox{\sf U}}$}\neg p$. To say that we are rewarded if $p$ has been true since $q$ was, we write $\mbox{$\Box$}(q \rightarrow (\mbox{\$} \makebox[1em]{$\mathbin{\mbox{\sf U}}$}\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 \makebox[1em]{$\mathbin{\mbox{\sf U}}$}((\neg p \wedge \neg q) \vee (q \wedge \mbox{\$}))$.