Главная » Все файлы » Просмотр файлов из архивов » PDF-файлы » Теормин 2014 (микро) (Мадорский)

Теормин 2014 (микро) (Мадорский), страница 3

Описание файла

PDF-файл из архива "Теормин 2014 (микро) (Мадорский)", который расположен в категории "к экзамену/зачёту". Всё это находится в предмете "математическая логика и логическое программирование" из седьмого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 3 страницы из PDF

в зависимости от устройства дерева T возможен один из трех исходов:1. Успех. Дерево T конечно, и все его ветви (SLD-резолютивные вычисления) являются тупиковыми.2. Неудача. При построении (обходе) дерева T было обнаружено успешное вычисление.3. Бесконечное вычисление. Дерево T бесконечно и при его построении (обходе) не былообнаружено успешных вычислений.Интуиционистская интерпретация — это реляционная система I = <S, R, ξ>, в которой1. S ≠ ∅ — множество состояний (состояний знания);2. R ⊆ S × S — отношение переходов на S, которое является отношением нестрогого частичного порядка:1. рефлексивное R(s, s);2.

транзитивное R(s1, s2)&R (s2, s3) ⇒ R(s1, s3);3. антисимметричное R(s1, s2) & R(s2, s1) ⇒ s1 = s2;3. ξ: S × P → {true, false} — оценка атомарных формул, удовлетворяющая условию монотонности:R (s1, s2) & ξ (P , s1) = true ⇒ ξ (P , s2) = true.Формула ϕ называется интуиционистски общезначимой (законом интуиционистской логики), если для любойинтерпретации I и для любого состояния s верно I, s |=I ϕ.Теорема (корректности SLDNF-резолюции): Если запрос G: ? not(C0) к хорновской логической программе P имеетуспешное SLDNF-резолютивное вычисление, то P |=CWA ¬∃y C0.Отношение выполнимости для модальных формул: Пусть I = <W , R, ξ> — модель Крипке.Тогда отношение выполнимости I, s |= ϕ формулы ϕ в мире s модели I определяется так:1. если ϕ = P ∈ P , то I, s |= ϕ ⇐⇒ ξ (w, P) = true;2.

I, w |= ϕ1&ϕ2 ⇐⇒ I, w |= ϕ1 и I, w |= ϕ2;3. I, w |= ϕ1 ∨ ϕ2 ⇐⇒ I, w |= ϕ1 или I, w |= ϕ2;4. I, w |= ϕ1 → ϕ2 ⇐⇒ I, w |≠ ϕ1 или I, w |= ϕ2;5. I, w |= ¬ϕ1 ⇐⇒ I, w |= ϕ1;6. I, w |= □ϕ ⇐⇒ для любого альтернативного мира w' если <w, w’> ∈ R, то I, w'|= ϕ;7. I, w |= ◊ϕ ⇐⇒ существует такой альтернативный мир w', что <w, w'> ∈ R и I, w' |= ϕ.Частичным вычислением программы π0 на оценке переменных θ0 в интерпретации I называетсяпоследовательность (конечная или бесконечная) состояний вычисления <π0, θ0>, <π1, θ1>, …, <πn−1, θn−1>, <πn,θn>, …, в которой для любого n, n ≥ 1, выполняется отношение <πn−1, θn−1> →I <πn, θn>.Вычислением программы π0 на оценке переменных θ0 в интерпретации I называется всякое частичноевычисление, которое нельзя продолжить.Программа π считается (частично) корректной, если для любых начальных данных, удовлетворяющихопределенному условию ϕ, результат вычисления (если вычисление завершается) удовлетворяетопределенному условию ψ.

Определение (частичной корректности программы): Пусть ϕ, ψ — формулы логикипредикатов, а π — императивная программа. Программа π называется частично корректной в интерпретации Iотносительно предусловия ϕ и постусловия ψ, если триплет ϕ{π}ψ выполним в интерпретации I, т. е. I |= ϕ{π}ψ.Определение. Триплетом Хоара (тройкой Хоара) называется всякое выражение вида ϕ{π}ψ, где ϕ, ψ — формулылогики предикатов, а π — императивная программа. Выполнимость триплетов Хоара в интерпретацияхопределяется так: I |= ϕ{π}ψ ⇐⇒ для любых оценок переменных θ, η, если I | = ϕθ и <π, θ> →∗I <∅, η>, то I |= ψη.Интерпретация PLTL — это темпоральная модель Крипке I = <N, ≤, ξ>, где1.

N = {0, 1, 2, …} — множество моментов времени2. ≤ — отношение нестрогого линейного порядка на N3. ξ: N × AP → {true, false} — оценка атомарных высказываний на шкале времени.Темп. логика выполнения: Пусть I = <N, ≤, ξ> — темпоральная интерпретация (вычислительная трасса), n ∈ N— момент времени (состояние вычисления), ϕ — формула PLTL.Тогда отношение выполнимости I, n |= ϕ формулы ϕ в момент времени n в интерпретации I определяется так.1. Если ϕ = p, p ∈ AP (т. е. ϕ — атомарное высказывание), то I, n |= ϕ ⇐⇒ ξn(p) = true.2. Если ϕ = ϕ1&ϕ2, то I, n |= ϕ ⇐⇒ I, n |= ϕ1 и I, n |= ϕ2.3. Аналогично ϕ1 ∨ ϕ2, ϕ1 → ϕ2, ¬ϕ14. Если ϕ = Xψ, то I, n |= ϕ ⇐⇒ I, n+1 |= ψ.5.

Если ϕ = Fψ, то I, n |= ϕ ⇐⇒ существует такое k, k≥0, что I, n+k |= ψ.6. Если ϕ = Gψ, то I, n |= ϕ ⇐⇒ для любого k, k ≥ 0, верно I, n+k |= ψ.7. Если ϕ = χUψ, то I, n |= ϕ ⇐⇒ существует такое k, k ≥ 0, что I, n+k |= ψ, и для любого i, 0 ≤ i < k , верно I,n+i |= χ.8. Если ϕ = χRψ, то I, n |= ϕ ⇐⇒ либо для любого k, k ≥ 0, верно I, n+k |= ψ, либо существует такое k, k ≥ 0,что I, n+k |= χ, и для любого i, 0 ≤ i ≤ k, верно I, n+i |= ψ.Будем называть формулу PLTL ϕ1. выполнимой в интерпретации I, если верно I, 0|= ϕ (обозначается I |= ϕ);2. PLTL-общезначимой, если для любой интерпретации I верно I |= ϕ (обозначается |= ϕ).Размеченная система переходов (LTS, Labelled Transition System) — это пятерка <AP, S, S0, →, ρ>, в которой AP —множество атомарных высказываний, S — непустое множество состояний вычислений, S0, S0 ⊆ S, — непустоеподмножество начальных состояний, →⊆ S × S, — тотальное отношение переходов, тотальность отношения →означает, что для любого состояния s, s ∈ S, существует такое состояние s’, что s → s’ (т.

е. из любого состоянияможно сделать хотя бы один переход), ρ: S → 2AP — функция разметки, приписывающая каждому состояниювычислений s, s ∈ S, множество ρ(s), ρ(s) ⊆ AP, всех тех атомарных высказываний, которые являются истиннымив состоянии s.LTS для распределенной системы, состоящей из двух процессов π1 и π2, взаимодействующих посредствомразделяемых переменных, строится на основе семантики чередующихся вычислений. Состояниями LTS длясистемы π1 || π2 объявляются наборы (count1, count2, ξ1, ξ2, χ), где count1, count2 — значения счетчиков командпроцессов π1 и π2, ξ1, ξ2 — подстановки, определяющие значения локальных переменных процессов π1 и π2, χ —подстановка, определяющая значения разделяемых переменных.Задача верификации моделей программ (model checking) для PLTL формулируется так: для заданной формулыPLTL ϕ и LTS M проверить M |= ϕ.Система Хинтики: Это раскрашенный ориентированный граф, в котором вершины – это пары состояние инекоторое согласованное множество, а рёбрами в графе являются те пары, которые позволяют подтвердить всеобещания основанные на next-подформулах и выполнить их в следующий момент.Раскраска идёт по until-release-подформулам (по сути цвет означает, что именно в этой вершине произошёлперескок в правиле U или R)Алгоритм верификации моделей программ: 1) Построить равносильную позитивную формулу, 2) Построитьсистему Хинтики, 3) Выделить множество подформул until-release и раскрасить граф, 4) Выделить радужныекомпоненты сильной связности, 5)Выделить множество всех вершин графа, из которых достижимы радужныекомпоненты сильной связности, 6) Выделить множество всех вершин, которые могут быть начальными,7) Пересечь множества из 5-го и 6-го пункта..

Свежие статьи
Популярно сейчас