Является ли "истинная U Φ" действительной формулой дерева вычислений Logi c?

Question

Я прохожу курс по проверке с помощью компьютера, и мы только начинаем охватывать логики вычислительного дерева c после охвата линейных временных логик c. В моей лекции говорилось, что true Φ ≡ «истинный U Φ» является действительным CTL, тогда как □ Φ не является действительным CTL. Я согласен со второй частью, потому что формула CTL - это Φ и правила для Φ не включают □ Φ. Но они также не включают ◇ Φ или «истинный U Φ» - только правила для Ψ включают их, и правила для Φ гласят, что любому Ψ должен предшествовать ∃ или ∀, и ни ◇ Φ, ни «истинный U Φ» " находятся. Википедия, похоже, согласна со мной в этом.

Он только что допустил ошибку или я что-то здесь упустил? Изображение правил для CTL нам дали

Answer 1

Я бы осмелился сказать, что ни одна из этих формул не принадлежит CTL. Возможно, возможно, возникло недоразумение, поэтому стоило бы связаться с вашим лектором в частном порядке и спросить об этой проблеме (вежливо).

---

Позвольте мне определить соответствие между вашей записью и той, Меня учили.

◇ := F ~ eventually
□ := G ~ globally
◯ := X ~ next
∀ := A ~ necessarily
∃ := E ~ possibly

Формула LTL ◇ϕ (Fϕ) гласит, что ϕ обязательно будет сохраняться в будущем . Соответствующая формулировка CTL будет ∀◇ϕ (AFϕ).

Формула LTL □ϕ (Gϕ) гласит, что ϕ означает , глобально удерживающий навсегда . Соответствующая формулировка CTL будет ∀□ϕ (AGϕ).

CTL, пока оператор не может появиться в одной из двух форм:

• ∀(ϕ1 U ϕ2): во всех возможных путях выполнения ϕ1 удерживается до ϕ2 удерживания (хотя бы один раз) .

• ∃(ϕ1 U ϕ2): хотя бы в одном пути выполнения, ϕ1 удерживается до тех пор, пока ϕ2 не удержит (хотя бы один раз) .

См. Также: Операторы CTL .