A <EM>behavior</EM> is an infinite sequence of 
 <A HREF = "states.html">states</A>.
It represents a possible history of the observable universe.
Terminating executions of a system are represented by behaviors ending
in an infinite sequence of
  <A HREF = "stuttering-step.html">stuttering steps</A>.