Соответствует ли следующая формула в CTL?

Question

Формула следующая:

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

Ответ - нет, но почему?

Сказано, что недопустимая формула. Подформула, начинающаяся с самого внутреннего А, не соответствует типу А (x U y).

Не является ли квантификатор пути 'A' для всего парантеза (обе формулы)?

Answer 1

Оператор CTL

A [ P U Q ]

Синтаксический анализатор не может определить, что такое P и что такое Q в вашей формуле, потому что единственные возможные варианты:

• P: = "(p" и Q: = "q) -> (r U q)" или
• P: = "(p U q) -> (r" и Q: = "q)"

и в любом случае P и Q являются неправильными формулами.