Лекции 12-23. Математическая логика (после колка) (1161871), страница 18
Текст из файла (страница 18)
Если ϕ = χRψ, тоI , n |= ϕ⇐⇒либо для любого k, k ≥ 0, верно I , n + k |= ψ,,rrrI , n |= ψ- ynI , n + 1 |= ψ- yn+1- yn+2- yI , n + k |= ψ- yn+k-r r rЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLСемантика PLTL7. Если ϕ = χRψ, тоI , n |= ϕ⇐⇒либо для любого k, k ≥ 0, верно I , n + k |= ψ,либо существует такое k, k ≥ 0, что I , n + k |= χ,и для любого i, 0 ≤ i ≤ k, верно I , n + i |= ψ.rrrI , n |= ψ- ynrrrI , n |= ψ- ynI , n + 1 |= ψ- yn+1I , n + 1 |= ψ- yn+1- y- yn+2I , n + k |= ψ- y-r r r-r r rn+kI,n+k |= χI,n+k −1 |= ψ I,n+k |= ψ- yn+2- y- yn+kЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLБудем называть формулу PLTL ϕI выполнимой в интерпретации I , если верно I , 0 |= ϕ(обозначается I |= ϕ);I PLTL-общезначимой , если для любой интерпретации Iверно I |= ϕ (обозначается |= ϕ).Чтобы облегчить запись формул и избавиться от лишнихскобок, условимся, чтоодноместные темпоральные операторы X, F, G обладают такимже приоритетом, как отрицание ¬,а двухместные темпоральные операторы U, R имеютнаивысший приоритет среди двухместных связок.Таким образом, записьXp1 Up2 &Fp3 → ¬p1 Rp2обозначает формулу((Xp1 )Up2 )&(Fp3 ) → (¬p1 )Rp2 .ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLРавносильные формулыТемпоральные операторы PLTL связаны друг с другомопределенными соотношениями (равносильностями).Вот наиболее важные из соотношений равносильности.Законы двойственности.1.
|= ¬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 6|= ϕUψ. Тогда согласноопределению отношения выполнимости для оператора U вернохотя бы одно из двух:1. либо для любого k, k ≥ 0, верно I , k 6|= ψI , 0 6|= ψ- y0I , 1 6|= ψ- y- y12- yI , k 6|= ψ- y-r r rk2. либо существует такое k, k ≥ 0, что I , k 6|= ψ, I , k 6|= ϕи при этом для любого i если 0 ≤ i < k, то I , k 6|= ψ, I , k |= ϕr r rI , 0 6|= ψI , 0 |= ϕ- y0I , 1 6|= ψI , 1 |= ϕ- y1I,k −1 6|= ψI,k −1 |= ϕ- y2- yI,k 6|= ψI,k 6|= ϕ- 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 |= ¬ψr r r- 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 ) ;или может быть это лучше выразить так:ϕ05 = G(busy R (¬(pr1 ∨ pr2 ))) ?или может быть так:ϕ005 = G((pr1 ∨ pr2 ) → busy ) ?РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВТеперь мы можем использовать PLTL в качестве формальногоязыка спецификации программ.Чтобы иметь возможность проверить, удовлетворяют ли всевычисления распределенной системы программ заданнымспецификациям, которые представлены формулами PLTL,нужно определить математическую модель программ.При разработке математической модели программ нужностремиться к тому, чтобыIкаждое вычисление распределенной системы программпредставляло собой темпоральную интерпретацию;Iвычисления программ в предложенной математическоймодели соответствовали реальному поведениювычислительных устройств, выполняющих эти программы;Iмодель программ имела простое устройство.В качестве такой модели программ мы будем использоватьразмеченные системы переходов .РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВОпределение LTSРазмеченная система переходов (LTS, Labelled TransitionSystem) — это пятерка hAP, S, S0 , −→, ρi, в которой1.
AP — множество атомарных высказываний;2. S — непустое множество состояний вычислений;3. S0 , S0 ⊆ S, — непустое подмножество начальныхсостояний;4. −→⊆ S × S, — тотальное отношение переходов,тотальность отношения −→ означает, что для любогосостояния s, s ∈ S, существует такое состояние s 0 , чтоs −→ s 0 (т. е. из любого состояния можно сделать хотя быодин переход);5. ρ : S → 2AP — функция разметки, приписывающаякаждому состоянию вычислений s, s ∈ S, множествоρ(s), ρ(s) ⊆ AP, всех тех атомарных высказываний,которые являются истинными в состоянии s.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSM = hAP, S, S0 , T , ρiAP = {p, q},S = {s1 , s2 , s3 , s4 , s5 , s6 , s7 },'s1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- yS0 = {s1 , s2 }@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и PLTL-интерпретацииТрассой в LTS M = hAP, S, S0 , −→, ρi называется всякаябесконечная последовательность состояний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 ) = hN, ≤, ξi, в которой для любогоn, n ≥ 0, и p, p ∈ AP, верно соотношениеξ(n, p) = true ⇐⇒ p ∈ ρ(sin ) .РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falsey0s2's1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- y@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = true- y0s21s4's1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- y@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = false- y- y1s42s30s2's1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- y@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = falsep = falseq = true- y- y- y1s42s33s50s2's1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- y@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = falsep = falseq = true- y- y- y1s42s33s50s2-'s1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- yr r r@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS, соответствующую программе π, можно построить так:IСостояниями LTS полагаются состояния вычисленияпрограммы.
Состояние вычисления программы π — этопара (состояние управления, состояние данных). Состояниеуправления — это значение счетчика команд программы.Состояние данных — это подстановка, указывающеясоответствие между переменными и их значениями.IЕсли в точке count1 программы π выполняется операторop, преобразующий данные из состояния ξ1 в состояние ξ2и передающий управление в точку count2 , то в LTSимеется переход (count1 , ξ1 ) −→ (count2 , ξ2 ).IАтомарным высказыванием p может быть любая формулалогики предикатов, зависящая от переменных программыи счетчика команд.
Разметка ρ определяется так:p ∈ ρ((count, ξ)) ⇐⇒ Iπ |= p[(count, ξ)].РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПрограмма драйвера π1while true doL1 : while R 6= 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, ξ 0 )во всевозможные состояния (l, ξ 0 ), в которых подстановки ξ 0 ,отличающиеся от ξ только значениями переменных, доступныхдля окружающей среды.Например, полагая, что регистр принтера R — это тумблер,который может переключаться сколь угодно часто в разныемоменты времени, получим следующую LTS, описывающуювзаимодействие драйвера принтера с окружающей средой(пользователем принтера).РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для системыπ1 k environment(L1 , {R/free})''-itI?iI'- ?i(L3 , {R/busy })I(L2 , {R/free})(L4 , {R/busy })&&?iI Rti (L1 , {R/busy })Ri(L2 , {R/busy })% R i (L , {R/free})3R?i%(L3 , {R/free})РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.Состояниями LTS для системы π1 k π2 объявляются наборы(count1 , count2 , ξ1 , ξ2 , χ), гдеIcount1 , count2 — значения счетчиков команд процессов π1и π2 ,Iξ1 , ξ2 — подстановки, определяющие значения локальныхпеременных процессов π1 и π2 ,Iχ — подстановка, определяющая значения разделяемыхпеременных.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.Переход (count1 , count2 , ξ1 , ξ2 , χ) −→ (count10 , count20 , ξ10 , ξ20 , χ0 )возможен в том и только том случае, когда выполнено одно издвух условий:Iв LTS M(π1 ) есть переход (count1 , ξ1 , χ) −→ (count10 , ξ10 , χ0 )и при этом count20 = count2 , ξ20 = ξ2 ;Iв LTS M(π2 ) есть переход (count2 , ξ2 , χ) −→ (count20 , ξ20 , χ0 )и при этом count10 = count1 , ξ10 = ξ1 .Таким образом, в семантике чередующихся вычисленийпараллельное выполнение процессов распределенной системымоделируется недетерминированным выбором того или иногопорядка, в котором выполняются действия разных процессов.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для программы π 0- it (L01 , free)'и программы π 00 t (L001 , free)i 't- i(L01 , busy )(L001 , busy )?i(L02 , free)?i(L002 , free) ?i ?i (L03 , busy )? 0i(L4 , busy )& ti (L003 , busy )? 00i(L4 , busy )&РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для системыπ10 k π100000- t(L1 , L1 , free)$'- i$@ (L01 , L002 , free)(L02 , L001 , free) tRt@ '$@66000R t@ (L2 , L2 , free) @ (L0 , L00 , busy )(L03 , L00, busy ) ? (L02 , L00(L01 , L00, busy ) ?13 , busy )332?R@-t ttt'$?@ R t(L03 , L003 , busy )@ I(L04 , L00(L01 , L001 , busy ) ?4 , busy )? t?t t?(L02 , L004 , busy )(L04 , L00, busy ) t&%2'000(L1 , L1 , busy )ti (L03 , L004 , busy ) ?(L04 , L00?3 , busy )t& - tH%YH*000L4 , busy ) H (L4 ,t H000000000, free) (L1 ,L4 , free)(L3 , L1 , free) ? (L4 , L1 H(L01 , L003 , free)H - t ?t - t- tHHHH,H(L02 , L00(L03 , L00, free) ? ?(L04, L00(L02 , L002 , free)4 free)23 , free)H?t ?- t- tt ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММИтак, для верификации распределенных программ нужныIтребования правильности (спецификации) вычисленийпрограммы, представленные формулой PLTL ϕ,Iматематическая модель распределенной программы π,представленная конечной LTS M(π).Тогда для проверки правильности программы π достаточнопроверить, что для любой трассы tr , tr ∈ Tr0 (M(π)), формулаϕ выполняется в темпоральной интерпретации I (tr ), т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
