Propoziciona Dinamička Logika

2023 Autor: Noah Black | [email protected]. Zadnja promjena: 2023-08-25 04:38

Ulazna navigacija

• Sadržaj unosa
• Bibliografija
• Akademske alate
• Prijatelji PDF pregled
• Podaci o autoru i citiranju
• Povratak na vrh

Propoziciona dinamička logika

Prvo objavljeno: 1. veljače 2007; suštinska revizija Pet siječnja 25, 2019

Logika programa su modalna logika koja proizlazi iz ideje o povezivanju svakog računalnog programa α programskog jezika s modalitetom [α]. Ta ideja proizlazi iz djela Engelera [1967], Hoare [1969], Yanova [1959] i drugih koji su formulirali i proučavali logičke jezike u kojima se mogu izraziti svojstva programskih veza. Algoritmička logika (AL) koju je prvi razvio Salwicki [1970] i dinamička logika (DL) koju je razradio Pratt [1976] pravi su nastavak ovih radova. Ovdje ćemo se koncentrirati na DL. Brojni radovi posvećeni DL-u i njegovim inačicama, kao i njegove višestruke primjene u provjeri programa i strukturi podataka pokazuju da on predstavlja koristan alat u proučavanju svojstava programa. Pratt je odlučio prikazati DL na onome što bi se moglo nazvati razinom prvog reda,i njegovo je djelo pokrenulo Fischera i Ladnera [1979] da definiraju prijedlošku varijantu DL-a par godina kasnije. Ovaj članak predstavlja uvod u PDL, propozicijsku varijantu DL-a.

• 1. Uvod

• 2. Definicije i temeljni rezultati

  • 2.1 Sintaksa i semantika
  • 2.2 Aksiomatizacija i cjelovitost
  • 2.3 Mogućnost odlučivanja i složenosti

• 3. Strukturirano programiranje i ispravnost programa

  • 3.1 Izračun proračuna
  • 3.2. Hoare račun i PDL
  • 3.3 Potpuna ispravnost

• 4. Neke varijante

  • 4.1 PDL bez testova
  • 4.2 PDL sa obrnutim
  • 4.3 PDL s ponavljanjem i petljom
  • 4.4 PDL s sjecištem
• 5. Zaključak
• Bibliografija
• Akademske alate
• Ostali internetski resursi
• Povezani unosi

1. Uvod

Dinamička logika (DL) su modalna logika za prikaz stanja i događaja dinamičnih sustava. Jezik DL-ova je i jezik tvrdnje koji može izraziti svojstva proračunskih stanja, i programski jezik koji može izraziti svojstva sistemskih prijelaza između tih stanja. DL-ovi su logika programa i omogućuju razgovor i razmišljanje o stanju stvari, procesima, promjenama i rezultatima.

Prattova originalna dinamička logika programa bila je modalna logika prvog reda. Propoziciona dinamička logika (PDL) je njezin propozicioni partner. U Fischeru i Ladneru [1979] predstavljena je sama po sebi logika. Budući da postoji prijedlog, jezik PDL ne koristi izraze, predikate ili funkcije. Dakle, u PDL-u postoje dvije sintaktičke kategorije: prijedlozi i programi.

Da bismo dali značenje izjavama u PDL-u, obično radimo sa apstraktnom semantikom u smislu označenih tranzicijskih sustava (LTS). LTS-ovi se mogu promatrati kao generalizacija Kripke modela, gdje su prijelazi između svjetova ili stanja "označeni" imenima atomskih programa. Vrednovanje za svaku državu pokazuje koje su tvrdnje u njoj istinite. Prijelaz označen s π iz jednog stanja x u stanje y-primijećeno x R (π) y, ili (x, y) ∈ R (π) - označava da započinjući s x, moguće je izvršavanje programa π koji završava u y. Ako je prijedlog A istinit u y, tada je formula A istinita u x: tj. U stanju x je moguće izvršenje programa α koji završava u stanju koji zadovoljava A. Prepoznaje se u modalitetu koji podsjeća na modalitet mogućnosti (često napomenuto ◊) modalne logike. Neiznenađujuće,postoji i odgovarajući pojam nužnosti (čiji se modalitet često primjećuje □). Formula [π] A će biti istinita u stanju x ako je A istinito u svakom stanju dosegnutom iz x tranzicijom označenom π.

Moguće izvršavanje složenih programa može se sljedeće kompozicijski definirati. Na primjer, program "najprije α, zatim β" složen je program, točnije niz. Moguća izvedba može se predstaviti u LTS-u sastavljanjem prijelaza u dva koraka - dakle prijelaza koji može biti označen s R (α; β) između stanja x i x ': moguće je izvršenje u x programa α koji završava u stanju y i moguće je izvršiti u programu programa β koji završava u x '. Ako je prijedlog A istinit u x ', tada će formula A biti točna u stanju x. Programi α i β mogli su i sami biti složeni programi. Ipak, više programa može se izraziti s više konstrukata koje ćemo prezentirati u dogledno vrijeme.

Program se tada vidi ekstenzivno: to je binarni odnos između parova stanja LTS-a. Upravo je to skup parova oblika (x, y) takav da se program može izvesti u stanju x i može dovesti u stanje y. S druge strane, prijedlog je izjava o državi; u stanju je ili istinita ili lažna. Stoga se prijedlog može promatrati i ekstenzivno: skup stanja LTS-a gdje je istina.

S akronimom PDL ovdje se upućujemo precizno na dinamiku logike prijedloga sa sljedećim programskim konstrukcijama: slijed, nedeterministički izbor, neograničena iteracija i test. Predstavljamo ga u odjeljku 2, zajedno s nekim svojstvima i temeljnim rezultatima. Osobito ćemo se pozabaviti njegovom aksiomatizacijom i odlučnošću.

Hoareovo računanje iz Hoare [1969] orijentir je za logiku programa. Odnosi se na istinitost izjava oblika {A} α {B}, što znači da uz preduvjet A program α uvijek ima B kao post-uvjet - i definiran je aksiomatski. To proizlazi iz želje za rigoroznim metodama da se razmotri svojstva programa i na taj način se aktivnosti programiranja da određeno mjesto u sferi znanosti. Burstall [1974] vidio je analogiju između modalne logike i razmišljanja o programima, ali stvarni rad na tome započeo je s Prattom [1976] kada ga je predložio R. Moore, njegov tadašnji student. PDL dolazi iz Prattove interpretacije Hoareove računice u formalizmu modalne logike. Uvod u genezu PDL-a može se naći u Prattu [1980b]. Hoare-trostruka {A} α {B} uhvaćena je PDL formulom A → [α] B što znači doslovno da ako je A istina, tada će svako uspješno završavanje izvršenja α završiti s B istinitim. Sa ovom povezanošću uspostavljena je rutina dokazivanja početnih pravila Hoareove računice koristeći isključivo aksiomatizaciju PDL-a. To ćemo detaljno učiniti u odjeljku 3, koji je koncentriran na obrazloženje o ispravnosti strukturiranih programa.

Dodatne teme povezane s PDL-om uključuju rezultate koji se odnose na usporednu moć izražavanja, odlučnost, složenost i cjelovitost brojnih zanimljivih varijanti dobivenih proširivanjem ili ograničavanjem PDL-a na različite načine. Od njegovog postanka mnoge su inačice PDL-a privukle pažnju. Ove varijante mogu razmotriti determinirane programe, ograničene testove, neredovite programe, programe kao automate, nadopunjavanje i sjecište programa, obrnuto i beskonačno računanje itd. Neke ćemo od njih predstaviti u odjeljku 4, pružajući neke upute u pogledu njihove relativne ekspresivnosti, njihove aksiomatizacije i računske složenosti.

Zaključujemo u odjeljku 5.

2. Definicije i temeljni rezultati

U odjeljku 2.1. Prikazujemo sintaksu i semantiku PDL-a. Teorija dokaza PDL-a prikazana je u odjeljku 2.2 s aksiomatizacijama i pokazivanjem literature na cjelovitost. Problematičnost i složenost obrađujemo u odjeljku 2.3.

2.1 Sintaksa i semantika

Propoziciona dinamička logika (PDL) dizajnirana je za predstavljanje i obrazloženje prijedloga svojstava programa. Njegova se sintaksa temelji na dva skupa simbola: brojiv skup Φ ₀ atomske formule i brojiv skup Π ₀ atomskog programa. Složene formule i složeni programi preko ove baze definirani su kako slijedi:

• Svaka atomska formula je formula
• 0 ("lažno") je formula
• Ako je A formula, tada je A ("nije A")
• Ako su A i B formule, tada je (A ∨ B) ("A ili B") formula
• Ako je α program, a A je formula, tada je [α] A ("svaka izvedba α iz postojećeg stanja vodi u stanje u kojem je A istina") formula
• Svaki atomski program je program
• Ako su α i β programi, tada je (α; β) ("učiniti α, a slijedi β") program
• Ako su α i β programi, tada je (α∪β) ("učiniti α ili β, nedeterministički") program,
• Ako je α program, onda je α * ("ponovite α ograničeno, ali ne determinirano, broj puta") program.
• Ako je A formula, onda A? ("Nastavite ako je točka A istina, u suprotnom") je program

Ostale boolove veze 1, ∧, → i ↔ koriste se kao kratice na standardni način. Pored toga, skraćujemo ¬ [α] ¬ A do A („neko izvršavanje α iz postojećeg stanja vodi u stanje u kojem je A istina“) kao u modalnoj logici. Pišemo α ⁿ za α;…; α sa n pojava od α. Formalnije:

• α ⁰ = _df 1?
• α ^{n +1} = _df α; α ⁿ

Također:

α ⁺ = _df α; α *

često je korisno predstavljati iteraciju koja nije povezana, ali se pojavljuje barem jednom. Napokon usvajamo standardna pravila za izostavljanje zagrada.

Formule se mogu koristiti za opisivanje svojstava koja su zadržana nakon uspješnog izvođenja programa. Na primjer, formula [α∪β] A znači da kad god se program α ili β uspješno izvrši, postiže se stanje u kojem A drži, dok formula A znači da postoji niz izmjeničnih izvršavanja α i β takvih da stanje je postignuto tamo gdje se drži A. Semantički gledano, formule se tumače skupima stanja, a programi se interpretiraju binarnim odnosima nad stanjima u tranzicijskom sustavu. Preciznije, značenje PDL formula i programa tumači se preko označenih tranzicijskih sustava (LTS) M = (W, R, V) gdje je W neprazan skup svjetova ili stanja, R je preslikavanje iz skupa Π ₀ atomske programa u binarne odnose na W i V je preslikavanje iz skupa Φ ₀ atomskih formula u podskupine W.

Neformalno, preslikavanje R dodjeljuje svakom atomskom programu π ∈ Π ₀ neki binarni odnos R (π) na W s namjeravanim značenjem x R (π) y ako postoji izvedba π iz x koja vodi u y, dok preslikavanje V dodjeljuje svakoj atomskoj formuli p ∈ Φ ₀ neki podskup V (p) od W s namjeravanim značenjem x ∈ V (p) iff p je istinit u x. S obzirom na naša očitanja od 0, ¬ A, A ∨ B, [α] A, α; β, α∪β, α * i A?, Jasno je da se R i V moraju induktivno produžiti kako slijedi kako bi se dobilo planirano značenje za složene programe i formule:

• x R (α; β) y ako postoji svijet z takav da x R (α) z i z R (β) y
• x R (α∪β) y iff x R (α) y ili x R (β) y
• x R (α *) y ako postoji negativni cijeli broj n i postoje svjetovi z ₀, …, z _n takvi da je z ₀  = x, z _n  = y i za sva k = 1.. n, z _{k −1} R (α) z _k
• x R (A?) y iff x = y i y ∈ V (A)
• V (0) = ∅
• V (¬ A) = W / V (A)
• V (A ∨ B) = V (A) ∪ V (B),
• V ([α] A) = {x: za sve svjetove y, ako je x R (α) y onda y ∈ V (A)}

Ako je x ∈ V (A), tada kažemo da je A zadovoljen u stanju x u M, ili "M, x sat A".

Nazovite M LTS prikazan gore s lijeve strane i M 'LTS prikazan s desne strane. Formalno definirano, imamo M = (W, R, V) s W = {x ₁, x ₂ }, R (π ₁) = {(x ₁, x ₁)}, R (π ₂) = {(x ₁, x ₂)}, V (p) = {x ₁ }, V (q) = {x ₂ }, a M '= (W', R ', V') imamo W '= {y ₁, y ₂, y ₃, y ₄ }, R (π ₁) = {(y ₁, y ₂), (y ₂, y ₂)}, R '(π₂) = {(y ₁, y ₃), (y ₂, y ₄)}, V '(p) = {y ₁, y ₂ }, V' (q) = {y ₃, y ₄ }. Imamo primjerice:

• M, x ₁ sat p
• M, x ₂ sat q
• M, x ₁ sat <π ₁ > p ∧ <π ₂ > q
• M, x ₁ sat [π ₁] p ∧ [π ₁ *] p
• M ', y ₁ sat <π ₁ *; π ₂ > q
• M ', y ₂ sat [π ₁ *] str
• M ', y ₁ sat [π ₁ ππ ₂] (q ∨ p)
• M ', y ₃ sat [π ₁ ππ ₂] 0

Sada razmotrimo formulu A. Kažemo da je A vrijedno u M ili da je M model A, ili "M ⊨ A", ako je za sve svjetove x, x ∈ V (A). Za A modele se kaže da vrijedi ili "⊨ A", iff za sve modele M, M ⊨ A. Kažemo da je A zadovoljavajući u M ili da M zadovoljava A, ili "M sat A", ako postoji svijet x takav da je x ∈ V (A). Za A se kaže da je zadovoljavajući, ili "sat A", ako postoji model M takav da je M sat A. Zanimljivo,

sat A iff ne ⊨ A

⊨ A iff ne sat ¬ A

Valjane su neke izvanredne formule PDL-a. (Čitatelj ih može pokušati formalno dokazati ili se barem uvjeriti u nekoliko prikazanih primjera.)

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

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

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

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

Ekvivalentno, možemo ih napisati pod njihovim dvojnim oblikom.

⊨ A ↔ A

⊨ A ↔ A ∨ A

⊨ A ↔ A ∨ A

⊨ <A?> B ↔ A ∧ B

Jedan zanimljiv pojam odnosi se na količinu informacija izraženih PDL formulama koje su sadržane u LTS-u. Ponašanje sustava opisanog kao LTS doista je često blago skriveno u svom obliku. Na primjer, jednostavnim pregledom, lako je uvjeriti se da dva gore prikazana LTS-a imaju isto ponašanje i zadovoljavaju iste PDL formule. Za kraj ovog odjeljka o sintaksi i semantika dajemo teoretski temelj ovih tvrdnji.

S obzirom na dva LTS-a, može se postaviti pitanje zadovoljavaju li iste formule. Pojam bisimulacije postao je standardna mjera za ekvivalenciju Kripke modela i označenih tranzicijskih sustava. Bisimulacija između LTSs M = (W, R, V) i M '= (W', R ', V') je binarni odnos Z između njihovih stanja, tako da je za sve svjetove x u M i za sve svjetove x ' u M ', ako je xZx' tada

• za sve atomske formule p ∈ Φ ₀, x ∈ V (p) iff x '∈ V' (p)
• za sve atomske programe π ∈ Π ₀ i za sve svjetove y u M, ako je x R (π) y, tada postoji svijet y 'u M' takav da su yZy 'i x' R '(π) y'
• za sve atomske programe π ∈ Π ₀ i za sve svjetove y 'u M', ako je x 'R' (π) y ', svijet postoji u M takvom da su yZy' i x R (π) y

Kažemo da su dva LTS-a međusobno slična kada postoji bisimulacija između njih. Od početka PDL-a poznato je da u dva slična LTS-a M i M ', za sve svjetove x u M i za sve svjetove x' u M ', ako je xZx', tada za sve PDL formule A, x ∈ V (A) iff x '∈ V' (A). Dakle, kada su dva LTS-a u skladu s gornjom definicijom bisimulacije, to je slučaj da, ako je xZx 'tada

• za sve programe α i za sve svjetove y u M, ako je x R (α) y onda svijet postoji y 'u M' takav da su yZy 'i x' R '(α) y'
• za sve programe α i za sve svjetove y 'u M', ako je x 'R' (α) y ', svijet postoji u M takav da su yZy' i x R (α) y

Stoga se jednostavno može usporediti ponašanja dvaju LTS-ova uvidom samo u atomske programe i sigurno ekstrapolirati na komparativno ponašanje ovih LTS-a čak i za složene programe. Kažemo da su programske konstrukcije PDL-a sigurne za bisimulaciju. Pogledajte Van Benthem [1998] za precizne karakterizacije programskih konstrukcija koje su sigurne za bisimulaciju.

Lako se vidi da su dva primjera LTS-a gore različita. Bisimulacija Z između M i M 'može se dati kao: Z = {(x ₁, y ₁), (x ₁, y ₂), (x ₂, y ₃), (x ₂, y ₄)}. Stanja x ₁ i y ₁ zadovoljavaju točno iste PDL formule. Tako čine stanja x ₁ i y ₂, itd.

2.2 Aksiomatizacija i cjelovitost

Svrha teorije dokaza je dati karakterizaciju svojstva ⊨ A u smislu aksioma i pravila zaključivanja. U ovom odjeljku definiramo prediktiv izvedljivosti ctive induktivno operacijama na formulama koje ovise samo o njihovoj sintaktičkoj strukturi na takav način da za sve formule A,

⊢ A iff ⊨ A.

Naravno, PDL je produžetak klasične propozicijske logike. Prvo očekujemo da su sve predložene tautologije pridržane i da su dopuštena sva propozicioniranja. Konkretno, modus ponens je valjano pravilo: od A i A → B zaključujemo s B. Za bilo koji program α, ograničavajući LTS na odnos R (α), dobivamo Kripkeov model u kojem je logika modaliteta [α] najslabija prijedloška normalna modalna logika, naime, logika K. Dakle, PDL sadrži svaku instancu poznate sheme aksioma distribucije:

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

a zatvara se prema sljedećem pravilu zaključivanja (nužno pravilo):

(N) iz A infer [α] A.

Modalna logika je normalna ako se pokorava (A0) i (N). Važna svojstva za sve α su ta da se [α] raspodjeljuje preko konjunkcije ∧, a pravilo monotonije, koje dopušta iz A → B da zaključi [α] A → [α] B, može se dokazati. Napokon, PDL je najmanje normalna modalna logika koja sadrži svaku instancu sljedećih aksiomskih shema

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

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

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

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

i zatvoreno prema sljedećem pravilu zaključivanja (pravilo invazije petlje):

(I) od A → [α] A zaključak A → [α *] A

Ako je X skup formula i A je formula, tada kažemo da se A može odrediti iz X, ili "X ⊢ A", ako postoji niz A ₀, A ₁, …, A _n formule takav da A _n  = A i za sve i ≤ n, A _i je primjer aksiomske sheme, ili formule X, ili potječe iz ranijih formula slijeda pomoću pravila zaključivanja. Nadalje, ⊢ A iff ∅ ⊢ A; u ovom slučaju kažemo da se A može odrediti u. Za X se kaže da je ⊢ -sljedan ako nije X ⊢ 0. Lako je ustanoviti da se (I) može zamijeniti sljedećom aksiomskom shemom (indukcijska aksiom shema):

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

Najprije ustanovimo da je (I) izvedeno pravilo sustava dokaza utemeljenog na (A1), (A2), (A3), (A4) i (A5):

1.	A → [α] A	pretpostavka
2.	[α *] (A → [α] A)	od 1 pomoću (N)
3.	[α *] (A → [α] A) → (A → [α *] A)	shema aksioma (A5)
4.	A → [α *] A	od 2 i 3 pomoću modusa ponens

Utvrdimo sljedeće da je (A5) ⊢-odrediti:

1.	[α *] (A → [α] A) ↔ (A → [α] A) ∧ [α] [α *] (A → [α] A)	shema aksioma (A3)
2.	A ∧ [α *] (A → [α] A) → [α] (A ∧ [α *] (A → [α] A))	od 1 koristeći propozicioniranje i distribuciju [α] na ∧
3.	A ∧ [α *] (A → [α] A) → [α *] (A ∧ [α *] (A → [α] A))	od 2 pomoću (I)
4.	[α *] (A → [α] A) → (A → [α *] A)	iz 3 koristeći propozicioniranje i distributivnost [α *] iznad ∧

U Segerbergu je predložena aksiomatizacija PDL na temelju aksiomskih shema (A1), (A2), (A3), (A4) i (A5) [1977]. Neposredno iz gornjih definicija ⊢ je zvuk u odnosu na ⊨, tj

Za sve formule A, ako je ⊢ A, onda je ⊨ A

Dokaz se nastavlja indukcijom na duljini odbitka A u ⊢. Pitanje cjelovitosti ⊢ u odnosu na ⊨, tj.

Za sve formule A, ako je ⊨ A, onda je ⊢ A

progonio je nekoliko logičara. Obrazloženje koje je predstavljeno u Segerbergu [1977] bio je prvi pokušaj dokazivanja cjelovitosti ⊢. Ubrzo je i Parikh došao do dokaza. Kad je početkom 1978. Segerberg pronašao nedostatak u svojoj argumentaciji (koju je na kraju popravio), Parikh je objavio ono što se u Parikhu može smatrati prvim dokazom potpunosti ⊢. Od tada su objavljeni različiti dokazi o cjelovitosti, npr. Kozen i Parikh [1981].

Također su tražene različite alternativne teorije dokaza o PDL-u. Čak i rano, osobito u Prattu [1978]. Spomenimo onda i cjelovitost povezanih teorija Nishimura [1979] i Vakarelova [1983].

Alternativna formulacija prediktivnog predikata za PDL omogućava upotrebu infinitarnog pravila zaključivanja, kao što je to slučaj, na primjer, u Goldblattu [1992a]. (Beskonačno pravilo zaključivanja zauzima beskonačni broj premisa.) Neka je ⊢ 'predikat izvedljivosti koji u jeziku prijedloge dinamičke logike odgovara najmanje normalnoj modalnoj logici koja sadrži svaki primjerak aksiomske sheme (A1), (A2), (A3) i (A4) i zatvoren je prema sljedećem infinitarnom pravilu:

(I ') iz {[β] [α ⁿ] A: n ≥ 0} zaključiti [β] [α *] A

Može se dokazati da je ⊢ 'zvučan i cjelovit s obzirom na ⊨, tj.

Za sve formule A, ⊢ 'A iff ⊨ A

Drugim riječima, što se tiče stvaranja skupa svih važećih formula, dokazni sustavi ⊢ i ⊢ 'su jednaki.

2.3 Mogućnost odlučivanja i složenosti

Cilj teorije složenosti je uspostaviti izračunavanje svojstva sat A u pogledu resursa vremena ili prostora. Složenost logike L često se poistovjećuje s problemom odlučivanja o zadovoljavanju njegovih formula koji je definiran kao:

(L-SAT) Da li je zadovoljavajuća formula A od L?

U ovom dijelu istražujemo složenost sljedećeg problema s odlukama:

(PDL-SAT) S obzirom na formulu A PDL-a, da li je zadovoljavajuća?

Kompletna aksiomatizacija PDL-a je rekurzivna definicija skupa valjanih PDL formula, ili drugim riječima, skupa formula čiji negacija nije zadovoljavajuća. Dakle, u vezi s problemom (PDL-SAT), imamo podprocedura koja bi odgovorila „ne“da PDL formula A ne bi bila zadovoljavajuća. Podprocedura (SP1) sastoji se u nabrajanju svih formula ⊢-deducibil, polazeći od aksioma i izvodeći ostale teoreme uz pomoć pravila zaključivanja. Ako se ima dovoljno vremena, ako se formula može odrediti ⊢, podprocedura bi je pronašla na kraju. Stoga, ako A nije zadovoljavajući, (SP1) na kraju mora pronaći ¬ A i odgovoriti „ne“kada to učini.

Međutim, ako je formula A zadovoljavajuća, tada (SP1) nikada neće naći ¬ A. Trčao bi zauvijek, a u to nitko nije mogao biti siguran. Ali iz ove nesigurnosti postoji izlaz. Također možemo razmišljati o drugom pod-postupku koji odgovara "da" ako je PDL formula zadovoljavajuća. Zapravo, jedan od najranijih rezultata na PDL-u bio je dokaz da PDL ima svojstvo konačnog modela, tj.

Za sve formule A, ako je sat A, postoji konačni model M takav da je M sat A.

Svojstvo konačnog modela nudi osnovu za pod-postupak (SP2) koji se sastoji u nabrajanju jednog po jednog konačnog modela PDL-a i testiranju zadovoljava li jedan od njih formulu. (Za sve formule A i za sve konačne modele M lako je provjeriti je li M sat A primjenom definicije V (A).) Dakle, ako je A zadovoljavajući, na kraju mora pronaći model M takav da je M sat A, i odgovorite "da" kad to učinite. Simetrično prema prvom potpostupku (SP1), ako formula A nije zadovoljavajuća, tada (SP2) nikada neće pronaći model koji je zadovoljava, pokrenut će se zauvijek, a u to nitko ne bi mogao biti siguran.

Sada, kombinirajući (SP1) i (SP2) zajedno, možemo odlučiti je li PDL formula A zadovoljavajuća. Dovoljno ih je pokrenuti paralelno: ako je A zadovoljavajući tada (SP2) će na kraju odgovoriti sa "da", ako A nije zadovoljavajući, tada će (SP1) odgovoriti sa "ne". Postupak se zaustavlja kada odgovor (ili SP1) ili (SP2) daje odgovor.

Ako je postupak koji je dobiven dovoljan da zaključi da je problem (PDL-SAT) moguće riješiti, u praksi je vrlo neučinkovit. Do rezultata dolazi zbog Fischera i Ladnera [1979], Kozena i Parikh [1981] - jača od svojstva konačnog modela, to je svojstvo malog modela:

Za sve formule A, ako je sat A, tada postoji konačni model M eksponencijalne veličine u A takav da je M sat A.

To znači da bismo sada znali kada prestati tražiti model koji zadovoljava formulu u postupku (SP2). Stoga možemo koristiti (SP2) za testiranje je li formula zadovoljavajuća, ali nakon što smo iscrpili sve male modele, možemo zaključiti da formula nije zadovoljavajuća. Tako se dobiva postupak koji se nedeterministički pokreće u eksponencijalnom vremenu (NEXPTIME): pogodite model veličine najviše pojedinačno eksponencijalne i provjerite zadovoljava li ona formula. No, ključni rezultati u teoriji složenosti PDL-a dolaze od Fischera i Ladnera [1979] i Pratta [1980a]. Primjećujući da formula PDL-a može učinkovito opisati izračunavanje izmjeničnog Turingovog stroja linearnim prostorom, Fischer i Ladner [1979] prvi su uspostavili donju granicu eksponencijalnog vremena (PDL-SAT). Pratt je dobio gornju granicu EXPTIME (PDL-SAT) [1980a],koji su koristili ekvivalent za PDL metode tableaux. Dakle, (PDL-SAT) je EXPTIME završen. (Algoritam učinkovitiji u praksi, iako još uvijek djeluje u determinističkom eksponencijalnom vremenu u najgorem slučaju, predložen je u De Giacomo i Massacci [2000].)

3. Strukturirano programiranje i ispravnost programa

Povijesno gledano, logika programa proizlazi iz djela računalnih znanstvenika zainteresiranih za dodjeljivanje značenja programskim jezicima u kasnim 1960-ima i pronalaženje strogog standarda za dokaze o programima. Na primjer, takvi dokazi mogu biti o ispravnosti programa s obzirom na očekivano ponašanje ili o prekidu programa. Seminarski rad je Floyd [1967], koji prikazuje analizu svojstava strukturiranih računalnih programa pomoću dijagrama tokova. Neki rani radovi poput Yanova [1959] ili Engelera [1967] imali su napredne i proučavane formalne jezike u kojima se mogu izraziti svojstva programskih veziva. Formalizam Hoarea (1969.) bio je prekretnica u nastupu PDL-a. Predložen je kao stroga aksiomatična interpretacija Floydovih dijagrama tokova. Često razgovaramo o Hoareovoj logici ili Floyd-Hoareovoj logici,ili Hoare računica kada se spominje ovaj formalizam. Hoareovo računanje bavi se istinitošću izjava ("Hoare trojke"), poput {A} α {B} koja uspostavlja vezu između preduvjeta A, programa α i postkondicije B. Označava da kad A stoji kao preduvjet izvršenja α, tada B vrijedi kao uvjet nakon uspješnog izvršenja α.

To je bila istina prije nekih desetljeća, a i dalje je slučaj: provjera programa je češće nego što se ne vrši testiranjem na razumnu raznoliku snagu podataka. Kad unos ne daje očekivani izlaz, ispravlja se "bug". Ako na kraju za svaki testirani unos dobijemo očekivani izlaz, razumno vjeruje da program nema pogreške. Međutim, ovo je dugotrajan način provjere valjanosti i ostavlja mjesto za neprovjerene unose koji neće uspjeti. Pronalaženje tih grešaka nakon što je program implementiran i uđe u upotrebu još je skuplje u resursima. Obrazloženje ispravnosti programa formalnim metodama ključno je za kritične sustave jer nudi iscrpan način dokazivanja da program nema grešaka.

3.1 Izračun proračuna

Za ilustraciju vrsta principa programa obuhvaćenih pravilima iz Hoareove računice dovoljno je konzultirati se s nekim od njih. (Napomena: pravila znače da ako svi iskazi iznad retka pravila drže - pretpostavke - onda i izjava pod linijom pravila - zaključak - drži.)

{A} α 1 {B} {B} α 2 {C}	(pravilo sastava)
{A} α 1; α 2 {C}

Pravilo kompozicije obuhvaća elementarnu sekvencijalnu kompoziciju programa. Kao pretpostavke imamo dvije pretpostavke o djelomičnoj ispravnosti dva programa α ₁ i α ₂. Prva pretpostavka je da kada se α ₁ izvrši u stanju koji zadovoljava A, tada će se završiti u stanju koji zadovoljava B, kad god se zaustavi. Druga pretpostavka je da kada α ₂ se izvodi u državnim zadovoljavajući B, tada će završiti u stanju zadovoljava C, kad god se zaustavlja. Zaključak pravila je o djelomičnoj ispravnosti programa α ₁; α ₂ (tj. Α _{1 koji je} uzastopno sastavljen s α ₂), što proizlazi iz dviju pretpostavki. Naime, možemo zaključiti da ako α ₁, α ₂ izvršava u stanje zadovoljavajući, onda to završi u stanju zadovoljavati C, kad god zastoji.

Pravilo iteracije je važno jer bilježi osnovnu sposobnost programa da izvršavaju neki dio koda više puta dok se određeni uvjet ne prestane držati.

{A ∧ B} α {A}	(pravilo ponavljanja)
{A} dok B činite α {¬ B ∧ A}

Konačno, dva su posljedica pravila temeljna da daju formalnu osnovu za intuitivno jasno obrazloženje koje uključuje slabije post-uvjete i snažnije preduvjete.

{A} α {B} B → C	(pravilo posljedice 1)
{A} α {C}

C → A {A} α {B}	(pravilo posljedice 2)
{C} α {B}

Iz formalizma predstavljenog u Hoareu (1969.) izostavljamo njegove aksiomske sheme jer bi zahtijevao jezik prvog reda. Konačno, u daljnjem radu o Hoareovoj logici često se dodaje i više pravila. Pogledajte Apt [1979] za rani pregled.

3.2. Hoare račun i PDL

Dinamička logika dolazi iz Prattove interpretacije Hoareovih trojki i Hoareove računice u formalizmu modalne logike. Pomoću modaliteta [α] možemo formalno izraziti da sva stanja koja su dostižna izvršavanjem α zadovoljavaju formulu A. To se postiže pisanjem [α] A. Stoga je Hoare trostruko {A} α {B} jednostavno zarobljeno PDL formulom

A → [α] B

Pored toga, važne programske konstrukcije u PDL se lako uvode definicijskom kraticom:

• ako je A tada α else β = _df ((A?; α) ∪ (¬ A?; β))
• dok je A do α = _df ((A?; α) *; ¬ A?)
• ponavljajte α sve dok A = _df (α; ((¬ A; α) *; A?))
• abort = _df 0?
• preskočite = _df 1?

Stoga se čini da smo s PDL-om dobro opremljeni da logično dokažemo ispravnost strukturiranih programa. Iza ove prilično mahajuće veze između PDL-a i Hoare računanja, možda još nije jasno kako se oni formalno odnose. PDL je zapravo generalizacija Hoareove računice u smislu da se sva pravila Hoareove računice mogu dokazati u aksiomatskom sustavu PDL-a. (Rigorozno, Hoareovo računanje sadrži aksiome kojima bi bio potreban proširen jezik dinamičke logike prvog reda.) To je prilično izvanredno, pa ćemo ovdje prikazati dva gore navedena pravila koja služe kao primjeri.

Dokazi započinju pretpostavkom pretpostavki pravila. Zatim, koristeći ove pretpostavke, aksiome i pravila PDL-a, i ništa drugo, cilj je ustanoviti da zaključak pravila logično slijedi. Dakle, za pravilo sastava, započinjemo pretpostavljanjem {A} α ₁ {B}, to je A → [α ₁] B u svojoj PDL formulaciji, i pretpostavljajući {B} α ₂ {C}, to je B → [α ₂] C. Cilj je dokazati da je {A} α ₁; α ₂ {C}. Upravo želimo da utvrdimo da se A → [α ₁; α ₂] C može odrediti iz skupa formula {A → [α ₁] B, B → [α ₂] C}.

1.	A → [α 1] B	pretpostavka {A} α 1 {B}
2.	B → [α 2] C	pretpostavka {B} α 2 {C}
3.	[α 1] B → [α 1] [α 2] C	Od 2 koji koriste monotoniju [α 1]
4.	A → [α 1] [α 2] C	od 1. i 3. koristeći prijedloge obrazloženja
5.	[α 1; α 2] C ↔ [α 1] [α 2] C	shema aksioma (A1)
6.	A → [α 1; α 2] C	od 4. i 5. koristeći prijedloge obrazloženja
-	{A} α 1; α 2 {C}

Nešto više sudjeluje dokaz pravila ponavljanja.

1.	A ∧ B → [α] A	pretpostavka {A ∧ B} α {A}
2.	A → (B → [α] A)	od 1 koristeći prijedloge obrazloženja
3.	[B?] [Α] A ↔ (B → [α] A)	shema aksioma (A4)
4.	A → [B?] [Α] A	od 2 i 3 koristeći prijedloge obrazloženja
5.	[B?; α] A ↔ [B?] [α] A	shema aksioma (A1)
6.	A → [B?; Α] A	od 4. i 5. koristeći prijedloge obrazloženja
7.	A → [(B?; Α) *] A	od 6 pomoću (I)
8.	A → (¬ B → (¬ B ∧ A))	prijedloška tautologija
9.	A → [(B?; Α) *] (¬ B → (¬ B ∧ A))	od 7 i 8 koristeći monotoniju [(B?; α) *] i propozicioniranje
10.	[¬ B?] (¬ B ∧ A) ↔ (¬ B → (¬ B ∧ A))	Shema aksioma (A4)
11.	A → [(B?; Α) *] [¬ B?] (¬ B ∧ A)	od 9 i 10 koristeći monotoniju [(B?; α) *] i propozicioniranje
12.	[(B?; Α) *; ¬ B?] (¬ B ∧ A) ↔ [(B?; Α) *] [¬ B?] (¬ B ∧ A)	shema aksioma (A1)
13.	A → [(B?; Α) *; ¬ B?] (¬ B ∧ A)	od 12. pomoću prijedloga obrazloženja
-	{A} dok B činite α {¬ B ∧ A}

U kontekstu PDL-a, dva posljedica pravila zapravo su posebni slučajevi pravila o sastavu. Da se postigne prvi pravilo, zamjena α ₁ s α i α ₂ s preskočiti. Kako bi se dobio drugi pravilo, zamjena α ₁ s preskočiti i α ₂ s α. Dovoljno je primijeniti aksiomsku shemu (A4) i primijetiti da je [α; preskoči] A ↔ [α] A i [α; preskoči] A ↔ [α] A se također može odrediti ⊢ za sve A i sve α.

3.3 Potpuna ispravnost

Prema Hoareovom priznanju u Hoareu [1979], njegov izvorni račun bio je samo polazna osnova i pretrpio je prilično ograničenja. Osobito, on dopušta samo jedan razlog za djelomičnu ispravnost. Odnosno, istina izjave {A} α {B} samo osigurava da će se sve egzekucije α koja počinju u stanju koje zadovoljava A završiti u stanju koji zadovoljava B, ili neće zaustaviti. Odnosno, djelomično ispravan program može imati neizvršene izvršavanje. (U stvari, program koji nema izvršenje završetka uvijek će biti djelomično točan. To je slučaj na primjer programa dok 1 preskače. Formula A → [ dok 1 ne preskočite] B se može zaključiti za sve formule A i B.) Izračun ne nudi osnovu za dokaz prekida programa. Može se izmijeniti kako bi se uzela u obzir potpuna ispravnost programa: djelomična ispravnost plus raskid. To se postiže izmjenom pravila iteracije. Ovdje ga ne predstavljamo i zainteresiranog čitatelja upućujemo na Apt [1981].

Primijetimo najprije da se za determinirane programe već može uhvatiti potpuna ispravnost pomoću takvih formula

A → B

Izraz B znači da postoji izvršenje α koje završava u stanju koji zadovoljava B. Štoviše, ako je α deterministički, ovo moguće okončanje izvršenja jedinstveno je izvršenje α. Dakle, ako se prvo uspije dokazati da je program determiniran, ovaj trik djeluje dovoljno dobro da dokaže njegovu potpunu ispravnost.

Općenito rješenje problema potpune ispravnosti postoji u području PDL-a. Ali moramo ga malo produljiti. Pratt je u Prattu [1980b] već aludirao da PDL nije dovoljno ekspresivan da bi uhvatio beskonačno petljanje programa. U reakciju, Streett [1982] uveo je PDL sa ponavljanjem (RPDL). Sadrži, za sve programe α, izraz Δα koji stoji za novi prijedlog sa semantikom

V (Δα) = {x: postoji beskonačan niz x ₀, x ₁,… stanja takvih da je x ₀  = x i za sva n ≥ 0, x _n R (α) x _{n +1} }

Streett [1982] je pretpostavio da se RPDL može aksiomatizirati dodavanjem preciznom sustavu PDL-a točno slijedećim aksiomama.

(A6) Δα → Δα

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

Dokaz pretpostavke pružen je u Sakalauskaite i Valiev [1990]. (Verzija pretpostavke u varijanti kombiniranog PDL također je dokazana u Gargov i Passy [1988].)

Lako je vidjeti da u Hoareovom računu koji je prikazan gore, ne-prekid može doći samo iz pravila iteracije. Analogno tome, ne-prekid PDL programa može doći samo korištenjem neograničene iteracije. Izraz Δα ukazuje da se α * može razilaziti, a to je upravo ona vrsta pojma koja nam je potrebna. Sada možemo induktivno definirati predikat ∞, tako da će za program α, formula ∞ (α) biti točna točno kad α može ući u računanje koje nema kraja.

∞ (π): = 0 gdje je π ∈ Π ₀

∞ (φ?): = 0

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

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

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

Konačno, potpuna ispravnost programa može se izraziti takvim formulama

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

što doslovno znači da ako je slučaj A, onda se program α ne može vječno pokretati i svaka uspješna izvedba završit će u stanju koji zadovoljava B.

4. Neke varijante

Rezultati koji se tiču komparativne moći izražavanja, odlučnosti, složenosti, aksiomatizacije i cjelovitosti niza varijanti PDL-a dobivenih proširivanjem ili ograničavanjem njegove sintakse i njegove semantike čine predmet velike literature. Toliko možemo reći, a mi ćemo se pozabaviti samo nekim od ovih inačica, ostavljajući velike dijelove inače važnog rada u dinamičkoj logici.

4.1 PDL bez testova

Čini se da shema aksioma [A?] B ↔ (A → B) ukazuje da za svaku formulu C postoji ekvivalentna formula bez testa bez testiranja, tj. Da postoji formula bez test-a C 'takva da je ⊨ C ↔ C '. Zanimljivo je primijetiti da je ta tvrdnja neistinita. Neka PDL ₀ bude ograničenje PDL-a na redovne programe bez testa, tj. Programe koji ne sadrže testove. Berman i Paterson [1981] razmatrali su PDL formulu <(p?; Π) *; ¬ p?; Π; p?> 1, što je

< dok p do π> p

i dokazao da ne postoji PDL ₀ formula jednaka istoj. Dakle, PDL ima ekspresivniju moć od PDL-a ₀. Njihov argument se zapravo može generalizirati na sljedeći način. Za svih n ≥ 0, neka je PDL _{n +1} podskup PDL-a u kojem programi mogu sadržavati testove A? samo ako je A PDL _n formula. Za svih n ≥ 0, Berman i Paterson smatrali su PDL _{n +1} formulu A _{n +1} definiranu s

< dok A _n do π _n > <π _n > A _n

gdje su A ₀  = p i π ₀  = π, a dokazano je da za sve n ≥ 0, ne postoji PDL _n formula ekvivalentna A _{n +1}. Dakle, za svih n ≥ 0, PDL _{n +1} ima veću izražajnu moć od PDL _n.

4.2 PDL sa obrnutim

CPDL je proširenje PDL-a sa obrnutim. To je konstrukt koji se razmatra od početka PDL-a. Za sve programe α, neka α ^-1 stoji za novi program sa semantikom

x R (α ^-1) y i y y R (α) x.

Konverzni konstrukt omogućava nam da izrazimo činjenice o stanjima koja su prethodila trenutnom i da rasuđujemo o unatrag oko programa. Na primjer, [α ^-1] A znači da se prije izvršavanja α moralo održati A. Imamo

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

Dodavanje obrnutog konstrukta ne mijenja svojstva PDL-a na bilo koji značajan način. Dodavanjem svake instance sljedećih aksiomskih shema:

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

(A9) A → [α ^-1] A

do sustava dokaza PDL-a dobivamo zvuk i potpunu prevodljivost na proširenom jeziku. Pojedinosti potražite u Parikh [1978]. CPDL ima svojstvo malog modela i (CPDL-SAT) je EXPTIME.

Lako je primijetiti da CPDL ima više izražajne moći od PDL-a. Da biste to vidjeli, razmotrite formulu CPDL <π ^-1 > 1 i LTSs M = (W, R, V) i M '= (W', R ', V') gdje je W = {x, y}, R (π) = {(x, y)}, W '= {y'}, R '(π) = ∅ i V (x) = V (y) = V' (y ') = ∅. Budući da je M, y sat <π ^-1 > 1, a ne M ', y' sat <π ^-1 > 1, i jer je za sve PDL formule A slučaj da je M, y sat A iff M ', y' sat A, tada je jasno da nijedna PDL formula nije ekvivalentna <π ^-1 > 1.

4.3 PDL s ponavljanjem i petljom

Već smo otkrili moć ponavljanja u odjeljku 3.3 uvođenjem RPDL-a. Ovdje ćemo sažeti više rezultata o RPDL-u i njegovoj povezanosti s drugim varijacijama na pojmu ponavljanja programa.

Što se tiče teorije složenosti RPDL-a, Streett [1982] je već utvrdio da RPDL ima svojstvo konačnog modela; upravo je ta da je svaka RPDL formula A koja je zadovoljavajuća u modelu veličine koja ima najviše trostruko eksponencijalnu duljinu A. Automatski teoretski argument dopuštao je zaključak da se problem (RPDL-SAT) može riješiti u determinističkom trostrukom eksponencijalnom vremenu (3-EXPTIME). Tako je otvoren jaz između ove gornje granice za odlučivanje (RPDL-SAT) i jednostavne donje granice eksponencijalnog vremena za odlučivanje (PDL-SAT). Problem se našao u velikoj mjeri s rastućim interesom računalnih znanstvenika za utvrđivanjem složenosti vremenske logike, točnije (prijedloga) modalnog kalkuliranja (MMC) zbog Kozena [1983], jer RPDL ima linearni udarac gore prijevod na MMC. Osim toga,Streettov argument donekle postavlja presedan u sve raširenijoj upotrebi tehnika automata u dokazivanju računskih svojstava logike programa i vremenske logike. U Vardi i Stockmeyeru [1985] prikazana je gornja granica u nedeterminističkom eksponencijalnom vremenu. U Emersonu i Jutli [1988], a u konačnom obliku u Emersonu i Jutli [1999], pokazano je da su (MMC-SAT) i (RPDL-SAT) EXPTIME-kompletni. Ako dodamo obratni operator iz odjeljka 4.2, dobiva se CRPDL. Složenost (CRPDL-SAT) ostala je otvorena nekoliko godina, ali može se pokazati da je i EXPTIME-potpun. To se postiže kombiniranjem tehnika Emersona i Jutle [1988] i Vardi [1985], kao u Vardi [1998]. U Vardi i Stockmeyeru [1985] prikazana je gornja granica u nedeterminističkom eksponencijalnom vremenu. U Emersonu i Jutli [1988], a u konačnom obliku u Emersonu i Jutli [1999], pokazano je da su (MMC-SAT) i (RPDL-SAT) EXPTIME-kompletni. Ako dodamo obratni operator iz odjeljka 4.2, dobiva se CRPDL. Složenost (CRPDL-SAT) ostala je otvorena nekoliko godina, ali može se pokazati da je i EXPTIME-potpun. To se postiže kombiniranjem tehnika Emersona i Jutle [1988] i Vardi [1985], kao u Vardi [1998]. U Vardi i Stockmeyeru [1985] prikazana je gornja granica u nedeterminističkom eksponencijalnom vremenu. U Emersonu i Jutli [1988], a u konačnom obliku u Emersonu i Jutli [1999], pokazano je da su (MMC-SAT) i (RPDL-SAT) EXPTIME-kompletni. Ako dodamo obratni operator iz odjeljka 4.2, dobiva se CRPDL. Složenost (CRPDL-SAT) ostala je otvorena nekoliko godina, ali može se pokazati da je i EXPTIME-potpun. To se postiže kombiniranjem tehnika Emersona i Jutle [1988] i Vardi [1985], kao u Vardi [1998]. Složenost (CRPDL-SAT) ostala je otvorena nekoliko godina, ali može se pokazati da je i EXPTIME-potpun. To se postiže kombiniranjem tehnika Emersona i Jutle [1988] i Vardi [1985], kao u Vardi [1998]. Složenost (CRPDL-SAT) ostala je otvorena nekoliko godina, ali može se pokazati da je i EXPTIME-potpun. To se postiže kombiniranjem tehnika Emersona i Jutle [1988] i Vardi [1985], kao u Vardi [1998].

U odjeljku 3.3 definirali smo predikat ∞, gdje ∞ (α) znači da α može imati računanje bez kraja. LPDL nazivamo logikom dobivenom dopunjavanjem PDL predikatom ∞. Jasno je da je RPDL barem toliko ekspresivan kao i LPDL; O tome svjedoči induktivna definicija ∞ (α) u jeziku RPDL. RPDL je u stvari strogo izraženiji od LPDL-a. To je prikazano u Harel i Sherman [1982]. Kao što se može sumnjati, i RPDL i LPDL imaju više izražajne moći od PDL-a. Dokazano je dokazivanjem da neke formule RPDL i LPDL nemaju ekvivalentni izraz u PDL. Dokaz uključuje tehniku filtracije koja je zamišljena da sruši LTS na konačni model, a ostavljajući invarijantnom istinu ili neistinu određenih formula. Za neki skup PDL formula X,ona se sastoji u grupiranju u klase ekvivalencije stanja LTS-a koja zadovoljavaju potpuno iste formule u X. Tako dobiven skup klasa ekvivalencije stanja postaje skup stanja filtrata, a preko njih se primjereno gradi prijelaz.

Pažljivo odabranim setom FL (A) koji ovisi o PDL formuli A (tzv. Fischer-Ladnerovo zatvaranje skupa pod-formula A), filtriranje LTS M daje konačni filtrat M ', takav da je A zadovoljavajući u svijetu u u M ako i samo ako je zadovoljavajući u razredu ekvivalencije koji sadrži u u filtratu. (Vidi Fischer i Ladner [1979].)

Sada možemo razmotriti filtracije LTS M = (W, R, V) gdje

• W = {(i, j): j i i cijeli brojevi, 0 ≤ j ≤ i} ∪ {u}
• (i, j) R (π) (i, j -1) kad je 1 ≤ j ≤ i
• u R (π) (i, i) za svaki i
• V (p) = ∅ za svaki p ∈ Φ ₀

U jednoj rečenici ono što se događa u M jest da iz svijeta u dolazi beskonačan broj konačnih π-staza rastuće duljine. Imamo i M, u sat ¬Δπ i M, u sat ¬∞ (π *). Ipak, za svaku PDL formulu A imat ćemo i Δπ i ∞ (π *) koji su zadovoljeni u ekvivalentnoj klasi u u modelu dobivenom filtracijom M s FL (A). Doista, filtracija mora urušiti neka stanja M i stvoriti neke petlje. Dakle, ne postoji PDL formula koja može izraziti ili Δπ ili ∞ (π *). pa ipak, imat ćemo i Δπ i ∞ (π *) koji su zadovoljeni u ekvivalentnoj klasi u u bilo kojem konačnom M filtratu. Dakle, ni Δπ niti ∞ (π *) se ne mogu izraziti u PDL-u.

Postoje i drugi načini koji omogućuju tvrdnju da se program može zauvijek izvršiti. Na primjer, Danecki [1984a] predložio je kazneno sloop kvalificirati programe koji mogu ući u jakim petlje, i to:

V (sloop (α)) = {x: x R (α) x}

Nazovimo SLPDL logikom dobivenom povećanjem PDL-a sa sloop (α). RPDL i SLPDL su u suštini neusporediva: predikat Δ nije odrediv u SLPDL, a predikat sloop nije odrediv u RPDL. SLPDL ne posjeduje svojstvo konačnog modela. Na primjer, formula

[π *] (1 ∧ ¬ nagib (π ⁺))

zadovoljava se samo u beskonačnim LTS-ovima. Unatoč tome, Danecki [1984a] je utvrdio decidabilnost formula (SLPDL-SAT) u determinističkom eksponencijalnom vremenu.

4.4 PDL s sjecištem

Proučen je još jedan konstrukt: sjecište programa. Dodavanjem sjecišta programa PDL-u dobivamo logički IPDL. U IPDL-u, za sve programe α, β, izraz α∩β označava novi program sa semantikom

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

Na primjer, namjeravano čitanje A je da ako izvršimo α i β u sadašnjem stanju, tada postoji stanje dostupno oba programa, a koje zadovoljava A. Kao rezultat toga, imamo

⊨ A → A ∧ A

ali, općenito, imamo

ne ⊨ A ∧ A → A

Iako sjecište programa igra važnu ulogu u raznim primjenama PDL-a na umjetnu inteligenciju i računalnu znanost, teorija dokaza i teorija složenosti PDL-a s sjecištem ostala su neistražena nekoliko godina. Što se tiče teorije složenosti IPDL-a, pojavljuju se poteškoće kada se razmotri svojstvo konačnog modela. Zapravo, konstrukcijski nagib (α) može se izraziti u IPDL. U prijedloškoj dinamičkoj logici s sjecištem ono je ekvivalentno 1. Možemo prilagoditi formulu IPDL iz odjeljka 4.3. I imamo to

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

zadovoljava se samo u beskonačnim LTS-ovima. Drugim riječima, IPDL ne posjeduje svojstvo konačnog modela. Danecki [1984b] je istraživao teoriju složenosti IPDL-a i pokazao da se odlučivanje (IPDL-SAT) može obaviti u determinističkom dvostrukom eksponencijalnom vremenu. (Moderni dokaz predstavljen je u Göller, Lohrey i Lutz [2007].) Razmak složenosti između ove dvostruke gornje granice eksponencijalnog vremena za odlučivanje (IPDL-SAT) i jednostavne donje granice eksponencijalnog vremena za odlučivanje (PDL-SAT) dobiveni od Fischera i Ladnera [1979], ostao je otvoren više od dvadeset godina. Lange [2005] je 2004. uspostavio donju granicu eksponencijalnog prostora (IPDL-SAT). 2006. god. Lange i Lutz [2005] dali su dokaz dvostruke eksponencijalno-vremenske donje granice problema zadovoljavanja za IPDL bez testova redukcijom s riječnog problema eksponencijalno ograničenih prostora na Turingovim strojevima. U ovom smanjenju uloga konstrukcije ponavljanja je ključna budući da je, prema Massacci [2001], problem zadovoljavanja za IPDL bez iteracije bez testova samo PSPACE-i. Dodavanjem obrnutog konstrukta u IPDL, dobivamo ICPDL. Göller, Lohrey i Lutz [2007] pokazali su da je problem zadovoljavanja ICPDL-a 2-EXPTIME-kompletan. Göller, Lohrey i Lutz [2007] pokazali su da je problem zadovoljavanja ICPDL-a 2-EXPTIME-kompletan. Göller, Lohrey i Lutz [2007] pokazali su da je problem zadovoljavanja ICPDL-a 2-EXPTIME-kompletan.

Što se tiče teorije dokaza IPDL-a, pojavljuju se poteškoće kada shvatimo da nijedna aksiomska shema, na jeziku PDL-a s presjekom, "odgovara" semantičkoj x R (α∩β) y iff x R (α) y i x R (β) y programa α∩β. To jest, ne na isti način, na primjer, da aksiomske sheme (A1) i (A2) "odgovaraju" semantičkim programima α; β i α∪β. Iz tog razloga, aksiomatizacija PDL-a s presijecanjem bila je otvorena sve dok cijeli sustav dokaza nije razvijen u Balbiani-u i Vakarelovu [2003].

U drugoj varijanti PDL-a, zbog Pelega (1987.) i koju je dalje proučio Goldblatt [1992b], izraz α∩β se tumači „do α i β paralelno“. U tom kontekstu, binarni odnosi R (α) i R (β) više nisu skupovi parova oblika (x, y) s svjetovima x, y, već skupovi parova oblika (x, Y) s xa svijet i Y skup svjetova. Inspirirala ga je Igra logike Parikh [1985], interpretacija PDL-a s "programima kao igrama". Igra logika pruža dodatnu konstrukciju programa koja dualistira programe, omogućujući tako definiranje sjecišta programa kao dvojnika nedeterminističkog izbora između programa.

5. Zaključak

Ovaj se članak usredotočio na dinamiku logike prijedloga i neke njegove značajne varijante. Do sada postoji niz knjiga - Goldblatt [1982], Goldblatt [1992a], Harel [1979] i Harel, Kozen i Tiuryn [2000] i istraživački radovi - Harel [1984], Kozen i Tiuryn [1990], Parikh [1983] - obrada PDL-a i srodnih formalizama. Tijelo istraživanja PDL-a sigurno je od velike važnosti u razvoju mnogih logičkih teorija dinamike sustava. Međutim, te teorije mogu se isključiti iz okvira ovog članka. Van Eijck i Stokhof [2006] noviji je pregled tema koje koriste dinamičku logiku, baveći se raznim temama koje su zanimljive za filozofe: npr. Dinamikom komunikacije ili semantikom prirodnog jezika. Nedavne knjige mnogo su detaljnije o novijim temama,poput dinamičke logike znanja (dinamička epistemička logika) u Van Ditmarschu, Van Der Hoek i Kooi [2007], i dinamičke logike kontinuiranih i hibridnih sustava (diferencijalna dinamička logika) u Platzeru [2010]. PDL je zamišljen prvenstveno zbog razmišljanja o programima. Postoje mnoge druge primjene modalne logike za zaključivanje o programima. Algoritamska logika bliža je PDL-u jer omogućuje eksplicitni razgovor o programima. Čitatelja se poziva da se savjetuje s radom proučenim u Mirkovskoj i Salwicki [1987]. Vremenska logika sada je glavna logika u teorijskoj računalnoj znanosti i usko je povezana s logikom programa. Omogućuju izražavanje vremenskog ponašanja tranzicijskih sustava jezikom koji apstrahira dalje od naljepnica (otuda i programi). Pogledajte primjerice Schneider [2004] za pregled osnova u ovom istraživačkom području.

Bibliografija

• Apt, K., 1981, „Deset godina Hoareove logike: Istraživanje - I dio“, ACM transakcije na programskim jezicima i sustavima, 3 (4): 431–483.
• Balbiani, P., i D. Vakarelov, 2003, „PDL s sjecištem programa: potpuna aksiomatizacija“, časopis za primijenjenu neklasičnu logiku, 13: 231-276.
• van Benthem, J., 1998, „Konstrukcije programa sigurne za bisimulaciju“, Studia Logica, 60: 311–330.
• Berman, F. i M. Paterson, 1981, "Propozicijska dinamika je slabija bez testova", Teoretska računalna znanost, 16: 321–328.
• Burstall, R., 1974, „Programiranje dokazano kao simulacija ruku s malo indukcije“, Obrada informacija 74: Zbornik radova IFIP kongresa 74, Amsterdam: North Holland Publishing Company, 308–312.
• Danecki, R., 1984a, „Propoziciona dinamička logika s jakim predikatom petlje“, u M. Chytil i V. Koubek, Matematički temelji računalnih znanosti, Berlin: Springer-Verlag, 573-581.
• –––, 1984b, „Neslušana dinamička logika prijedloga s presijecanjem je odlučujuća“, u: A. Skowron (ur.), Teorija računanja, Berlin: Springer-Verlag, 34-53.
• De Giacomo, G. i F. Massacci, 2000, „Kombiniranje dedukcije i provjere modela u tablici i algoritmi za obrnuti PDL“, Informacije i računanje, 160: 109–169.
• van Ditmarsch, H., W. van Der Hoek i B. Kooi, 2007, Dinamička epiztemska logika, Dordrecht: Springer-Verlag.
• van Eijck, J. i M. Stokhof, 2006, "Raspon dinamičke logike", u D. Gabbay i J. Woods (ur.), Priručnik povijesti logike, svezak 7- Logika i modaliteti u Twentieth Century, Amsterdam: Elsevier, 499–600.
• Emerson, E. i Jutla, C., 1988., "Složenost drvenih automata i logike programa (prošireni sažetak)", u Zborniku 29. godišnjeg simpozija o osnovama računarskih znanosti, Los Alamitos, Kalifornija: IEEE Computer Society, 328–337.
• –––, 1999., „Složenost drvenih automata i logike programa“, u SIAM časopisu za računarstvo, 29: 132–158.
• Engeler, E., 1967, „Algoritmička svojstva struktura“, Teorija matematičkih sustava, 1: 183–195.
• Fischer, M. i R. Ladner, 1979, "Propoziciona dinamika redovitih programa", časopis za računalne i sistemske znanosti, 18: 194–211.
• Floyd, R., 1967, „Dodjeljivanje značenja programima“, Zbornik radova Simpozija o primijenjenoj matematici Američkog matematičkog društva (svezak 19), Providence, RI: Američko matematičko društvo, 19–31.
• Gargov, G. i S. Passy, 1988., "Određivanje i petlje u kombiniranom PDL-u", Teorijska računalna znanost, Amsterdam: Elsevier, 259–277.
• Goldblatt, R., 1982, Axiomatising the Logic of Computer Programming, Berlin: Springer-Verlag.
• –––, 1992a, Logika vremena i računanja, Stanford: Centar za proučavanje jezičnih i informacijskih publikacija.
• –––, 1992b, „Paralelno djelovanje: Istodobna dinamička logika s neovisnim modalitetima“, Studia Logica, 51: 551–578.
• Göller, S., M. Lohrey i C. Lutz, 2007, „PDL sa sjecištem i obratom je kompletan 2EXP“, Temelji softverske znanosti i računskih struktura, Berlin: Springer, 198–212.
• Harel, D., 1979, dinamička logika prvog reda, Berlin: Springer-Verlag.
• –––, 1983, „Ponavljajuće se domine: čineći krajnje nerazumljivim vrlo razumljivim“, u M. Karpinski (ur.), Temelji teorije računanja, Berlin: Springer-Verlag, 177–194.
• –––, 1984, „Dinamička logika“, u D. Gabbay i F. Guenthner (ur.), Priručnik filozofske logike (svezak II), Dordrecht: D. Reidel, 497–604.
• Harel, D., D. Kozen i J. Tiuryn, 2000, Dynamic Logic, Cambridge, MA: MIT Press.
• Harel, D. i Sherman, R., 1982, „Looping vs. Ponavljanje u dinamičkoj logici“, Informacije i kontrola, 55: 175–192.
• Hoare, C., 1969, „Aksiomatična osnova za računalno programiranje“, Komunikacije Udruženja računskih strojeva, 12: 576–580.
• Kozen, D., 1983, „Rezultati propozicijskog-kalkula“, Teoretska informatika, 27: 333–354.
• Kozen, D. i R. Parikh, 1981., „Elementarni dokaz cjelovitosti PDL-a“, Teorijska informatika, 14: 113–118.
• Kozen, D. i J. Tiuryn, 1990, "Logika programa", u J. Van Leeuwen (ur.), Priručnik teorijskih računalnih znanosti (svezak B), Amsterdam: Elsevier, 789–840.
• Lange, M., 2005, "Donja složenost ograničena za prijedlošku dinamičku logiku s presijecanjem", u: R. Schmidt, I. Pratt-Hartmann, M. Reynolds i H. Wansing (ur.), Napredovanje u modalnoj logici (svezak 5), London: King's College Publikacije, 133–147.
• Lange, M. i C. Lutz, 2005, "2-EXPTIME niže granice za prijedloge dinamičke logike s presijecanjem", Journal of Symbolic Logic, 70: 1072–1086.
• Lutz, C., 2005, „PDL sa sjecištem i obratom je decidabilno“. U L. Ong (ur.), Computer Science Logic, Berlin: Springer-Verlag, 413-427.
• Massacci, F., 2001, „Postupci odlučivanja za izražajne logike opisa s presijecanjem, sastavom, preokretom uloga i identitetom uloga“, u B. Nebel (ur.), 17. međunarodna zajednička konferencija o umjetnoj inteligenciji, San Francisco: Morgan Kaufmann, 193-198.
• Mirkowska, G. i A. Salwicki, 1987., Algoritamska logika, Dordrecht: D. Reidel.
• Nishimura, H., 1979, "Sekvencijalna metoda u prijedložnoj dinamičkoj logici", Acta Informatica, 12: 377–400.
• Parikh, R., 1978, „Potpunost dinamike logike prijedloga“, u J. Winkowski (ur.), Matematički temelji računalnih znanosti, Berlin: Springer-Verlag, 1978, 403-415.
• –––, 1983, „Propoziciona logika programa: novi smjerovi“, u M. Karpinski (ur.), Temelji teorije računanja, Berlin: Springer-Verlag, 347-359.
• –––, 1985., „Logika igara i njezine primjene“, Anali diskretne matematike, 24: 111–140.
• Peleg, D., 1987, „Paralelna dinamička logika“, časopis Asocijacije za računske strojeve, 34: 450–479.
• Platzer, A., 2010, Logička analiza hibridnih sustava: Dokazivanje teorema za složenu dinamiku, Berlin: Springer, 2010.
• Pratt, V., 1976., „Semantička razmatranja o Floyd-Hoareovoj logici“, u Zbornicima 17. IEEE-ovog simpozija o osnovama računarskih znanosti, Los Alamitos, CA: IEEE Computer Society, 109–121.
• –––, 1978., „Praktična metoda odlučivanja o dinamičkoj logici prijedloga“, Zbornik radova 10. godišnjeg simpozija ACM-a o teoriji računarstva, New York, NY: ACM, 326–337.
• –––, 1980a, „Gotovo optimalna metoda za zaključivanje o djelovanju“, časopis za računalne i sistemske znanosti, 20: 231–254.
• –––, 1980b, „Primjena modalne logike u programiranju“, Studia Logica, 39: 257–274.
• Sakalauskaite, J. i M. Valiev, 1990, "Potpunost dinamike logike prijedloga s beskonačnim ponavljanjem", u P. Petkov (ur.), Matematička logika, New York: Plenum Press, 339–349.
• Salwicki, A., 1970, "Formalizirani algoritmički jezici", Bilten de l'Academie Polonaise des Sciences, Serie des matematike znanosti, astronomike i fizike, 18: 227–232.
• Segerberg, K., 1977, „Teorem cjelovitosti u modalnoj logici programa“, Obavijesti American Mathematical Society, 24: 522.
• Schneider, K., 2004, Verifikacija reaktivnih sustava, Berlin: Springer-Verlag.
• Streett, R., 1982, „Propozicijska dinamika petlje i obrnuto je elementarno odlučujuća“, Informacije i kontrola, 54: 121–141.
• Vakarelov, D., 1983, „Teorema filtracije za dinamičke algebre s testovima i inverznim operatorom“, u A. Salwicki (ur.), Logika programa i njihove primjene, Berlin: Springer-Verlag, 314–324.
• Vardi, M., 1985, „Ukroćivanje obrnutosti: rasuđivanje o dvosmjernom računanju“, u Bilješke predavanja iz informatike (svezak 193), Berlin-Heidelberg: Springer, 413–423.
• –––, 1998, „Razmišljanje o prošlosti dvosmjernim automatama“, u predavanjima Bilješke iz računalnih znanosti (svezak 1443), Berlin-Heidelberg: Springer, 628–641.
• Vardi, M. i Stockmeyer, L., 1985, „Poboljšane gornje i donje granice modalne logike programa: preliminarno izvješće“, u zborniku Zbornika 17. godišnjeg simpozija ACM-a o teoriji računanja, New York, NY: ACM, 240 -251.
• Yanov, J., 1959, “O ekvivalentnosti shema operatora”, Problemi kibernetike, 1: 1–100.

Akademske alate

	Kako navesti ovaj unos.
	Pregledajte PDF verziju ovog unosa na Društvu prijatelja SEP-a.
	Pogledajte ovu temu unosa na projektu Internet Filozofska ontologija (InPhO).
	Poboljšana bibliografija za ovaj unos na PhilPapersu, s vezama na njegovu bazu podataka.

Ostali internetski resursi

[Molimo kontaktirajte autora s prijedlozima.]