For any 
 <A HREF = "temporal-formula.html">temporal formula</A>
<CODE>F</CODE>, the 
 <A HREF = "temporal-formula.html">temporal formula</A>
<CODE>[]F</CODE> asserts that <CODE>F</CODE> is <EM>always</EM> true.

<P><BR><BR>
More precisely, <CODE>[]F</CODE> is true for a 
 <A HREF = "behavior.html">behavior</A> 
<PRE> 
  s , s , s , ... 
   1   2   3
</PRE> if and only if <CODE>F</CODE>
is true for the 
 <A HREF = "behavior.html">behavior</A> 
<PRE>
  s , s   , s   , ...
   N   N+1   N+2
</PRE> 
for all <CODE>N &gt; 0</CODE>.

<P><BR><BR>
The symbol <CODE>[]</CODE> also appears as an indivisible part of
the operator 
<PRE>
  <A HREF = "box-sqact.html">[][A]</A>
       <A HREF = "box-sqact.html">v</A>
</PRE>
where <CODE>A</CODE> is an
 <A HREF = "action.html">action</A>
and  <CODE>v</CODE> is a
 <A HREF = "state-function.html">state function</A>.