Ещё одни лекции В.А. Захарова, страница 35

|= ¬Xϕ ≡ X¬ϕ;2. |= ¬Fϕ ≡ G¬ϕ;3. |= ¬Gϕ ≡ F¬ϕ;4. |= ¬(ϕUψ) ≡ ¬ϕR¬ψ;5. |= ¬(ϕRψ) ≡ ¬ϕU¬ψ.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLРавносильные формулыТемпоральные операторы PLTL связаны друг с другомопределенными соотношениями (равносильностями).Вот наиболее важные из соотношений равносильности.Законы двойственности.1. |= ¬Xϕ ≡ X¬ϕ;2. |= ¬Fϕ ≡ G¬ϕ;3. |= ¬Gϕ ≡ F¬ϕ;4. |= ¬(ϕUψ) ≡ ¬ϕR¬ψ;5. |= ¬(ϕRψ) ≡ ¬ϕU¬ψ.Доказательство.

Следует непосредственно из определенияотношения выполнимости.Покажем справедливость соотношения 4).ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLДоказательство.Пусть I , 0 |= ¬(ϕUψ), т. е. I , 0 |= ϕUψ. Тогда согласноопределению отношения выполнимости для оператора U вернохотя бы одно из двух:1. либо для любого k, k ≥ 0, верно I , k |= ψI , 0 |= ψ- y0I , 1 |= ψ- y- y12- yI , k |= ψ- y-r r rk2.

либо существует такое k, k ≥ 0, что I , k |= ψ, I , k |= ϕи при этом для любого i если 0 ≤ i < k, то I , k |= ψ, I , k |= ϕrrrI , 0 |= ψI , 0 |= ϕ- y0I , 1 |= ψI , 1 |= ϕ- y1I,k −1 |= ψI,k −1 |= ϕ- y2- yI,k |= ψI,k |= ϕ- yk-r r rЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLДоказательство.Но это означает, что верно хотя бы одно из двух:1. либо для любого k, k ≥ 0, верно I , k |= ¬ψI , 0 |= ¬ψ I , 1 |= ¬ψ- y- y- y012- yI , k |= ¬ψ- y-r r rk2. либо существует такое k, k ≥ 0, что I , k |= ¬ψ, I , k |= ¬ϕи при этом для любого i если 0 ≤ i < k, то I , k |= ¬ψI , 0 |= ¬ψ I , 1 |= ¬ψrrr- y0- y1I,k −1 |= ¬ψ- y2- yI,k |= ¬ψI,k |= ¬ϕ- y-n+kА это как раз и означает, что I , 0 |= (¬ϕ)R(¬ψ).Значит, I |= ¬(ϕUψ) → ¬ϕR¬ψ для любой интерпретации I .r r rЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLДоказательство.Проводя аналогичные рассуждения покажите самостоятельно ,что верно соотношениеI |= ¬ϕR¬ψ → ¬(ϕUψ),а также остальные законы двойственности темпоральныхоператоров.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLРавносильные формулыЗаконы взаимной зависимости.1.

|= Fϕ ≡ ¬G¬ϕ;2. |= Gϕ ≡ ¬F¬ϕ;3. |= ϕUψ ≡ ¬(¬ϕR¬ψ);4. |= ϕRψ ≡ ¬(¬ϕU¬ψ);5. |= Fϕ ≡ true Uϕ;6. |= Gϕ ≡ false Rϕ.Доказательство. Самостоятельно.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLРавносильные формулыЗаконы неподвижной точки.1. |= Fϕ ≡ ϕ ∨ XFϕ;2. |= Gϕ ≡ ϕ & XGϕ;3. |= ϕUψ ≡ ψ ∨ (ϕ & X(ϕUψ);4. |= ϕRψ ≡ ψ & (ϕ ∨ X(ϕRψ).Доказательство. Самостоятельно.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLРавносильные формулыА какие законы дистрибутивности верны?1.

|= F(ϕ ∨ ψ) ≡???;2. |= G(ϕ ∨ ψ) ≡???;3. |= F(ϕ&ψ) ≡???;4. |= G(ϕ&ψ) ≡???;5. |= ϕU(ψ ∨ χ) ≡???;6. |= ϕU(ψ&χ) ≡???7. |= (ϕ ∨ χ)Uχ ≡???;8. |= (ϕ&χ)Uχ ≡???.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTLА теперь посмотрим, насколько адекватно и просто можновыражать при помощи PLTL те требования, которыепредъявляются к поведению распределенных систем программ.1. Всякий раз, когда принтер свободен и хотя бы одинкомпьютер собирается отправить данные на печать,принтер будет рано или поздно занят;2. Всякий раз, после того как принтер оказался занят, ондолжен когда-нибудь приступить к печати;3.

Компьютер, завершивший печать, должен когда-нибудьосвободить принтер;4. Данные на печать всегда передает не более чем одинкомпьютер.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTLВведем следующие атомарные высказывания, соответствующиеосновным событиям вычислений программы:1. tryi — i-ый компьютер собирается отправить данные напечать;2. pri — i-ый компьютер передает данные на печать;3. free — принтер свободен;4. busy — принтер занят.Пусть имеется система, состоящая из 2 компьютеров.Тогда все перечисленные требования выражаются формуламиPLTL так.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTL1.

Всякий раз, когда принтер свободен и хотя бы одинкомпьютер собирается отправить данные на печать,принтер будет рано или поздно занят:ϕ1 = G((free & (try1 ∨ try2 )) → Fbusy ) ;2. Всякий раз, после того как принтер оказался занят, ондолжен когда-нибудь приступить к печати:ϕ2 = G(free & Xbusy → XF(pr1 ∨ pr2 )) ;ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTL3.

Компьютер, завершивший печать, должен когда-нибудьосвободить принтер:ϕ3i = G(pri & X¬pri → XFfree) ;4. Данные на печать всегда передает не более чем одинкомпьютер:ϕ4 = G(¬(pr1 & pr2 )) .ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTL5. До тех пор пока хотя бы один компьютер отправляетданные на печать, принтер остается занятым:ϕ5 = G((¬(pr1 ∨ pr2 ) R busy ) ;или может быть это лучше выразить так:ϕ5 = G(busy R (¬(pr1 ∨ pr2 ))) ?или может быть так:ϕ5 = G((pr1 ∨ pr2 ) → busy ) ?РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВТеперь мы можем использовать PLTL в качестве формальногоязыка спецификации программ.Чтобы иметь возможность проверить, удовлетворяют ли всевычисления распределенной системы программ заданнымспецификациям, которые представлены формулами PLTL,нужно определить математическую модель программ.При разработке математической модели программ нужностремиться к тому, чтобыкаждое вычисление распределенной системы программпредставляло собой темпоральную интерпретацию;вычисления программ в предложенной математическоймодели соответствовали реальному поведениювычислительных устройств, выполняющих эти программы;модель программ имела простое устройство.В качестве такой модели программ мы будем использоватьразмеченные системы переходов .РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВОпределение LTSРазмеченная система переходов (LTS, Labelled TransitionSystem) — это пятерка AP, S, S0 , −→, ρ, в которой1.

AP — множество атомарных высказываний;2. S — непустое множество состояний вычислений;3. S0 , S0 ⊆ S, — непустое подмножество начальныхсостояний;4. −→⊆ S × S, — тотальное отношение переходов,тотальность отношения −→ означает, что для любогосостояния s, s ∈ S, существует такое состояние s , чтоs −→ s (т. е. из любого состояния можно сделать хотя быодин переход);5. ρ : S → 2AP — функция разметки, приписывающаякаждому состоянию вычислений s, s ∈ S, множествоρ(s), ρ(s) ⊆ AP, всех тех атомарных высказываний,которые являются истинными в состоянии s.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSM = AP, S, S0 , T , ρAP = {p, q},S = {s1 , s2 , s3 , s4 , s5 , s6 , s7 },'s1 , {p, q}s3 , ∅yI@@@@ys2 , {p}- y6s5 , {q}- yS0 = {s1 , s2 }@@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и PLTL-интерпретацииТрассой в LTS M = AP, S, S0 , −→, ρ называется всякаябесконечная последовательность состоянийtr = si0 , si1 , .

. . , sin , sin+1 , . . . ,(∗)в которой для любого n, n > 0, верно (sin −→ sin+1 ).Если si0 — начальное состояние, si0 ∈ S0 , то трасса trназывается начальной трассой.Запись Tr (M) обозначает множество всех трасс LTS M, азапись Tr0 (M) — множество всех начальных трасс LTS M.Каждой трассе tr ∈ Tr (M) вида (∗) сопоставимPLTL-интерпретацию I (tr ) = N, ≤, ξ, в которой для любогоn, n ≥ 0, и p, p ∈ AP, верно соотношениеξ(n, p) = true ⇐⇒ p ∈ ρ(sin ) .РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falsey0s2's1 , {p, q}s3 , ∅yI@@@@ys2 , {p}- y6s5 , {q}- y@@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = true- y0s21s4's1 , {p, q}s3 , ∅yI@@@@ys2 , {p}- y6s5 , {q}- y@@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = false- y- y1s42s30s2's1 , {p, q}s3 , ∅yI@@@@ys2 , {p}- y6s5 , {q}- y@@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = falsep = falseq = true- y- y- y1s42s33s50s2's1 , {p, q}s3 , ∅yI@@@@ys2 , {p}- y6s5 , {q}- y@@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = falsep = falseq = true- y- y- y1s42s33s50s2-'s1 , {p, q}s3 , ∅yI@@@@ys2 , {p}- y6s5 , {q}- yr r r@@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS, соответствующую программе π, можно построить так:Состояниями LTS полагаются состояния вычисленияпрограммы.

Состояние вычисления программы π — этопара (состояние управления, состояние данных). Состояниеуправления — это значение счетчика команд программы.Состояние данных — это подстановка, указывающеясоответствие между переменными и их значениями.Если в точке count1 программы π выполняется операторop, преобразующий данные из состояния ξ1 в состояние ξ2и передающий управление в точку count2 , то в LTSимеется переход (count1 , ξ1 ) −→ (count2 , ξ2 ).Атомарным высказыванием p может быть любая формулалогики предикатов, зависящая от переменных программыи счетчика команд.

Разметка ρ определяется так:p ∈ ρ((count, ξ)) ⇐⇒ Iπ |= p[(count, ξ)].РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПрограмма драйвера π1while true doL1 : while R = free do wait od ;L2 : R = busy ;L3 : output(X,printer );L4 : R = free;odРАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для программы π1t (L1 , {R/free})'- i t i(L1 , {R/busy })?i(L2 , {R/free}) ? i(L3 , {R/busy })&?i(L4 , {R/busy })РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыНекоторые переменные программы могут быть доступны длядругих программ (т. н. разделяемые переменные ) или дляокружающей среды (датчики, сенсоры, средства управления).В том случае, когда программа π взаимодействует сокружающей средой, в LTS Mπ вносятся следующиеизменения:для каждого состояния (l, ξ) вводятся переходы (l, ξ) −→ (l, ξ )во всевозможные состояния (l, ξ ), в которых подстановки ξ ,отличающиеся от ξ только значениями переменных, доступныхдля окружающей среды.Например, полагая, что регистр принтера R — это тумблер,который может переключаться сколь угодно часто в разныемоменты времени, получим следующую LTS, описывающуювзаимодействие драйвера принтера с окружающей средой(пользователем принтера).РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для системыπ1  environment(L1 , {R/free})''- tiI Rti (L1 , {R/busy })?iI'- ?i(L3 , {R/busy }) IRi(L4 , {R/busy })R?i(L2 , {R/free})&&?iI(L2 , {R/busy })% R i (L , {R/free})3%(L3 , {R/free})РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.Состояниями LTS для системы π1  π2 объявляются наборы(count1 , count2 , ξ1 , ξ2 , χ), гдеcount1 , count2 — значения счетчиков команд процессов π1и π2 ,ξ1 , ξ2 — подстановки, определяющие значения локальныхпеременных процессов π1 и π2 ,χ — подстановка, определяющая значения разделяемыхпеременных.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.Переход (count1 , count2 , ξ1 , ξ2 , χ) −→ (count1 , count2 , ξ1 , ξ2 , χ )возможен в том и только том случае, когда выполнено одно издвух условий:в LTS M(π1 ) есть переход (count1 , ξ1 , χ) −→ (count1 , ξ1 , χ )и при этом count2 = count2 , ξ2 = ξ2 ;в LTS M(π2 ) есть переход (count2 , ξ2 , χ) −→ (count2 , ξ2 , χ )и при этом count1 = count1 , ξ1 = ξ1 .Таким образом, в семантике чередующихся вычисленийпараллельное выполнение процессов распределенной системымоделируется недетерминированным выбором того или иногопорядка, в котором выполняются действия разных процессов.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для программы π - it (L1 , free)'и программы π i 't- it (L1 , free)(L1 , busy )(L1 , busy )?i(L2 , free)?i(L2 , free) ?i ?i (L3 , busy )? i(L4 , busy )& ti (L3 , busy )? i(L4 , busy )&РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для системыπ1  π1- t(L1 , L1 , free)$'- i$@ (L1 , L2 , free)(L2 , L1 , free) tRt@ '$@66R t@ (L2 , L2 , free)@ (L , L , busy )(L3 , L, busy ) ? (L2 , L, busy ) ?(L1 , L13323 , busy )?R@t-t tt$'?@ R t(L3 , L3 , busy )@ I(L4 , L(L1 , L1 , busy ) ?4 , busy )? t?t t?(L2 , L4 , busy )(L4 , L, busy ) t&%2'(L1 , L1 , busy )ti (L3 , L4 , busy ) ?(L , L3 , busy )t4 -? - tH%&YH*L4 , busy ) H (L4 ,t H(L3 , L1 , free) ? (L4 , L1 H, free) (L1 ,L , free)(L1 , L3 , free)t- t ?HH 4 - t- tHHH , L , free)(L3 , L, free) ? ?(L2 , Lfree) ? ?(L2 , L224 ,H3 , free)- t- t(L4H t t ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММИтак, для верификации распределенных программ нужнытребования правильности (спецификации) вычисленийпрограммы, представленные формулой PLTL ϕ,математическая модель распределенной программы π,представленная конечной LTS M(π).Тогда для проверки правильности программы π достаточнопроверить, что для любой трассы tr , tr ∈ Tr0 (M(π)), формулаϕ выполняется в темпоральной интерпретации I (tr ), т.