Семинар 3. Алгоритмы проверки CTL-формул. ROBDD (1185514)

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

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

Математические методыверификации схем и программСеминар 3Алгоритмы проверкиCTL-формул. ROBDD.Упражнение 1Применив табличный алгоритм, вычислить множествосостояний модели Крипке, в которых выполнена заданнаяCTL-формулаaa, baФормула: AG(a ∨ b)bbУпражнение 1Применив табличный алгоритм, вычислить множествосостояний модели Крипке, в которых выполнена заданнаяCTL-формулаa, baФормула:1. EGEXAXb2. A(EXAXbUa)bУпражнение 2Применив табличный алгоритм, вычислить множествосостояний справедливой модели Крипке, в которых выполненазаданная CTL-формулаaa, baФормула:I AGAF(a & b)I AFAG(a → AX¬a)Ограничения справедливости:I ∅bbУпражнение 2Применив табличный алгоритм, вычислить множествосостояний справедливой модели Крипке, в которых выполненазаданная CTL-формулаaa, baФормула:I AGAF(a & b)I AFAG(a → AX¬a)Ограничения справедливости:I {{ }}I {{ }}bbУпражнение 2Применив табличный алгоритм, вычислить множествосостояний справедливой модели Крипке, в которых выполненазаданная CTL-формулаaa, baФормула:I AGAF(a & b)I AFAG(a → AX¬a)Ограничения справедливости:I {{ ,}}I {{ } , { }}bbУпражнение 3Построить 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Упражнение 4Записать дизъюнктивную нормальную форму, реализующую туже функцию, что и заданная ROBDDxy01Упражнение 4Записать дизъюнктивную нормальную форму, реализующую туже функцию, что и заданная ROBDDyzx1uyz0Упражнение 5Применить операцию к одной или двум ROBDD:x¬y01Упражнение 5Применить операцию к одной или двум ROBDD:xy01x∨y10Упражнение 5Применить операцию к одной или двум ROBDD:xxy&z0z101Упражнение 5Применить операцию к одной или двум ROBDD:xyy ←1z01Упражнение 61.

Записать булевы формулы, кодирующие отношениепереходов и разметку операторов заданной модели Крипке2. Применив символьный алгоритм, вычислить множествосостояний модели, в которых выполнена заданная формулаa, baФормула:1. EGEXAXb2. A(EXAXbUa)b.

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

Тип файла PDF

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

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

Список файлов семинаров