Используя индукцию по n, можно доказать, что модель M и модель M
n
невозможно различить никакой CTL-формулой темпоральной
глубины не больше n. Это означает, что φ CTL, ||φ|| ≤ n: M
n
, s
0
╞═ φ
если и только если M, s
0
╞═ φ (и аналогичное утверждение для s
1
вместо s
0
). Это утверждение следует из трех фактов, проверяемых
непосредственно:
1. Для любого n ≥ 0 любая формула φ темпоральной глубины 0 не
различает модели M и M
n
.
2. Если ни формула φ, ни формула ψ не различают модели M и M
n
, то
такие формулы, как φ и φ ψ, тоже не различают эти модели.
3. Если ни формула φ, ни формула ψ не различают модели M, M
n
и
M
n+1
, то такие формулы, как EX φ, AX φ, E[φ U ψ] и A[φ U ψ], не
различают модели M и M
n+1
.
Последний шаг доказательства состоит в следующем. Пусть
существует CTL-формула φ, эквивалентная формуле A[FG a] (или,
соответственно, A[F(a X a)]). С одной стороны, из того, что
M, s
0
A[FG a] и M
n
, s
0
╞═ A[FG a] (для всех n), следует, что M, s
0
φ
и M
||φ||
, s
0
╞═ φ. С другой стороны, из того, что модели M и M
||φ||
невозможно различить CTL-формулой темпоральной глубины не
более ||φ||, следует, что φ имеет одно и то же истинностное значение на
моделях M и M
||φ||
. Это приводит к противоречию.
Существует формула в CTL, но формула в LTL отсутствует.
Формула AG EF p – это CTL-формула, для которой нет эквивалентной
формулы в LTL. Это свойство используется на практике, так как оно
выражает тот факт, что можно добраться до состояния, в котором
верно p, независимо от текущего состояния. Если p характеризует
состояние, в котором исправляется определенная ошибка, то формула
выражает, что всегда можно восстановиться после определенной
ошибки. Доказательство того, что для AG EF p нет эквивалентной
формулы в LTL, состоит в следующем.
Пусть φ – это LTL-формула, для которой A φ эквивалентно AG EF p.
Рассмотрим модель M на рис. 2.23 (а). Так как M, s╞═ AG EF p,
отсюда следует, что M, s╞═ A φ. Пусть M' – подмодель M, показанная
на рис. 2.23 (б). Пути, стартующие из s в M', входят в множество
путей, начинающихся из s в M. Следовательно, M', s╞═ A φ. Однако
при этом свойство M', s╞═ AG EF p не выполняется, так как p
никогда не становится верным вдоль единственного пути s
ω
.
Аналогичный факт можно доказать для случая, когда LTL-формулы
квантифицируются не по всем путям, а по некоторому пути. Пусть φ –
это LTL-формула, для которой E φ эквивалентно AG EF p.