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

Темпоральные логики

Темпоральные (временные) логики применяются для описания и исследования причинно-следственных зависимостей, развивающихся во времени. Модальный оператор □ означает «всегда», а оператор ◊ — «когда-нибудь».

2 разновидности темпоральных логик:

1. Логика линейного времени LTL

2. Логика деревьев вычислений CTL (частный случай «Логики ветвящегося времени»), использует темпоральные операторы 2-х типов: универсальные и экзистенциальные ∀□, ∀◊, ∃□, ∃◊.

Логика деревьев вычислений CTL

Пусть I = <S, R, ξ> — древесная модель Крипке для логики CTL, s₀ ∈ S — одно из состояний модели. Тогда

1. I, s₀|= ∀□ϕ ⇐⇒ в каждом состоянии s, достижимом из состояния s₀, верно I, s |= ϕ;

2. I, s₀|= ∃□ϕ ⇐⇒ существует ветвь, исходящая из состояния s₀, в каждом состоянии s которой верно I, s |= ϕ;

3. I, s₀|= ∀◊ϕ ⇐⇒ в каждой ветви, исходящей из состояния s₀, есть состояние s, в котором верно I, s |= ϕ;

4. I, s₀|= ∃◊ϕ ⇐⇒ существует ветвь, исходящая из состояния s₀, в одном из состоянии s которой верно I, s |= ϕ.

Лекция 20. Правильные программы. Императивные программы. Задача верификации программ. Логика Хоара. Автоматическая проверка правильности программ.

Описание требований правильности функционирования программы называется спецификацией программы.

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

Определение

присваивание ::= «переменная» ⇐ «терм»

условие ::= «атом» | (¬условие ) | (условие & условие ) | (условие ∨ условие )

программа ::= присваивание | программа ; программа | if «условие» then программа else программа fi | while условие do программа od

Определение (состояния вычисления)

Пусть Var — это множество переменных, а GTerm — это множество основных термов сигнатуры σ.

Оценкой переменных (состоянием данных) будем называть всякое отображение (подстановку) θ: Var → GTerm.

Состоянием управления будем называть всякую программу, а также специальный символ ∅.

Состоянием вычисления будем называть всякую пару <π, θ>, где π — состояние управления, а θ — оценка переменных.

Запись State_σ будет обозначать множество всевозможных состояний вычислений сигнатуры σ.

Определение (отношения переходов)

Пусть I — это интерпретация сигнатуры σ. Тогда отношение переходов для императивных программ — это бинарное отношение →_I на множестве состояний вычисления State_σ, удовлетворяющее следующим требованиям:

1. ASS: <x ⇒ t, θ> →_I <∅, {x/t}θ>;

2. COMP_∅: <π1; π2, θ> →_I <π2, η> тогда и только тогда, когда <π1, θ> →_I <∅, η>;

3. COMP: <π1; π2, θ> →_I <π'₁; π₂, η> тогда и только тогда, когда <π1, θ> →_I <π’₁, η> и π’₁ ≠ ∅;

Определение (отношения переходов)

1. IF_1: <if C then π₁ else π₂ fi, θ> →_I <π₁, θ> тогда и только тогда, когда I |= Cθ;

2. IF_0: <if C then π₁ else π₂ fi, θ> →_I <π₂, θ> тогда и только тогда, когда I |≠ Cθ;

3. WHILE_1: <while C do π od, θ> →_I <π; while C do π od, θ> тогда и только тогда, когда I |= Cθ;

4. WHILE_0: <while C do π od, θ> →_I <∅, θ> тогда и только тогда, когда I |≠ Cθ.

Частичным вычислением программы π₀ на оценке переменных θ₀ в интерпретации I называется последовательность (конечная или бесконечная) состояний вычисления <π₀, θ₀>, <π₁, θ₁>, …, <π_n−1, θ_n−1>, <π_n, θ_n>, …, в которой для любого n, n ≥ 1, выполняется отношение <π_n−1, θ_n−1> →_I <π_n, θ_n>.

Вычислением программы π₀ на оценке переменных θ₀ в интерпретации I называется всякое частичное вычисление, которое нельзя продолжить.

Как следует из определения, любое вычисление либо является бесконечной последовательностью, либо завершается состоянием <∅, η>. В последнем случае оценка η называется результатом вычисления.

Будем использовать запись →^∗_I для обозначения рефлексивного и транзитивного замыкания отношения переходов →_I.

Неформальная постановка задачи верификации программ.

Программа π считается (частично) корректной, если для любых начальных данных, удовлетворяющих определенному условию ϕ, результат вычисления (если вычисление завершается) удовлетворяет определенному условию ψ.

Ограничение ϕ, которое налагается на начальные данные, называется предусловием, а требование ψ, которому должны удовлетворять результаты вычисления, называется постусловием программы.

Задача верификации программы π заключается в проверке частичной корректности программы π относительно заданного предусловия ϕ и заданного постусловия ψ.

Определение. Триплетом Хоара (тройкой Хоара) называется всякое выражение вида ϕ{π}ψ, где ϕ, ψ — формулы логики предикатов, а π — императивная программа.

Обозначим HT_σ множество триплетов Хоара сигнатуры σ.

Выполнимость триплетов Хоара в интерпретациях определяется так:

I |= ϕ{π}ψ ⇐⇒ для любых оценок переменных θ, η, если I | = ϕθ и <π, θ> →^∗_I <∅, η>, то I |= ψη.

Определение (частичной корректности программы)

Пусть ϕ, ψ — формулы логики предикатов, а π — императивная программа.

Программа π называется частично корректной в интерпретации I относительно предусловия ϕ и постусловия ψ, если триплет ϕ{π}ψ выполним в интерпретации I, т. е. I |= ϕ{π}ψ.

Правила вывода Хоара

1. ASS: ϕ{x/t} {x ⇐ t} ϕ  true,

2. CONS: ϕ{π}ψ  ϕ → ϕ₀, ϕ₀{π}ψ₀, ψ₀→ ψ,

3. COMP: ϕ{π₁; π₂}ψ  ϕ{π₁}χ, χ{π₂}ψ,

4. IF: ϕ{if C then π₁ else π₂ fi}ψ  (ϕ&C){π₁}ψ, (ϕ&¬C){π₂}ψ,

5. WHILE: ϕ{while C do π od} (ϕ&¬C)  (ϕ&C){π}ϕ.

Определение вывода в логике Хоара

Вывод в логике Хоара триплета Φ₀ = ϕ₀{π₀}ψ₀ — это корневое дерево, вершинами которого служат триплеты и формулы логики предикатов и при этом

1. корнем дерева является триплет Φ₀;

2. из вершины Φ_i исходят дуги в вершину Φ_j ⇐⇒ Φ_i  Φ_j — правило табличного вывода;

3. из вершины Φ₁ исходят дуги в вершины ϕ₁ , Φ₃, ϕ₂ ⇐⇒ Φ₁ϕ1, Φ₃, ϕ₂ — правило табличного вывода;

4. листьями дерева являются формулы логики предикатов.

Вывод триплета Φ₀ = ϕ₀{π₀}ψ₀ в логике Хоара называется успешным в интерпретации I, если дерево вывода является конечным, и все его листовые вершины — это истинные в интерпретации I формулы логики предикатов.

Теорема корректности

Для любой интерпретации I и для любого правила вывода логики Хоара ΦΨ, Φϕ, ΦΨ₁,Ψ₂, Φϕ,Ψ,ψ, если I |= Ψ, I |= ϕ, , то I |=Ф

(Докажем поочереди все павила ass, cons, comp, if, while. Для ass - возьмём некоторую произвольную оценку переменных. Согласно операционной семантике императивных программ существует единственное вычисление, …)

Следствие.

Если триплет ϕ{π}ψ имеет успешный в интерпретации I вывод, то программа π частично корректна в интерпретации I относительно предусловия ϕ и постусловия ψ.

Полнота правил вывода Хоара

1. Верно ли, что для каждой интерпретации I существует система правил вывода, позволяющая для каждого триплета Φ = ϕ{π}ψ построить успешный вывод Φ в интерпретации I и доказать его успешность в случае I |= Φ?

(Нет, следует из теоремы Гёделя о неполноте)

1. Верно ли, что для каждой интерпретации I существует система правил вывода, позволяющая для каждого триплета Φ = ϕ{π}ψ построить успешный вывод Φ в интерпретации I (но не гарантирующая доказательства его успешности) в случае I |= Φ?

(Может не найтись нужных формул для применения правила Хоара cons, если базовые предикаты сигнатуры будут недостаточно выразительными)

1. Верно ли, что для некоторых интерпретаций I существует система правил вывода Хоара, которая позволяет для каждого триплета Φ = ϕ{π}ψ построить успешный вывод Φ в интерпретации I в случае I |= Φ?

(Да, достаточно чтобы для цикла существовал терм, который для любой оценки переменных был равен n+1 лишь тогда, когда цикл в вычислении совершает n итераций)

Определение

Пусть заданы интерпретация I , императивная программа π и постусловие ψ. Тогда формула ϕ₀ называется слабейшим предусловием (weakest postcondition) для программы π и постусловия ψ, если

1. I |= ϕ₀{π}ψ,

2. для любой формулы ϕ, если I |= ϕ{π}ψ, то I |= ϕ → ϕ₀.

Слабейшее предусловие для программы π и постусловия ψ условимся обозначать wpr (π, ψ).

Теорема

I |= ϕ{π}ψ ⇐⇒

Таким образом, задача построения успешного вывода сводится к задаче вычисления wpr (π, ψ).

Теорема

wpr (x ⇐ t , ψ) = ψ{x/t},

wpr (π₁; π₂, ψ) = wpr (π₁, wpr (π₂, ψ)),

wpr (if C then π₁ else π₂ fi, ψ) =C & wpr (π₁, ψ) ∨ ¬C & wpr (π₂, ψ)

Лекция 21. Верификация распределенных программ. Логика линейного времени PLTL. Размеченные системы переходов. Задача верификации моделей программ.

Такой подход к проверке правильности программ называется верификацией моделей программ (англ. model-checking).

Верификацию распределенных систем нужно автоматизировать. Это можно сделать, например, так.

1. Выбрать логический язык L, на котором можно описывать требования, предъявляемые к программе. Представить эти требования в виде формул ϕ₁, …, ϕ_n.

2. Выбрать математическую модель M, адекватно представляющую все вычисления программы. Модель должна быть устроен так, чтобы каждое вычисление I в модели M являлось интерпретацией языка L.

3. Проверить выполнимость формул ϕ₁, …, ϕ_n на всех вычислениях модели M. Для проверки выполнимости формул языка L на модели программы M должен быть разработан эффективный алгоритм.

Синтаксис PLTL

В PLTL наряду с булевыми логическими связками для описания причинно-следственной зависимости событий во времени применяются темпоральные операторы

1. X (neXttime) «в следующий момент времени»;

2. F (sometime in Future) «когда-то в будущем»;

3. G (Globally) «всегда в будущем»;

4. U (Until) «до тех пор пока»;

5. R (Release) «высвободить, открепить».

Пусть задано множество булевых переменных AP = {p₁, p₂, …, p_n, …} (будем называть их атомарными высказываниями). Формула PLTL — это

• p_i, если p_i ∈ AP

• (ϕ&ψ), (ϕ∨ψ), (ϕ→ψ), (¬ϕ) если ϕ и ψ — формулы

• (Xϕ), «в следующий момент будет верно ϕ»

• (Fϕ), «когда-то в будущем будет верно ϕ»

• (Gϕ), «всегда верно ϕ»

• (ϕUψ), «ϕ остается верной, пока не станет верной ψ»

• (ϕRψ), «ψ может перестать быть верной только после того, как станет верной ϕ».

Семантика PLTL

Интерпретация PLTL — это темпоральная модель Крипке I = <N, ≤, ξ>, где

1. N = {0, 1, 2, …} — множество моментов времени

2. ≤ — отношение нестрогого линейного порядка на N

3. ξ: N × AP → {true, false} — оценка атомарных высказываний на шкале времени.

Пусть I = <N, ≤, ξ> — темпоральная интерпретация (вычислительная трасса), n ∈ N — момент времени (состояние вычисления), ϕ — формула PLTL.

Тогда отношение выполнимости I, n |= ϕ формулы ϕ в момент времени n в интерпретации I определяется так.

1. Если ϕ = p, p ∈ AP (т. е. ϕ — атомарное высказывание), то I, n |= ϕ ⇐⇒ ξ_n(p) = true.

2. Если ϕ = ϕ₁&ϕ₂, то I, n |= ϕ ⇐⇒ I, n |= ϕ₁ и I, n |= ϕ₂.

3. Аналогично ϕ₁ ∨ ϕ₂, ϕ₁ → ϕ₂, ¬ϕ₁

4. Если ϕ = 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 |= ϕ (обозначается |= ϕ).

Законы двойственности.

1. |= ¬Xϕ ≡ X¬ϕ;

2. |= ¬Fϕ ≡ G¬ϕ;

3. |= ¬Gϕ ≡ F¬ϕ;

4. |= ¬(ϕUψ) ≡ ¬ϕR¬ψ;

5. |= ¬(ϕRψ) ≡ ¬ϕU¬ψ.

Законы взаимной зависимости.

1. |= Fϕ ≡ ¬G¬ϕ;

2. |= Gϕ ≡ ¬F¬ϕ;

3. |= ϕUψ ≡ ¬(¬ϕR¬ψ);

4. |= ϕRψ ≡ ¬(¬ϕU¬ψ);

5. |= Fϕ ≡ true Uϕ;

6. |= Gϕ ≡ false Rϕ.

Законы неподвижной точки.

1. |= Fϕ ≡ ϕ ∨ XFϕ;

2. |= Gϕ ≡ ϕ & XGϕ;

3. |= ϕUψ ≡ ψ ∨ (ϕ & X(ϕUψ);

4. |= ϕRψ ≡ ψ & (ϕ ∨ X(ϕRψ).

Определение LTS