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

Это просто(достаточно использовать определение согласованности)Замыкание Фишера-ЛаднераА обязано ли непротиворечивое предположение бытьсогласованным?УтверждениеПусть I — темпоральная интерпретацияи ϕ — позитивная формаТогда для любого момента времени n множество{ψ | ψ ∈ [ϕ]FL и I, n |= ψ}является согласованным предположениемДоказательство. Это просто(достаточно использовать определение согласованности)А насколько просто перебирать и сравнивать между собойсогласованные предположения?Замыкание Фишера-ЛаднераУтверждениеДля любой позитивной формы ϕ верно следующее:1.

для любой пары множеств HP ⊆ [ϕ]P , HX ⊆ [ϕ]Xсуществует согласованное предположение H, такоечто H ∩ [ϕ]P = HP и H ∩ [ϕ]X = HXЗамыкание Фишера-ЛаднераУтверждениеДля любой позитивной формы ϕ верно следующее:1. для любой пары множеств HP ⊆ [ϕ]P , HX ⊆ [ϕ]Xсуществует согласованное предположение H, такоечто H ∩ [ϕ]P = HP и H ∩ [ϕ]X = HX2. для любых согласованных предположений H1 , H2верно следующее:H1 = H2 ⇔ H1 ∩ P = H2 ∩ P иH1 ∩ [ϕ]X = H2 ∩ [ϕ]XЗамыкание Фишера-ЛаднераУтверждениеДля любой позитивной формы ϕ верно следующее:1. для любой пары множеств HP ⊆ [ϕ]P , HX ⊆ [ϕ]Xсуществует согласованное предположение H, такоечто H ∩ [ϕ]P = HP и H ∩ [ϕ]X = HX2.

для любых согласованных предположений H1 , H2верно следующее:H1 = H2 ⇔ H1 ∩ P = H2 ∩ P иH1 ∩ [ϕ]X = H2 ∩ [ϕ]XДоказательство. Попробуйте самиЗамыкание Фишера-ЛаднераУтверждениеДля любой позитивной формы ϕ верно следующее:1. для любой пары множеств HP ⊆ [ϕ]P , HX ⊆ [ϕ]Xсуществует согласованное предположение H, такоечто H ∩ [ϕ]P = HP и H ∩ [ϕ]X = HX2. для любых согласованных предположений H1 , H2верно следующее:H1 = H2 ⇔ H1 ∩ P = H2 ∩ P иH1 ∩ [ϕ]X = H2 ∩ [ϕ]XДоказательство. Попробуйте самиСледствие. Если позитивная форма ϕ содержит nопераций, то число различных согласованныхпредположений не превосходит 23nТабличный метод model checking∃tr ∈ Tr0 (M) :tr |= ϕ?А как выдвижение согласованных предположений поможетрешить исходную задачу?Табличный метод model checking∃tr ∈ Tr0 (M) :tr |= ϕ?А как выдвижение согласованных предположений поможетрешить исходную задачу?Iбудем обходить LTS M всеми возможными способамиТабличный метод model checking∃tr ∈ Tr0 (M) :tr |= ϕ?А как выдвижение согласованных предположений поможетрешить исходную задачу?IIбудем обходить LTS M всеми возможными способамидля каждого шага обхода будем выдвигать согласованноепредположение о том, какие формулы из [ϕ]FLвыполняются на текущем шаге в текущем состоянии, акакие не выполняютсяТабличный метод model checking∃tr ∈ Tr0 (M) :tr |= ϕ?А как выдвижение согласованных предположений поможетрешить исходную задачу?IIIбудем обходить LTS M всеми возможными способамидля каждого шага обхода будем выдвигать согласованноепредположение о том, какие формулы из [ϕ]FLвыполняются на текущем шаге в текущем состоянии, акакие не выполняютсякроме (внутренней) согласованности предположенийпотребуем их согласованность на соседних шагах обходаТабличный метод model checking∃tr ∈ Tr0 (M) :tr |= ϕ?А как выдвижение согласованных предположений поможетрешить исходную задачу?IIIIбудем обходить LTS M всеми возможными способамидля каждого шага обхода будем выдвигать согласованноепредположение о том, какие формулы из [ϕ]FLвыполняются на текущем шаге в текущем состоянии, акакие не выполняютсякроме (внутренней) согласованности предположенийпотребуем их согласованность на соседних шагах обходапроверим, используя разметку LTS M предположениями,существует ли в M требуемая трасса trТабличный метод model checking∃tr ∈ Tr0 (M) :tr |= ϕ?А как выдвижение согласованных предположений поможетрешить исходную задачу?IIIIбудем обходить LTS M всеми возможными способамидля каждого шага обхода будем выдвигать согласованноепредположение о том, какие формулы из [ϕ]FLвыполняются на текущем шаге в текущем состоянии, акакие не выполняютсякроме (внутренней) согласованности предположенийпотребуем их согласованность на соседних шагах обходапроверим, используя разметку LTS M предположениями,существует ли в M требуемая трасса trА как может выглядеть LTS, размеченная предположениямисогласованным образом?Табличный метод model checkingСистема Хинтикки1 для LTS M = (S, S0 , →, ρ) и позитивнойформы ϕ — это ориентированный граф ΓM,ϕ = (V , E )следующего вида:1Каарло Яакко Юхани Хинти́ккаТабличный метод model checkingСистема Хинтикки1 для LTS M = (S, S0 , →, ρ) и позитивнойформы ϕ — это ориентированный граф ΓM,ϕ = (V , E )следующего вида: H — согласованное предположение;I V =(s, H) s ∈ S; H ∩ P = ρ(s)I1то есть вершина ΓM,ϕ — это состояние M, помеченноесогласованным предположением, подтверждающимсяразметкой sКаарло Яакко Юхани Хинти́ккаТабличный метод model checkingСистема Хинтикки1 для LTS M = (S, S0 , →, ρ) и позитивнойформы ϕ — это ориентированный граф ΓM,ϕ = (V , E )следующего вида: H — согласованное предположение;I V =(s, H) s ∈ S; H ∩ P = ρ(s)II (s1 , H1 ), (s2 , H2 ) ∈ V ; s → s2 ;E = (s1 , H1 ) → (s2 , H2 ) 1 если Xψ ∈ [ϕ]X , тоXψ ∈ H1 ⇔ ψ ∈ H2I1то есть вершина ΓM,ϕ — это состояние M, помеченноесогласованным предположением, подтверждающимсяразметкойsто есть каждая дуга основана на переходе в M, и всепредположения вида Xψ в начале дуги подтверждаются вконце дугиКаарло Яакко Юхани Хинти́ккаТабличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:Табличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:I пронумеруем формулы множества [ϕ]UR :[ϕ]UR = {ϕ1 , ϕ2 , .

. . , ϕm }Табличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:I пронумеруем формулы множества [ϕ]UR :[ϕ]UR = {ϕ1 , ϕ2 , . . . , ϕm }I для каждой формулы ϕi заведём цвет iТабличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:I пронумеруем формулы множества [ϕ]UR :[ϕ]UR = {ϕ1 , ϕ2 , .

. . , ϕm }I для каждой формулы ϕi заведём цвет iI окрасим вершину (s, H) в цвет i, еслиТабличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:I пронумеруем формулы множества [ϕ]UR :[ϕ]UR = {ϕ1 , ϕ2 , . . . , ϕm }I для каждой формулы ϕi заведём цвет iI окрасим вершину (s, H) в цвет i, еслиIϕi = ψUχ, и выполнено хотя бы одно из двух условий:χ ∈ H,X(ψUχ) ∈/HТабличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:I пронумеруем формулы множества [ϕ]UR :[ϕ]UR = {ϕ1 , ϕ2 , .

. . , ϕm }I для каждой формулы ϕi заведём цвет iI окрасим вершину (s, H) в цвет i, еслиIIϕi = ψUχ, и выполнено хотя бы одно из двух условий:χ ∈ H,X(ψUχ) ∈/Hϕi = ψRχ, и выполнено хотя бы одно из двух условий:χ∈/ H,X(ψRχ) ∈ HТабличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:I пронумеруем формулы множества [ϕ]UR :[ϕ]UR = {ϕ1 , ϕ2 , . . . , ϕm }I для каждой формулы ϕi заведём цвет iI окрасим вершину (s, H) в цвет i, еслиIIϕi = ψUχ, и выполнено хотя бы одно из двух условий:χ ∈ H,X(ψUχ) ∈/Hϕi = ψRχ, и выполнено хотя бы одно из двух условий:χ∈/ H,X(ψRχ) ∈ HРезультат такой раскраски назовём раскрашенной системойХинтикки и будем обозначать так: ΓM,ϕТабличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:I пронумеруем формулы множества [ϕ]UR :[ϕ]UR = {ϕ1 , ϕ2 , .

. . , ϕm }I для каждой формулы ϕi заведём цвет iI окрасим вершину (s, H) в цвет i, еслиIIϕi = ψUχ, и выполнено хотя бы одно из двух условий:χ ∈ H,X(ψUχ) ∈/Hϕi = ψRχ, и выполнено хотя бы одно из двух условий:χ∈/ H,X(ψRχ) ∈ HРезультат такой раскраски назовём раскрашенной системойХинтикки и будем обозначать так: ΓM,ϕБесконечный путь в графе ΓM,ϕ назовём радужным, есликаждый цвет (1, 2, . . . , m) встречается в нём бесконечно частоТабличный метод model checkingРаскрасим граф ΓM,ϕ следующим образом:I пронумеруем формулы множества [ϕ]UR :[ϕ]UR = {ϕ1 , ϕ2 , .

. . , ϕm }I для каждой формулы ϕi заведём цвет iI окрасим вершину (s, H) в цвет i, еслиIIϕi = ψUχ, и выполнено хотя бы одно из двух условий:χ ∈ H,X(ψUχ) ∈/Hϕi = ψRχ, и выполнено хотя бы одно из двух условий:χ∈/ H,X(ψRχ) ∈ HРезультат такой раскраски назовём раскрашенной системойХинтикки и будем обозначать так: ΓM,ϕБесконечный путь в графе ΓM,ϕ назовём радужным, есликаждый цвет (1, 2, . . . , m) встречается в нём бесконечно частоИ как понимать эту радужность?Табличный метод model checkingРассмотрим нерадужный путь в ΓM,ϕ :(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . . .Табличный метод model checkingРассмотрим нерадужный путь в ΓM,ϕ :(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → .

. .Существует цвет i, встречающийся в tr лишь конечное числоразТабличный метод model checkingРассмотрим нерадужный путь в ΓM,ϕ :(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . . .Существует цвет i, встречающийся в tr лишь конечное числоразЗначит, существует суффикс tr |j этого пути, в котором ни однавершина не покрашена в цвет iТабличный метод model checkingРассмотрим нерадужный путь в ΓM,ϕ :(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . . .Существует цвет i, встречающийся в tr лишь конечное числоразЗначит, существует суффикс tr |j этого пути, в котором ни однавершина не покрашена в цвет iСлучай 1: цвет i сопоставлен формуле ψUχТабличный метод model checkingРассмотрим нерадужный путь в ΓM,ϕ :(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → .

. .Существует цвет i, встречающийся в tr лишь конечное числоразЗначит, существует суффикс tr |j этого пути, в котором ни однавершина не покрашена в цвет iСлучай 1: цвет i сопоставлен формуле ψUχЧто означает “вершина не окрашена в цвет i”?Табличный метод model checkingРассмотрим нерадужный путь в ΓM,ϕ :(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . . .Существует цвет i, встречающийся в tr лишь конечное числоразЗначит, существует суффикс tr |j этого пути, в котором ни однавершина не покрашена в цвет iСлучай 1: цвет i сопоставлен формуле ψUχЧто означает “вершина не окрашена в цвет i”?χ∈/ H и X(ψUχ) ∈ HТабличный метод model checkingРассмотрим нерадужный путь в ΓM,ϕ :(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → .