logic - 线性时序逻辑等价

Question

对于 LTL 公式FG p & FG q，我想嘲笑或拒绝它等同于 F (G p & Gq). 我认为根据分布规律，我们可以F(Gp&Gq)写成FG(p&q). 我们也可以说FG p & FG q = FG(p&q)吗？

Answer 1

这仅适用于您的特定情况，因为p和q是原子命题。通常，很难确定哪些公式允许分配运算符，哪些不允许分配（参见 Samer 和 Veith：关于 LTL 规范的分布，2010 年）。您可以证明您的特定声明的另一种方法是通过 Buechi 自动机，在所有三种情况下都如下所示（参见http://www.lsv.fr/~gastin/ltl2ba/index.php）。通常，LTL 公式的等价性是 PSpace 完全的，因此如果没有 Buechi 自动机，通常不会那么容易回答。