Лекция 10. Временные автоматы. Регионная модель Крипке. Сведение МС к TCTL и CTL, страница 2

. . , 0)]модель содержит следующие переходы:IIIIесли автомат содержит переход (`, λ, g , C, `0 ), r |= g иreset(r , C) |= I (`0 ), то модель содержит переход(`, r ) → (`0 , reset(r , C))если r |= I (`) и succ(r ) |= I (`), то модель содержит переход(`, r ) → (`, succ(r ))состояние модели (`, r ) помечено всеми высказываниямииз ALC (A) ∪ ATC (ϕ), верными в регионе rРегионная модель Крипке — это и есть то, что ранее условноназывалось сжатиемРегионная модель КрипкеПримерx ≤ 1x = 1`2x`1x < 1, x`3x ≤ 0ϕ: AG(A.`2 & x = 1 → A(x ≥ 1UA.`2 ))Достижимый фрагмент регионной модели Крипке для этихавтомата и формулы выглядит так:`3 ,0`1 ,0`1 ,(0, 1)`1 ,1`1 ,(1, ∞)`2 ,0`2 ,(0, 1)`2 ,1Сведение MCTAк MC моделей Крипке относительно CTLТеоремаДля любых временного автомата A и TCTL-формулы ϕ,если из модели M(A) “справедливостью” исключеныконвергентные вычисления, тоM(A) |=TCTL ϕ ⇔ Mr (A, ϕ) |= ϕДоказательство (идея).Попробуем построить отношение состояний M(A) и Mr (A), какможно более похожее на бисимуляциюНастолько похожее, чтобы идеи равновыполнимости формул вбисимуляционно эквивалентных моделях были применимы и кэтому отношениюСостоянию (`, d) модели M(A) поставим в соответствие регион[(`, d)] = (`, [d])Сведение MCTAк MC моделей Крипке относительно CTLТеоремаДля любых временного автомата A и TCTL-формулы ϕ,если из модели M(A) “справедливостью” исключеныконвергентные вычисления, тоM(A) |=TCTL ϕ ⇔ Mr (A, ϕ) |= ϕДоказательство (идея).Какие свойства делают отношение [] похожим на бисимуляцию?Какими бы ни были переход (`, r ) → (`0 , r 0 ) в модели Mr (A) и []прообраз (`, d) состояния (`, r ), модель M(A) содержит переход(`, d) → (`0 , d 0 ), где d 0 ∈ r 0Обратное почти верно: если переход (`, d) → (`0 , d 0 ) в M(A) —Iизменение состояния, то модель Mr (A) содержит переход(`, [d]) → (`0 , [d 0 ])Iпродвижение времени, то всё хуже: модель Mr (A) можетсодержать 0, 1 или несколько соответствующих переходовСведение MCTAк MC моделей Крипке относительно CTLТеоремаДля любых временного автомата A и TCTL-формулы ϕ,если из модели M(A) “справедливостью” исключеныконвергентные вычисления, тоM(A) |=TCTL ϕ ⇔ Mr (A, ϕ) |= ϕДоказательство (идея).I продвижение времени, то всё хуже: модель Mr (A) можетсодержать 0, 1 или несколько соответствующих переходовОдин переход — если [d 0 ] = succ([d])Ни одного перехода, если [d] = [d 0 ] и это не открытый регионНесколькопереходовчерезрегионы[d], succ([d]), succ(succ([d])), .

. . , [d 0 ] в остальных случаях“Несколько переходов” — это не страшно, а вот “ни одного перехода” — это плохое свойствоСведение MCTAк MC моделей Крипке относительно CTLТеоремаДля любых временного автомата A и TCTL-формулы ϕ,если из модели M(A) “справедливостью” исключеныконвергентные вычисления, тоM(A) |=TCTL ϕ ⇔ Mr (A, ϕ) |= ϕДоказательство (идея).I продвижение времени, то всё хуже: модель Mr (A) можетсодержать 0, 1 или несколько соответствующих переходовЕсли [d] = [d 0 ], можно “заглянуть вперёд” в вычисление после(`, d) → (`, d 0 ):Iесли с этого момента постоянно продвигается время, тотак как это вычисление дивергентно, в модели Mr (A) естьпуть, в котором аналогичным образом продвигается времяСведение MCTAк MC моделей Крипке относительно CTLТеоремаДля любых временного автомата A и TCTL-формулы ϕ,если из модели M(A) “справедливостью” исключеныконвергентные вычисления, тоM(A) |=TCTL ϕ ⇔ Mr (A, ϕ) |= ϕДоказательство (идея).I продвижение времени, то всё хуже: модель Mr (A) можетсодержать 0, 1 или несколько соответствующих переходовЕсли [d] = [d 0 ], можно “заглянуть вперёд” в вычисление после(`, d) → (`, d 0 ):Iесли дальше в вычислении несколько раз продвигаетсявремя и затем изменяется состояние, то в Mr (A) можнонекоторым числом переходов поднять время до того жеуровня и точно так же изменить состояниеСведение MCTAк MC моделей Крипке относительно CTLТеоремаДля любых временного автомата A и TCTL-формулы ϕ,если из модели M(A) “справедливостью” исключеныконвергентные вычисления, тоM(A) |=TCTL ϕ ⇔ Mr (A, ϕ) |= ϕДоказательство (идея).Описанное соответствие одного перехода M(A) произвольномучислу переходов в Mr (A) делает отношение [] достаточно похожим на бисимуляцию, чтобы утверждать справедливость теоремыHА где в доказательстве переход от семантики TCTL к семантикеCTL?Сведение MCTAк MC моделей Крипке относительно CTLИтог:Для любого временного автомата A и любой формулы ϕлогики TCTLM(A) |=TCTL ϕ⇔Mr (A) |= ϕКонец лекции 10.