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

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

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

. . , xm ) — и записывать конфигурациюавтомата как состояние, после которого располагаются значениявсех таймеров: (`, k1 , . . . , km )Начальная конфигурация автомата имеет вид (`0 , 0, 0, . . . , 0)Семантика временных автоматовБолее строгое описаниеШаг вычисления временного автомата — это изменение конфигурации (`, d) на конфигурацию (`0 , d 0 ) одним из двух способов:I продвижение времени:(`, d)→(`0 , d 0 )II`0 = `существует константа k ∈ R>0 , такая что∀x(x ∈ C → d 0 (x) = d(x) + k)IIIинвариант I (`) выполнен для значений таймеров d 0IIболее короткая запись: d 0 = d + kR>0 — множество всех положительных действительныхчиселболее короткая запись: d 0 |= I (`)изменение состояния:IIIв автомате есть переход (`, σ, g , C, `0 )d |= gd 0 (x) = 0 для x ∈ C и d 0 (y ) = d(y ) для y ∈/CII(`, d)→(`0 , d 0 )более короткая запись: d 0 = reset(d, C)d 0 |= I (`0 )Семантика временных автоматовБолее строгое описаниеВычисление временного автомата — это бесконечная последовательность конфигураций, в которой следующая конфигурацияполучается из предыдущей продвижением времени или изменением состоянияНеправдоподобные вычисленияЕсли разрешить временному автомату продвигать время иизменять состояния произвольным образом, то немедленновозникают вычисления автомата, неадекватные по отношениюк поведению реальных СРВСтагнация системы(livelock)Возможна ситуация, в которой автомат всегда может изменитьсостояние, но вместо этого постоянно продвигает время:(`, 0)→(`, 1)→(`, 2)→(`, 3)→ .

. .В реальной системе действуют “законы справедливости”: ситуация, в которой состояние может быть изменено, но никогда неизменяется, считается неправдоподобнойНеправдоподобные вычисленияЕсли разрешить временному автомату продвигать время иизменять состояния произвольным образом, то немедленновозникают вычисления автомата, неадекватные по отношениюк поведению реальных СРВКонвергентные вычисленияДля временного автомата возможна следующая ситуация: онсможет изменить состояние, если пройдёт некоторое время (скажем, единица времени), однако в бесконечном вычислении единица времени никогда не проходит:(`, 0)→(`, 21 )→(`, 34 )→(`, 78 )→ . . .Для реальной системы такая ситуация невозможна: любой момент времени должен рано или поздно наступитьНеправдоподобные вычисленияЕсли разрешить временному автомату продвигать время иизменять состояния произвольным образом, то немедленновозникают вычисления автомата, неадекватные по отношениюк поведению реальных СРВВычисления ЗенонаВозможна и более “хитрая” вариация конвергентности вычисления: автомат бесконечное число раз как изменяет состояние,так и продвигает время, однако существует граница протёкшеговремени, которая никогда не достигается:(`, 0)→(`, 21 )→(`0 , 0)→(`0 , 14 )→(`, 0)→ .

. .Такие вычисления служат иллюстрацией апорий Зенона, сутькоторых сводится к выполнению бесконечного числа действий вконечное времяТакие вычисления также считаются неправдоподобными(как и апории Зенона)Неправдоподобные вычисленияИ как же исключить неправдоподобные вычисления изсемантики временного автомата?Почти все неправдоподобные вычисления исключаютсяследующим ограничением:Iавтомату запрещено два раза подряд продвигать времяСтагнация системы:(`, 0)→(`, 1)→(`, 2)→ . . . — невозможнаКонвергентное вычисление:(`, 0)→(`, 12 )→(`, 34 )→ . . . — невозможноВычисление Зенона:(`, 0)→(`, 12 )→(`0 , 0)→(`0 , 14 )→ .

. . — возможноМодель в формализме временных автоматов,содержащая вычисления Зенона, — это некорректнопостроенная модельСемантика временных автоматовРанее в лекциях семантика каждой системы в конечном итогеописывалась моделью КрипкеА можно ли сделать так и для временных автоматов?Модель Крипке M(A) для временного автомата A определяетсятак:Iсостояния модели Крипке — это всевозможныеконфигурации автоматаIпереходами связаны пары конфигураций, отличающихсяодним шагом вычисленияIначальное состояние модели Крипке — это начальнаяконфигурация автоматаСемантика временных автоматовА какими высказываниями размечены состояния этой моделиКрипке?Состояние модели Крипке помечается всевозможнымивыполнеными в этом состоянии элементарнымиограничениями, к которым при разметке добавляются атомывида A.`: “автомат A находится в состоянии `”(множество всех атомов вида A.` обозначим записью ALC (A))А будет ли отношение переходов модели Крипке тотальным?Не обязательно, но временной автомат, модель Крипкекоторого нетотальна, — это некорректно построенныйавтоматА как быть с чередованием типов шагов вычисления?Можно расценивать это как особый вид справедливости,специфичный для временных автоматовА действительно ли это модель Крипке?Не совсем: модель Крипке для временного автомата в общемслучае бесконечнаСемантика временных автоматовsingle, x = 1x ≤ 1click, xclick, x < 1, xdoublex ≤ 0Модель Крипке для этого автомата будет выглядеть так:`3 ,0∞`1 ,0∞`1 ,k∞`2 ,0∞∞∞`2 ,m∞Композиция временных автоматовСРВ, описанная в формализме временных автоматов, какправило состоит из нескольких временных автоматов,взаимодействующих между собой посредством событийНапример, параллельно автомату, распознающему щелчок идвойной щелчок мышки, в системе может присутствоватьавтомат, моделирующий поведение пользователя, щёлкающегомышкойАвтомат пользователя и автомат, распознающий щелчки,связываются между собой через событие щёлчка мышкойКомпозиция временных автоматовКак правило, при взаимодействии автоматов через событияодин автомат генерирует событие, тогда как другой автоматпринимает это событие и обрабатывает егоНапример, пользователь генерирует событие щелчка мышкой,тогда как компьютер принимает и обрабатывает это событиеТакое использование событий может быть переформулированоследующим образом:Iмежду автоматами существует канал взаимодействия chIгенерация — это событие посылки сигнала в канал ch: ch!Iприём и обработка — это событие приёма сигнала изканала ch: ch?Композиция временных автоматовСамый распространённый тип взаимодействия автоматов черезканалы, — это синхронное взаимодействие типа точка-точка(рандеву)Рандеву временных автоматов происходит следующим образом:Iвыбирается автомат, согласно предусловию переходаспособный послать сигнал в канал взаимодействияIвыбирается автомат, согласно предусловию переходаспособный принять сигнал из каналаIесли при сбросе всех таймеров, размечающих двавыбранных перехода, инварианты новых состоянийавтоматов выполнены, то выбранные переходыодновременно выполняютсяIв противном случае выбранная пара переходов не можетбыть выполненаСети временных автоматовСеть временных автоматов — это система(C , Chan, (A1 , .

. . , Ak )), гдеIC — конечное множество общих таймеровIChan — конечное множество общих каналоввзаимодействияIAi = (Li , `i0 , {ch!, ch? | ch ∈ Chan} , C , I i , T i ) — временнойавтомат над общими таймерами и общими каналамивзаимодействияАвтоматы сети работают асинхронно согласно семантикечередующихся вычисленийЕдинственная возможность синхронной работы автоматов —это рандевуСети временных автоматовКонфигурация сети (C , Chan, (A1 , .

. . , Am )),Ai = (Li , `i0 , Σ, C , I i , T i ), — это система (`1 , . . . , `m , d), где`i ∈ Li и d : C → R≥0Начальная конфигурация сети имеет вид (`10 , . . . , `m0 , 0, 0, . . . , 0)Шаг вычисления сети — это изменение конфигурации(`1 , . . . , `k , d) на конфигурацию (`01 , . . . , `0m , d 0 ) одним из трёхспособов:1. продвижение времени:III`01 = `1 , . .

. , `0k = `mсуществует константа k ∈ R>0 , такая что d 0 = d + kd 0 |= I 1 (l1 ) & . . . & I m (lm )Сети временных автоматовКонфигурация сети (C , Chan, (A1 , . . . , Am )),Ai = (Li , `i0 , Σ, C , I i , T i ), — это система (`1 , . . . , `m , d), где`i ∈ Li и d : C → R≥0Начальная конфигурация сети имеет вид (`10 , .

. . , `m0 , 0, 0, . . . , 0)Шаг вычисления сети — это изменение конфигурации(`1 , . . . , `k , d) на конфигурацию (`01 , . . . , `0m , d 0 ) одним из трёхспособов:2. асинхронное изменение состояния автомата Ai :IIIII`0p = `p для p 6= i(`i , λ, g , C, `0i ) ∈ T id |= gd 0 = reset(d, C)d 0 |= I i (`0i )Сети временных автоматовКонфигурация сети (C , Chan, (A1 , . . . , Am )),Ai = (Li , `i0 , Σ, C , I i , T i ), — это система (`1 , . . . , `m , d), где`i ∈ Li и d : C → R≥0Начальная конфигурация сети имеет вид (`10 , . . . , `m0 , 0, 0, . .

. , 0)Шаг вычисления сети — это изменение конфигурации(`1 , . . . , `k , d) на конфигурацию (`01 , . . . , `0m , d 0 ) одним из трёхспособов:3. синхронное изменение состояний автоматов Ai , Aj :IIIIII`0p = `p для p 6= i, p 6= j(`i , c!, g 0 , C 0 , `0i ) ∈ T i(`j , c?, g 00 , C 00 , `0j ) ∈ T jd |= g 0 & g 00d 0 = reset(d, C 0 ∪ C 00 )d 0 |= I i (`0i ) & I j (`0j )Сети временных автоматовОпределения вычисления сети и модели Крипке A(N) для сетиN дословно совпадают с теми же определениями для одногоавтоматаКак и для временного автомата, для сети остаётсянеустранимая проблема наличия вычислений Зенона и другихнеправдоподобных вычисленийПримерПопробуем добавить к автомату, распознающему одинарный идвойной щелчки мыши,Iавтомат, моделирующий поведение пользователя:произвольным образом генерирующий события щелчкамышиIавтомат, обрабатывающий одинарный и двойной щелчки:на обработку каждого щелчка тратится от 2 до 3 единицвремениСети временных автоматовs!, x == 1x ≤ 1cl?, x < 1, xcl?, xd!x ≤ 0cl!y ≤3d?, ys?, yy ≥2y ≥2Корректно ли работает эта система?Нет, а почему?y ≤3Сети временных автоматовs!, x = 20x ≤ 20s`0cl?, x < 20, xcl?, xdd!x ≤ 0z ≤ 20 `2cl!z ≤ 0 `1z ≥ 10, cl!, zz ≥ 20, zy ≤ 3 dd?, yy ≥ 2`0`0z ≥ 20, zrz ≤ 0cl!, zs?, ys y ≤ 3y ≥ 2А если сделать пользователя более “разумным” и медленным,то система будет работать корректноTimed CTLФормальная семантика автоматов и сетей — это модельКрипке, а значит, можно попытаться сформулироватьтребования к этим системам в виде CTL-формулПри попытке это сделать “в лоб” возникает проблеманесоответствия формального смысла формул тому, чтосодержательно вкладывается в эти формулыЭту проблему можно проиллюстрировать таким примером:`Предъявим к этой системе такое требование: AFx = 1Timed CTL`ϕ : AFx = 1Тот, кто формулировал это требование, скорее всего вкладывалв него такой содержательный смысл:как бы ни работала система,рано или поздно наступит момент времени 1Значит, это требование должно быть вернымПри этом существует, например, такое вычисление автомата:(`, 0) → (`, 2) → .

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

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