Курсовая работа: дз 3. Проверка CTL. ROBDD

Сразу на всякий случай небольшой совет (т.к. я могу недооценить степень трудолюбия и упорства): если вдруг возникнет вопрос "обожемой, мне что, рисовать все *** десятков вершин?", то ответ: нет, я бы не стал давать задачку, которую не смогу проверить. Но с другой стороны, в условиях домашнего задания не сказано, что нельзя рисовать *** десятков вершин, так что это только небольшой совет.

Решение через табличный алгоритм.

Лирическое отступление:

0) прочитав подсказку, я понял, что ни в коем случае не нужно строить модель Крипке, а надо подойти какими-то другими путями

Наверное, можно будет написать программу на питоне, которая быстро построит мне модель для graphwiz, займёт не больше часа.

Но сначала - я решил поковыряться руками, пытаясь доказать невозможность как минимум первого (типо в него нельзя попасть ни из одного другого состояния), за счёт вырисовки лишь частей модели Крипке.

Решение:

1) модель Крипке построена, рисунок должен быть приложен к письму.

состояние модели Крипке - это "мультимножество" ("мульти" это важно, ибо порядок нас не волнует) из 4-х цифр, в котором отображено текущее состояние системы.

переход в модели Крипке - это обозначение числа, которое стояло на той позиции, которую мы собрались заменить.

Лирическое отступление:

Модель Крипке внезапно нарисовалась.

Окей) наверное подсказку нужно было понимать, как: "рисуйте модель, она не большая, я ведь не дал бы большую модель, ибо большую - трудно проверить".

2) записать требования в виде CTL-формул

1) В этой игре можно выиграть

aaa = [мы в 1111]

AX(EF(aaa)) = AX( E( True U aaa )) = not EX (not E ( True U aaa ))

5 = not 4

4 = EX 3

3 = not 2

2 = E ( True U 1 )

1 = aaa

2) В квадрате можно избавиться от всех единиц, не получая при этом больше одной двойки

ccc = [2-ек не больше 1]

ddd = [нету единиц]

E( ccc U ( ccc and ddd ) )

3 = E( 1 U 2 )

2 = ccc and ddd

1 = ссс

3) Если очень захотеть, то в эту игру можно сыграть так, чтобы через некоторое число раундов всегда либо иметь три двойки, либо быть способным получить три двойки за один раунд.

bbb = [3 двойки]

EF(EG(bbb or EX bbb)) = E( True U EG(bbb or EX bbb) )

4 = E ( True U 3 )

3 = EG (1 or 2)

2 = EX 1

1 = bbb

3) опишем алгоритм

см. приложенные картинки - там предикаты, как надо размечены.

1) ложь, т.е. в этой игре - нельзя выиграть

2) ложь, т.е. нельзя избавиться от всех единиц, не получая при этом больше двойки

(3-й предикат нигде не выполнен, т.к. нам нужно идти от вершин помеченных 2-кой против шерсти по вершинам с предикатом единицей, но у нас нету 2-к)

3) в исходной вершине выполняется предикат 4 => истина.

// После проверки задания, преподаватель написал:

// всё верно, кроме незамеченного пункта правил, что если есть возможность изменить числа, то мы не можем прибавлять так, чтобы числа не менялись (в терминах модели Крипке - кроме того, что все состояния оказываются без петель)

Домашнее задание 3, по желанию:

написать письмо с любым содержанием и заголовком "[Ver 2016 hw2] Фамилия И.О."

в ответ будут присланы описание системы и требований к этой системе

задача: поработать в качестве табличного или символьного алгоритма верификации CTL-формул и донести результат в любом виде

табличный алгоритм:

нарисовать модель Крипке

записать требования в виде CTL-формул

описать шаги работы алгоритма настолько (не)строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы

символьный алгоритм:

записать набор формул для модели Крипке

записать требования в виде CTL-формул

описать шаги работы алгоритма (включающее BDD, QBF или аналогичную формальную запись) настолько (не)строго, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы

Домашнее задание 4, по желанию, сложное:

этим заданием покрывается домашнее задание 3

привести описание символьного алгоритма верификации CTL-формул, работающего в условиях справедливости для CTL

можно написать псевдокод с пояснениями

можно описать на естественном языке, но так, чтобы можно было без чрезмерных усилий строго восстановить каждый шаг работы алгоритма

можно написать программу

...

привести пример работы алгоритма, иллюстрирующий его отличие от "несправедливого" символьного алгоритма