Пусть заданы модель Крипке M и CTL
*
-формула φ. Требуется
определить множество состояний модели, для которых формула
выполняется. Рассмотрим все подформулы формулы φ, имеющие вид
A β или E β, где β – LTL-формула, которая не содержит
квантификаторов пути. Запустим алгоритм проверки LTL-формул для
формул β или β, соответственно, и получим в результате множество
состояний модели, на которых выполняются рассматриваемые
формула A β или E β. Пометим все эти состояния в модели M
данными подформулами. После этого будем интерпретировать эти
подформулы как пропозициональные переменные. Можно даже
заменить их новыми атомарными предложениями, поскольку теперь
для каждого состояния модели известно, какие из новых атомарных
предложений в нем соблюдаются. При этом в исходной формуле
число квантификаторов пути уменьшается как минимум на единицу.
Дальше этот процесс следует повторить с другими подформулами
формулы φ, внешними по отношению к уже обработанным, и
обработать их аналогичным образом до тех пор, пока, в конечном
счете, не будет обработана исходная формула φ.
При этом для модели M будет получено множество состояний, в
которых соблюдается формула φ.
Замечания о длине формулы
Вспомним, что проверка моделей для LTL выполняется за
экспоненциальное время относительно размера формулы. Несмотря на
то, что разница во временной сложности по отношению к длине
формулы выглядит серьезной, здесь следует сделать несколько
замечаний. Формулы в LTL никогда не бывают длиннее, и, как
правило, бывают короче, чем эквивалентные формулы в CTL. Это
следует из того факта, что для формул, которые могут быть
переведены из CTL в LTL, эквивалентная LTL-формула получается
путем удаления всех квантификаторов пути, и поэтому она обычно
получается короче. Более того, для каждой модели M существует
LTL-формула φ такая, что любая CTL-формула, эквивалентная E φ
(или A φ) – если такая формула существует в CTL – имеет более чем
полиномиальную длину по отношению к длине LTL-формулы (либо
ее нельзя построить за полиномиальное время при условии, что
P ≠ NP). Это наглядно иллюстрируется адаптированным примером
[36], приводимым ниже.
Для требования, которое может быть специфицировано и в CTL, и в
LTL, кратчайшая возможная формулировка в LTL никогда не бывает
длиннее CTL-формулы, и, более того, может быть экспоненциально