从不声明是否证明了线性时间逻辑公式？答案

【问题标题】：Does a never claim prove a Linear Temporal Logic formula?从不声明是否证明了线性时间逻辑公式？
【发布时间】：2015-09-03 20:00:00
【问题描述】：

我有一个 LTL 公式，它是从我使用的程序自动生成的：

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

读作

    a && F(b && Fc)

然后我使用了从这里下载的 ltl2BA-win.exe 程序： LTL 2 BA 并得到了从未声明为输出。该网站还可以为 LTL 公式生成 Büchi Automaton（我在使用此网站时未选中“使用 Spin 语法”和“使用 Spin 4.3.0”选项）。

我的问题是： 1. 是从不证明 LTL 公式还是制造了 Büchi Automaton 的事实？ 2. 从不声明本身是否足以证明 LTL 公式，或者从不声明是否需要输入到模型检查器（例如 Spin）中以进行额外处理以提供证明？

【问题讨论】：

【解决方案1】：

进一步阅读后，我找到了答案，让我更清楚地了解永不索赔和 Büchi 自动机的目的：The Model Checker Spin 和 Temporal Claims。

根据该文献，仅通过确定存在或不存在从未声明就足以证明或反驳 LTL 公式。

【讨论】：