Лекции В.А. Захарова (1157993), страница 34
Текст из файла (страница 34)
Если ϕ = p, p ∈ AP (т. е. ϕ — атомарное высказывание), тоI , n |= ϕ ⇐⇒ ξ(p) = true.rrrξ(p) = true- yn- yn+1- yn+2- y- y-r r rЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLСемантика PLTL2. Если ϕ = ϕ1 &ϕ2 , тоI , n |= ϕ ⇐⇒ I , n |= ϕ1 и I , n |= ϕ2 .rrrI , n |= ϕ1I , n |= ϕ2- yn- yn+1- y- y- y-r r rn+2Для формул вида ϕ1 ∨ ϕ2 , ϕ1 → ϕ2 , ¬ϕ1 отношениевыполнимости в темпоральной модели определяется точно также, как в классической логике предикатов.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLСемантика PLTL3.
Если ϕ = Xψ, тоI , n |= ϕ ⇐⇒ I , n + 1 |= ψ.rrr- ynI , n + 1 |= ψ- yn+1- y- y- y-r r rn+24. Если ϕ = Fψ, тоI , n |= ϕ ⇐⇒ существует такое k, k ≥ 0, что I , n + k |= ψ.rrr- yn- yn+1- yn+2- yI , n + k |= ψ- yn+k-r r rЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLСемантика PLTL5. Если ϕ = Gψ, тоI , n |= ϕ ⇐⇒ для любого k, k ≥ 0, верно I , n + k |= ψ.rrrI , n |= ψ- yI , n + 1 |= ψ- ynn+1- y- yn+2I , n + k |= ψ- y-r r rn+k6. Если ϕ = χUψ, тоI , n |= ϕrrr⇐⇒I , n |= χ- ynсуществует такое k, k ≥ 0, что I , n + k |= ψ,и для любого i, 0 ≤ i < k, верно I , n + i |= χ.I , n + 1 |= χ- yn+1I,n+k −1 |= χ I,n+k |= ψ- yn+2- y- yn+k-r r rЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLСемантика PLTL7.
Если ϕ = χ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 полагаются состояния вычисленияпрограммы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
