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,4all 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{\$}))$.
Sylvie Thiebaux 2006-01-20