2016 Экзаменационные задачи (2016 Экзаменационные задачи.pdf)
Описание файла
PDF-файл из архива "2016 Экзаменационные задачи.pdf", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Математические методы верификации схем и программОглавлениеМатематические методы верификации схем и программ ................................... 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Задача 2Запишите формулу PLTL, которая адекватно соответствует следующемуутверждению: «Верно хотя бы одно из двух: либо событие происходитпочти всегда, либо сразу после каждого события два раза подряд случаетсясобытие ».3Задача 3Определите, в каких( ) ( )12{}Ø4Øсостояниях5{}выполнима6{}3модели89{}Ø7{}{, }4формула10Ø12Ø11{}Задача 4Выбрав подходящий порядок переменных, построить ROBDD наименьшегоразмера для булевой функции(1 , 2 , 3 , 4 , 5 , 6 ) = (2 ⊕ 6 )˄(4 ≡ 3 )˄(1 ⊕ 5 )5Задача 5Определите, какие пары состояний модели являются бисимуляционноэквивалентными.1{, }2{}4{, }5{}3{}6{, }87{}{}69{}10{, }12{, }11{}Задача 6Какая формула называется инвариантом цикла?7Задача 7Какое условие, налагаемое на пути в моделях программ, называетсяограничением сильной справедливости? Зачем возникает необходимость виспользовании ограничений справедливости?8Задача 8Что называется неподвижной точкой преобразователя предикатов намножестве состояний модели программ? Докажите, что предикат является неподвижной точкой преобразователя предикатов () = ˄.9Задача 9Какое отношение между моделями Крипке называется отношениембисимуляции? Верно ли, что если две модели Крипке бисимуляционноэквивалентны, то на этих моделях выполняются одни и те же формулылогики CTL*?10Задача 10Приведите определение понятия «временный автомат».
Какое вычислениевременного автомата называется вычислением Зенона?11Вариант 2Задача 1Докажите частичную корректность программы < ≔ + ; ≔ − ; ≔ − < ≔ +1 ;относительно предусловия + = и постусловия + = .12Задача 2Запишите формулу PLTL, которая адекватно соответствует следующемуутверждению: «Верно, что если событие происходит почти всегда, то послетрёх будет ».13Задача 3Определите, в каких( ) ( )1{, }2{}4{, }состояниях5{}выполнима6{}3модели{, }87{}Ø14формула9{}10{, }12{, }11{}Задача 4Выбрав подходящий порядок переменных, построить ROBDD наименьшегоразмера для булевой функции(1 , 2 , 3 , 4 , 5 , 6 ) = (1 ⊕ 5 )˄(2 ≡ 3 )˄(4 ≡ 6 )15Задача 5Определите, какие пары состояний модели являются бисимуляционноэквивалентными.1{, }2{}4{, }5{}3{}6{, }87{}{, }169{}10{, }12{, }11{}Задача 6Какое предусловие ψ называется слабейшим для функции π и условия φ.17Задача 7Определение свойства живучести.
Пример двух свойств системы, где одно –свойство живучести, а другое нет.18Задача 8Обобщённый автомат Бюхи и какие слова он распознаёт?19Задача 9Конус влияния и зачем он нужен?20Задача 10Определение задачи BMC. Коэффициент сложности.21.