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

. . , (tr [n], Hn ), . . .образует радужный путь в графе ΓM,ϕОбоснование табличного метода model checking(⇒):(tr [1], H1 ), (tr [2], H2 ), . . . , (tr [n], Hn ), . . .Обоснование табличного метода model checking(⇒):(tr [1], H1 ), (tr [2], H2 ), . . .

, (tr [n], Hn ), . . .I. Для любого i ≥ 1 верно tr [i] → tr [i + 1], так как tr — трасса вMОбоснование табличного метода model checking(⇒):(tr [1], H1 ), (tr [2], H2 ), . . . , (tr [n], Hn ), . . .I. Для любого i ≥ 1 верно tr [i] → tr [i + 1], так как tr — трасса вMII. Для любого i ≥ 1 и любой формулы Xψ ∈ [ϕ]FL верноXψ ∈ Hi ⇔ ψ ∈ Hi+1 ,так какXψ ∈ HiОбоснование табличного метода model checking(⇒):(tr [1], H1 ), (tr [2], H2 ), . . . , (tr [n], Hn ), .

. .I. Для любого i ≥ 1 верно tr [i] → tr [i + 1], так как tr — трасса вMII. Для любого i ≥ 1 и любой формулы Xψ ∈ [ϕ]FL верноXψ ∈ Hi ⇔ ψ ∈ Hi+1 ,так какXψ ∈ Hi⇔по выбору предположенияtr |i |= XψОбоснование табличного метода model checking(⇒):(tr [1], H1 ), (tr [2], H2 ), . . . , (tr [n], Hn ), . . .I. Для любого i ≥ 1 верно tr [i] → tr [i + 1], так как tr — трасса вMII. Для любого i ≥ 1 и любой формулы Xψ ∈ [ϕ]FL верноXψ ∈ Hi ⇔ ψ ∈ Hi+1 ,так какXψ ∈ Hi⇔по выбору предположенияtr |i |= Xψ⇔по определению выполнимости LTL-формулtr |i+1 |= ψОбоснование табличного метода model checking(⇒):(tr [1], H1 ), (tr [2], H2 ), .

. . , (tr [n], Hn ), . . .I. Для любого i ≥ 1 верно tr [i] → tr [i + 1], так как tr — трасса вMII. Для любого i ≥ 1 и любой формулы Xψ ∈ [ϕ]FL верноXψ ∈ Hi ⇔ ψ ∈ Hi+1 ,так какXψ ∈ Hi⇔по выбору предположенияtr |i |= Xψ⇔по определению выполнимости LTL-формулtr |i+1 |= ψ⇔по выбору предположенияψ ∈ Hi+1Обоснование табличного метода model checking(⇒):(tr [1], H1 ), (tr [2], H2 ), . . .

, (tr [n], Hn ), . . .I. Для любого i ≥ 1 верно tr [i] → tr [i + 1], так как tr — трасса вMII. Для любого i ≥ 1 и любой формулы Xψ ∈ [ϕ]FL верноXψ ∈ Hi ⇔ ψ ∈ Hi+1 ,так какXψ ∈ Hi⇔по выбору предположенияtr |i |= Xψ⇔по определению выполнимости LTL-формулtr |i+1 |= ψ⇔по выбору предположенияψ ∈ Hi+1III. tr [1] ∈ S0 , так как tr — начальная трасса в MОбоснование табличного метода model checking(⇒):(tr [1], H1 ), (tr [2], H2 ), . .

. , (tr [n], Hn ), . . .I. Для любого i ≥ 1 верно tr [i] → tr [i + 1], так как tr — трасса вMII. Для любого i ≥ 1 и любой формулы Xψ ∈ [ϕ]FL верноXψ ∈ Hi ⇔ ψ ∈ Hi+1 ,так какXψ ∈ Hi⇔по выбору предположенияtr |i |= Xψ⇔по определению выполнимости LTL-формулtr |i+1 |= ψ⇔по выбору предположенияψ ∈ Hi+1III. tr [1] ∈ S0 , так как tr — начальная трасса в MIV. ϕ ∈/ H1 по выбору предположения H1Обоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → .

. .Осталось показать, что:V. Путь P является радужнымОбоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → . . .Осталось показать, что:V. Путь P является радужнымПредположим, что он не является радужнымОбоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → . . .Осталось показать, что:V. Путь P является радужнымПредположим, что он не является радужнымДостаточно вспомнить рассуждения о нерадужных путяхОбоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → . .

.Осталось показать, что:V. Путь P является радужнымПредположим, что он не является радужнымДостаточно вспомнить рассуждения о нерадужных путях:I существуют цвет i и суффикс tr |j трассы tr , такие что ниодна вершина tr |j не покрашена в цвет iОбоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → . . .Осталось показать, что:V.

Путь P является радужнымПредположим, что он не является радужнымДостаточно вспомнить рассуждения о нерадужных путях:I существуют цвет i и суффикс tr |j трассы tr , такие что ниодна вершина tr |j не покрашена в цвет iI если цвет i соответствует формуле ψUχ, тоIχ∈/ Hj+1 , χ ∈/ Hj+2 , . . .IX(ψUχ) ∈ HjОбоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → .

. .Осталось показать, что:V. Путь P является радужнымПредположим, что он не является радужнымДостаточно вспомнить рассуждения о нерадужных путях:I существуют цвет i и суффикс tr |j трассы tr , такие что ниодна вершина tr |j не покрашена в цвет iI если цвет i соответствует формуле ψUχ, тоIχ∈/ Hj+1 , χ ∈/ Hj+2 , . . .IX(ψUχ) ∈ HjIи по выбору предположений получаем tr |j+1 6|= ψUχОбоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → .

. .Осталось показать, что:V. Путь P является радужнымПредположим, что он не является радужнымДостаточно вспомнить рассуждения о нерадужных путях:I существуют цвет i и суффикс tr |j трассы tr , такие что ниодна вершина tr |j не покрашена в цвет iI если цвет i соответствует формуле ψUχ, тоIχ∈/ Hj+1 , χ ∈/ Hj+2 , . . .IX(ψUχ) ∈ HjIIи по выбору предположений получаем tr |j+1 6|= ψUχпо определению графа ΓM,ϕ , ψUχ ∈ Hj+1Обоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → . .

.Осталось показать, что:V. Путь P является радужнымПредположим, что он не является радужнымДостаточно вспомнить рассуждения о нерадужных путях:I существуют цвет i и суффикс tr |j трассы tr , такие что ниодна вершина tr |j не покрашена в цвет iI если цвет i соответствует формуле ψUχ, тоIχ∈/ Hj+1 , χ ∈/ Hj+2 , . . .IX(ψUχ) ∈ HjIIIи по выбору предположений получаем tr |j+1 6|= ψUχпо определению графа ΓM,ϕ , ψUχ ∈ Hj+1по выбору предположений, tr |j+1 |= ψUχОбоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → . .

.Осталось показать, что:V. Путь P является радужнымПредположим, что он не является радужнымДостаточно вспомнить рассуждения о нерадужных путях:I существуют цвет i и суффикс tr |j трассы tr , такие что ниодна вершина tr |j не покрашена в цвет iI если цвет i соответствует формуле ψUχ, тоIχ∈/ Hj+1 , χ ∈/ Hj+2 , . . .IX(ψUχ) ∈ HjIIIIи по выбору предположений получаем tr |j+1 6|= ψUχпо определению графа ΓM,ϕ , ψUχ ∈ Hj+1по выбору предположений, tr |j+1 |= ψUχполученно противоречиеОбоснование табличного метода model checking(⇒):P: (tr [1], H1 ) → (tr [2], H2 ) → · · · → (tr [n], Hn ) → .

. .Осталось показать, что:V. Путь P является радужнымПредположим, что он не является радужнымДостаточно вспомнить рассуждения о нерадужных путях:I существуют цвет i и суффикс tr |j трассы tr , такие что ниодна вершина tr |j не покрашена в цвет iI если цвет i соответствует формуле ψUχ, тоIχ∈/ Hj+1 , χ ∈/ Hj+2 , . . .IX(ψUχ) ∈ HjIIIIIи по выбору предположений получаем tr |j+1 6|= ψUχпо определению графа ΓM,ϕ , ψUχ ∈ Hj+1по выбору предположений, tr |j+1 |= ψUχполученно противоречиеесли цвет i соответствует формуле ψRχ, то аналогичныерассуждения приводят к аналогичному противоречиюHАлгоритм model checking для LTLА насколько просто проверить наличие в графе ΓM,ϕ требуемогорадужного пути?Алгоритм model checking для LTLА насколько просто проверить наличие в графе ΓM,ϕ требуемогорадужного пути?Ориентированный граф G называется сильно связным, если длялюбых его вершин u, v существует путь из u в vАлгоритм model checking для LTLА насколько просто проверить наличие в графе ΓM,ϕ требуемогорадужного пути?Ориентированный граф G называется сильно связным, если длялюбых его вершин u, v существует путь из u в vКомпонента сильной связности графа G — это максимальныйсильно связный подграф этого графаАлгоритм model checking для LTLА насколько просто проверить наличие в графе ΓM,ϕ требуемогорадужного пути?Ориентированный граф G называется сильно связным, если длялюбых его вершин u, v существует путь из u в vКомпонента сильной связности графа G — это максимальныйсильно связный подграф этого графаКомпоненту сильной связности G системы Хинтикки ΓM,ϕ будемназывать радужной, если для каждого цвета (1, 2, .

. . , |[ϕ]UR |)существует окрашенная в него вершина GАлгоритм model checking для LTLА насколько просто проверить наличие в графе ΓM,ϕ требуемогорадужного пути?Ориентированный граф G называется сильно связным, если длялюбых его вершин u, v существует путь из u в vКомпонента сильной связности графа G — это максимальныйсильно связный подграф этого графаКомпоненту сильной связности G системы Хинтикки ΓM,ϕ будемназывать радужной, если для каждого цвета (1, 2, . . . , |[ϕ]UR |)существует окрашенная в него вершина GТеоремаВ раскрашенной системе Хинтикки ΓM,ϕ из вершины vисходит хотя бы один радужный путь⇔в ΓM,ϕ существует путь из v в какую-либо вершинукакой-либо радужной компоненты сильной связностиАлгоритм model checking для LTLА насколько просто проверить наличие в графе ΓM,ϕ требуемогорадужного пути?Ориентированный граф G называется сильно связным, если длялюбых его вершин u, v существует путь из u в vКомпонента сильной связности графа G — это максимальныйсильно связный подграф этого графаКомпоненту сильной связности G системы Хинтикки ΓM,ϕ будемназывать радужной, если для каждого цвета (1, 2, .

. . , |[ϕ]UR |)существует окрашенная в него вершина GТеоремаВ раскрашенной системе Хинтикки ΓM,ϕ из вершины vисходит хотя бы один радужный путь⇔в ΓM,ϕ существует путь из v в какую-либо вершинукакой-либо радужной компоненты сильной связностиДоказательство. Это простоАлгоритм model checking для LTLВход алгоритма: LTS M = (S, S0 , →, ρ), LTL-формула ϕВыход алгоритма: “M |= ϕ?”Описание алгоритма:I построить позитивную форму ψ, равносильную ϕI построить систему Хинтикки ΓM,ψI раскрасить систему Хинтикки (построить граф ΓM,ψ )I выделить радужные компоненты сильной связности в ΓM,ψI вычислить множество вершин V , из которых достижимахотя бы одна радужная компонента сильной связностиI выдать ответ:“содержится ли в V вершина (s, H),такая что s ∈ S0 и ψ ∈ H”Алгоритм model checking для LTLПримерϕ = pUqLTS M:'s1'- iξ(s1 ) = {p} 6&s0$s2?i$ξ(s2 ) = {q}%yξ(s0 ) = {p}'s3&- iξ(s3 ) = {p} 6&$s4?iξ(s4 ) = {p}%%Алгоритм model checking для LTLПримерϕ = pUq1.

Позитивная форма ϕ1 = pUq[ϕ1 ]FL = {p, ¬p, q, ¬q, pUq, X(pUq)}[ϕ1 ]X = {X(pUq)}[ϕ1 ]UR = {pUq}Алгоритм model checking для LTL2. Строим систему ХинтиккиGϕ1 ,M{p, ¬q}- ?is1's2's1'- i{p, ¬q,6ϕ1 , Xϕ1 }s0{p, ¬q}s0i{p, ¬q,ϕ1 , Xϕ1 }6%s2?i$${¬p, q}ϕ1 , Xϕ1 }is3&- i{p, ¬q} 6s4?i{p, ¬q}- is3%{p, ¬q}ϕ1 , Xϕ1 }&{¬p, q}iϕ1 , Xϕ1 }s4?{p, ¬q}i%Алгоритм model checking для LTL3.