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

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

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

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

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

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

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

. .Существует цвет i, встречающийся в tr лишь конечное числоразЗначит, существует суффикс tr |j этого пути, в котором ни однавершина не покрашена в цвет iСлучай 2: цвет i сопоставлен формуле ψRχЧто означает “вершина не окрашена в цвет i”?χ ∈ H и X(ψUχ) ∈/Hχχχ¬X(ψRχ) ¬X(ψRχ)sjsj+1¬ψRχ...¬X(ψRχ)sj+n¬ψRχНижняя строка: для трассы tr |j+1 верно ¬(ψRχ)Верхняя строка: для трассы tr |j+1 верно ψRχ...Табличный метод 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Итог: предположения, сделанные в раскрашенной системеХинтикки для нерадужного пути, содержат противоречияВ результате имеется три способа избежать противоречий привыдвижении предположений:Табличный метод model checkingРассмотрим нерадужный путь в ΓM,ϕ :(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . . .Существует цвет i, встречающийся в tr лишь конечное числоразЗначит, существует суффикс tr |j этого пути, в котором ни однавершина не покрашена в цвет iИтог: предположения, сделанные в раскрашенной системеХинтикки для нерадужного пути, содержат противоречияВ результате имеется три способа избежать противоречий привыдвижении предположений:1.

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

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

. .Существует цвет i, встречающийся в tr лишь конечное числоразЗначит, существует суффикс tr |j этого пути, в котором ни однавершина не покрашена в цвет iИтог: предположения, сделанные в раскрашенной системеХинтикки для нерадужного пути, содержат противоречияВ результате имеется три способа избежать противоречий привыдвижении предположений:3.

рассматривать только радужные путиIа этого хватит, чтобы утверждать, что отсутствуют неявныепротиворечия из-за формул [ϕ]UR ?Табличный метод model checkingОказывается, что хватит:Теорема (табличный метод model checking для LTL)Для любой позитивной формы ϕ и любой LTSM = (S, S0 , →, ρ) верно следующее:M |6 = ϕ⇔в графе ΓM,ϕ существует радужный путь,исходящий из вершины (s, H),где s ∈ S0 и ϕ ∈/HОбоснование табличного метода model checking(⇐):Обоснование табличного метода model checking(⇐):Рассмотрим радужный путь(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . .

.в графе ΓM,ϕ , такой что s1 ∈ S0 и ϕ ∈/ H1Обоснование табличного метода model checking(⇐):Рассмотрим радужный путь(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . . .в графе ΓM,ϕ , такой что s1 ∈ S0 и ϕ ∈/ H1По определению системы Хинтикки в LTS M существует такаяначальная трасса tr :s1 → s2 → · · · → sn → . . .Обоснование табличного метода model checking(⇐):Рассмотрим радужный путь(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . . .в графе ΓM,ϕ , такой что s1 ∈ S0 и ϕ ∈/ H1По определению системы Хинтикки в LTS M существует такаяначальная трасса tr :s1 → s2 → · · · → sn → . . .Покажем индукцией по числу связок, что для любойформулы ψ ∈ [ϕ]FL и любого натурального n верноψ ∈ Hn ⇔ tr |n |= ψОбоснование табличного метода model checking(⇐):Рассмотрим радужный путь(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → .

. .в графе ΓM,ϕ , такой что s1 ∈ S0 и ϕ ∈/ H1По определению системы Хинтикки в LTS M существует такаяначальная трасса tr :s1 → s2 → · · · → sn → . . .Покажем индукцией по числу связок, что для любойформулы ψ ∈ [ϕ]FL и любого натурального n верноψ ∈ Hn ⇔ tr |n |= ψПроще говоря, покажем, что все предположения, сделанные длярадужного пути, действительно верныОбоснование табличного метода model checking(⇐):Рассмотрим радужный путь(s1 , H1 ) → (s2 , H2 ) → · · · → (sn , Hn ) → . .