Search code examples
logicformulaproof

Does a never claim prove a Linear Temporal Logic formula?

I have an LTL formula, that was automatically generated from a program I used:

    (((a))&&F((((b))&&F((c)))))

which reads as 

    a && F(b && Fc)

I then used the ltl2BA-win.exe program downloaded from here: LTL 2 BA 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).

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?

Solution

  • After further reading I found answers that give me a clearer picture regarding the purpose of never claims and Büchi automata here: The Model Checker Spin and Temporal Claims.

    According to this literature, just by establishing the presence or absence of a never claim is enough to prove or disprove the LTL formula.