Семинар 2. Модели Крипке. CTL_ LTL. Безопасность_ живость_ справедливость

Математические методыверификации схем и программСеминар 2Модели Крипке, CTL, LTL,Безопасность, живость,справедливостьУпражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система:cobegin p1 | | p2 coend , гдеp1:p2:x := 1 ;y := 2y := 1 ;x := 2Начальное состояние данных: x = 0, y = 0Атомарные высказывания:x = i,y =i(i ∈ Z)Упражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система:cobegin x := x + x | | x := x + x coendНачальное состояние данных: x = 1Атомарные высказывания: x = i(i ∈ Z)Упражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система:cobegin x := x + x | | x := x + x coendНачальное состояние данных: x = 1Атомарные высказывания: x = i(i ∈ Z)А если операция сложения не атомарна?Построить модель в предположении, что присваивание x := y + zреализуется как четыре неделимые команды работы с локальнымстеком программы: положить в стек значение y ; положить в стекзначение z; выбрать из стека два верхних значения, сложить иположить результат в стек; выбрать значение из стека и загрузитьв переменнуюУпражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система — схема из функциональных элементов с задержкой:x⊕∨¬ÿyАтомарные предикаты: x0 , x1 , y0 , y1 , ÿ0 , ÿ1(индекс — текущее значение переменной/задержки)Упражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система: волк, коза, капуста и лодочник в задаче о переправе1.

Лодочник переправляет мгновенно и может отдыхать наберегу сколько угодно, поедание не мгновенно2. Лодочник переправляет дольше, чем происходит поедание,и не отдыхает на берегу3. Лодочник переправляет дольше, чем происходит поедание,и может отдыхать на берегуАтомарные предикаты: волк переправлен (wr ), коза переправлена (gr ), капуста переправлена (cr ), коза жива (ga), капуста несъедена (ca)Упражнение 2Описать множество всех трасс заданной модели Крипке.aa∅a, bУпражнение 3Является ли множество P свойствома) безопасностиб) живоститрасс над непустым множеством атомарных высказываний AP?1.2.3.4.5.6.7.P = AP ωP =∅AP = {a, b, c},AP = {a, b}, PAP = {a, b}, PAP = {a, b, c},AP = {a, b}, PP = {a, b}ω= {a}∗ · {b} · {a}ω= {a, b}∗ · {a}ωP = {a, b}∗ · {c} · {a}ω= {ab}ωX ω = {w1 w2 w3 · · · | wi ∈ X }X ∗ = {w1 w2 .

. . wk | wi ∈ X , k ∈ N0 }X · Y = {wx wy | wx ∈ X , wy ∈ Y }Упражнение 4Всегда ли верны следующие утверждения?1. Если P1 и P2 — свойства безопасности, то P1 ∩ P2 —свойство безопасности2. Если P1 и P2 — свойства безопасности, то P1 ∪ P2 —свойство безопасности3. Если P1 и P2 — свойства живости, то P1 ∩ P2 — свойствоживости4. Если P1 и P2 — свойства живости, то P1 ∪ P2 — свойствоживостиУпражнение 5Записать формулу логики LTL, адекватно формализующуюследующее высказывание:1.

Кто много тренируется, тот обязательно достигнетсовершенства2. Если лифт отправился, то он обязательно остановится, и вовремя движения двери не откроются3. Два процесса никогда не займут критическую секциюодновременно4. Сообщение может быть потеряно в канале связи лишьконечное число раз5. Приём и обработка сообщения обязательно чередуются6. Операция выполняется процессором ровно 4 такта7.

Как только система сломалась, она начнёт бесконечночасто сигнализировать о неисправности, пока её питание неотключатУпражнение 6В каких состояниях приведённой ниже модели выполняетсязаданная LTL-формула?baIIIIIIIAXaAXXXaAGaAGFaAFGaAG(bUa)AF(aUb)∅a, bУпражнение 6В каких состояниях приведённой ниже модели выполняетсязаданная LTL-формула?p, qqpp, q∅IAF(XpUG¬q)p∅Упражнение 7Записать формулу логики CTL, адекватно формализующуюследующее высказывание:1. Если постоянно запрашивать вход в критическую секцию,то когда-нибудь доступ в неё будет получен2.

Между приёмом и обработкой сообщения оно никогда неудаляется3. Когда компьютер запущен, всегда есть возможность еговыключить4. Если компьютер сломался, то это навсегда5. Если когда-нибудь я захочу всё бросить, то всегда смогуэто сделать на следующий день6. Если когда-нибудь обнаружится, что я не сдал сессию, томеня обязательно вышвырнут на следующий деньУпражнение 8В каких состояниях приведённой ниже модели выполняетсязаданная CTL-формула?dac1.2.3.4.5.AGAFaEFbAFbEGbEG¬bbУпражнение 8В каких состояниях приведённой ниже модели выполняетсязаданная CTL-формула?dac1.2.3.4.5.EXdAXdE(cU¬c)A(¬cUEFc)A(bUA(aUd))bУпражнение 9Будет ли верным для любых модели M и состояния sследующее утверждение:если M, s |= ϕ, то M, s |= ψ ?1.2.3.4.5.6.7.8.ϕ = AFAGp, ψ = AFGpϕ = AFGp, ψ = AFAGpϕ = AFEGp, ψ = AFGpϕ = AFGp, ψ = AFEGpϕ = AGAFp, ψ = AGFpϕ = AGFp, ψ = AGAFpϕ = AGEFp, ψ = AGFpϕ = AGFp, ψ = AGEFpУпражнение 10Какие пути приведённой ниже модели M не входят в множествоTr (M, Fair ) для ограничений справедливостиFair = (WeakFair , StrongFair )?αγβα1.2.3.4.5.6.WeakFairWeakFairWeakFairWeakFairWeakFairWeakFair= ∅, StrongFair = ∅;= {α}, StrongFair = ∅;= {α, β}, StrongFair = ∅;= {α}, StrongFair = {β};= ∅, StrongFair = {α, β};= ∅, StrongFair = {α, β, γ};Упражнение 11Описать всевозможные условия справедливостиFair = (WeakFair , StrongFair ), для которых будет верносоотношение M, Fair |= AGFa?γ∅∅γγδγM:a∅αβ.