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

.tr [n]tr [n + 1]tr [n + i]|= χ|= χ|= χ|= ψRχ|= ψОбоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχОбоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχПолагаем, что ψRχ ∈/ HnОбоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχПолагаем, что ψRχ ∈/ HnПусть формуле ψRχ соответствует цвет kОбоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχПолагаем, что ψRχ ∈/ HnПусть формуле ψRχ соответствует цвет kПуть tr является радужным, а значит, существует вершинаtr [n + i], окрашенная в цвет k(i ≥ 0)Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχПолагаем, что ψRχ ∈/ HnПусть формуле ψRχ соответствует цвет kПуть tr является радужным, а значит, существует вершинаtr [n + i], окрашенная в цвет k(i ≥ 0)Считаем i минимально возможным:если 0 ≤ j < i, то вершина tr [n + j] не окрашена в цвет kОбоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχПолагаем, что ψRχ ∈/ HnПусть формуле ψRχ соответствует цвет kПуть tr является радужным, а значит, существует вершинаtr [n + i], окрашенная в цвет k(i ≥ 0)Считаем i минимально возможным:если 0 ≤ j < i, то вершина tr [n + j] не окрашена в цвет kПо определению раскраски графа ΓM,ϕ ,всего возможны два случая:Случай 1: χ ∈/ Hn+iСлучай 2: X(ψRχ) ∈ Hn+iОбоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 1: χ ∈/ Hn+i¬(ψRχ)tr [n]tr [n + 1]¬X(ψRχ)¬(ψRχ) ¬χ¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 1: χ ∈/ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+j¬X(ψRχ) ¬X(ψRχ)¬(ψRχ)χχtr [n]tr [n + 1]¬X(ψRχ)¬(ψRχ) ¬χ¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 1: χ ∈/ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j < i¬X(ψRχ)¬(ψRχ)χtr [n]¬X(ψRχ)¬(ψRχ)χtr [n + 1]¬X(ψRχ)¬(ψRχ) ¬χ¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 1: χ ∈/ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j < iПо определению согласованности, ψ ∈/ Hn+j при 0 ≤ j < i¬X(ψRχ)¬(ψRχ)χ ¬ψtr [n]¬X(ψRχ)¬(ψRχ)χ¬ψtr [n + 1]¬X(ψRχ)¬(ψRχ) ¬χ¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 1: χ ∈/ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j < iПо определению согласованности, ψ ∈/ Hn+j при 0 ≤ j < iПо индуктивному предположению,tr |n+j 6|= ψ и tr |n+j |= χ при 0 ≤ j < i, а также tr |n+i 6|= χ¬X(ψRχ)¬(ψRχ)χ ¬ψtr [n]|= χ 6|= ψ¬X(ψRχ)¬(ψRχ)χ¬ψtr [n + 1]|= χ 6|= ψ¬X(ψRχ)¬(ψRχ) ¬χ¬χ...tr [n + i]6|= χ...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 1: χ ∈/ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j < iПо определению согласованности, ψ ∈/ Hn+j при 0 ≤ j < iПо индуктивному предположению,tr |n+j 6|= ψ и tr |n+j |= χ при 0 ≤ j < i, а также tr |n+i 6|= χПо определению выполнимости LTL-формул, tr |n 6|= ψRχ¬X(ψRχ) ¬X(ψRχ)¬X(ψRχ)¬(ψRχ)¬(ψRχ)¬(ψRχ) ¬χχ ¬ψχ¬ψ¬χ......tr [n]tr [n + 1]tr [n + i]|= χ 6|= ψ |= χ 6|= ψ6|= χ6|= ψRχОбоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 2: X(ψRχ) ∈ Hn+i¬(ψRχ)tr [n]tr [n + 1]¬X(ψRχ) X(ψRχ)¬(ψRχ)¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 2: X(ψRχ) ∈ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+j¬X(ψRχ) ¬X(ψRχ)¬(ψRχ)χχtr [n]tr [n + 1]¬X(ψRχ) X(ψRχ)¬(ψRχ)¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 2: X(ψRχ) ∈ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j ≤ i¬X(ψRχ)¬(ψRχ)χtr [n]¬X(ψRχ)¬(ψRχ)χtr [n + 1]¬X(ψRχ) X(ψRχ)¬(ψRχ) ¬(ψRχ)¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 2: X(ψRχ) ∈ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j ≤ iПо определению согласованности, ψ ∈/ Hn+j при 0 ≤ j < i¬X(ψRχ)¬(ψRχ)χ ¬ψtr [n]¬X(ψRχ)¬(ψRχ)χ¬ψtr [n + 1]¬X(ψRχ) X(ψRχ)¬(ψRχ) ¬(ψRχ)¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 2: X(ψRχ) ∈ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j ≤ iПо определению согласованности, ψ ∈/ Hn+j при 0 ≤ j < i,а также χ ∈/ Hn+i¬X(ψRχ)¬(ψRχ)χ ¬ψtr [n]¬X(ψRχ)¬(ψRχ)χ¬ψtr [n + 1]¬X(ψRχ) X(ψRχ)¬(ψRχ) ¬(ψRχ)¬χ¬χ...tr [n + i]...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 2: X(ψRχ) ∈ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j ≤ iПо определению согласованности, ψ ∈/ Hn+j при 0 ≤ j < i,а также χ ∈/ Hn+iПо индуктивному предположению,tr |n+j 6|= ψ и tr |n+j |= χ при 0 ≤ j < i, а также tr |n+i 6|= χ¬X(ψRχ)¬(ψRχ)χ ¬ψtr [n]|= χ 6|= ψ¬X(ψRχ)¬(ψRχ)χ¬ψtr [n + 1]|= χ 6|= ψ¬X(ψRχ) X(ψRχ)¬(ψRχ) ¬(ψRχ)¬χ¬χ...tr [n + i]6|= χ...Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈/ Hn ⇒ tr |n 6|= ψRχСлучай 2: X(ψRχ) ∈ Hn+iВершины tr [n + j] не окрашены в цвет k при 0 ≤ j < i, а значит,χ ∈ Hn+j и X(ψRχ) ∈/ Hn+jПо определению графа ΓM,ϕ , ψRχ ∈/ Hn+j при 0 ≤ j ≤ iПо определению согласованности, ψ ∈/ Hn+j при 0 ≤ j < i,а также χ ∈/ Hn+iПо индуктивному предположению,tr |n+j 6|= ψ и tr |n+j |= χ при 0 ≤ j < i, а также tr |n+i 6|= χПо определению выполнимости LTL-формул, tr |n 6|= ψRχ¬X(ψRχ) ¬X(ψRχ)¬X(ψRχ) X(ψRχ)¬(ψRχ)¬(ψRχ)¬(ψRχ) ¬(ψRχ)χ ¬ψχ¬ψ¬χ¬χ......tr [n]tr [n + 1]tr [n + i]|= χ 6|= ψ |= χ 6|= ψ6|= χ6|= ψRχОбоснование табличного метода model checking(⇐):Индуктивный переход: ψUχ ∈/ Hn ⇔ tr |n 6|= ψUχОбоснование табличного метода model checking(⇐):Индуктивный переход: ψUχ ∈/ Hn ⇔ tr |n 6|= ψUχРассуждения аналогичны случаю “ψRχ ⇔ tr |n 6|= ψRχ”Обоснование табличного метода model checking(⇐):Индуктивный переход: ψUχ ∈/ Hn ⇔ tr |n 6|= ψUχРассуждения аналогичны случаю “ψRχ ⇔ tr |n 6|= ψRχ”Попробуйте их записать самостоятельноОбоснование табличного метода model checking(⇒):Полагаем, что M 6|= ϕПокажем, что в графе ΓM,ϕ существует радужный путь,исходящий из вершины (s, H), такой что s ∈ S0 и ϕ ∈/HОбоснование табличного метода model checking(⇒):Полагаем, что M 6|= ϕПокажем, что в графе ΓM,ϕ существует радужный путь,исходящий из вершины (s, H), такой что s ∈ S0 и ϕ ∈/HПо определению графа ΓM,ϕ , в LTS M существует начальнаятрасса tr , такая что tr 6|= ϕОбоснование табличного метода model checking(⇒):Полагаем, что M 6|= ϕПокажем, что в графе ΓM,ϕ существует радужный путь,исходящий из вершины (s, H), такой что s ∈ S0 и ϕ ∈/HПо определению графа ΓM,ϕ , в LTS M существует начальнаятрасса tr , такая что tr 6|= ϕВыдвинем такие предположения:Hi = {ψ | ψ ∈ [ϕ]FL , tr |i |= ψ}Обоснование табличного метода model checking(⇒):Полагаем, что M 6|= ϕПокажем, что в графе ΓM,ϕ существует радужный путь,исходящий из вершины (s, H), такой что s ∈ S0 и ϕ ∈/HПо определению графа ΓM,ϕ , в LTS M существует начальнаятрасса tr , такая что tr 6|= ϕВыдвинем такие предположения:Hi = {ψ | ψ ∈ [ϕ]FL , tr |i |= ψ}По одному из доказанных ранее утверждений,все предположения Hi являются согласованнымиОбоснование табличного метода model checking(⇒):Полагаем, что M 6|= ϕПокажем, что в графе ΓM,ϕ существует радужный путь,исходящий из вершины (s, H), такой что s ∈ S0 и ϕ ∈/HПо определению графа ΓM,ϕ , в LTS M существует начальнаятрасса tr , такая что tr 6|= ϕВыдвинем такие предположения:Hi = {ψ | ψ ∈ [ϕ]FL , tr |i |= ψ}По одному из доказанных ранее утверждений,все предположения Hi являются согласованнымиОсталось показать, что последовательность пар(tr [1], H1 ), (tr [2], H2 ), .