Презентация 18 (Лекции)

Математическая логикаи логическое программированиеЛектор:Подымов Владислав Васильевич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ψ? .