title: Does a never claim prove a Linear Temporal Logic formula?
body: <p>I have an LTL formula, that was automatically generated from a program I used:</p>
  
  <pre><code>    (((a))&amp;&amp;F((((b))&amp;&amp;F((c)))))
  </code></pre>
  
  <p>which reads as </p>
  
  <pre><code>    a &amp;&amp; F(b &amp;&amp; Fc)
  </code></pre>
  
  <p>I then used the ltl2BA-win.exe program downloaded from here:
  <a href="http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php" rel="nofollow">LTL 2 BA</a> and got a never claim as output. The website can also generate a Büchi Automaton for an LTL formula (I left the "Use Spin Syntax" and "Use Spin 4.3.0" options unchecked when using this site).</p>
  
  <p>My questions are: 
  1. Is it the never claim that proves the LTL formula or the fact that a Büchi Automaton was produced? 
  2. Is a never claim on its own enough to prove an LTL formula or does the never claim need feeding into a model checker, such as Spin, for extra processing to provide the proof?</p>