Пропозиционна динамична логика

Съдържание:

Пропозиционна динамична логика
Пропозиционна динамична логика
Anonim

Навигация за влизане

  • Съдържание за участие
  • библиография
  • Академични инструменти
  • Friends PDF Preview
  • Информация за автора и цитирането
  • Върнете се в началото

Пропозиционна динамична логика

За първи път публикувана на 1 февруари 2007 г.; съществена ревизия Fri Fri 25, 2019

Логиката на програмите е модална логика, произтичаща от идеята за свързване с всяка компютърна програма α на език на програмиране като модалност [α]. Тази идея произтича от линията на произведения на Енглер [1967], Хоаре [1969], Янов [1959] и други, които формулират и изучават логически езици, в които могат да се изразят свойствата на програмните съединители. Алгоритмичната логика (AL), разработена първо от Salwicki [1970], и динамичната логика (DL), разработена от Pratt [1976], са правилното продължение на тези работи. Тук ще се концентрираме върху DL. Многобройните доклади, посветени на DL и неговите варианти, както и многобройните му приложения в проверката на програмите и структурите от данни показват, че той представлява полезен инструмент при изучаване на свойствата на програмите. Прат избра да изобрази DL на това, което може да се нарече ниво от първи ред,и именно неговата работа задейства Фишер и Ладнър [1979], за да определи предложения вариант на DL няколко години по-късно. Тази статия представя въведение към PDL, предложения вариант на DL.

  • 1. Въведение
  • 2. Определения и основни резултати

    • 2.1 Синтаксис и семантика
    • 2.2 Аксиоматизация и пълнота
    • 2.3 Решимост и сложност
  • 3. Структурирано програмиране и коректност на програмите

    • 3.1 Изчисление на Hoare
    • 3.2 Изчисляване на Hoare и PDL
    • 3.3 Пълна коректност
  • 4. Някои варианти

    • 4.1 PDL без тестове
    • 4.2 PDL с обратна
    • 4.3 PDL с повтарящи се и циклични
    • 4.4 PDL с пресичане
  • 5. Заключение
  • библиография
  • Академични инструменти
  • Други интернет ресурси
  • Свързани записи

1. Въведение

Динамичната логика (DL) е модална логика за представяне на състоянията и събитията на динамичните системи. Езикът на DLs е едновременно език за твърдение, способен да изразява свойствата на изчислителните състояния, и език за програмиране, способен да изразява свойствата на системни преходи между тези състояния. DL-ите са логика на програмите и позволяват да се говори и да се разсъждава за състояния, процеси, промени и резултати.

Първоначалната динамична логика на програмите на Прат беше модална логика от първи ред. Пропозиционната динамична логика (PDL) е нейният предлог. Тя е представена като логика сама по себе си във Фишер и Ладнър [1979]. Бидейки предложения, езикът на PDL не използва термини, предикати или функции. Така в PDL има две синтактични категории: предложения и програми.

За да придадем смисъл на изявленията в PDL, обикновено работим с абстрактна семантика по отношение на етикетирани преходни системи (LTS). LTS могат да се разглеждат като обобщение на крипке модели, при които преходите между светове или състояния са „етикетирани“от имена на атомни програми. Оценката показва за всеки щат какви предложения са верни в него. Преход, означен с π от едно състояние x в състояние y-отбелязано x R (π) y, или (x, y) ∈ R (π) - означава, че като започнем от x, е възможно изпълнение на програмата π, която завършва през у. Ако предложението A е вярно в y, то формулата A е вярна в x: т.е. в състояние x има възможно изпълнение на програмата α, което завършва в състояние, удовлетворяващо A. Човек разпознава в модалност, напомняща модалността на възможността (често отбелязвана ◊) на модалната логика. Не е изненадващо,съществува и съответно понятие за необходимост (чиято модалност често се отбелязва □). Формулата [π] A ще бъде вярна в състояние x, ако A е вярна във всяко състояние, достижимо от x чрез преход, обозначен с π.

Възможните изпълнения на сложни програми могат да се определят композиционно. Например, програма „първо α, след това β“е сложна програма, по-точно последователност. Възможно изпълнение може да бъде представено в LTS чрез съставяне на двустепенен преход - следователно преход, който може да бъде обозначен с R (α; β) между състоянията x и x ': има възможно изпълнение в x на програмата α, която завършва в състояние y и има възможно изпълнение в y на програмата β, която завършва в x '. Ако предложението A е вярно в x ', тогава формулата A ще бъде вярна в състояние x. Програмите α и β могат сами да бъдат сложна програма. Още повече програми могат да бъдат изразени с повече конструкции, които ще представим своевременно.

След това се разглежда програма по разширен начин: тя е двоична връзка между двойки състояния на LTS. Точно това е набор от двойки от формата (x, y), така че програмата може да бъде изпълнена в състояние x и може да доведе до състояние y. От друга страна, предложението е изявление за състояние; тя е или вярна, или невярна в състояние. Следователно предложението може да се разглежда и по разширителен начин: множеството състояния на LTS, където е истина.

С PDL за съкращение тук се отнасяме точно за динамичната логика на предложенията със следните програмни конструкции: последователност, недетерминиран избор, неограничена итерация и тест. Представяме го в раздел 2, заедно с някои свойства и основни резултати. По-специално ще се спрем на неговата аксиоматизация и нейното разрешимост.

Изчислението на Hoare от Hoare [1969] е забележителност за логиката на програмите. Той се отнася до истинността на твърденията от формата {A} α {B}, което означава, че с условието A програмата α винаги има B като пост-условие и се дефинира аксиоматично. Това идва от желанието на строги методи да се разсъждава върху свойствата на програмите и по този начин се дава на дейността на програмирането определено място в сферата на науката. Бърстал [1974] вижда аналогията между модалната логика и разсъжденията за програми, но реалната работа по нея започва с Прат [1976], когато му е предложена от Р. Мур, негов ученик по това време. PDL произлиза от интерпретацията на Прат на смятането на Хоаре във формализма на модалната логика. Въведение в генезиса на PDL може да се намери в Pratt [1980b]. Hoare-тройната {A} α {B} се улавя от PDL формулата A → [α] B, което означава буквално, че ако A е вярно, то всяко успешно прекратяващо изпълнение на α ще завърши с B е вярно. При реализирането на тази връзка е рутинно да се доказват първоначалните правила за смятане на Хоаре, използвайки изключително аксиоматизацията на PDL. Това ще направим подробно в раздел 3, който се съсредоточава върху разсъжденията за правилността на структурираните програми.

Допълнителните теми, свързани с PDL, включват резултати относно сравнителната сила на изразяване, решимостта, сложността и пълнотата на редица интересни варианти, получени чрез разширяване или ограничаване на PDL по различни начини. От създаването си много варианти на PDL са получили внимание. Тези варианти могат да обмислят детерминирани програми, ограничени тестове, нередовни програми, програми като автомати, допълване и пресичане на програми, обратни и безкрайни изчисления и др. Ще представим някои от тях в раздел 4, предоставяйки някои указания относно тяхната относителна експресивност, техните аксиоматизации и изчислителната им сложност.

Заключваме в раздел 5.

2. Определения и основни резултати

Представяме синтаксиса и семантиката на PDL в раздел 2.1. Теорията на доказателствата на PDL е представена в раздел 2.2 с аксиоматизации и указатели към литературата за пълнотата. Разглеждаме проблема с разтворимостта и сложността в раздел 2.3.

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

Динамичната логика на предложенията (PDL) е предназначена за представяне и разсъждение за предложенията на свойствата на програмите. Неговият синтаксис се основава на два набора символи: счетлив набор Φ 0 от атомни формули и счетлив набор Π 0 от атомни програми. Сложните формули и сложните програми над тази база се дефинират, както следва:

  • Всяка атомна формула е формула
  • 0 ("false") е формула
  • Ако A е формула, тогава ¬ A („не A“) е формула
  • Ако A и B са формули, тогава (A ∨ B) („A или B“) е формула
  • Ако α е програма и A е формула, тогава [α] A („всяко изпълнение на α от настоящото състояние води до състояние, в което A е вярно“) е формула
  • Всяка атомна програма е програма
  • Ако α и β са програми, тогава (α; β) („направи α, последвано от β“) е програма
  • Ако α и β са програми, тогава (α∪β) („направи α или β, недетерминирано“) е програма,
  • Ако α е програма, тогава α * („повторете α краен, но недетерминиран, определен брой пъти“) е програма.
  • Ако A е формула, тогава A? („Продължете, ако A е вярно, иначе се проваля“) е програма

Останалите булеви съединители 1, ∧, → и ↔ се използват като съкращения по стандартния начин. В допълнение ние съкращаваме ¬ [α] ¬ A до A („известно изпълнение на α от настоящото състояние води до състояние, в което A е вярно“), както в модалната логика. Пишем α n за α;…; α с n събития на α. По-официално:

  • α 0 = df 1?
  • α n +1 = df α; α n

Също:

α + = df α; α *

често е полезно да представлява итерация, която не е ограничена, но се появява поне веднъж. Накрая приемаме стандартните правила за пропускане на скоби.

Формулите могат да се използват за описание на свойствата, които се държат след успешното изпълнение на програма. Например, формулата [α∪β] A означава, че когато програмата α или β се изпълни успешно, се достига състояние, при което A се държи, докато формулата A означава, че има последователност от редуващи се изпълнения на α и β, така че състояние е достигнато там, където A задържа. Семантично казано, формулите се интерпретират от множество състояния, а програмите се интерпретират от бинарни отношения над състояния в преходна система. По-точно, значението на PDL формулите и програмите се интерпретира чрез етикетирани преходни системи (LTS) M = (W, R, V), където W е непразен набор от светове или състояния, R е картографиране от множеството Π 0 на атомните програми в двоични отношения на W и V е съпоставяне от множеството Φ 0 на атомни формули в подмножества на W.

Неофициално картографирането R присвоява на всяка атомна програма π ∈ Π 0 някакво двоично отношение R (π) на W с предвидено значение x R (π) y, ако има изпълнение на π от x, което води до y, докато картографирането V присвоява на всяка атомна формула p ∈ Φ 0 някакъв подмножество V (p) от W с предвидено значение x ∈ V (p) iff p е вярно в x. Като се имат предвид нашите показания от 0, ¬ A, A ∨ B, [α] A, α; β, α∪β, α * и A?, Ясно е, че R и V трябва да се разширяват индуктивно, както следва, за да предоставят предвидените значения за сложните програми и формули:

  • x R (α; β) y ако съществува свят z такъв, че x R (α) z и z R (β) y
  • x R (α∪β) y iff x R (α) y или x R (β) y
  • x R (α *) y ако има отрицателно цяло число n и има светове z 0, …, z n такива, че z 0  = x, z n  = y и за всички k = 1.. n, z k −1 R (α) z k
  • x R (A?) y iff x = y и y ∈ V (A)
  • V (0) = ∅
  • V (¬ A) = W / V (A)
  • V (A ∨ B) = V (A) ∪ V (B),
  • V ([α] A) = {x: за всички светове y, ако x R (α) y, то y ∈ V (A)}

Ако x ∈ V (A), тогава казваме, че A е изпълнено в състояние x в M, или „M, x sat A“.

Две биподобни LTS
Две биподобни LTS

Обадете се на M LTS, изобразен по-горе вляво и M 'на LTS, изобразен вдясно. Формално дефинирано, имаме M = (W, R, V) с W = {x 1, x 2 }, R (π 1) = {(x 1, x 1)}, R (π 2) = {(x 1, x 2)}, V (p) = {x 1 }, V (q) = {x 2 } и имаме M '= (W', R ', V') с W '= {y 1, y 2, y 3, y 4 }, R (π 1) = {(y 1, y 2), (y 2, y 2)}, R '(π2) = {(y 1, y 3), (y 2, y 4)}, V '(p) = {y 1, y 2 }, V' (q) = {y 3, y 4 }. Имаме например:

  • M, x 1 sat p
  • M, x 2 sat q
  • M, x 1 sat <π 1 > p ∧ <π 2 > q
  • M, x 1 sat [π 1] p ∧ [π 1 *] p
  • M ', y 1 sat <π 1 *; π 2 > q
  • M ', y 2 sat [π 1 *] p
  • M ', y 1 sat [π 1 ππ 2] (q ∨ p)
  • M ', y 3 sat [π 1 ππ 2] 0

Сега помислете за формула А. Ние казваме, че A е валидно в M или че M е модел на A, или „M ⊨ A“, ако е за всички светове x, x ∈ V (A). Казва се, че A е валиден или "⊨ A", iff за всички модели M, M ⊨ A. Ние казваме, че A е удовлетворителен в M или че M удовлетворява A, или „M sat A“, ако съществува свят x такъв, че x ∈ V (A). Казва се, че A е удовлетворителен, или "sat A", ако съществува модел M такъв, че M sat A. Интересното е, че

sat A iff не ⊨ ¬ A

⊨ A iff not sat ¬ A

Някои забележителни формули на PDL са валидни. (Читателят може да се опита да ги докаже официално или поне да започне да се убеждава в малкото показани по-горе примери.)

⊨ [α; β] A ↔ [α] [β] A

⊨ [α∪β] A ↔ [α] A ∧ [β] A

⊨ [α *] A ↔ A ∧ [α] [α *] A

⊨ [A?] B ↔ (A → B)

Еквивалентно можем да ги запишем под тяхната двойна форма.

⊨ A ↔ A

⊨ A ↔ A ∨ A

⊨ A ↔ A ∨ A

⊨ <A?> B ↔ A ∧ B

Едно интересно понятие се отнася до количеството информация, изразено с PDL формули, която се съдържа в LTS. Поведението на система, описана като LTS, наистина често е леко скрита във формата си. Например, при обикновена проверка е лесно да се убедим, че двете LTS, изобразени по-горе, имат едно и също поведение и отговарят на едни и същи PDL формули. За да завършим този раздел относно синтаксиса и семантиката, ние даваме теоретичната основа на тези твърдения.

Като се имат предвид две LTS, човек може да попита дали отговарят на едни и същи формули. Понятието бисимулация се е превърнало в стандартна мярка за еквивалентност на крипке модели и маркирани преходни системи. Бисимулация между LTSs M = (W, R, V) и M '= (W', R ', V') е двоична връзка Z между техните състояния, така че за всички светове x в M и за всички светове x ' в M ', ако xZx' тогава

  • за всички атомни формули p ∈ Φ 0, x ∈ V (p) iff x '∈ V' (p)
  • за всички атомни програми π ∈ Π 0 и за всички светове y в M, ако x R (π) y тогава има свят y 'в M', така че yZy 'и x' R '(π) y'
  • за всички атомни програми π ∈ Π 0 и за всички светове y 'в M', ако x 'R' (π) y 'тогава има свят y в M такъв, че yZy' и x R (π) y

Казваме, че две LTS са еднакви, когато има бисимулация между тях. От началото на PDL е известно, че в два еднообразни LTSs M и M ', за всички светове x в M и за всички светове x' в M ', ако xZx', тогава за всички PDL формули A, x ∈ V (A) iff x '∈ V' (A). Следователно, когато две LTS си приличат по дефиницията на бисимулация по-горе, случаят е, че ако xZx 'тогава

  • за всички програми α и за всички светове y в M, ако x R (α) y тогава има свят y 'в M' такъв, че yZy 'и x' R '(α) y'
  • за всички програми α и за всички светове y 'в M', ако x 'R' (α) y 'тогава има свят y в M такъв, че yZy' и x R (α) y

Следователно може просто да се сравни поведението на две LTS, като се инспектират единствено атомните програми и безопасно се екстраполира сравнителното поведение на тези LTS дори за сложни програми. Ние казваме, че програмните конструкции на PDL са безопасни за бисимулация. Вижте Van Benthem [1998] за точните характеристики на програмните конструкции, които са безопасни за бисимулация.

Лесно се вижда, че двата случая на LTS по-горе са еднакви. Бисимулация Z между M и M 'може да бъде дадена като: Z = {(x 1, y 1), (x 1, y 2), (x 2, y 3), (x 2, y 4)}. Състоянията х 1 и у 1 отговарят на абсолютно същите PDL формули. Така направете състоянията х 1 и у 2 и т.н.

2.2 Аксиоматизация и пълнота

Целта на теорията на доказването е да даде характеристика на свойството ⊨ A по отношение на аксиоми и правила на извода. В този раздел ние дефинираме предикат на изводимост ⊢ индуктивно чрез операции върху формули, които зависят само от тяхната синтактична структура по такъв начин, че за всички формули A,

⊢ A iff ⊨ A.

Разбира се, PDL е продължение на класическата логика на предложенията. Първо очакваме, че всички предложения на тавтологии са предложени и всички предложения за разсъждения са позволени. По-специално, modus ponens е валидно правило: от A и A → B извежда B. За всяка програма α, ограничавайки LTS до съотношението R (α), получаваме модел на Kripke, в който логиката на модалността [α] е най-слабата предложена нормална модална логика, а именно логиката K. По този начин PDL съдържа всеки инстанция на познатата схема на аксиома на разпределение:

(A0) [α] (A → B) → ([α] A → [α] B)

и той е затворен при следното правило за извод (правило за необходимост):

(N) от A infer [α] A.

Модалната логика е нормална, ако се подчинява (A0) и (N). Важни свойства за всички α са, че [α] се разпределя върху съединението ∧ и правилото за монотонността, което позволява от A → B да извежда [α] A → [α] B, може да бъде доказано. И накрая, PDL е най-малко нормалната модална логика, съдържаща всеки екземпляр от следните аксиомни схеми

(A1) [α; β] A ↔ [α] [β] A

(A2) [α∪β] A ↔ [α] A ∧ [β] A

(A3) [α *] A ↔ A ∧ [α] [α *] A

(A4) [A?] B ↔ (A → B)

и е затворено при следното правило за извод (правило за инвариантност на цикъла):

(I) от A → [α] A извода A → [α *] A

Ако X е набор от формули и A е формула, тогава казваме, че A е u-изводима от X, или „X ⊢ A“, ако има последователност A 0, A 1,…, A n от формули, така че A n  = A и за всички i ≤ n, A i е екземпляр от схема на аксиома или формула на X, или идва от по-ранни формули на последователността чрез правило на извод. Освен това ⊢ A iff ∅ ⊢ A; в този случай казваме, че A е ded-изводим. Казва се, че X е consistent -последователен, ако не е X ⊢ 0. Лесно е да се установи, че (I) може да бъде заменен със следната аксиома (индукционна аксиома):

(A5) [α *] (A → [α] A) → (A → [α *] A)

Нека първо установим, че (I) е производно правило на системата за доказване, базирано на (A1), (A2), (A3), (A4) и (A5):

1. A → [α] A предпоставка
2. [α *] (A → [α] A) от 1 използване (N)
3. [α *] (A → [α] A) → (A → [α *] A) аксиома схема (A5)
4. A → [α *] A от 2 и 3, използвайки modus ponens

След това нека установим, че (A5) е u-изводим:

1. [α *] (A → [α] A) ↔ (A → [α] A) ∧ [α] [α *] (A → [α] A) аксиома схема (A3)
2. A ∧ [α *] (A → [α] A) → [α] (A ∧ [α *] (A → [α] A)) от 1, използвайки предложения за разсъждения и разпределение на [α] над ∧
3. A ∧ [α *] (A → [α] A) → [α *] (A ∧ [α *] (A → [α] A)) от 2 използване (I)
4. [α *] (A → [α] A) → (A → [α *] A) от 3, използвайки предложения за разсъждения и разпределение на [α *] над ∧

Аксиоматизацията на PDL на базата на аксиомни схеми (A1), (A2), (A3), (A4) и (A5) е предложена в Segerberg [1977]. От определенията по-горе е непосредствено, че ⊢ е звук по отношение на ⊨, т.е.

За всички формули A, ако ⊢ A, тогава ⊨ A

Доказателството продължава чрез индукция на дължината на A приспадане в ⊢. Въпросът за пълнотата на ⊢ по отношение на ⊨, т.е.

За всички формули A, ако ⊨ A, тогава ⊢ A

е преследван от няколко логици. Линията на разсъждения, представена в Segerberg [1977], беше първият опит за доказване на пълнотата на ⊢. Скоро Парих излезе и с доказателство. Когато в началото на 1978 г. Сегерберг намери недостатък в аргумента си (който в крайна сметка поправи), Парих публикува онова, което може да се счита за първото доказателство за пълнотата на ⊢ в Парих [1978]. Оттогава са публикувани различни доказателства за пълнотата,, например Kozen и Parikh [1981].

Потърсени са и различни алтернативни теории за доказателство на PDL. Дори в началото, особено в Прат [1978]. Тогава нека споменем и пълнотата на сродните теории на Нишимура [1979] и Вакарелов [1983].

Алтернативно формулиране на предикат за изводимост за PDL позволява използването на инфинитарно правило на извода, както например в Goldblatt [1992a]. (Инфинитариалното правило на извода отнема безкраен брой предпоставки.) Нека pred 'е изводът за изводимост, съответстващ на езика на предложената динамична логика на най-малко нормалната модална логика, съдържаща всеки екземпляр от аксиомните схеми (A1), (A2), (A3) и (A4) и е затворен при следното инфинитариално правило на извода:

(I ') от {[β] [α n] A: n ≥ 0} извеждам [β] [α *] A

Може да се докаже, че ⊢ 'е едновременно звук и завършен по отношение на ⊨, т.е.

За всички формули A, ⊢ 'A iff ⊨ A

С други думи, що се отнася до генерирането на множеството на всички валидни формули, системите за доказателство ⊢ и ⊢ 'са еквивалентни.

2.3 Решимост и сложност

Целта на теорията за сложността е да се установи изчислимостта на свойството sat A по отношение на ресурсите на времето или пространството. Сложността на логиката L често се отъждествява с проблема за решаване на удовлетворяемостта на нейните формули, дефиниран като:

(L-SAT) Имайки предвид формула А от L, удовлетворява ли се?

В този раздел изследваме сложността на следния проблем с решението:

(PDL-SAT) Предвид формула А от PDL, удовлетворява ли се?

Пълната аксиоматизация на PDL е рекурсивно дефиниране на набора от валидни PDL формули или с други думи на множеството формули, чието отрицание не е изпълнимо. Следователно, относно проблема (PDL-SAT), имаме подпроцедура, която ще отговори на „не“, ако формулата А PDL не беше удовлетворима. Подпроцедурата (SP1) се състои в изброяване на всички формули ⊢-изводими, започвайки от аксиомите и извеждайки други теореми с помощта на правилата за извод. Като се има достатъчно време, ако формула е ded-изводима, под-процедурата ще я намери в крайна сметка. Следователно, ако A не е удовлетворителен, (SP1) в крайна сметка трябва да намери ¬A и да отговори „не“, когато го прави.

Ако обаче формулата A е удовлетворима, тогава (SP1) никога няма да се намери ¬A. Тя ще работи завинаги и човек не може да бъде сигурен за това по всяко време. Но има изход от тази несигурност. Можем да помислим и за втора под-процедура, която отговаря „да“, ако формулата на PDL е удовлетворима. Всъщност един от най-ранните резултати на PDL беше доказателството, че PDL има свойството на крайния модел, т.е.

За всички формули A, ако sat A, тогава съществува краен модел M такъв, че M sat A.

Свойството на крайния модел предлага основа за под-процедура (SP2), която се състои в изброяване един по един на крайните модели на PDL и тестване дали един от тях удовлетворява формулата. (За всички формули A и за всички крайни модели M е лесно да се тества дали M sat A чрез прилагане на дефиницията на V (A).) Следователно, ако A е удовлетворителен, в крайна сметка трябва да намери модел M такъв, че M sat A и отговорете „да“, когато това е така. Симетрично на първата под-процедура (SP1), ако формулата А не е удовлетворима, тогава (SP2) никога няма да намери модел, който я удовлетворява, тя ще работи завинаги и човек не би могъл да бъде сигурен за нея по всяко време.

Сега, комбинирайки (SP1) и (SP2) заедно, имаме начин да решим дали PDL формула А е удовлетворима. Достатъчно е да ги стартирате паралелно: ако A е удовлетворителен, тогава (SP2) в крайна сметка ще отговори „да“, ако A не е удовлетворителен, тогава (SP1) в крайна сметка ще отговори „не“. Процедурата спира, когато или (SP1) или (SP2) предоставя отговор.

Ако получената процедура е достатъчна за заключение, че проблемът (PDL-SAT) е решим, той е много неефективен на практика. Има резултат, дължащ се на Фишер и Ладнер [1979] и Козен и Парих [1981] - по-силен от свойството на крайния модел, това е свойство на малък модел:

За всички формули A, ако sat A, тогава съществува краен модел M с експоненциален размер в A, такъв, че M sat A.

Това означава, че сега ще знаем кога да спрем да търсим модел, удовлетворяващ формула в процедурата (SP2). Следователно можем да използваме (SP2), за да тестваме дали дадена формула е удовлетворима, но след като сме изчерпали всички малки модели, можем да заключим, че формулата не е удовлетворима. Това води до процедура, която работи недетерминистично в експоненциално време (NEXPTIME): познайте модел на размер най-много единично експоненциален и проверете дали той отговаря на формулата. Но основните резултати в теорията за сложността на PDL идват от Фишер и Ладнър [1979] и Прат [1980a]. Като забелязват, че формула на PDL може да опише ефективно изчисляването на линейно ограничено от пространството променлива машина на Тюринг, Фишер и Ладнер [1979] първо установяват долната граница на експоненциално време на (PDL-SAT). Горната граница на EXPTIME на (PDL-SAT) е получена от Pratt [1980a],които са използвали еквивалента за PDL на метода на tableaux. По този начин (PDL-SAT) е EXPTIME-пълен. (Алгоритъм, който е по-ефективен на практика, въпреки че все още работи в детерминирано експоненциално време в най-лошия случай, е предложен в De Giacomo и Massacci [2000].)

3. Структурирано програмиране и коректност на програмите

В исторически план логиката на програмите произтича от работата в края на 60-те години на компютърни учени, които се интересуват от приписването на смисъла на езиците за програмиране и намирането на строг стандарт за доказателства за програмите. Например такива доказателства могат да се отнасят за коректността на дадена програма по отношение на очакваното поведение или за прекратяването на програма. Семинарна книга е Floyd [1967], която представя анализ на свойствата на структурираните компютърни програми, използващи блок-схеми. Някои ранни произведения като Янов [1959] или Енглер [1967] имат усъвършенствани и изучени формални езици, в които свойствата на програмните съединители могат да бъдат изразени. Формализмът на Hoare [1969] беше крайъгълен камък в появата на PDL. Той беше предложен като строга аксиоматична интерпретация на блок-схемите на Флойд. Често говорим за логиката на Хоар или логиката на Флойд-Хоар,или Hoare смятане, когато се говори за този формализъм. Изчислението на Хоаре е свързано с истинността на твърденията („тройки на Хоаре“), като {A} α {B}, която установява връзка между предварително условие A, програма α и след условие B. Той показва, че когато A е предпоставка за изпълнение на α, тогава B се запазва като условие след успешното изпълнение на α.

Това беше вярно преди няколко десетилетия и все още е така: валидирането на дадена програма е по-често, отколкото не, като се тества на разумно разнообразие от данни. Когато входът не даде очаквания резултат, „бъгът“е фиксиран. Ако в крайна сметка за всеки тестван вход получим очакваната продукция, човек има основателно убеждение, че програмата няма грешка. Това обаче е времеемък метод на валидиране и той оставя място за непроверени входни данни, които биха се провалили. Намирането на тези грешки след изпълнение на програмата и преминаване в употреба е още по-скъпо в ресурсите. Разсъждението за коректността на програмата с формалните методи е от решаващо значение за критичните системи, тъй като предлага начин да се докаже изчерпателно, че програмата няма грешки.

3.1 Изчисление на Hoare

За илюстрация на принципите на програмите, заснети от правилата в изчислението на Хоаре, е достатъчно да се консултирате с някои от тях. (Забележка: правилата означават, че ако всички изрази над реда от правилото притежават - помещенията - тогава и изявлението под реда на правилото - заключението - се задържа.)

{A} α 1 {B} {B} α 2 {C} (правило за състава)
{A} α 1; α 2 {C}

Правилото за композиция улавя елементарната последователна композиция на програмите. Като предпоставки имаме две предположения за частичната коректност на две програми α 1 и α 2. Първото предположение е, че когато α 1 се изпълни в състояние, удовлетворяващо A, то той ще завърши в състояние, удовлетворяващо B, винаги, когато спре. Второто предположение е, че когато α 2 се изпълни в състояние, удовлетворяващо B, тогава той ще завърши в състояние, удовлетворяващо С, винаги, когато спре. Заключението на правилото е за частичната коректност на програмата α 1; α 2 (т.е. α 1, последователно съставена с α 2), което следва от двете предположения. А именно, можем да заключим, че ако α 1; α 2 се изпълнява в състояние, удовлетворяващо A, то той завършва в състояние, удовлетворяващо C, винаги когато спира.

Правилото за итерация е важно, тъй като улавя основната способност на програмите да изпълняват неколкократно част от кода, докато определено условие не престане да се задържа.

{A ∧ B} α {A} (правило за итерация)
{A} докато B правим α {¬ B ∧ A}

И накрая, двете последични правила са основни, за да дадат формална основа за интуитивно ясно разсъждение, включващо съответно по-слаби условия и по-силни предпоставки.

{A} α {B} B → C (правило на следствие 1)
{A} α {C}
C → A {A} α {B} (правило на следствие 2)
{C} α {B}

От формализма, представен в Hoare [1969], ние оставяме без негови аксиомни схеми, тъй като ще изисква език от първи ред. И накрая, в следващата работа по логиката на Хоаре често се добавят и повече правила. Вижте Apt [1979] за ранен преглед.

3.2 Изчисляване на Hoare и PDL

Динамичната логика идва от интерпретацията на Прат на тройките на Хоаре и смятането на Хоар във формализма на модалната логика. С модалността [α] можем да изразим формално, че всички състояния, достъпни чрез изпълнение на α, отговарят на формулата A. Това става чрез писане на [α] A. По този начин, тройната Hoare {A} α {B} е просто уловена от PDL формулата

A → [α] B

В допълнение, важните програмни конструкции лесно се въвеждат в PDL чрез определено съкращение:

  • ако A тогава α else β = df ((A?; α) ∪ (¬ A?; β))
  • докато A do α = df ((A?; α) *; ¬ A?)
  • повтаряйте α, докато A = df (α; ((¬ A; α) *; A?))
  • аборт = df 0?
  • пропуснете = df 1?

По този начин изглежда, че с PDL ние сме добре подготвени да докажем логичността на структурираните програми. Отвъд тази по-скоро махаща ръка връзка между PDL и Hoare смятане, може би все още не е ясно как те се отнасят официално. PDL всъщност е обобщение на изчислението на Hoare в смисъл, че всички правила на изчислението на Hoare могат да бъдат доказани в аксиоматичната система на PDL. (Строго, смятането на Хоаре съдържа аксиоми, които биха изисквали разширения език на първокласна динамична логика.) Това е доста забележително, така че тук ще покажем двете горни правила, които да служат като примери.

Доказателствата започват с приемането на предпоставките на правилата. След това, използвайки тези предположения, аксиоми и правила на PDL и нищо друго, целта е да се установи, че заключението на правилата логично следва. Следователно, за правилото на състава, започваме с приемането на {A} α 1 {B}, това е A → [α 1] B в неговата PDL формулировка, и като приемаме {B} α 2 {C}, това е B → [α 2] С. Целта е да се докаже, че {A} α 1; α 2 {C}. Точно искаме да установим, че A → [α 1; α 2] C е ⊢-изводим от множеството формули {A → [α 1] B, B → [α 2] C}.

1. A → [α 1] B предположение {A} α 1 {B}
2. B → [α 2] C предположение {B} α 2 {C}
3. 1] B → [α 1] [α 2] C От 2, използващи монотонността на [α 1]
4. A → [α 1] [α 2] C от 1 и 3, като се използват предложения за разсъждения
5. 1; α 2] C ↔ [α 1] [α 2] C аксиома схема (A1)
6. A → [α 1; α 2] С от 4 и 5, използвайки предложения за разсъждения
- {A} α 1; α 2 {C}

Доказателството за правилото на итерацията е малко по-ангажирано.

1. A ∧ B → [α] A предположение {A ∧ B} α {A}
2. A → (B → [α] A) от 1, използвайки предложения за разсъждения
3. [B?] [Α] A ↔ (B → [α] A) схема на аксиома (A4)
4. A → [B?] [Α] A от 2 и 3, използвайки предложения за разсъждения
5. [B?; α] A ↔ [B?] [α] A аксиома схема (A1)
6. A → [B?; Α] A от 4 и 5, използвайки предложения за разсъждения
7. A → [(B?; Α) *] A от 6 използване (I)
8. A → (¬ B → (¬ B ∧ A)) предложенията тавтология
9. A → [(B?; Α) *] (¬ B → (¬ B ∧ A)) от 7 и 8, използвайки монотонността на [(B?; α) *] и предложения за разсъждения
10. [¬ B?] (¬ B ∧ A) ↔ (¬ B → (¬ B ∧ A)) Схема на аксиома (A4)
11. A → [(B?; Α) *] [¬ B?] (¬ B ∧ A) от 9 и 10, използвайки монотонността на [(B?; α) *] и предложения за разсъждения
12. [(B?; Α) *; ¬ B?] (¬ B ∧ A) ↔ [(B?; Α) *] [¬ B?] (¬ B ∧ A) аксиома схема (A1)
13. A → [(B?; Α) *; ¬ B?] (¬ B ∧ A) от 12, използвайки предложения за разсъждения
- {A} докато B правим α {¬ B ∧ A}

В контекста на PDL, двете последични правила всъщност са специални случаи на правилото за състав. За да получите първото правило, заменете α 1 с α и α 2 с pres pres. За да получите второто правило, заменете α 1 с пропускане и α 2 с α. Достатъчно е да приложим схемата за аксиома (A4) и да отбележим, че [α; пропуснете] A ↔ [α] A и [α; пропуснете] A ↔ [α] A също са ⊢-изводими за всички A и всички α.

3.3 Пълна коректност

По собствено признание на Hoare в Hoare [1979], първоначалният му анализ е бил просто отправна точка и е претърпял доста ограничения. По-специално, той позволява само да се разсъждава за частична коректност. Тоест, истинността на едно твърдение {A} α {B} само гарантира, че всички изпълнения на α, започващи в състояние, удовлетворяващо A, ще завършат в състояние, удовлетворяващо B, или няма да спрат. Тоест, частично правилната програма може да има незавършени изпълнения. (Всъщност програма, която няма прекратяващо изпълнение, винаги ще бъде частично правилна. Такъв е например случаят с програмата, докато 1 пропуснете. Формулата A → [ докато 1 пропуснете] B е изводим за всички формули A и B.) Изчислението не предлага основа за доказателство, че дадена програма се прекратява. Тя може да бъде модифицирана така, че да отчита пълната коректност на програмите: частична коректност плюс прекратяване. Постига се чрез изменение на правилото за итерация. Ние не го представяме тук и насочваме заинтересования читател към Apt [1981].

Нека първо да отбележим, че за детерминираните програми вече може да се улови пълна коректност чрез формули от този вид

A → B

Изразът B означава, че има изпълнение на α, което завършва в състояние, което удовлетворява B. Освен това, ако α е детерминистично, това възможно прекратяващо изпълнение е уникалното изпълнение на α. По този начин, ако човек първо успее да докаже, че дадена програма е детерминирана, този трик работи достатъчно добре, за да докаже пълната си коректност.

В сферата на PDL съществува общо решение на проблема за пълната коректност. Но трябва да го разширим малко. Прат вече спомена в Pratt [1980b], че PDL не е достатъчно изразителен, за да улови безкрайното циклиране на програмите. В реакция, Streett [1982] се въвежда PDL с повторение (RPDL). Той съдържа за всички програми α изразът Δα, представляващ ново предложение със семантика

V (Δα) = {x: съществува безкрайна последователност x 0, x 1,… на състояния, такива, че x 0  = x и за всички n ≥ 0, x n R (α) x n +1 }

Streett [1982] предположи, че RPDL може да бъде аксиоматизиран, като добави към доказателствената система на PDL точно следните аксиомни схеми.

(A6) Δα → Δα

(A7) [α *] (A → A) → (A → Δα)

Доказателството за предположението е предоставено в Сакалаускайте и Валиев [1990]. (Версия на предположението във варианта на комбинативно PDL е доказана и в Гаргов и Паси [1988].)

Лесно е да се види, че в изчислението на Хоаре, представено по-горе, не прекратяването може да произтича само от правилото за повторение. Аналогично, не прекратяването на PDL програма може да дойде само от използването на неограничената итерация. Изразът Δα показва, че α * може да се разминава и това е само вида на понятието, от което се нуждаем. Вече можем да определим индуктивно предикат ∞, така че за програма α, формулата ∞ (α) ще бъде вярна точно, когато α може да въведе изчисление без край.

∞ (π): = 0, където π ∈ Π 0

∞ (φ?): = 0

∞ (α ∪ β): = ∞ (α) ∨ ∞ (β)

∞ (α; β): = ∞ (α) ∨ ∞ (β)

∞ (α *): = Δα ∨ ∞ (α)

И накрая, пълната коректност на дадена програма може да бъде изразена чрез подобни формули

A → (¬∞ (α) ∧ [α] B)

което означава буквално, че ако A е така, програмата α не може да работи вечно и всяко успешно изпълнение ще завърши в състояние, удовлетворяващо B.

4. Някои варианти

Резултатите относно сравнителната сила на изразяване, решимостта, сложността, аксиоматизацията и пълнотата на редица варианти на PDL, получени чрез разширяване или ограничаване на неговия синтаксис и неговата семантика, са обект на богата литература. Можем да кажем само толкова много и ще се спрем само на няколко от тези варианти, оставяйки големи парчета от иначе важната работа в динамичната логика.

4.1 PDL без тестове

Схемата на аксиомата [A?] B ↔ (A → B) изглежда показва, че за всяка формула C съществува еквивалентна формула без тест C '-ее, има формула без тест C' такава, че ⊨ C ↔ ° С '. Интересно е да се наблюдава, че това твърдение е невярно. Нека PDL 0 е ограничението на PDL за редовни програми без тестове, т.е. програми, които не съдържат тестове. Berman и Paterson [1981] разглеждат PDL формулата <(p?; Π) *; ¬ p?; Π; p?> 1, което е

< докато p do π> p

и доказа, че няма PDL 0 формула, еквивалентна на нея. Следователно PDL има по-изразителна сила от PDL 0. Техният аргумент всъщност може да се обобщи по следния начин. За всички n ≥ 0, PDL n +1 е подмножеството на PDL, в които програмите могат да съдържат тестове A? само ако A е PDL n формула. За всички n ≥ 0, Берман и Патерсън считат PDL n +1 формула A n +1, дефинирана от

< докато A n do π n > <π n > A n

където A 0  = p и π 0  = π и доказа, че за всички n ≥ 0, няма PDL n формула, еквивалентна на A n +1. Следователно, за всички n ≥ 0, PDL n +1 има по-изразителна сила от PDL n.

4.2 PDL с обратна

CPDL е разширението на PDL с обратна. Това е конструкция, която се разглежда от началото на PDL. За всички програми α, нека α -1 стои за нова програма със семантика

x R (α -1) y iff y R (α) x.

Обратната конструкция ни позволява да изразим факти за състояния, предхождащи текущото и да разсъждаваме назад за програмите. Например, [α -1] A означава, че преди да изпълни α, A трябваше да задържи. Ние имаме

⊨ A → [α] <α -1 > A, ⊨ A → [α -1] A.

Добавянето на обратната конструкция не променя свойствата на PDL по някакъв съществен начин. Чрез добавяне на всеки екземпляр от следните аксиомни схеми:

(A8) A → [α] <α -1 > A

(A9) A → [α -1] A

към системата за доказване на PDL получаваме звуков и пълен изводим предикат на разширения език. Вижте Parikh [1978] за подробности. CPDL има свойството на малкия модел и (CPDL-SAT) е завършен EXPTIME.

Лесно е да се отбележи, че CPDL има по-изразителна сила от PDL. За да видите това, помислете за формулата CPDL <π -1 > 1 и LTSs M = (W, R, V) и M '= (W', R ', V'), където W = {x, y}, R (π) = {(x, y)}, W '= {y'}, R '(π) = ∅ и V (x) = V (y) = V' (y ') = ∅. Тъй като M, y sat <π -1 > 1, а не M ', y' sat <π -1 > 1, и тъй като за всички PDL формули A е така, че M, y sat A iff M ', y' sat А, тогава е ясно, че нито една PDL формула не е еквивалентна на <π -1 > 1.

4.3 PDL с повтарящи се и циклични

Вече изложихме силата на повторение в раздел 3.3, като въведем RPDL. Тук обобщаваме повече резултати относно RPDL и връзката му с други вариации на понятието повтарящи се програми.

По отношение на теорията за сложността на RPDL, Streett [1982] вече беше установил, че RPDL има свойството на крайния модел; точно, че всяка изпълнена с RPDL формула A е изпълнима в модел с размер най-много три пъти експоненциален по дължината на A. Автоматично-теоретичен аргумент, позволяващ да се заключи, че проблемът (RPDL-SAT) може да бъде решен в детерминирано тройно експоненциално време (3-EXPTIME). Следователно пропастта между тази горна граница за вземане на решение (RPDL-SAT) и простата долна граница на експоненциално време за вземане на решение (PDL-SAT) беше отворена. Проблемът се оказа силно свързан с нарастващия интерес на компютърните учени към установяването на сложността на времевата логика и по-точно на (предложеното) модално μ-смятане (MMC) поради Козен [1983], тъй като RPDL има линеен удар- нагоре превод до MMC. Освен това,Аргументът на Стрийт донякъде поставя прецедент в широко разпространеното използване на автоматични техники за доказване на изчислителни свойства на логиката на програмите и на временната логика. Във Vardi и Stockmeyer [1985] е показана горна граница в недетерминирано експоненциално време. В Emerson и Jutla [1988] и в окончателната му форма в Emerson и Jutla [1999] е показано, че (MMC-SAT) и (RPDL-SAT) са EXPTIME-пълни. Ако добавим и обратния оператор от раздел 4.2, един получава CRPDL. Сложността на (CRPDL-SAT) остава отворена за няколко години, но може да се окаже, че е и EXPTIME-пълна. Това се постига чрез комбиниране на техниките на Emerson и Jutla [1988] и Vardi [1985], както във Vardi [1998]. Във Vardi и Stockmeyer [1985] е показана горна граница в недетерминирано експоненциално време. В Emerson и Jutla [1988] и в окончателната му форма в Emerson и Jutla [1999] е показано, че (MMC-SAT) и (RPDL-SAT) са EXPTIME-пълни. Ако добавим и обратния оператор от раздел 4.2, един получава CRPDL. Сложността на (CRPDL-SAT) остава отворена за няколко години, но може да се окаже, че е и EXPTIME-пълна. Това се постига чрез комбиниране на техниките на Emerson и Jutla [1988] и Vardi [1985], както във Vardi [1998]. Във Vardi и Stockmeyer [1985] е показана горна граница в недетерминирано експоненциално време. В Emerson и Jutla [1988] и в окончателната му форма в Emerson и Jutla [1999] е показано, че (MMC-SAT) и (RPDL-SAT) са EXPTIME-пълни. Ако добавим и обратния оператор от раздел 4.2, един получава CRPDL. Сложността на (CRPDL-SAT) остава отворена за няколко години, но може да се окаже, че е и EXPTIME-пълна. Това се постига чрез комбиниране на техниките на Emerson и Jutla [1988] и Vardi [1985], както във Vardi [1998]. Сложността на (CRPDL-SAT) остава отворена за няколко години, но може да се окаже, че е и EXPTIME-пълна. Това се постига чрез комбиниране на техниките на Emerson и Jutla [1988] и Vardi [1985], както във Vardi [1998]. Сложността на (CRPDL-SAT) остава отворена за няколко години, но може да се окаже, че е и EXPTIME-пълна. Това се постига чрез комбиниране на техниките на Emerson и Jutla [1988] и Vardi [1985], както във Vardi [1998].

В раздел 3.3 ние сме дефинирали предикат ∞, където ∞ (α) означава, че α може да има неспиращи изчисления. Наричаме LPDL логиката, получена чрез увеличаване на PDL с предиката ∞. Ясно е, че RPDL е поне толкова изразителен, колкото LPDL; Индуктивното определение на ∞ (α) в езика на RPDL е свидетелство за това. RPDL всъщност е строго по-изразителен от LPDL. Това е показано в Харел и Шерман [1982]. Както може да се подозира, и RPDL, и LPDL имат по-изразителна сила от PDL. Установява се чрез доказване, че някои формули на RPDL и на LPDL нямат еквивалентен израз в PDL. Доказателството включва техниката на филтриране, която е предназначена да срине LTS до ограничен модел, като същевременно оставя инвариантна истинността или лъжливостта на определени формули. За някои набор от PDL формули X,тя се състои в групиране в класове на еквивалентност състоянията на LTS, които отговарят на абсолютно същите формули в X. Така полученият набор от класове на еквивалентност на състояния се превръща в множеството състояния на филтратния модел и над тях е изграден подходящ преход.

С внимателно подбран набор FL (A), който зависи от PDL формула A (така нареченото затваряне на Фишер-Ладнер на множеството под-формули на A), филтрирането на LTS M води до финален филтрат M ', такъв че A е удовлетворителен в свят u в M, ако и само ако е удовлетворителен в класа на еквивалентност, съдържащ u във филтрата. (Виж Фишер и Ладнър [1979].)

Вече можем да разгледаме филтрациите на LTS M = (W, R, V) където

  • W = {(i, j): j и i положителни числа, 0 ≤ j ≤ i} ∪ {u}
  • (i, j) R (π) (i, j -1), когато 1 ≤ j ≤ i
  • u R (π) (i, i) за всяко i
  • V (p) = ∅ за всяко p ∈ Φ 0

В едно изречение това, което се случва в M, е, че от света u, има безкраен брой крайни π-пътеки с нарастваща дължина. Имаме и M, u sat ¬Δπ и M, u sat ¬∞ (π *). И все пак, за всяка PDL формула A, ще имаме както Δπ, така и ∞ (π *), които са удовлетворени при класа на еквивалентност на u в модела, получен чрез филтриране на M с FL (A). Всъщност филтрацията трябва да срине някои състояния на М и да създаде някои бримки. По този начин не съществува PDL формула, която да изразява или Δπ, или ∞ (π *). и все пак, ще имаме както Δπ, така и ∞ (π *), които са удовлетворени в класа на еквивалентност на u във всеки краен филтрат на M. По този начин, нито Δπ, нито ∞ (π *) не могат да бъдат изразени в PDL.

Има и други начини да се направи твърдението, че една програма може да се изпълнява завинаги. Например, Danecki [1984a] предложи предсказателен склоп, за да отговаря на програмите, които могат да влизат в силни контури, т.е.

V (наклон (α)) = {x: x R (α) x}

Нека да наречем SLPDL логиката, получена чрез увеличаване на PDL с наклон (α). RPDL и SLPDL по същество са несравнимо: предикатното делта не е определима в SLPDL и предикат писта разположени не е определима в RPDL. SLPDL не притежава свойството на крайния модел. Например формулата

[π *] (1 ∧ ¬ наклон+))

е удовлетворителен само в безкрайните LTS. Независимо от това, Danecki [1984a] установява определяемостта на (SLPDL-SAT) формулите в детерминирано експоненциално време.

4.4 PDL с пресичане

Изследвана е друга конструкция: пресечната точка на програмите. Чрез добавяне на пресичане на програми към PDL получаваме логическия IPDL. В IPDL, за всички програми α, β, изразът α∩β означава нова програма със семантика

x R (α∩β) y iff x R (α) y и x R (β) y

Например, предвиденото четене на A е, че ако изпълним α и β в сегашното състояние, тогава съществува състояние, достъпно от двете програми, което удовлетворява A. В резултат имаме

→ A → A ∧ A

но като цяло имаме

не ⊨ A ∧ A → A

Въпреки че пресичането на програми играе важна роля в различни приложения на PDL към изкуствения интелект и компютърните науки, теорията на доказателствата и теорията на сложността на PDL с пресичане останаха неизследвани няколко години. Относно теорията за сложността на IPDL се появяват трудности, когато човек разгледа свойството на крайния модел. В действителност, конструктовият склоп (α) може да се изрази в IPDL. При динамичната логика на предложенията с пресичане тя е еквивалентна на 1. По този начин можем да адаптираме формулата на IPDL от раздел 4.3 и имаме това

[π *] (1 ∧ [π + ∩1?] 0)

е удовлетворителен само в безкрайните LTS. С други думи, IPDL не притежава свойството на крайния модел. Danecki [1984b] изследва теорията за сложността на IPDL и показва, че решаването (IPDL-SAT) може да се извърши в детерминирано двойно експоненциално време. (Съвременно доказателство е представено в Göller, Lohrey и Lutz [2007].) Разликата в сложността между тази двойна горна граница на експоненциално време за вземане на решение (IPDL-SAT) и простата долна граница на експоненциално време за вземане на решение (PDL-SAT) получена от Фишер и Ладнър [1979] остава отворена повече от двадесет години. През 2004 г. Ланге [2005] установи долната граница на експоненциалното пространство на (IPDL-SAT). През 2006г. Lange и Lutz [2005] дадоха доказателство за двойна долна граница на експоненциално време на задачата за удовлетворяемост за IPDL без тестове чрез намаление от словния проблем на редуващи се в експоненциално редуващи се машини на Тюринг. При това намаление ролята на итерационната конструкция е от съществено значение, тъй като според Massacci [2001], проблемът за удовлетворяемостта на без итерация IPDL без тестове е само PSPACE-пълен. Добавяйки обратната конструкция към IPDL, получаваме ICPDL. Доказано е, че проблемът на удовлетворяемостта на ICPDL е 2-EXPTIME-завършен от Göller, Lohrey и Lutz [2007]. Доказано е, че проблемът на удовлетворяемостта на ICPDL е 2-EXPTIME-завършен от Göller, Lohrey и Lutz [2007]. Доказано е, че проблемът на удовлетворяемостта на ICPDL е 2-EXPTIME-завършен от Göller, Lohrey и Lutz [2007].

Относно теорията на доказателствата за IPDL възникват трудности, когато осъзнаем, че никоя схема на аксиома на езика на PDL със пресичане „не съответства“на семантиката x R (α∩β) y iff x R (α) y и x R (β) y на програмата α∩β. Тоест, не по същия начин, например, че аксиомните схеми (А1) и (А2) съответно „съответстват“на семантиката на програмите α; β и α∪β. Поради тази причина аксиоматизацията на PDL с пресичане е отворена до пълната система за доказване, разработена в Balbiani и Vakarelov [2003].

В друг вариант на PDL, поради Peleg [1987] и по-нататъшно проучен от Goldblatt [1992b], изразът α interpreβ се интерпретира „правя паралелно α и β“. В този контекст бинарните отношения R (α) и R (β) вече не са множество от двойки от формата (x, y) с x, y светове, а по-скоро множества от двойки от формата (x, Y) с xa свят и Y набор от светове. Тя е вдъхновена от Game Logic of Parikh [1985], интерпретация на PDL с „програми като игри“. Game Logic предоставя допълнителна програмна конструкция, която дуализира програмите, като по този начин позволява да се определи пресечната точка на програмите като двойник на недетерминирания избор между програмите.

5. Заключение

Тази статия се фокусира върху динамичната логика на предложенията и някои от нейните значими варианти. Към момента има редица книги - Goldblatt [1982], Goldblatt [1992a], Harel [1979] и Harel, Kozen и Tiuryn [2000] - и проучвателни документи - Harel [1984], Kozen и Tiuryn [1990], Parikh [1983] - лечение на PDL и свързани с него формализми. Тялото на изследванията върху PDL със сигурност е от съществено значение за разработването на много логически теории за системната динамика. Тези теории обаче могат да се окажат извън обхвата на настоящия член. Van Eijck and Stokhof [2006] е по-скорошен преглед на теми, използващи динамична логика, засягащи различни теми, които представляват определен интерес за философите: напр. Динамиката на комуникацията или естествената езикова семантика. Напоследък книгите излизат с много подробности по по-нови теми,като динамична логика на знанието (динамична епистемична логика) в Van Ditmarsch, Van Der Hoek и Kooi [2007] и динамичната логика на непрекъснатите и хибридни системи (диференциална динамична логика) в Platzer [2010]. PDL е замислен основно за разсъждения за програми. Има много други приложения на модална логика за разсъждения за програми. Алгоритмичната логика е по-близка до PDL, тъй като позволява да се говори изрично за програми. Читателят е поканен да се консултира с работата, изучена в Mirkowska и Salwicki [1987]. Временната логика сега е главната логика в теоретичните компютърни науки и има тясна връзка с логиката на програмите. Те позволяват да се изрази временното поведение на преходните системи с език, който се абстрахира от етикетите (оттук и програмите). Вижте например Schneider [2004] за преглед на основите в тази изследователска област.

библиография

  • Apt, K., 1981, „Десет години от логиката на Hoare: Проучване - част I“, ACM транзакции на езици и системи за програмиране, 3 (4): 431–483.
  • Балбиани, П. и Д. Вакарелов, 2003, „PDL с пресичане на програми: пълна аксиоматизация“, сп. „Приложна некласическа логика“, 13: 231-276.
  • van Benthem, J., 1998, „Програмни конструкции, безопасни за бисимулация“, Studia Logica, 60: 311–330.
  • Berman, F. и M. Paterson, 1981, „Пропозиционната динамична логика е по-слаба без тестове“, Теоретична компютърна наука, 16: 321–328.
  • Burstall, R., 1974, „Програмата, доказваща се като симулация на ръцете с малко индукция“, обработка на информация 74: Материали на конгрес 74 на IFIP, Амстердам: Издателска компания North Holland, 308–312.
  • Danecki, R., 1984a, „Пропозиционна динамична логика със силен цикъл на предикат“, в М. Читил и В. Кубек, Математически основи на компютърните науки, Берлин: Springer-Verlag, 573-581.
  • –––, 1984b, „Недетерминираната динамична логика на предложенията с пресичане е разрешима“, в A. Skowron (ed.), Computation Theory, Berlin: Springer-Verlag, 34-53.
  • De Giacomo, G. и F. Massacci, 2000, „Комбиниране на дедукция и проверка на модела в таблици и алгоритми за обратна PDL“, Информация и изчисления, 160: 109–169.
  • van Ditmarsch, H., W. van Der Hoek и B. Kooi, 2007, Динамична епистемична логика, Dordrecht: Springer-Verlag.
  • van Eijck, J. и M. Stokhof, 2006, „Гамата на динамичната логика“, в D. Gabbay и J. Woods (ред.), Наръчникът по история на логиката, том 7- логика и модалностите в Двадесети век, Амстердам: Elsevier, 499–600.
  • Emerson, E. и Jutla, C., 1988, „Сложността на дървесните автомати и логиката на програмите (разширено резюме)“, в сборника на 29-ия годишен симпозиум за основите на компютърните науки, Лос Аламитос, Калифорния: IEEE Computer Society, 328–337.
  • –––, 1999, „Сложността на автоматите на дърветата и логиката на програмите“, в SIAM Journal of Computing, 29: 132–158.
  • Енглер, Е., 1967, „Алгоритмични свойства на структурите“, Теория на математическите системи, 1: 183–195.
  • Фишер, М. и Р. Ладнер, 1979, „Пропозиционна динамична логика на редовни програми“, сп. „Компютърни и системни науки“, 18: 194–211.
  • Флойд, Р., 1967, „Присвояване на значения на програмите“, Proceedings of the American Mathematical Society Symposia on Applied Mathematics (том 19), Providence, RI: American Mathematical Society, 19–31.
  • Гаргов, Г. и С. Паси, 1988, „Детерминизъм и цикличност в комбинативно PDL“, Теоретична компютърна наука, Амстердам: Elsevier, 259–277.
  • Goldblatt, R., 1982, Axiomatising the Logic of Computer Programming, Berlin: Springer-Verlag.
  • –––, 1992a, „Логика на времето и изчисленията“, Станфорд: Център за изучаване на езикови и информационни публикации.
  • –––, 1992b, „Паралелно действие: Паралелна динамична логика с независими модалности“, Studia Logica, 51: 551–578.
  • Göller, S., M. Lohrey и C. Lutz, 2007, „PDL с пресичане и обратно е 2EXP-пълно“, Основи на софтуерната наука и изчислителни структури, Берлин: Springer, 198–212.
  • Харел, Д., 1979, Динамична логика от първи ред, Берлин: Спрингер-Верлаг.
  • –––, 1983, „Повтарящи се домино: правейки силно неразбираеми много разбираеми“, в М. Карпински (съст.), Основи на теорията на изчисленията, Берлин: Спрингер-Верлаг, 177–194.
  • –––, 1984, „Динамична логика“, в D. Gabbay и F. Guenthner (ред.), Наръчник по философска логика (том II), Dordrecht: D. Reidel, 497–604.
  • Harel, D., D. Kozen и J. Tiuryn, 2000, Dynamic Logic, Cambridge, MA: MIT Press.
  • Harel, D. and Sherman, R., 1982, „Looping vs. Repeating in Dynamic Logic“, Information and Control, 55: 175–192.
  • Hoare, C., 1969, „Аксиоматична основа за компютърно програмиране“, Съобщения на Асоциацията на компютърните машини, 12: 576–580.
  • Козен, Д., 1983, „Резултати от предложеното м-смятане“, Теоретична компютърна наука, 27: 333–354.
  • Kozen, D. и R. Parikh, 1981, „Елементарно доказателство за пълнотата на PDL“, Теоретична компютърна наука, 14: 113–118.
  • Kozen, D. и J. Tiuryn, 1990, "Логика на програмите", в J. Van Leeuwen (съст.), Наръчник по теоретична компютърна наука (Том B), Амстердам: Elsevier, 789–840.
  • Ланге, М., 2005, „По-ниска сложност, ограничена за предложена динамична логика със пресичане“, в R. Schmidt, I. Pratt-Hartmann, M. Reynolds и H. Wansing (ред.), Напредък в модалната логика (том 5), Лондон: Публикации на King's College, 133–147.
  • Lange, M. и C. Lutz, 2005, „2-EXPTIME долни граници за предложения за динамична логика със пресичане“, Journal of Symbolic Logic, 70: 1072–1086.
  • Lutz, C., 2005, „PDL с пресичане и обратно е разрешимо“. In L. Ong (ed.), Computer Science Logic, Berlin: Springer-Verlag, 413-427.
  • Massacci, F., 2001, „Процедури за вземане на решения за изразителни описателни логики с пресичане, композиция, обратна роля и идентичност на ролите“, в B. Nebel (съст.), 17-та Международна съвместна конференция за изкуствен интелект, Сан Франциско: Morgan Kaufmann, 193-198.
  • Mirkowska, G. и A. Salwicki, 1987, Algorithmic Logic, Dordrecht: D. Reidel.
  • Нишимура, Х., 1979, „Последователен метод в динамичната логика на предложенията”, Acta Informatica, 12: 377–400.
  • Parikh, R., 1978, „Пълнотата на динамичната логика на предложенията“, в J. Winkowski (съст.), Математически основи на компютърните науки, Берлин: Springer-Verlag, 1978, 403-415.
  • –––, 1983, „Пропозиционна логика на програмите: нови направления“, в М. Карпински (съст.), Основи на теорията на изчисленията, Берлин: Springer-Verlag, 347-359.
  • –––, 1985 г., „Логиката на игрите и нейните приложения“, Анали на дискретната математика, 24: 111–140.
  • Peleg, D., 1987, „Паралелна динамична логика“, списание на Асоциацията на изчислителните машини, 34: 450–479.
  • Platzer, A., 2010, Логически анализ на хибридни системи: Доказване на теореми за сложна динамика, Берлин: Springer, 2010.
  • Прат, В., 1976, „Семантични съображения относно логиката на Флойд-Хоар“, в сборника от 17-ия IEEE симпозиум за основите на компютърните науки, Лос Аламитос, Калифорния: IEEE Computer Society, 109–121.
  • –––, 1978 г., „Практически метод за решение за динамична логика на предложенията“, в сборника на 10-ия годишен симпозиум на ACM по теория на компютрите, Ню Йорк, Ню Йорк, ACM, 326–337.
  • –––, 1980a, „Близо-оптимален метод за разсъждение за действие“, Journal of Computer and System Sciences, 20: 231–254.
  • –––, 1980b, „Приложение на модалната логика към програмирането“, Studia Logica, 39: 257–274.
  • Sakalauskaite, J. и M. Valiev, 1990, „Пълнота на динамичната логика на предложенията с безкрайно повтарящи се“, в П. Петков (съст.), Математическа логика, Ню Йорк: Пленум Прес, 339–349.
  • Salwicki, A., 1970, "Формализирани алгоритмични езици", Bulletin de l'Academie Polonaise des Sciences, Serie des Sciences mathematiques, astronomiques et physiques, 18: 227–232.
  • Сегерберг, К., 1977, „Теорема за пълнота в модалната логика на програмите“, Известия на Американското математическо общество, 24: 522.
  • Schneider, K., 2004, Проверка на реактивни системи, Берлин: Springer-Verlag.
  • Streett, R., 1982, „Пропозиционната динамична логика на цикъла и обратното е елементарно решаваща“, Информация и контрол, 54: 121–141.
  • Вакарелов, Д., 1983, „Теорема за филтрация за динамични алгебри с тестове и обратен оператор”, в А. Салвицки (съст.), Логика на програмите и техните приложения, Берлин: Спрингер-Верлаг, 314–324.
  • Vardi, M., 1985, „Укротяване на обратното: разсъждение за двупосочни изчисления“, в бележки от лекции по компютърни науки (том 193), Берлин-Хайделберг: Springer, 413–423.
  • –––, 1998, „Разсъждение за миналото с двупосочни автомати“, в Бележки по лекции по компютърни науки (том 1443), Берлин-Хайделберг: Спрингер, 628–641.
  • Vardi, M., and Stockmeyer, L., 1985, „Подобрени горни и долни граници за модална логика на програмите: предварителен доклад“, в сборника от 17-ия годишен симпозиум на ACM по теория на изчисленията, Ню Йорк, Ню Йорк: ACM, 240 -251.
  • Янов, Й., 1959, „За еквивалентността на операторските схеми“, кибернетични проблеми, 1: 1–100.

Академични инструменти

сеп човек икона
сеп човек икона
Как да цитирам този запис.
сеп човек икона
сеп човек икона
Вижте PDF версията на този запис в Дружеството на приятелите на SEP.
inpho икона
inpho икона
Разгледайте тази тема за вписване в интернет философския онтологичен проект (InPhO).
Фил хартия икона
Фил хартия икона
Подобрена библиография за този запис в PhilPapers, с връзки към неговата база данни.

Други интернет ресурси

[Моля, свържете се с автора с предложения.]

Препоръчано: