是否從未聲明證明線性時間邏輯公式？

Question

我有一個LTL式，這是自動地從節目我用生成：

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

其內容

a && F(b && Fc) 

我然後用於從這裏下載的ltl2BA-win.exe後程序： LTL 2 BA並得到了一個從未聲稱作爲輸出。該網站還可以爲LTL公式生成一個Büchi自動機（在使用本網站時，我沒有選中「使用自旋語法」和「使用自旋4.3.0」選項）。

我的問題是： 1.是從未聲稱證明LTL公式或Büchi自動機生產的事實嗎？ 2.是否從未聲稱自己足以證明LTL公式或從未聲稱需要投入模型檢查器（如Spin）以進行額外處理以提供證明？

Answer 1

經過進一步閱讀，我找到了答案，讓我更清晰地瞭解從未聲明和Büchi自動機在這裏的目的：The Model Checker Spin和Temporal Claims。

根據這些文獻，只要確定存在或不存在從未索賠就足以證明或反駁LTL公式。