logic - CTL中的以下公式是否有效？

Question

公式如下：

AF A[(p U q) --> (r U q)]

答案是否定的，但为什么呢？

说，不是一个有效的公式。从最里面的 A 开始的子公式不符合类型 A (x U y)。

不是整个括号（两个公式）的路径量词“A”吗？

Answer 1

CTL 运算符是

一个[ P U Q ]

解析器无法找出公式中的P和Q是什么，因为唯一可能的选择是

• P := "(p "和Q := " q) --> (r U q)"，或者
• P := "(p U q) --> (r "和Q := " q)"

在任何一种情况下，P和Q都是格式错误的公式。