Презентация 18 (1131946)
Текст из файла
Математическая логикаи логическое программированиеЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2016, весенний семестрЗадача model checking для LTLдля заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕЗадача model checking для LTLдля заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕНасколько трудна эта задача?Задача model checking для LTLдля заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕНасколько трудна эта задача?Она кажется не особо простойЗадача model checking для LTLдля заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕНасколько трудна эта задача?Она кажется не особо простой, так какI интерпретации LTL-формул бесконечныЗадача model checking для LTLдля заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕНасколько трудна эта задача?Она кажется не особо простой, так какI интерпретации LTL-формул бесконечныI LTS содержит бесконечно много интерпретаций (трасс)Задача model checking для LTLдля заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕНасколько трудна эта задача?Она кажется не особо простой, так какI интерпретации LTL-формул бесконечныI LTS содержит бесконечно много интерпретаций (трасс)Тем не менее она имеет эффективное решениеЗадача model checking для LTLдля заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕНасколько трудна эта задача?Она кажется не особо простой, так какI интерпретации LTL-формул бесконечныI LTS содержит бесконечно много интерпретаций (трасс)Тем не менее она имеет эффективное решение, так какI все интерпретации описаны конечной структурой — LTS MЗадача model checking для LTLдля заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕНасколько трудна эта задача?Она кажется не особо простой, так какI интерпретации LTL-формул бесконечныI LTS содержит бесконечно много интерпретаций (трасс)Тем не менее она имеет эффективное решение, так какI все интерпретации описаны конечной структурой — LTS MКак же выглядит алгоритм проверки соотношения M |= ϕ?(табличный метод)Задача model checking для LTLСначала ещё немного обозначенийЗадача model checking для LTLСначала ещё немного обозначенийРассмотрим трассу tr LTS M:tr : s1 → s2 → s3 → .
. .и LTL-формулу ϕЗадача model checking для LTLСначала ещё немного обозначенийРассмотрим трассу tr LTS M:tr : s1 → s2 → s3 → . . .и LTL-формулу ϕtr |= ϕ — сокращение для записи I(tr ), 1 |= ϕЗадача model checking для LTLСначала ещё немного обозначенийРассмотрим трассу tr LTS M:tr : s1 → s2 → s3 → . . .и LTL-формулу ϕtr |= ϕ — сокращение для записи I(tr ), 1 |= ϕtr [j] — j-е состояние трассы tr : sjЗадача model checking для LTLСначала ещё немного обозначенийРассмотрим трассу tr LTS M:tr : s1 → s2 → s3 → .
. .и LTL-формулу ϕtr |= ϕ — сокращение для записи I(tr ), 1 |= ϕtr [j] — j-е состояние трассы tr : sjtr |j — суффикс трассы tr , начинающийся с состояния tr [j]:sj → sj+1 → sj+2 → . . .Задача model checking для LTLУтверждение. Пусть M — LTS и ϕ — LTL-формулаТогдаM 6|= ϕ ⇔ существует начальная трасса tr LTS M,такая что t 6|= ϕЗадача model checking для LTLУтверждение. Пусть M — LTS и ϕ — LTL-формулаТогдаM 6|= ϕ ⇔ существует начальная трасса tr LTS M,такая что t 6|= ϕДоказательство. По опредлению соотношения M 6|= ϕHЗадача model checking для LTLУтверждение. Пусть M — LTS и ϕ — LTL-формулаТогдаM 6|= ϕ ⇔ существует начальная трасса tr LTS M,такая что t 6|= ϕДоказательство. По опредлению соотношения M 6|= ϕЗначит, достаточно решить такую задачу:найти начальную трассу tr LTS M,для которой верно tr |= ψH(ψ = ¬ϕ)Задача model checking для LTLУтверждение.
Пусть M — LTS и ϕ — LTL-формулаТогдаM 6|= ϕ ⇔ существует начальная трасса tr LTS M,такая что t 6|= ϕДоказательство. По опредлению соотношения M 6|= ϕЗначит, достаточно решить такую задачу:найти начальную трассу tr LTS M,для которой верно tr |= ψIIТрасса найдена: M 6|= ϕТакой трассы не существует: M |= ϕH(ψ = ¬ϕ)Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?Упростим формулу ϕ (как в методе резолюций)Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?Упростим формулу ϕ (как в методе резолюций)Формула ϕ находится в позитивной форме(или является позитивной формой), если в нейI не содержится символов →, F, GIIто есть используются только операции &, ∨, ¬, X, U, Rсвязка ¬ применяется только к атомарным высказываниямЗадача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?Упростим формулу ϕ (как в методе резолюций)Формула ϕ находится в позитивной форме(или является позитивной формой), если в нейI не содержится символов →, F, GIIто есть используются только операции &, ∨, ¬, X, U, Rсвязка ¬ применяется только к атомарным высказываниямУтверждениеДля любой LTL-формулы ϕ существует равносильнаяей позитивная формаЗадача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?УтверждениеДля любой LTL-формулы ϕ существует равносильнаяей позитивная формаДоказательство.Явно построим требуемую позитивную форму ψЗадача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?УтверждениеДля любой LTL-формулы ϕ существует равносильнаяей позитивная формаДоказательство.Явно построим требуемую позитивную форму ψДля этого достаточноI удалить связки →:ϕ1 → ϕ2 ≈ ¬ϕ1 ∨ ϕ2Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?УтверждениеДля любой LTL-формулы ϕ существует равносильнаяей позитивная формаДоказательство.Явно построим требуемую позитивную форму ψДля этого достаточноI удалить связки →:ϕ1 → ϕ2 ≈ ¬ϕ1 ∨ ϕ2I удалить операторы F:Fϕ1 ≈ true Uϕ1Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?УтверждениеДля любой LTL-формулы ϕ существует равносильнаяей позитивная формаДоказательство.Явно построим требуемую позитивную форму ψДля этого достаточноI удалить связки →:ϕ1 → ϕ2 ≈ ¬ϕ1 ∨ ϕ2I удалить операторы F:Fϕ1 ≈ true Uϕ1I удалить операторы G:Gϕ1 ≈ false Rϕ1Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?УтверждениеДля любой LTL-формулы ϕ существует равносильнаяей позитивная формаДоказательство.Явно построим требуемую позитивную форму ψДля этого достаточноI удалить связки →:ϕ1 → ϕ2 ≈ ¬ϕ1 ∨ ϕ2I удалить операторы F:Fϕ1 ≈ true Uϕ1I удалить операторы G:Gϕ1 ≈ false Rϕ1I продвинуть отрицания вглубь формулы:¬(ϕ1 ∨ ϕ2 ) ≈ ¬ϕ1 & ¬ϕ2¬Xϕ1 ≈ X¬ϕ1¬(ϕ1 & ϕ2 ) ≈ ¬ϕ1 ∨ ¬ϕ2¬(ϕ1 Uϕ2 ) ≈ ¬ϕ1 R¬ϕ2¬¬ϕ1 ≈ ϕ1¬(ϕ1 Rϕ2 ) ≈ ¬ϕ1 U¬ϕ2HЗадача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?ПримерG(free & Xbusy →XF(pr1 ∨ pr2 ))Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?ПримерG(free & Xbusy →XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ XF(pr1 ∨ pr2 ))Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?ПримерG(free & Xbusy →XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 )))Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?ПримерG(free & Xbusy →XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 )))≈false R(¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 )))Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?ПримерG(free & Xbusy →XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 )))≈false R(¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 )))≈false R(¬free ∨ ¬Xbusy ∨ X(true U(pr1 ∨ pr2 )))Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?ПримерG(free & Xbusy →XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ XF(pr1 ∨ pr2 ))≈G(¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 )))≈false R(¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 )))≈false R(¬free ∨ ¬Xbusy ∨ X(true U(pr1 ∨ pr2 )))≈false R(¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 )))Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?Попытаемся решить задачу индукцией по построению формулыЗадача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?Попытаемся решить задачу индукцией по построению формулы:I пусть ϕ = OP ψ1 или ϕ = ψ1 OP ψ2Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?Попытаемся решить задачу индукцией по построению формулы:I пусть ϕ = OP ψ1 или ϕ = ψ1 OP ψ2I для каждой подформулы ψi и каждого соотояния s LTS Mрешим задачу “∃tr ∈ Tr0 (M(s)) : tr |= ϕ?”ILTS M(s) получается из LTS M заменой заменоймножества начальных состояний на {s}Задача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?Попытаемся решить задачу индукцией по построению формулы:I пусть ϕ = OP ψ1 или ϕ = ψ1 OP ψ2I для каждой подформулы ψi и каждого соотояния s LTS Mрешим задачу “∃tr ∈ Tr0 (M(s)) : tr |= ϕ?”IILTS M(s) получается из LTS M заменой заменоймножества начальных состояний на {s}предоставим ответ, основанный на ответах для ψ1 , ψ2 и наоперации OPЗадача model checking для LTL∃tr ∈ Tr0 (M) :tr |= ϕ?Попытаемся решить задачу индукцией по построению формулы:I пусть ϕ = OP ψ1 или ϕ = ψ1 OP ψ2I для каждой подформулы ψi и каждого соотояния s LTS Mрешим задачу “∃tr ∈ Tr0 (M(s)) : tr |= ϕ?”IILTS M(s) получается из LTS M заменой заменоймножества начальных состояний на {s}предоставим ответ, основанный на ответах для ψ1 , ψ2 и наоперации OPКакие сложности возникают в таком индуктивном решении?Задача model checking для LTL......ϕ & ψ?......;......Задача model checking для LTL...ϕ & ψ?......ϕ, ψ?;.........Задача model checking для LTL......ϕ ∨ ψ?......;......Задача model checking для LTL...ϕ ∨ ψ?......ϕ, ψ?;.........Задача model checking для LTL......¬ϕ?......;......Задача model checking для LTL...¬ϕ?......ϕ?;.........Задача model checking для LTL......Xϕ?......;......Задача model checking для LTL...Xϕ?......;ϕ?...ϕ?...ϕ?...Задача model checking для LTL...ϕUψ?......;?Задача model checking для LTL...ϕUψ?......;?Вспомним закон неподвижной точки:ϕUψ ≈ ψ ∨ ϕ & X(ϕUψ)Задача model checking для LTL...ϕUψ?......ψ, ϕ?;X(ϕUψ)?Вспомним закон неподвижной точки:ϕUψ ≈ ψ ∨ ϕ & X(ϕUψ)ϕUψ? .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
