我正在学习计算机辅助验证课程，在介绍线性时间逻辑之后，我们才刚刚开始介绍计算树逻辑。我的演讲说 ◇Φ ≡ "true U Φ" 是有效的 CTL，而 □Φ 不是有效的 CTL。我同意第二部分，因为 CTL 公式是 Φ 并且 Φ 的规则不包括 □Φ。但它们也不包括 ◇Φ 或“真 U Φ”——只有 Ψ 的规则包括那些，而 Φ 的规则规定任何 Ψ 必须以 ∃ 或 ∀ 开头，而 ◇Φ 或“真 U Φ”都不是“ 是。维基百科似乎同意我的观点。
他只是犯了一个错误，还是我在这里遗漏了什么？我们已经给出的 CTL 规则的图像
