Теормин 2014 (avasite), страница 7

Размеченная система переходов (LTS, Labelled Transition System) — это пятерка <AP, S, S₀, →, ρ>, в которой

1. AP — множество атомарных высказываний

2. S — непустое множество состояний вычислений

3. S₀, S₀ ⊆ S, — непустое подмножество начальных состояний

4. →⊆ S × S, — тотальное отношение переходов, тотальность отношения → означает, что для любого состояния s, s ∈ S, существует такое состояние s’, что s → s’ (т. е. из любого состояния можно сделать хотя бы один переход)

5. ρ: S → 2^AP — функция разметки, приписывающая каждому состоянию вычислений s, s ∈ S, множество ρ(s), ρ(s) ⊆ AP, всех тех атомарных высказываний, которые являются истинными в состоянии s.

LTS и PLTL-интерпретации

Трассой в LTS M = <AP, S, S₀, →, ρ> называется всякая бесконечная последовательность состояний

tr = s_i0, s_i1, …, s_in, s_in+1, …, (∗)

в которой для любого n, n > 0, верно (s_in → s_in+1). Если s_i0 — начальное состояние, s_i0 ∈ S₀, то трасса tr называется начальной трассой.

Запись Tr(M) обозначает множество всех трасс LTS M, а запись Tr₀(M) — множество всех начальных трасс LTS M.

Каждой трассе tr ∈ Tr(M) вида (∗) сопоставим PLTL-интерпретацию I(tr) = <N, ≤, ξ>, в которой для любого n, n ≥ 0, и p, p ∈ AP, верно соотношение ξ (n, p) = true ⇐⇒ p ∈ ρ(s_in).

LTS и распределенные программы

LTS для распределенной системы, состоящей из двух процессов π₁ и π₂, взаимодействующих посредством разделяемых переменных, строится на основе семантики чередующихся вычислений. Состояниями LTS для системы π1 || π2 объявляются наборы (count₁, count₂, ξ₁, ξ₂, χ), где

1. count₁, count₂ — значения счетчиков команд процессов π₁ и π₂,

2. ξ₁, ξ₂ — подстановки, определяющие значения локальных переменных процессов π₁ и π₂,

3. χ — подстановка, определяющая значения разделяемых переменных.

Задача верификации моделей программ (model checking) для PLTL формулируется так:

для заданной формулы PLTL ϕ и LTS M проверить M |= ϕ.

Лекция 22. Задача верификации моделей программ. Подформулы Фишера-Ладнера. Табличный метод верификации моделей программ. Алгоритм верификации моделей.

Здесь должна быть лекция 22, но из-за лагов с кодировкой у меня ничего не вышло, так что сокращённый вариант – т.е. без формулировок

Задача верификации моделей программ

Утверждение 1

Для любой LTS M и формула PLTL ϕ верно, что M |≠ ϕ ⇔ существует такая начальная трасса tr, tr ∈ Tr₀(M), для которой tr |≠ ϕ.

(следует из задачи верификации моделей программ)

Утверждение 2

В результате применения равносильных преобразований этапа 1 (удаление импликации и темпоральных операторов G, F на основе законов взаимной зависимости), и преобразований этапа 2 (продвижение отрицания в глубь на основании законов двойственности) любая формула PLTL ϕ приводится равносильной формуле ϕ’, представленной в позитивной форме, в которой используются только логические связки и, или, не, и темпоряльные операторы X, F, G, а отрицание применяется только к атомарным высказываниям p ∈ AP.

Подформулы Фишера-Ладнера – FLSub_ϕ1

Их суть том, что мы вместе с самой PLTL-формулой d позитивной форме включаем ещё и большинство её подформул, на которые она разбирается и для каждого атома, являющегося атомарным высказыванием – мы включаем его отрицание, а для U и R – берём их же в следующий момент времени X, а для самого X – включаем его подформулу.

Утверждение 3

Если ϕ₁ содержит n логических связок и темпоральных операторов, то |FLSub_ϕ1| ≤ 3n

Next-подформулы

XSub_ϕ1= {ψ : ψ = Xχ, ψ ∈ FLSub_ϕ1}

(Until-Release)-подформулы

URSub_ϕ1= {ψ : ψ = χ₁Uχ₂, ψ ∈ FLSub_ϕ1} ∪ {ψ : ψ = χ₁Rχ₂, ψ ∈ FLSub_ϕ1}

Согласованное множество подформул

Это всякое подмножество множества Фишера-Ладнера FLSub_ϕ1, которое удовлетворяет условиям – true принадлежит, а false – нет, для любого высказывания выполняется лишь одно из 2-х включений – либо атом, либо его отрицание, для дизъюнкции – или то или другое, для конъюнкции – и то и другое, для U и R – по особенному.

(По сути это множества формул, которые не содержат явных противоречий, т.е. противоречий, которые можно обнаружить в текущий момент времени)

Con_ϕ1 – совокупность всех возможных согласованных множеств подформул Фишера-Ладнера

Утверждение 4.

Пусть I – произвольная темпоральная интерпретация, и ϕ₁ – произвольная формула в позитивной форме.

Тогда для любого момента времени n множество формул B_n = {ψ: ψ ∈ FLSub_ϕ1 и I, n |= ψ} является согласованным.

(Доказывается непосредственно из определения согласованного множества)

Утверждение 5

Утверждение 6

Если ϕ₁ содержит n логических связок и темпоральных операторов, то число различных согласованных множеств подформул Фишера-Ладнера не превосходит величины 2³ⁿ

Система Хинтики

Это раскрашенный ориентированный граф, в котором вершины – это пары состояние и некоторое согласованное множество, а рёбрами в графе являются те пары, которые позволяют подтвердить все обещания основанные на next-подформулах и выполнить их в следующий момент.

Раскраска идёт по until-release-подформулам (по сути цвет означает, что именно в этой вершине произошёл перескок в правиле U или R)

Бесконечный маршрут в графе называется радужным, если в нём бесконечно часто встречаются вершины каждого цвета.

Основная теорема

Для любой формулы PLTL ϕ₁ в позитивной форме и LTS M = <AP, S, S₀, ->, ρ>

M |≠ ϕ₁  в графе Г_ϕ1,M существует хотя бы один радужный маршрут, исходящий из вершины v₀ = (s₀, B₀), в которой s₀ ∈ S₀ и ϕ₁ ∉ B₀

(Доказательство через индукцию)

Ориентированный граф Г называется сильно связным, если для любой пары вершин u и v в графе Г существует маршрут в обоих направлениях.

Всякий максимальный сильно связный подграф графа Г называется компонентой сильной связности.

Компоненту сильной связности будем называть радужной, если в ней содержатся вершины всех цветов.

Теорема

Из вершины v в графе Г_ϕ1,M исходит радужный маршрут тогда и только тогда, когда существует маршрут, ведущий из вершины v хотя бы в одну из вершины хотя бы одной радужной компоненты сильной связности.

Алгоритм верификации моделей программ

1. Построить равносильную позитивную формулу

2. Построить систему Хинтики

3. Выделить множество подформул until-release и раскрасить граф

4. Выделить радужные компоненты сильной связности

5. Выделить множество всех вершин графа, из которых достижимы радужные компоненты сильной связности

6. Выделить множество всех вершин, которые могут быть начальными

7. Пересечь множества из 5-го и 6-го пункта

Лекция 23.

∈∉≠∅θ→Ψλφϕξνλρτχψωδε≡¬v∃∀⇔⇒αβµη∩□◊Qπ≤∪∩

https://ru.wikipedia.org/wiki/%D0%A2%D0%B0%D0%B1%D0%BB%D0%B8%D1%86%D0%B0_%D0%BC%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B8%D1%85_%D1%81%D0%B8%D0%BC%D0%B2%D0%BE%D0%BB%D0%BE%D0%B2