2016 Экзаменационные задачи (2016 Экзаменационные задачи.docx)
Описание файла
Документ из архива "2016 Экзаменационные задачи.docx", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Онлайн просмотр документа "2016 Экзаменационные задачи"
Текст из документа "2016 Экзаменационные задачи"
Математические методы верификации схем и программ
Оглавление
Математические методы верификации схем и программ 1
Вариант 1 2
Задача 1 2
Задача 2 3
Задача 3 4
Задача 4 5
Задача 5 6
Задача 6 7
Задача 7 8
Задача 8 9
Задача 9 10
Задача 10 11
Вариант 2 12
Задача 1 12
Задача 2 13
Задача 3 14
Задача 4 15
Задача 5 16
Задача 6 17
Задача 7 18
Задача 8 19
Задача 9 20
Задача 10 21
Вариант 1
Задача 1
Докажите частичную корректность программы
относительно предусловия 
и постусловия .
Задача 2
Запишите формулу PLTL, которая адекватно соответствует следующему утверждению: «Верно хотя бы одно из двух: либо событие 
происходит почти всегда, либо сразу после каждого события 
два раза подряд случается событие ».
Задача 3
Определите, в каких состояниях модели 
выполнима формула 
Задача 4
Выбрав подходящий порядок переменных, построить ROBDD наименьшего размера для булевой функции
Задача 5
Определите, какие пары состояний модели являются бисимуляционно эквивалентными.
Задача 6
Какая формула называется инвариантом цикла?
Задача 7
Какое условие, налагаемое на пути в моделях программ, называется ограничением сильной справедливости? Зачем возникает необходимость в использовании ограничений справедливости?
Задача 8
Что называется неподвижной точкой преобразователя предикатов на множестве состояний модели программ? Докажите, что предикат 
является неподвижной точкой преобразователя предикатов 
.
Задача 9
Какое отношение между моделями Крипке называется отношением бисимуляции? Верно ли, что если две модели Крипке бисимуляционно эквивалентны, то на этих моделях выполняются одни и те же формулы логики CTL*?
Задача 10
Приведите определение понятия «временный автомат». Какое вычисление временного автомата называется вычислением Зенона?
Вариант 2
Задача 1
Докажите частичную корректность программы
относительно предусловия и постусловия .
Задача 2
Запишите формулу PLTL, которая адекватно соответствует следующему утверждению: «Верно, что если событие происходит почти всегда, то после трёх будет ».
Задача 3
Определите, в каких состояниях модели выполнима формула 
Задача 4
Выбрав подходящий порядок переменных, построить ROBDD наименьшего размера для булевой функции
Задача 5
Определите, какие пары состояний модели являются бисимуляционно эквивалентными.
Задача 6
Какое предусловие ψ называется слабейшим для функции π и условия φ.
Задача 7
Определение свойства живучести. Пример двух свойств системы, где одно – свойство живучести, а другое нет.
Задача 8
Обобщённый автомат Бюхи и какие слова он распознаёт?
Задача 9
Конус влияния и зачем он нужен?
Задача 10
Определение задачи BMC. Коэффициент сложности.
