Редактирование: ВПнМ, 02 лекция (от 15 февраля)

* Программа, написанная на инженерном ЯП, предназначена для того, чтобы данные обрабатывать

* Абстракция от лишних состояний

Мы хотим уменьшить пространство состояний. Что же такое состояние программы?

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

Первая задача, которую мы получим по курсу --- будет прислан текст программы на С, и нужно будет оценить число потенциальных и достижимых состояний, оценка должна быть обоснована. По этому поводу лектор просит до следующей среды написать на адрес model-checking@cs.msu.su, ФИО и группу и попросить дать порграмму. Если есть старосты групп, лектор просит прислать списки групп.

Если у всех состояний нашей системы переходов есть только один потомок, то у нас система детерминированная. Иначе недетерминированная.

Недетерминизм полезен для:

Мы наблюдае не за состоянием, а за изменением...

Чтобы посчитать достижимость, нужно отследить все фрагменты вычислений.

Последовательность разметки состояний. Мы фокусируемся на наблюдаемых свойствах системы. Свойства описываются атомарными предикатами.

=== Свойства линейного времени (СЛВ)===

Проверять мы можем свойства линейного времени. СЛВ определяет множество трасс, можно сказать, что оно принадлежит множеству трасс.

Система переходов удовлетворяет свойству линейного времени,если система трасс системы переходов включается в систему трасс свойства.

Формальное описание отношения абстракции. Трассу можно представить как интерпретацию: Множество натуральных чисел, отношение порядка и разметка кси, она для каждого порядкового номера говорит, что заданный в нём предикат истинный или ложен.

Рассмотрим две трассы, нам надо определить, что они связаны отношением абстракции. Эти две трассы имеют разные функции разметки (у одной может быть больше, у другой меньше), кроме того, состояниям могут соответствовать элементы трассы с разным номером. Будем говорить, что одна трасса является абстракцией другой, если множество наблюдаемых предикатов первой является подмножеством множества второй, сохраняются свойства частичного порядка и определено отображение и если какой-то предикат наблюдается в абстрактной трассе, то значение у него должно быть точно такое же, как и в детальной.

мы рассмотрим свойства p и q, и есть предикаты p, q, r...

Возникает вопрос, как строить системы переходов, которые генерируют трассы, которые удовлетворяют отношению абстракции.

Пусть есть система, модель, свойство ЛВ. Если свойство выполняется на модели, то оно выполняется на системе. Мы тоже переформолируем это условие как ограничение на трассы. То есть, для любой трассы, которую может сгенерировать система, существует такая, которая может сгенерировать модель такую, что она является абстракцией системы. Если свойство выполняется на всех трассах модели, то, поскольку каждой трассе системы соответствует трасса модели, то свойство выполняется на трассах системы, и система корректна. Вопрос, как такое условие проверить, поскольку оно, вообщем в соотв. с этим опр., потребует большое количество ресурсов. Давайте сформулируем достаточное условие:

Пусть у нас есть система переходов исходной программы и модели. Чем они отл.: в модели прост. сост. меньше, алфавит действий меньше, в модели другое отн. переходов, другой алфавит предикатов, соотв. поменяется разметка. Мы поменяли всё. Если абстрактно поменяяем как угодно, то всё испортится. Наложим условие, как менять: множество состояний модели (первое условие в прямоугольнике лишнее), но вот алфавит предикатов модели совершенно точно включ. в алфавит системы, .... На отобрадение накл. ограничение, что нач. сост. системы должно отобр. в нач. сост. модели. Условие на сист. переходов: (Act' ∈ Act) каждому переходу из системы переходов системы должен соответствовать переход в модели.

Есть изьян в этом условии: можно построить такую модель, что нарушим одно из свойств.

Можно назвать это условие условно правильным.

Если посмотреть расписание, то увидим разные практикумы. У СП два практикума. А у АСВК практикума Петровского нет.