【发布时间】：2018-06-05 05:05:05
【问题描述】：
对于一个 LTL 公式FG p & FG q，我想嘲笑或拒绝它等同于F (G p & Gq)。我认为根据分配规律，我们可以将F(Gp&Gq) 写成FG(p&q)。我们也可以说FG p & FG q = FG(p&q) 吗？
【问题讨论】：
标签： logic temporal automata-theory
【发布时间】：2018-06-05 05:05:05
【问题描述】：
这仅适用于您的特定情况，因为 p 和 q 是原子命题。通常，很难确定哪些公式允许分配运算符，哪些不允许分配（参见 Samer 和 Veith：关于 LTL 规范的分布，2010）。您可以证明您的特定主张的另一种方法是通过 Buechi 自动机，在所有三种情况下都如下所示（参见http://www.lsv.fr/~gastin/ltl2ba/index.php）。通常，LTL 公式的等价性是 PSpace-complete 的，因此在没有 Buechi 自动机的情况下通常不太容易回答。
【讨论】：