title: Linear Temporal Logic Questions (2)
body: <p>If you are not familiar with LTL (linear temporal logic), please skip this question! And yes, LTL is very significant to programming, as it is a core to the model checking system we use to verify programs.</p>
  
  <p>Given these proposition symbols and their meanings...<br>
  Gp - always P<br>
  Fp - sometimes P</p>
  
  <p>What do the following statements mean?</p>
  
  <pre><code>GFGp = ?  
  FGFp = ?
  </code></pre>
  
  <p>I'm having a hard time with the logic surrounding LTL, and can't wrap my head around the above statements, thanks for any help!</p>