 In particular, in the pointed model \((M,w)\) pictured in Figure 1, the formula \(\lnot[\{a,b\}*]([a]p\mid p)\) is true because there is a path that begins at w, contains only p-worlds, uses only arrows in \(\{a,b\}\), and ends on the \(\lnot[a]p\)-world u. 