Reading Temporal Logic Aloud: an informal guide to CTL*
Robert Seater 3/28/05

given a state...
      A...	"all"		along all paths beginning here...
      E...	"exists"	along some path beginning here...
(by default use the initial state of the system)
(if given a path, just consider the first state of that path)

given a path...
      F...	"finally"	in at least one of its states...
      G...	"generally"	in all of its states...
      X...	"next"		   in the second state...
      fU...	"until"		      f holds until...
(cannot be given a state)

basic 4 combinations
      AG...	everywhere
      EF...	somewhere
      AF...	you can always get to a place where...
        EG...   it's possible to always satisfy...

another example
	EFAX...	somewhere out there is a state from which you can only go to a place where...