Презентация 18 (1131946), страница 5
Текст из файла (страница 5)
.в графе ΓM,ϕ , такой что s1 ∈ S0 и ϕ ∈/ H1По определению системы Хинтикки в LTS M существует такаяначальная трасса tr :s1 → s2 → · · · → sn → . . .Покажем индукцией по числу связок, что для любойформулы ψ ∈ [ϕ]FL и любого натурального n верноψ ∈ Hn ⇔ tr |n |= ψПроще говоря, покажем, что все предположения, сделанные длярадужного пути, действительно верныТогда достаточно будет использовать условие ϕ ∈/ H1 , чтобызаключить, что tr 6|= ϕ и M 6|= ϕОбоснование табличного метода model checking(⇐):База индукции:Первая часть: p ∈ Hn ⇔ tr |n |= pp ∈ HnВторая часть: ¬p ∈ Hn ⇔ tr |n 6|= p¬p ∈ HnОбоснование табличного метода model checking(⇐):База индукции:Первая часть: p ∈ Hn ⇔ tr |n |= pp ∈ Hn⇔определение ΓM,ϕp ∈ ρ(sn )Вторая часть: ¬p ∈ Hn ⇔ tr |n 6|= p¬p ∈ HnОбоснование табличного метода model checking(⇐):База индукции:Первая часть: p ∈ Hn ⇔ tr |n |= pp ∈ Hn⇔определение ΓM,ϕp ∈ ρ(sn )⇔определение выполнимости LTL-формулtr |n |= pВторая часть: ¬p ∈ Hn ⇔ tr |n 6|= p¬p ∈ HnОбоснование табличного метода model checking(⇐):База индукции:Первая часть: p ∈ Hn ⇔ tr |n |= pp ∈ Hn⇔определение ΓM,ϕp ∈ ρ(sn )⇔определение выполнимости LTL-формулtr |n |= pВторая часть: ¬p ∈ Hn ⇔ tr |n 6|= p¬p ∈ Hnопределение согласованности⇔p∈/ HnОбоснование табличного метода model checking(⇐):База индукции:Первая часть: p ∈ Hn ⇔ tr |n |= pp ∈ Hn⇔определение ΓM,ϕp ∈ ρ(sn )⇔определение выполнимости LTL-формулtr |n |= pВторая часть: ¬p ∈ Hn ⇔ tr |n 6|= p¬p ∈ Hnопределение согласованности⇔p∈/ Hn⇔первая часть базыtr |n 6|= pОбоснование табличного метода model checking(⇐):База индукции:Первая часть: p ∈ Hn ⇔ tr |n |= pp ∈ Hn⇔определение ΓM,ϕp ∈ ρ(sn )⇔определение выполнимости LTL-формулtr |n |= pВторая часть: ¬p ∈ Hn ⇔ tr |n 6|= p¬p ∈ Hnопределение согласованности⇔p∈/ Hn⇔первая часть базыtr |n 6|= p⇔определение выполнимости LTL-формулtr |n |= ¬pОбоснование табличного метода model checking(⇐):Индуктивный переход: ψ & χ ∈ Hn ⇔ t|n |= ψ & χψ & χ ∈ HnОбоснование табличного метода model checking(⇐):Индуктивный переход: ψ & χ ∈ Hn ⇔ t|n |= ψ & χψ & χ ∈ Hnопределение согласованности⇔ψ ∈ Hn и χ ∈ HnОбоснование табличного метода model checking(⇐):Индуктивный переход: ψ & χ ∈ Hn ⇔ t|n |= ψ & χψ & χ ∈ Hnопределение согласованности⇔ψ ∈ Hn и χ ∈ Hnиндуктивное предположение⇔tr |n |= ψ и tr |n |= χОбоснование табличного метода model checking(⇐):Индуктивный переход: ψ & χ ∈ Hn ⇔ t|n |= ψ & χψ & χ ∈ Hnопределение согласованности⇔ψ ∈ Hn и χ ∈ Hnиндуктивное предположение⇔tr |n |= ψ и tr |n |= χ⇔определение выполнимости LTL-формулtr |n |= ψ & χОбоснование табличного метода model checking(⇐):Индуктивный переход: ψ & χ ∈ Hn ⇔ t|n |= ψ & χψ & χ ∈ Hnопределение согласованности⇔ψ ∈ Hn и χ ∈ Hnиндуктивное предположение⇔tr |n |= ψ и tr |n |= χ⇔определение выполнимости LTL-формулtr |n |= ψ & χИндуктивный переход: ψ ∨ χ ∈ Hn ⇔ tr |n |= ψ ∨ χψ ∨ χ ∈ HnОбоснование табличного метода model checking(⇐):Индуктивный переход: ψ & χ ∈ Hn ⇔ t|n |= ψ & χψ & χ ∈ Hnопределение согласованности⇔ψ ∈ Hn и χ ∈ Hnиндуктивное предположение⇔tr |n |= ψ и tr |n |= χ⇔определение выполнимости LTL-формулtr |n |= ψ & χИндуктивный переход: ψ ∨ χ ∈ Hn ⇔ tr |n |= ψ ∨ χψ ∨ χ ∈ Hnопределение согласованности⇔ψ ∈ Hn или χ ∈ HnОбоснование табличного метода model checking(⇐):Индуктивный переход: ψ & χ ∈ Hn ⇔ t|n |= ψ & χψ & χ ∈ Hnопределение согласованности⇔ψ ∈ Hn и χ ∈ Hnиндуктивное предположение⇔tr |n |= ψ и tr |n |= χ⇔определение выполнимости LTL-формулtr |n |= ψ & χИндуктивный переход: ψ ∨ χ ∈ Hn ⇔ tr |n |= ψ ∨ χψ ∨ χ ∈ Hnопределение согласованности⇔ψ ∈ Hn или χ ∈ Hnиндуктивное предположение⇔tr |n |= ψ или tr |n |= χОбоснование табличного метода model checking(⇐):Индуктивный переход: ψ & χ ∈ Hn ⇔ t|n |= ψ & χψ & χ ∈ Hnопределение согласованности⇔ψ ∈ Hn и χ ∈ Hnиндуктивное предположение⇔tr |n |= ψ и tr |n |= χ⇔определение выполнимости LTL-формулtr |n |= ψ & χИндуктивный переход: ψ ∨ χ ∈ Hn ⇔ tr |n |= ψ ∨ χψ ∨ χ ∈ Hnопределение согласованности⇔ψ ∈ Hn или χ ∈ Hnиндуктивное предположение⇔tr |n |= ψ или tr |n |= χ⇔определение выполнимости LTL-формулtr |n |= ψ ∨ χОбоснование табличного метода model checking(⇐):Индуктивный переход: Xψ ∈ Hn ⇔ tr |n |= XψXψ ∈ HnОбоснование табличного метода model checking(⇐):Индуктивный переход: Xψ ∈ Hn ⇔ tr |n |= XψXψ ∈ Hn⇔определение графа ΓM,ϕψ ∈ Hn+1Обоснование табличного метода model checking(⇐):Индуктивный переход: Xψ ∈ Hn ⇔ tr |n |= XψXψ ∈ Hn⇔определение графа ΓM,ϕψ ∈ Hn+1индуктивное предположение⇔tr |n+1 |= ψОбоснование табличного метода model checking(⇐):Индуктивный переход: Xψ ∈ Hn ⇔ tr |n |= XψXψ ∈ Hn⇔определение графа ΓM,ϕψ ∈ Hn+1индуктивное предположение⇔tr |n+1 |= ψ⇔определение выполнимости LTL-формулtr |n |= XψОбоснование табличного метода model checking(⇐):Индуктивный переход: Xψ ∈ Hn ⇔ tr |n |= XψXψ ∈ Hn⇔определение графа ΓM,ϕψ ∈ Hn+1индуктивное предположение⇔tr |n+1 |= ψ⇔определение выполнимости LTL-формулtr |n |= XψИндуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχОбоснование табличного метода model checking(⇐):Индуктивный переход: Xψ ∈ Hn ⇔ tr |n |= XψXψ ∈ Hn⇔определение графа ΓM,ϕψ ∈ Hn+1индуктивное предположение⇔tr |n+1 |= ψ⇔определение выполнимости LTL-формулtr |n |= XψИндуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχПолагаем, что ψRχ ∈ HnОбоснование табличного метода model checking(⇐):Индуктивный переход: Xψ ∈ Hn ⇔ tr |n |= XψXψ ∈ Hn⇔определение графа ΓM,ϕψ ∈ Hn+1индуктивное предположение⇔tr |n+1 |= ψ⇔определение выполнимости LTL-формулtr |n |= XψИндуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχПолагаем, что ψRχ ∈ HnВсего возможны два случая:Случай 1: для любого i ≥ 0 верно X(ψRχ) ∈ Hn+iСлучай 2: существует i ≥ 0, такое что X(ψRχ) ∈/ Hn+iОбоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 1: для любого i ≥ 0 верно X(ψRχ) ∈ Hn+iX(ψRχ)ψRχX(ψRχ)tr [n]tr [n + 1]X(ψRχ)ψRχ.χ.
.X(ψRχ)tr [n + i]X(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 1: для любого i ≥ 0 верно X(ψRχ) ∈ Hn+iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+i для любого i ≥ 0X(ψRχ)ψRχX(ψRχ)ψRχtr [n]tr [n + 1]X(ψRχ)ψRχ.χ. .X(ψRχ)ψRχtr [n + i]X(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 1: для любого i ≥ 0 верно X(ψRχ) ∈ Hn+iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+i для любого i ≥ 0По определению согласованности, χ ∈ Hn+i для любого i ≥ 0X(ψRχ)ψRχχtr [n]X(ψRχ)ψRχχtr [n + 1]X(ψRχ)ψRχ.χ. .X(ψRχ)ψRχχtr [n + i]X(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 1: для любого i ≥ 0 верно X(ψRχ) ∈ Hn+iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+i для любого i ≥ 0По определению согласованности, χ ∈ Hn+i для любого i ≥ 0По индуктивному предположению, tr |n+i |= χ для любого i ≥ 0X(ψRχ)ψRχχtr [n]|= χX(ψRχ)ψRχχtr [n + 1]|= χX(ψRχ)ψRχ.χ.
.X(ψRχ)ψRχχtr [n + i]|= χX(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 1: для любого i ≥ 0 верно X(ψRχ) ∈ Hn+iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+i для любого i ≥ 0По определению согласованности, χ ∈ Hn+i для любого i ≥ 0По индуктивному предположению, tr |n+i |= χ для любого i ≥ 0По определению выполнимости LTL-формул, tr |n |= ψRχX(ψRχ)ψRχχtr [n]|= χ|= ψRχX(ψRχ)ψRχχtr [n + 1]|= χX(ψRχ)ψRχ.χ. .X(ψRχ)ψRχχtr [n + i]|= χX(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 2: существует i ≥ 0, такое что X(ψRχ) ∈ Hn+iψRχtr [n]tr [n + 1]X(ψRχ)ψRχ.χ.
.¬X(ψRχ)tr [n + i]X(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 2: существует i ≥ 0, такое что X(ψRχ) ∈ Hn+iСчитаем i минимально возможным:X(ψRχ) ∈ Hn+j для 0 ≤ j < iX(ψRχ)ψRχX(ψRχ)tr [n]tr [n + 1]X(ψRχ)ψRχ.χ. .¬X(ψRχ)tr [n + i]X(ψRχ)ψRχ.χ.
.Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 2: существует i ≥ 0, такое что X(ψRχ) ∈ Hn+iСчитаем i минимально возможным:X(ψRχ) ∈ Hn+j для 0 ≤ j < iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+j для 0 ≤ j ≤ iX(ψRχ)ψRχX(ψRχ)ψRχtr [n]tr [n + 1]X(ψRχ)ψRχ.χ. .¬X(ψRχ)ψRχtr [n + i]X(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 2: существует i ≥ 0, такое что X(ψRχ) ∈ Hn+iСчитаем i минимально возможным:X(ψRχ) ∈ Hn+j для 0 ≤ j < iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+j для 0 ≤ j ≤ iПо определению согласованности,ψ ∈ Hn+iX(ψRχ)ψRχX(ψRχ)ψRχtr [n]tr [n + 1]X(ψRχ)ψRχ.χ. .¬X(ψRχ)ψRχψtr [n + i]X(ψRχ)ψRχ.χ.
.Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 2: существует i ≥ 0, такое что X(ψRχ) ∈ Hn+iСчитаем i минимально возможным:X(ψRχ) ∈ Hn+j для 0 ≤ j < iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+j для 0 ≤ j ≤ iПо определению согласованности,ψ ∈ Hn+i и χ ∈ Hn+j для 0 ≤ j ≤ iX(ψRχ)ψRχχtr [n]X(ψRχ)ψRχχtr [n + 1]X(ψRχ)ψRχ.χ.
.¬X(ψRχ)ψRχχψtr [n + i]X(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 2: существует i ≥ 0, такое что X(ψRχ) ∈ Hn+iСчитаем i минимально возможным:X(ψRχ) ∈ Hn+j для 0 ≤ j < iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+j для 0 ≤ j ≤ iПо определению согласованности,ψ ∈ Hn+i и χ ∈ Hn+j для 0 ≤ j ≤ iПо индуктивному предположению,tr |n+i |= ψ и tr |n+j |= χ для 0 ≤ j ≤ iX(ψRχ)ψRχχtr [n]|= χX(ψRχ)ψRχχtr [n + 1]|= χX(ψRχ)ψRχ.χ.
.¬X(ψRχ)ψRχχψtr [n + i]|= χ|= ψX(ψRχ)ψRχ.χ. .Обоснование табличного метода model checking(⇐):Индуктивный переход: ψRχ ∈ Hn ⇒ tr |n |= ψRχСлучай 2: существует i ≥ 0, такое что X(ψRχ) ∈ Hn+iСчитаем i минимально возможным:X(ψRχ) ∈ Hn+j для 0 ≤ j < iПо определению графа ΓM,ϕ , ψRχ ∈ Hn+j для 0 ≤ j ≤ iПо определению согласованности,ψ ∈ Hn+i и χ ∈ Hn+j для 0 ≤ j ≤ iПо индуктивному предположению,tr |n+i |= ψ и tr |n+j |= χ для 0 ≤ j ≤ iПо определению выполнимости LTL-формул, tr |n |= ψRχX(ψRχ)X(ψRχ)X(ψRχ) ¬X(ψRχ)X(ψRχ)ψRχψRχψRχψRχψRχχχχψχ....χ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
