3. Справедливость. CTL - формализация, табличный и символьный алгоритмы. ROBDD. (1185950)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевич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.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций