3. Справедливость. CTL - формализация, табличный и символьный алгоритмы. ROBDD.
Описание файла
PDF-файл из архива "3. Справедливость. CTL - формализация, табличный и символьный алгоритмы. ROBDD.", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 11 семестр (3 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2017Семинар 3СправедливостьCTLТабличный алгоритм для CTLBDDСимвольный алгоритм для CTLУпражнение 1Какие пути приведённой ниже модели M не входят вмножество Tr (M, Fair ) для ограничений справедливостиFair = (WeakFair , StrongFair )?αγβα1. WeakFair = ∅, StrongFair = ∅;2. WeakFair = {α}, StrongFair = ∅;3. WeakFair = {α, β}, StrongFair = ∅;4. WeakFair = {α}, StrongFair = {β};5. WeakFair = ∅, StrongFair = {α, β};6. WeakFair = ∅, StrongFair = {α, β, γ};Упражнение 2Описать всевозможные условия справедливостиFair = (WeakFair , StrongFair ), для которых будет верносоотношение M, Fair |= AGFaM:γγγδγaβαУпражнение 3Записать CTL-формулу, адекватно формализующую следующеевысказывание:1. Если постоянно запрашивать вход в критическую секцию,то когда-нибудь доступ в неё будет получен2.
Между приёмом и обработкой сообщения оно никогда неудаляется3. Когда компьютер запущен, всегда есть возможность еговыключить4. Если компьютер сломался, то это навсегда5. Если когда-нибудь я захочу всё бросить, то всегда смогуэто сделать на следующий день6. Если когда-нибудь обнаружится, что я не сдал сессию, томеня обязательно вышвырнут на следующий деньУпражнение 4В каких состояниях приведённой ниже модели выполняетсязаданная CTL-формула?dac1. AGAFa2.
EFb3. AFb4. EGb5. EG¬bbУпражнение 4В каких состояниях приведённой ниже модели выполняетсязаданная CTL-формула?dac1. EXd2. AXd3. E(cU¬c)4. A(¬cUEFc)5. A(bUA(aUd))bУпражнение 5Верно ли, что для любой модели Крипке M и любогосостояния s этой модели верно следующее утверждение:если M, s |= ϕ, то M, s |= ψ ?1. ϕ = AFAGp, ψ = AFGp2. ϕ = AFGp, ψ = AFAGp3. ϕ = AFEGp, ψ = AFGp4. ϕ = AFGp, ψ = AFEGp5. ϕ = AGAFp, ψ = AGFp6. ϕ = AGFp, ψ = AGAFp7. ϕ = AGEFp, ψ = AGFp8.
ϕ = AGFp, ψ = AGEFpУпражнение 6Применив табличный алгоритм, вычислить множествосостояний заданной модели Крипке, в которых выполненазаданная CTL-формулаaa, baФормула: AG(a ∨ b)bbУпражнение 6Применив табличный алгоритм, вычислить множествосостояний заданной модели Крипке, в которых выполненазаданная CTL-формулаa, baФормула:1.
EGEXAXb2. A(EXAXbUa)bУпражнение 7Применив табличный алгоритм, вычислить множествосостояний заданной справедливой модели Крипке, в которыхвыполнена заданная CTL-формулаaa, baФормула:IAGAF(a & b)IAFAG(a → AX¬a)Ограничения справедливости:I∅bbУпражнение 7Применив табличный алгоритм, вычислить множествосостояний заданной справедливой модели Крипке, в которыхвыполнена заданная CTL-формулаaa, baФормула:IAGAF(a & b)IAFAG(a → AX¬a)Ограничения справедливости:I{{ }}I{{ }}bbУпражнение 7Применив табличный алгоритм, вычислить множествосостояний заданной справедливой модели Крипке, в которыхвыполнена заданная CTL-формулаaa, baФормула:IAGAF(a & b)IAFAG(a → AX¬a)Ограничения справедливости:}}I{{ ,I{{ } , { }}bbУпражнение 8Построить ROBDD для заданного порядка переменных,реализующую ту же функцию, что и заданная формула1.
x → y для порядков x < y и y < x2. x & y ∨ x & z ∨ y & z для порядка x < y < z3. x &(y ⊕ z) ∨ ¬x &(¬y ⊕ ¬z) для порядка x < y < z4. (x → y ) ⊕ ((y → ¬z) → x & y ) для порядков x < y < z иz <y <x5. x & x 0 ∨ y & y 0 ∨ z & z 0 для порядковx < y < z < x0 < y0 < z0 и x < x0 < y < y0 < z < z0Упражнение 9Записать дизъюнктивную нормальную форму, реализующую туже функцию, что и заданная ROBDDxy01Упражнение 9Записать дизъюнктивную нормальную форму, реализующую туже функцию, что и заданная ROBDDyzx1uyz0Упражнение 10Применить операцию к одной или двум ROBDD:x¬y01Упражнение 10Применить операцию к одной или двум ROBDD:xy01x∨y10Упражнение 10Применить операцию к одной или двум ROBDD:xxy&z0z101Упражнение 10Применить операцию к одной или двум ROBDD:xyy ←1z01Упражнение 111. Записать булевы формулы, кодирующие отношениепереходов и разметку операторов заданной модели Крипке2.
Применив символьный алгоритм, вычислить множествосостояний модели, в которых выполнена заданная формулаa, baФормула:1. EGEXAXb2. A(EXAXbUa)b.