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

Математические методыверификации схем и программСеминар 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.