Презентация 17 (Лекции), страница 4

Достаточно использовать определениеЛогика линейного времениЗаконы двойственности.I ¬Xϕ ≈ X¬ϕI ¬Fϕ ≈ G¬ϕI ¬Gϕ ≈ F¬ϕI ¬(ϕUψ) ≈ ¬ϕR¬ψI ¬(ψRϕ) ≈ ¬ϕU¬ψЗаконы исключения.I Fϕ ≈ ¬G¬ϕI Gϕ ≈ ¬F¬ϕI ϕUψ ≈ ¬(¬ϕR¬ψ)I ϕRψ ≈ ¬(¬ϕU¬ψ)I Fϕ ≈ true UϕI Gϕ ≈ false RϕЗаконы неподвижной точки.I Fϕ ≈ ϕ ∨ XFϕI Gϕ ≈ ϕ & XGϕI ϕUψ ≈ ψ ∨ (ϕ & X(ϕUψ))I ϕRψ ≈ ψ &(ϕ ∨ X(ϕRψ))Доказательство.

Достаточно использовать определениеПокажем справедливость закона ¬(ϕUψ) ≈ ¬ϕR¬ψЛогика линейного времениДоказательство.Рассмотрим произвольную темпоральную интерпретацию IЛогика линейного времениДоказательство.Рассмотрим произвольную темпоральную интерпретацию II |= ¬(ϕUψ)Логика линейного времениДоказательство.Рассмотрим произвольную темпоральную интерпретацию II |= ¬(ϕUψ)⇔I 6|= ϕUψЛогика линейного времениДоказательство.Рассмотрим произвольную темпоральную интерпретацию II |= ¬(ϕUψ)⇔I 6|= ϕUψ⇔справедливо хотя бы одно из двух:I: для любого k ≥ 1 верно I , k 6|= ψII: существует k ≥ 1, такое что I , k 6|= ϕи для любого i, 0 < i ≤ k, верно I , i 6|= ψЛогика линейного времениДоказательство.Рассмотрим произвольную темпоральную интерпретацию II |= ¬(ϕUψ)⇔I 6|= ϕUψ⇔справедливо хотя бы одно из двух:I: для любого k ≥ 1 верно I , k 6|= ψ (то есть I , k |= ¬ψ)¬ψ1¬ψ2¬ψ3...¬ψkII: существует k ≥ 1, такое что I , k 6|= ϕи для любого i, 0 < i ≤ k, верно I , i 6|= ψ...Логика линейного времениДоказательство.Рассмотрим произвольную темпоральную интерпретацию II |= ¬(ϕUψ)⇔I 6|= ϕUψ⇔справедливо хотя бы одно из двух:I: для любого k ≥ 1 верно I , k 6|= ψ (то есть I , k |= ¬ψ)¬ψ1¬ψ2¬ψ3...¬ψk...II: существует k ≥ 1, такое что I , k 6|= ϕ (то есть I , k |= ¬ϕ)и для любого i, 0 < i ≤ k, верно I , i 6|= ψ (то есть I , i |= ¬ψ)¬ψ1¬ψ2¬ψ3...¬ϕ, ¬ψk...Логика линейного времениДоказательство.Рассмотрим произвольную темпоральную интерпретацию II |= ¬(ϕUψ)⇔I 6|= ϕUψ⇔справедливо хотя бы одно из двух:I: для любого k ≥ 1 верно I , k 6|= ψ (то есть I , k |= ¬ψ)¬ψ1¬ψ2¬ψ3...¬ψk...II: существует k ≥ 1, такое что I , k 6|= ϕ (то есть I , k |= ¬ϕ)и для любого i, 0 < i ≤ k, верно I , i 6|= ψ (то есть I , i |= ¬ψ)¬ψ1¬ψ2¬ψ3...¬ϕ, ¬ψk...Но это в точности определение для соотношения I , 1 |= ¬ϕR¬ψHЛогика линейного времениЗадача для самостоятельного размышленияВерны ли какие-нибудь законы дистрибутивности?IIIIIIIIF(ϕ ∨ ψ) ≈ ?F(ϕ & ψ) ≈ ?G(ϕ ∨ ψ) ≈ ?G(ϕ & ψ) ≈ ?ϕU(ψ ∨ χ) ≈ ?ϕU(ψ & χ) ≈ ?(ϕ ∨ ψ)Uχ ≈ ?(ϕ & ψ)Uχ ≈ ?Логика линейного времениВыразительные возможности LTLВернёмся к примеру с сетевым принтером, для простоты полагая,что в сети ровно два компьютераЛогика линейного времениВыразительные возможности LTL1.

данные на принтер всегда передаёт не более чем одинкомпьютер2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занят3. если принтер оказался занят, то он рано или поздноприступит к печати4. принтер, завершивший печать, обязательно освободитсяЛогика линейного времениВыразительные возможности LTL1. данные на принтер всегда передаёт не более чем одинкомпьютер2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занят3. если принтер оказался занят, то он рано или поздноприступит к печати4.

принтер, завершивший печать, обязательно освободитсяМожно ли адекватно выразить эти требования LTL-формулами?Логика линейного времениВыразительные возможности LTLВведём атомарные события, используемые в требованиях ксистемеЛогика линейного времениВыразительные возможности LTLВведём атомарные события, используемые в требованиях ксистеме:1. tryi : i-й компьютер собирается отправить данные на печатьЛогика линейного времениВыразительные возможности LTLВведём атомарные события, используемые в требованиях ксистеме:1. tryi : i-й компьютер собирается отправить данные на печать2.

pri : i-й компьютер передаёт данные на печать(и принтер печатает)Логика линейного времениВыразительные возможности LTLВведём атомарные события, используемые в требованиях ксистеме:1. tryi : i-й компьютер собирается отправить данные на печать2. pri : i-й компьютер передаёт данные на печать(и принтер печатает)3. busy : принтер занятЛогика линейного времениВыразительные возможности LTLВведём атомарные события, используемые в требованиях ксистеме:1. tryi : i-й компьютер собирается отправить данные на печать2.

pri : i-й компьютер передаёт данные на печать(и принтер печатает)3. busy : принтер занят4. free: принтер свободенЛогика линейного времениВыразительные возможности LTLВведём атомарные события, используемые в требованиях ксистеме:1. tryi : i-й компьютер собирается отправить данные на печать2. pri : i-й компьютер передаёт данные на печать(и принтер печатает)3. busy : принтер занят4. free: принтер свободенТребования к системе с сетевым принтером можно записать так:Логика линейного времениВыразительные возможности LTLВведём атомарные события, используемые в требованиях ксистеме:1.

tryi : i-й компьютер собирается отправить данные на печать2. pri : i-й компьютер передаёт данные на печать(и принтер печатает)3. busy : принтер занят4. free: принтер свободенТребования к системе с сетевым принтером можно записать так:1. данные на принтер всегда передаёт не более чем одинкомпьютерG¬(pr1 & pr2 )Логика линейного времениВыразительные возможности LTL2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занятG(free &(try1 ∨ try2 ) → Fbusy )Логика линейного времениВыразительные возможности LTL2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занятG(free &(try1 ∨ try2 ) → Fbusy )3.

если принтер оказался занят, то он рано или поздноприступит к печатиG(free & Xbusy → XF(pr1 ∨ pr2 ))Логика линейного времениВыразительные возможности LTL2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занятG(free &(try1 ∨ try2 ) → Fbusy )3. если принтер оказался занят, то он рано или поздноприступит к печатиG(free & Xbusy → XF(pr1 ∨ pr2 ))4. принтер, завершивший печать, обязательно освободитсяG(pr1 & X¬pr1 → XFfree) &G(pr2 & X¬pr2 → XFfree)Логика линейного времениВыразительные возможности LTL2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занятG(free &(try1 ∨ try2 ) → Fbusy )3. если принтер оказался занят, то он рано или поздноприступит к печатиG(free & Xbusy → XF(pr1 ∨ pr2 ))4.

принтер, завершивший печать, обязательно освободитсяG(pr1 & X¬pr1 → XFfree) &G(pr2 & X¬pr2 → XFfree)или так:G(pr1 & X¬pr1 ∨ pr2 & X¬pr2 → XFfree)Логика линейного времениВыразительные возможности LTL5. пока хотя бы один компьютер отправляет данные на печать,принтер остаётся занятымG(¬(pr1 ∨ pr2 )Rbusy )Логика линейного времениВыразительные возможности LTL5.

пока хотя бы один компьютер отправляет данные на печать,принтер остаётся занятымG(¬(pr1 ∨ pr2 )Rbusy )а почему бы не вот такG(busy R¬(pr1 ∨ pr2 )) ?Логика линейного времениВыразительные возможности LTL5. пока хотя бы один компьютер отправляет данные на печать,принтер остаётся занятымG(¬(pr1 ∨ pr2 )Rbusy )а почему бы не вот такG(busy R¬(pr1 ∨ pr2 )) ?а может, вообще вот такG(pr1 ∨ pr2 → busy ) ?Логика линейного времениВыразительные возможности LTL5.

пока хотя бы один компьютер отправляет данные на печать,принтер остаётся занятымG(¬(pr1 ∨ pr2 )Rbusy )а почему бы не вот такG(busy R¬(pr1 ∨ pr2 )) ?а может, вообще вот такG(pr1 ∨ pr2 → busy ) ?Так какая же формула адекватная и почему?Логика линейного времениМы убедились, что формализм LTL подходит для описаниятребований к распределённым системамЛогика линейного времениМы убедились, что формализм LTL подходит для описаниятребований к распределённым системамА как проверить выполнение этих требований?Логика линейного времениМы убедились, что формализм LTL подходит для описаниятребований к распределённым системамА как проверить выполнение этих требований?Для этого прежде всего необходимо определить математическуюмодель, описывающую устройство распределённой системыЛогика линейного времениМы убедились, что формализм LTL подходит для описаниятребований к распределённым системамА как проверить выполнение этих требований?Для этого прежде всего необходимо определить математическуюмодель, описывающую устройство распределённой системыЭта модель должна быть удобной для анализаЛогика линейного времениМы убедились, что формализм LTL подходит для описаниятребований к распределённым системамА как проверить выполнение этих требований?Для этого прежде всего необходимо определить математическуюмодель, описывающую устройство распределённой системыЭта модель должна быть удобной для анализа, а именно:Iона должна иметь простое устройствоЛогика линейного времениМы убедились, что формализм LTL подходит для описаниятребований к распределённым системамА как проверить выполнение этих требований?Для этого прежде всего необходимо определить математическуюмодель, описывающую устройство распределённой системыЭта модель должна быть удобной для анализа, а именно:IIона должна иметь простое устройствокаждое вычисление в этой модели должно представлятьсобой темпоральную интерпретациюЛогика линейного времениМы убедились, что формализм LTL подходит для описаниятребований к распределённым системамА как проверить выполнение этих требований?Для этого прежде всего необходимо определить математическуюмодель, описывающую устройство распределённой системыЭта модель должна быть удобной для анализа, а именно:IIIона должна иметь простое устройствокаждое вычисление в этой модели должно представлятьсобой темпоральную интерпретациювычисления в модели должны достаточно точносоответствовать сценариям работы распределённойсистемыЛогика линейного времениМы убедились, что формализм LTL подходит для описаниятребований к распределённым системамА как проверить выполнение этих требований?Для этого прежде всего необходимо определить математическуюмодель, описывающую устройство распределённой системыЭта модель должна быть удобной для анализа, а именно:IIIона должна иметь простое устройствокаждое вычисление в этой модели должно представлятьсобой темпоральную интерпретациювычисления в модели должны достаточно точносоответствовать сценариям работы распределённойсистемыВ качестве такой модели будем использовать размеченныесистемы переходов: LTSs (Labelled Transition Systems)Размеченные системы переходовРазмеченная система переходов (LTS) над множествоматомарных событий P — это система (S, S0 , →, ρ), где:Размеченные системы переходовРазмеченная система переходов (LTS) над множествоматомарных событий P — это система (S, S0 , →, ρ), где:IS — непустое множество состояний вычисленияРазмеченные системы переходовРазмеченная система переходов (LTS) над множествоматомарных событий P — это система (S, S0 , →, ρ), где:IIS — непустое множество состояний вычисленияS0 ⊆ S — непустое множество начальных состоянийРазмеченные системы переходовРазмеченная система переходов (LTS) над множествоматомарных событий P — это система (S, S0 , →, ρ), где:IIIS — непустое множество состояний вычисленияS0 ⊆ S — непустое множество начальных состояний→: S × S — тотальное отношение переходовТотальность отношения переходов означает, что из любогосостояния вычисления s можно совершить переход: ∃s 0 (s → s 0 )Размеченные системы переходовРазмеченная система переходов (LTS) над множествоматомарных событий P — это система (S, S0 , →, ρ), где:IIIIS — непустое множество состояний вычисленияS0 ⊆ S — непустое множество начальных состояний→: S × S — тотальное отношение переходовρ : S → 2P — функция разметкиТотальность отношения переходов означает, что из любогосостояния вычисления s можно совершить переход: ∃s 0 (s → s 0 )Функция разметки сопоставляет каждому состояниювычисления s истинные в нём атомарные события ρ(s), то естьпротекающие в этом состоянии событияРазмеченные системы переходовРазмеченная система переходов (LTS) над множествоматомарных событий P — это система (S, S0 , →, ρ), где:IIIIS — непустое множество состояний вычисленияS0 ⊆ S — непустое множество начальных состояний→: S × S — тотальное отношение переходовρ : S → 2P — функция разметкиТотальность отношения переходов означает, что из любогосостояния вычисления s можно совершить переход: ∃s 0 (s → s 0 )Функция разметки сопоставляет каждому состояниювычисления s истинные в нём атомарные события ρ(s), то естьпротекающие в этом состоянии событияЕсли быть точным, то это особый вид системы переходов:структура Крипке(Kripke structure)Размеченные системы переходовПримерP = {p, q}LTS ({.