Лекция 9. Временные автоматы. Timed CTL (1185509), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

. .В этом вычислении момент времени 1 никогда не наступаетявно, а значит, требование ϕ не выполнено для автоматаЧтобы устранить такое несоответствие содержательного иформального смыслов формул, следует адаптироватьсемантику CTL к работе в реальном времениTimed CTLСинтаксис формул логики TCTL (Timed CTL) для автоматаA = (L, `0 , Σ, C , I , T ) [сети N = (C , Chan, (A1 , . . . , Am ))]совпадает с синтаксисом формул логики CTL без оператора Xнад множеством атомарных высказываний ATC (C ) ∪ ALC (A)[ATC (C ) ∪ ALC (A1 ) ∪ · · · ∪ ALC (Am )]При этом семантики TCTL- и CTL-формул различаютсяПеред тем как описать различия этих семантик, введем однотехническое понятиеДля шага вычисления (`, d) → (`0 , d 0 ) допустимымпродвижением времени назовём константу k ∈ R≥0 , такую что:Iесли d 0 = d + p, то 0 ≤ k ≤ pIесли d 0 получается из d сбросом некоторых таймеров, тоk=0Timed CTLРассмотрим вычисление временного автомата:tr = (`0 , d0 ) → · · · → (`i , di ) → .

. .Тогда tr |= ϕUψ (в семантике TCTL) в том и только томслучае, если существуют конфигурация (`i , di ) и допустимоепродвижение k для этой конфигурации и следующей, такие чтоI(`i , di + k) |= ψIдля любой конфигурации (`j , dj ), j < i, и для любогодопустимого продвижения времени k 0 для j-й и (j + 1)-йконфигураций верно (`j , dj + k 0 ) |= ϕIдля любого k 0 , 0 ≤ k 0 < k, верно (`i , di + k 0 ) |= ϕСемантика остальных темпоральных операторов задаётсяестественным образом: Fϕ = trueUϕ, Gϕ = ¬F¬ϕВыполнимость формулы ϕ в модели M в изменённой такимобразом семантике будем обозначать так: M |=TCTL ϕTimed CTLПримеры требований, предъявляемых к сети, состоящей израспознавателя щелчков мыши R, пользователя U иобработчика щелчков H:IAG(!H.`0 → AFH.`0 ): обработчик щелчков обязательнозавершает обработку каждого набора щелчковIAG(!R.`0 → x ≤ 20): таймер распознавателя щелчков неподнимается выше 20 единиц времени при обработкещелчкаIEFH.d: пользователь может добиться того, чтобы системараспознала его работу с мышью как двойной щелчокIAG(z − x ≥ 0): таймер z не может обнулиться, если x 6= 0Конец лекции 9.

Характеристики

Список файлов лекций