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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

если ϕ = 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-го пункта..

Характеристики

Список файлов ответов (шпаргалок)