 Then, it is possible to build formulas as \(p \rightarrow [(q \qbin \scbin a) \bcup (\lnot q \qbin \scbin b)]r\) (“if p holds, then r will be achieved by choosing between actions a and b according to whether q holds”) and \(\lnot p \rightarrow \langle a \scbin (\lnot q \qbin \scbin a)^{\ast} \scbin q \qbin \rangle p\) (“if the desired requirement p is not true yet, it is possible to achieve it by a repeated execution of a”).