Propositionele Dynamische Logica

2023 Auteur: Noah Black | [email protected]. Laatst gewijzigd: 2023-11-26 16:11

Toegang navigatie

• Inhoud van het item
• Bibliografie
• Academische hulpmiddelen
• Vrienden PDF-voorbeeld
• Info over auteur en citaat
• Terug naar boven

Propositionele dynamische logica

Voor het eerst gepubliceerd op 1 februari 2007; inhoudelijke herziening vr 25 jan.2019

Logica van programma's zijn modale logica die voortkomt uit het idee om met elk computerprogramma α van een programmeertaal een modaliteit [α] te associëren. Dit idee komt voort uit de lijn van werken van Engeler [1967], Hoare [1969], Yanov [1959] en anderen die logische talen hebben geformuleerd en bestudeerd waarin de eigenschappen van programmaconnectives kunnen worden uitgedrukt. De algoritmische logica (AL) die voor het eerst is ontwikkeld door Salwicki [1970] en de dynamische logica (DL) die is uitgewerkt door Pratt [1976] zijn goede voortzettingen van deze werken. We zullen ons hier concentreren op DL. Uit de talrijke artikelen die zijn gewijd aan DL en zijn varianten, evenals de veelzijdige toepassingen ervan in programmaverificatie en gegevensstructuren, blijkt dat het een nuttig hulpmiddel is bij het bestuderen van eigenschappen van programma's. Pratt koos ervoor om DL af te beelden op wat men het eerste-orde niveau zou kunnen noemen,en het was zijn werk dat Fischer en Ladner [1979] ertoe bracht een paar jaar later de propositionele variant van DL te definiëren. Dit artikel presenteert een inleiding tot PDL, de propositionele variant van DL.

• 1. Inleiding

• 2. Definities en fundamentele resultaten

  • 2.1 Syntaxis en semantiek
  • 2.2 Axiomatisatie en volledigheid
  • 2.3 Beslisbaarheid en complexiteit

• 3. Gestructureerde programmering en correctheid van programma's

  • 3.1 Hoare calculus
  • 3.2 Hoare calculus en PDL
  • 3.3 Totale correctheid

• 4. Enkele varianten

  • 4.1 PDL zonder tests
  • 4.2 PDL met omgekeerde
  • 4.3 PDL met herhalen en herhalen
  • 4.4 PDL met kruispunt
• 5. Conclusie
• Bibliografie
• Academische hulpmiddelen
• Andere internetbronnen
• Gerelateerde vermeldingen

1. Inleiding

Dynamic Logics (DL) zijn modale logica's voor het weergeven van de toestanden en gebeurtenissen van dynamische systemen. De taal van DL's is zowel een beweringstaal die eigenschappen van berekeningstoestanden kan uitdrukken, als een programmeertaal die eigenschappen van systeemovergangen tussen deze toestanden kan uitdrukken. DL's zijn logica's van programma's en maken het mogelijk te praten en te redeneren over zaken, processen, veranderingen en resultaten.

De oorspronkelijke dynamische logica van programma's van Pratt was een modale logica van de eerste orde. Propositionele dynamische logica (PDL) is de propositionele tegenhanger ervan. Het werd op zichzelf gepresenteerd als een logica in Fischer en Ladner [1979]. Omdat het propositioneel is, maakt de taal van PDL geen gebruik van termen, predikaten of functies. In PDL zijn er dus twee syntactische categorieën: proposities en programma's.

Om betekenis te geven aan uitspraken in PDL, werken we doorgaans met een abstracte semantiek in termen van Labeled Transition Systems (LTS). LTS's kunnen worden gezien als een generalisatie van Kripke-modellen, waarbij overgangen tussen werelden of staten worden "gelabeld" met namen van atoomprogramma's. Een taxatie geeft voor elke staat aan welke proposities daarin kloppen. Een overgang met het label π van een staat x naar een staat y-genoteerd x R (π) y of (x, y) ∈ R (π) -geeft aan dat vanaf x er een mogelijke uitvoering van het programma π is dat eindigt in y. Als de propositie A waar is in y, dan is de formule A waar in x: dat wil zeggen, in de toestand x is er een mogelijke uitvoering van het programma α dat eindigt in een toestand die voldoet aan A. Men herkent in een modaliteit die doet denken aan de modaliteit van mogelijkheid (vaak opgemerkt ◊) van modale logica. Niet verrassend,er is ook een bijbehorend idee van noodzaak (waarvan de modaliteit vaak wordt opgemerkt □). De formule [π] A is waar in de toestand x als A waar is in elke toestand die bereikbaar is vanaf x door een overgang met het label π.

De mogelijke uitvoeringen van complexe programma's kunnen vervolgens compositiebepaald worden. Een programma 'eerst α, dan β' is bijvoorbeeld een complex programma, meer specifiek een reeks. Een mogelijke uitvoering kan worden weergegeven in een LTS door een tweestapsovergang samen te stellen - vandaar een overgang die kan worden aangeduid met R (α; β) - tussen de toestanden x en x ': er is een mogelijke uitvoering in x van het programma α die eindigt in een staat y en er is een mogelijke uitvoering in y van het programma β dat eindigt op x '. Als de propositie A waar is in x ', dan is de formule A waar in de toestand x. De programma's α en β kunnen zelf een complex programma zijn. Nog meer programma's kunnen worden uitgedrukt met meer constructen die we te zijner tijd zullen presenteren.

Een programma wordt dan op een extensieve manier bekeken: het is een binaire relatie tussen toestandsparen van een LTS. Het is precies de set van paren van de vorm (x, y) zodat het programma kan worden uitgevoerd in de toestand x en kan leiden tot de toestand y. Aan de andere kant is een voorstel een verklaring over een staat; het is waar of onwaar in een staat. Een propositie kan dus ook op een extensieve manier worden bekeken: de verzameling toestanden van de LTS waar deze waar is.

Met de afkorting PDL verwijzen we hier precies naar de propositionele dynamische logica met de volgende programmaconstructies: sequentie, niet-deterministische keuze, onbegrensde iteratie en test. We presenteren het in sectie 2, samen met enkele eigenschappen en fundamentele resultaten. We zullen in het bijzonder ingaan op de axiomatisatie en de beslisbaarheid ervan.

De Hoare-calculus van Hoare [1969] is een mijlpaal voor logica van programma's. Het betreft de waarheid van uitspraken in de vorm {A} α {B} - wat betekent dat met de voorwaarde A het programma α altijd B heeft als postconditie - en axiomatisch wordt gedefinieerd. Het komt door een gebrek aan rigoureuze methoden om te redeneren over de eigenschappen van programma's, en zo de activiteit van programmeren een bepaalde plaats te geven in het rijk van de wetenschap. Burstall [1974] zag de analogie tussen modale logica en redenering over programma's, maar het eigenlijke werk eraan begon met Pratt [1976] toen het hem werd voorgesteld door R. Moore, een student van hem in die tijd. PDL komt van Pratts interpretatie van Hoare's calculus in het formalisme van modale logica. Een inleiding tot het ontstaan van PDL is te vinden in Pratt [1980b]. De Hoare-triple {A} α {B} wordt vastgelegd door de PDL-formule A → [α] B, wat letterlijk betekent dat als A waar is, dan zal elke succesvolle beëindiging van de uitvoering van α eindigen met B als waar. Met deze verbinding gerealiseerd, is het een routine om de initiële regels van Hoare's calculus te bewijzen met uitsluitend de axiomatisatie van PDL. Dit is iets dat we in detail zullen doen in paragraaf 3, die zich richt op de redenering over de juistheid van gestructureerde programma's.

Bijkomende onderwerpen met betrekking tot PDL zijn onder meer resultaten betreffende vergelijkende uitdrukkingskracht, beslisbaarheid, complexiteit en volledigheid van een aantal interessante varianten die zijn verkregen door PDL op verschillende manieren uit te breiden of te beperken. Sinds de oprichting hebben veel varianten van PDL aandacht gekregen. Deze varianten kunnen deterministische programma's, beperkte tests, niet-reguliere programma's, programma's als automaten, complementatie en kruising van programma's, omgekeerde en oneindige berekeningen, enz. Overwegen. We zullen er enkele in paragraaf 4 presenteren, met enkele aanwijzingen met betrekking tot hun relatieve expressiviteit, hun axiomatisaties en hun computationele complexiteit.

We sluiten af in paragraaf 5.

2. Definities en fundamentele resultaten

We presenteren de syntaxis en semantiek van PDL in paragraaf 2.1. De bewijstheorie van PDL wordt gepresenteerd in paragraaf 2.2 met axiomatisaties en verwijzingen naar de literatuur over volledigheid. We behandelen het probleem van beslisbaarheid en complexiteit in paragraaf 2.3.

2.1 Syntaxis en semantiek

Propositionele dynamische logica (PDL) is ontworpen voor het representeren en redeneren over propositionele eigenschappen van programma's. De syntaxis is gebaseerd op twee sets symbolen: een telbare set Φ ₀ van atoomformules en een telbare set Π ₀ van atoomprogramma's. Complexe formules en complexe programma's over deze basis worden als volgt gedefinieerd:

• Elke atoomformule is een formule
• 0 ("false") is een formule
• Als A een formule is, dan is ¬ A ("niet A") een formule
• Als A en B formules zijn, dan is (A ∨ B) ("A of B") een formule
• Als α een programma is en A een formule, dan is [α] A ("elke uitvoering van α vanuit de huidige toestand leidt tot een toestand waarin A waar is") een formule
• Elk atoomprogramma is een programma
• Als α en β programma's zijn, dan is (α; β) ("do α gevolgd door β") een programma
• Als α en β programma's zijn, dan is (α∪β) ("do α of β, niet-deterministisch") een programma,
• Als α een programma is, is α * ("herhaal α een eindig, maar niet-deterministisch bepaald aantal keren") een programma.
• Als A een formule is, dan A? ("Ga verder als A waar is, anders mislukt") is een programma

De andere Booleaanse connectieven 1, ∧, → en ↔ worden standaard als afkortingen gebruikt. Bovendien verkorten we ¬ [α] ¬ A tot A ("enige uitvoering van α vanuit de huidige toestand leidt tot een toestand waarin A waar is") zoals in de modale logica. We schrijven α ⁿ voor α;…; α met n keer α. Meer formeel:

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

Ook:

α ⁺ = _df α; α *

is vaak nuttig om een niet-begrensde iteratie weer te geven die minstens één keer voorkomt. Ten slotte hanteren we de standaardregels voor het weglaten van haakjes.

Formules kunnen worden gebruikt om de eigenschappen te beschrijven die behouden blijven na de succesvolle uitvoering van een programma. De formule [α∪β] A betekent bijvoorbeeld dat wanneer programma α of β met succes wordt uitgevoerd, een toestand wordt bereikt waar A geldt, terwijl formule A betekent dat er een reeks afwisselende uitvoeringen van α en β is, zodat een staat wordt bereikt waar A geldt. Semantisch gesproken worden formules geïnterpreteerd door sets van staten en worden programma's geïnterpreteerd door binaire relaties over staten in een overgangssysteem. Meer precies, de betekenis van PDL-formules en -programma's wordt geïnterpreteerd over gelabelde overgangssystemen (LTS) M = (W, R, V) waar W een niet-lege verzameling werelden of toestanden is, R is een afbeelding van de verzameling Π ₀ van atomaire programma's in binaire relaties op W en V is een afbeelding van de set Φ ₀ van atoomformules in subsets van W.

Informeel wijst de afbeelding R aan elk atoomprogramma π ∈ Π ₀ een binaire relatie R (π) toe op W met de bedoelde betekenis x R (π) y als er een uitvoering van π van x bestaat die naar y leidt, terwijl de afbeelding V wijst aan elke atoomformule p ∈ Φ ₀ een deelverzameling V (p) van W toe met de bedoelde betekenis x ∈ V (p) als f p waar is in x. Gezien onze metingen van 0, ¬ A, A ∨ B, [α] A, α; β, α∪β, α * en A?, Is het duidelijk dat R en V inductief als volgt moeten worden uitgebreid om de beoogde betekenissen te leveren voor de complexe programma's en formules:

• x R (α; β) y als er een wereld z bestaat zodat x R (α) z en z R (β) y
• x R (α∪β) y iff x R (α) y of x R (β) y
• x R (α *) y als er een niet-negatief geheel getal n bestaat en er werelden z ₀, …, z _{n zijn} zodat z ₀  = x, z _n  = y en voor alle k = 1.. n, z _{k -1} R (α) z _k
• x R (A?) y iff x = y en y ∈ V (A)
• V (0) = ∅
• V (¬ A) = W / V (A)
• V (A ∨ B) = V (A) ∪ V (B),
• V ([α] A) = {x: voor alle werelden y, als x R (α) y dan y ∈ V (A)}

Als x ∈ V (A) dan zeggen we dat A tevreden is in toestand x in M, of "M, x zat A".

Noem M de LTS hierboven links afgebeeld en M 'de LTS rechts afgebeeld. Formeel gedefinieerd hebben we M = (W, R, V) met W = {x ₁, x ₂ }, R (π ₁) = {(x ₁, x ₁)}, R (π ₂) = {(x ₁, x ₂)}, V (p) = {x ₁ }, V (q) = {x ₂ }, en we hebben M '= (W', R ', V') met W '= {y ₁, y ₂, y ₃, y ₄ }, R (π ₁) = {(y ₁, y ₂), (y ₂, y ₂)}, R '(π₂) = {(y ₁, y ₃), (y ₂, y ₄)}, V '(p) = {y ₁, y ₂ }, V' (q) = {y ₃, y ₄ }. We hebben bijvoorbeeld:

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

Overweeg nu een formule A. We zeggen dat A geldig is in M of dat M een model is van A, of "M ⊨ A", iff voor alle werelden x, x ∈ V (A). A is geldig, of "⊨ A", indien voor alle modellen M, M ⊨ A. We zeggen dat A bevredigend is in M of dat M voldoet aan A, of "M sat A", als er een wereld x bestaat zodat x ∈ V (A). A wordt als bevredigend beschouwd, of "zat A", als er een model M bestaat zodat M sat A. Interessant is dat

zat A indien niet ⊨ ¬ A

⊨ A indien niet niet ¬ A

Enkele opmerkelijke formules van PDL zijn geldig. (De lezer kan proberen ze formeel te bewijzen, of op zijn minst zichzelf te overtuigen van de enkele hierboven weergegeven voorbeelden.)

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

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

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

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

Evenzo kunnen we ze in hun dubbele vorm schrijven.

⊨ A ↔ A

⊨ A ↔ A ∨ A

⊨ A ↔ A ∨ A

⊨ <A?> B ↔ A ∧ B

Een interessant idee betreft de hoeveelheid informatie, uitgedrukt in PDL-formules, die in een LTS is vervat. Het gedrag van een systeem dat wordt beschreven als een LTS is inderdaad vaak enigszins verborgen in zijn vorm. Bij eenvoudige inspectie is het bijvoorbeeld gemakkelijk om uzelf ervan te overtuigen dat de twee hierboven afgebeelde LTS's hetzelfde gedrag vertonen en aan dezelfde PDL-formules voldoen. Om deze sectie over syntaxis en semantiek af te sluiten, geven we de theoretische basis van deze beweringen.

Bij twee LTS's kan men zich afvragen of ze aan dezelfde formules voldoen. Het begrip bisimulatie is de standaardmaatstaf geworden voor de gelijkwaardigheid van Kripke-modellen en gelabelde overgangssystemen. Een bisimulatie tussen de LTSs M = (W, R, V) en M '= (W', R ', V') is een binaire relatie Z tussen hun toestanden zodat voor alle werelden x in M en voor alle werelden x ' in M ', als xZx' dan

• voor alle atoomformules p ∈ Φ ₀, x ∈ V (p) iff x '∈ V' (p)
• voor alle atoomprogramma's π ∈ Π ₀ en voor alle werelden y in M, als x R (π) y dan bestaat er een wereld y 'in M' zodat yZy 'en x' R '(π) y'
• voor alle atoomprogramma's π ∈ Π ₀ en voor alle werelden y 'in M', als x 'R' (π) y 'dan bestaat er een wereld y in M zodat yZy' en x R (π) y

We zeggen dat twee LTS's bisimilar zijn wanneer er een bisimulatie tussen bestaat. Het is sinds het begin van PDL bekend dat in twee bisimilar LTSs M en M ', voor alle werelden x in M en voor alle werelden x' in M ', als xZx' dan voor alle PDL-formules A, x ∈ V (A) iff x '∈ V' (A). Dus als twee LTS's bisimilar zijn onder de definitie van bisimulatie hierboven, is het zo dat, als xZx 'dan

• voor alle programma's α en voor alle werelden y in M, als x R (α) y dan bestaat er een wereld y 'in M' zodat yZy 'en x' R '(α) y'
• voor alle programma's α en voor alle werelden y 'in M', als x 'R' (α) y 'dan bestaat er een wereld y in M zodat yZy' en x R (α) y

Daarom kan men het gedrag van twee LTS's eenvoudig vergelijken door alleen de atoomprogramma's te inspecteren en veilig te extrapoleren naar het vergelijkende gedrag van deze LTS's, zelfs voor complexe programma's. We zeggen dat de programmaconstructies van PDL veilig zijn voor bisimulatie. Zie Van Benthem [1998] voor nauwkeurige karakterisering van programmaconstructies die veilig zijn voor bisimulatie.

Het is gemakkelijk te zien dat de twee bovenstaande LTS's vergelijkbaar zijn. Een bisimulatie Z tussen M en M 'kan worden gegeven als: Z = {(x ₁, y ₁), (x ₁, y ₂), (x ₂, y ₃), (x ₂, y ₄)}. De toestanden x ₁ en y ₁ voldoen aan exact dezelfde PDL-formules. Dus doe de toestanden x ₁ en y ₂, enz.

2.2 Axiomatisatie en volledigheid

Het doel van de bewijstheorie is het karakteriseren van de eigenschap ⊨ A in termen van axioma's en gevolgtrekkingen. In deze sectie definiëren we een inductief predicaat ⊢ inductief door bewerkingen op formules die alleen afhankelijk zijn van hun syntactische structuur op een zodanige manier dat voor alle formules A,

⊢ Een iff ⊨ A.

Natuurlijk is PDL een uitbreiding van de klassieke propositionele logica. We verwachten eerst dat alle propositionele tautologieën geldig zijn en dat alle propositionele redenering is toegestaan. Met name modus ponens is een geldige regel: van A en A → B afleiden B. Voor elk programma α, dat een LTS beperkt tot de relatie R (α), verkrijgen we een Kripke-model waarin de logica van de modaliteit [α] de zwakste propositionele normale modale logica is, namelijk de logica K. PDL bevat dus elke instantie van het bekende distributie axioma schema:

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

en het is gesloten onder de volgende inferentieregel (noodzakelijkheidsregel):

(N) uit A leiden [a] A af.

Een modale logica is normaal als ze gehoorzaamt aan (A0) en (N). Belangrijke eigenschappen voor alle α zijn dat [α] zich over de conjunctie ∧ verspreidt, en de regel van eentonigheid, die het van A → B toestaat om [α] A → [α] B af te leiden, kan worden bewezen. Ten slotte is PDL de minst normale modale logica die elk exemplaar van de volgende axioma-schema's bevat

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

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

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

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

en gesloten onder de volgende inferentieregel (lusinvariantieregel):

(I) van A → [α] A leiden A → [α *] A af

Als X een reeks formules is en A een formule is, dan zeggen we dat A ⊢ afleidbaar is van X of "X ⊢ A", als er een reeks A ₀, A ₁, … bestaat, A _n van formules zodat A _n  = A en voor alle i ≤ n, A _i is een instantie van een axioma-schema, of een formule van X, of komt uit eerdere formules van de reeks door een inferentieregel. Verder ⊢ A iff ∅ ⊢ A; in dit geval zeggen we dat A ⊢ aftrekbaar is. X zou ⊢-consistent zijn, zo niet X ⊢ 0. Het is gemakkelijk vast te stellen dat (I) kan worden vervangen door het volgende axioma-schema (inductie axioma-schema):

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

Laten we eerst vaststellen dat (I) een afgeleide regel is van het bewijssysteem gebaseerd op (A1), (A2), (A3), (A4) en (A5):

1.	A → [α] A	premisse
2.	[α *] (A → [α] A)	vanaf 1 met (N)
3.	[α *] (A → [α] A) → (A → [α *] A)	axioma schema (A5)
4.	A → [α *] A	van 2 en 3 met modus ponens

Laten we vervolgens vaststellen dat (A5) ⊢-aftrekbaar is:

1.	[α *] (A → [α] A) ↔ (A → [α] A) ∧ [α] [α *] (A → [α] A)	axioma schema (A3)
2.	A ∧ [α *] (A → [α] A) → [α] (A ∧ [α *] (A → [α] A))	vanaf 1 met propositioneel redeneren en distributiviteit van [α] over ∧
3.	A ∧ [α *] (A → [α] A) → [α *] (A ∧ [α *] (A → [α] A))	vanaf 2 met (I)
4.	[α *] (A → [α] A) → (A → [α *] A)	vanaf 3 met propositioneel redeneren en distributiviteit van [α *] over ∧

De axiomatisatie van PDL op basis van axiomaschema's (A1), (A2), (A3), (A4) en (A5) is voorgesteld in Segerberg [1977]. Het is direct uit de bovenstaande definities dat ⊢ gezond is met betrekking tot ⊨, dat wil zeggen

Voor alle formules A, als ⊢ A, dan ⊨ A

Het bewijs wordt geleverd door inductie op de duur van de aftrek van A in ⊢. De vraag naar de volledigheid van ⊢ met betrekking tot ⊨, dat wil zeggen,

Voor alle formules A, als ⊨ A, dan ⊢ A

werd nagestreefd door verschillende logici. De redenering in Segerberg [1977] was de eerste poging om de volledigheid van ⊢ te bewijzen. Al snel kwam Parikh ook met een bewijs. Toen Segerberg begin 1978 een fout vond in zijn argument (dat hij uiteindelijk herstelde), publiceerde Parikh in Parikh [1978] wat kan worden beschouwd als het eerste bewijs van de volledigheid van ⊢. Sindsdien zijn verschillende bewijzen van volledigheid van published gepubliceerd, bv. Kozen en Parikh [1981].

Er is ook gezocht naar verschillende alternatieve bewijstheorieën van PDL. Zelfs al vroeg, met name in Pratt [1978]. Laten we dan ook de volledigheid noemen van verwante theorieën van Nishimura [1979] en Vakarelov [1983].

Een alternatieve formulering van een afleidbaarheidspredikaat voor PDL maakt het gebruik van een oneindige inferentieregel mogelijk, zoals bijvoorbeeld in Goldblatt [1992a]. (Een oneindige regel van gevolgtrekking heeft een oneindig aantal premissen.) Laat ⊢ 'het afleidbaarheidspredikaat zijn dat correspondeert in de taal van de propositionele dynamische logica met de minst normale modale logica die elk exemplaar van de axioma-schema's bevat (A1), (A2), (A3) en (A4) en gesloten onder de volgende oneindige regel van gevolgtrekking:

(I ') van {[β] [α ⁿ] A: n ≥ 0} afleiden [β] [α *] A

Het kan worden bewezen dat ⊢ 'zowel gezond als compleet is met respect ⊨, dat wil zeggen,

Voor alle formules A, ⊢ 'A iff ⊨ A

Met andere woorden, voor het genereren van de verzameling van alle geldige formules zijn de bewijssystemen ⊢ en ⊢ 'equivalent.

2.3 Beslisbaarheid en complexiteit

Het doel van de complexiteitstheorie is om de berekenbaarheid van de eigenschap sat A vast te stellen in termen van tijd of ruimte. De complexiteit van een logische L wordt vaak geïdentificeerd met het probleem van het bepalen van de bevrediging van de formules, gedefinieerd als:

(L-SAT) Gegeven een formule A van L, is A bevredigend?

In deze sectie onderzoeken we de complexiteit van het volgende beslissingsprobleem:

(PDL-SAT) Is A, gegeven formule A van PDL, bevredigend?

De volledige axiomatisatie van PDL is een recursieve definitie van de set geldige PDL-formules, of met andere woorden, van de set formules waarvan de negatie niet bevredigend is. Daarom hebben we met betrekking tot het probleem (PDL-SAT) een subprocedure die "nee" zou antwoorden als de PDL-formule A niet bevredigend zou zijn. De subprocedure (SP1) bestaat uit het opsommen van alle formules ⊢-afleidbaar, uitgaande van de axioma's en het afleiden van andere stellingen met behulp van de inferentieregels. Als een formule ⊢-afleidbaar is, zou de subprocedure er bij voldoende tijd uiteindelijk in slagen. Dus als A niet bevredigend is, moet (SP1) uiteindelijk ¬ A vinden en "nee" antwoorden als dat wel het geval is.

Als de formule A echter bevredigend is, zal (SP1) ¬ A nooit vinden. Het zou voor altijd blijven bestaan en men kon er op geen enkel moment zeker van zijn. Maar er is een uitweg uit deze onzekerheid. We kunnen ook een tweede subprocedure bedenken die "ja" antwoordt als een PDL-formule bevredigend is. Een van de eerste resultaten op PDL was inderdaad het bewijs dat PDL de eindige modeleigenschap heeft, dwz

Voor alle formules A, als sat A, dan bestaat er een eindig model M zodat M sat A.

De eindige modeleigenschap biedt een basis voor een subprocedure (SP2) die bestaat uit het één voor één opsommen van de eindige modellen van PDL en testen of een ervan voldoet aan de formule. (Voor alle formules A en voor alle eindige modellen M is het gemakkelijk om te testen of M sat A door de definitie van V (A) toe te passen.) Dus als A bevredigend is, moet het uiteindelijk een model M vinden zodat M sat A en antwoord "ja" als dat het geval is. Symmetrisch aan de eerste subprocedure (SP1), als de formule A niet bevredigend is, zal (SP2) nooit een model vinden dat eraan voldoet, het zal voor altijd lopen en men kan er op geen enkel moment zeker van zijn.

Door nu (SP1) en (SP2) samen te combineren, kunnen we beslissen of een PDL-formule A bevredigend is. Het is voldoende om ze parallel uit te voeren: als A bevredigend is, zal (SP2) uiteindelijk "ja" antwoorden, als A niet bevredigend is, zal (SP1) uiteindelijk "nee" antwoorden. De procedure stopt wanneer (SP1) of (SP2) een antwoord geeft.

Als de verkregen procedure voldoende is om te concluderen dat het probleem (PDL-SAT) beslissend is, is het in de praktijk zeer ineffectief. Er is een resultaat te danken aan Fischer en Ladner [1979] en Kozen en Parikh [1981] - sterker dan de eindige modeleigenschap, dat is een kleine modeleigenschap:

Voor alle formules A, als sat A dan bestaat er een eindig model M van exponentiële grootte in A zodat M sat A.

Dit betekent dat we nu zouden weten wanneer we moeten ophouden met het zoeken naar een model dat voldoet aan een formule in de procedure (SP2). Daarom kunnen we (SP2) gebruiken om te testen of een formule bevredigend is, maar zodra we alle kleine modellen hebben uitgeput, kunnen we concluderen dat de formule niet bevredigend is. Dit levert een procedure op die niet-deterministisch verloopt in exponentiële tijd (NEXPTIME): raad een model van hoogstens afzonderlijk exponentieel en controleer of het voldoet aan de formule. Maar de belangrijkste resultaten in de complexiteitstheorie van PDL komen van Fischer en Ladner [1979] en Pratt [1980a]. Fischer en Ladner [1979] constateerden dat een formule van PDL de berekening van een lineaire ruimte-begrensde alternerende Turing-machine efficiënt kan beschrijven, en stelden eerst de ondergrens van de exponentiële tijd van (PDL-SAT) vast. De EXPTIME bovengrens van (PDL-SAT) is verkregen door Pratt [1980a],die het equivalent voor PDL van de methode van tableaux gebruikte. (PDL-SAT) is dus EXPTIME-compleet. (Een algoritme dat in de praktijk efficiënter is, hoewel het in het ergste geval nog steeds in een deterministische exponentiële tijd loopt, wordt voorgesteld in De Giacomo en Massacci [2000].)

3. Gestructureerde programmering en correctheid van programma's

Historisch gezien komen logica van programma's voort uit het werk aan het eind van de jaren zestig van informatici die geïnteresseerd waren in het toekennen van betekenis aan programmeertalen en het vinden van een rigoureuze standaard voor bewijzen over de programma's. Dergelijke bewijzen kunnen bijvoorbeeld gaan over de juistheid van een programma met betrekking tot verwacht gedrag, of over het beëindigen van een programma. Een baanbrekende paper is Floyd [1967], die een analyse van de eigenschappen van gestructureerde computerprogramma's met stroomdiagrammen presenteert. Sommige vroege werken zoals Yanov [1959] of Engeler [1967] hadden geavanceerde en bestudeerde formele talen waarin de eigenschappen van programmaconnectives kunnen worden uitgedrukt. Het formalisme van Hoare [1969] was een mijlpaal in de komst van PDL. Het werd voorgesteld als een rigoureuze axiomatische interpretatie van de stroomschema's van Floyd. We praten vaak over Hoare-logica, of Floyd-Hoare-logica,of Hoare-calculus bij verwijzing naar dit formalisme. Hoare calculus houdt zich bezig met de waarheid van uitspraken ("Hoare triples"), zoals {A} α {B} die een verband legt tussen een voorwaarde A, een programma α en een postconditie B. Het geeft aan dat wanneer A geldt als voorwaarde voor de uitvoering van α, B geldt als voorwaarde na de succesvolle uitvoering van α.

Het was enkele decennia geleden waar, en het is nog steeds het geval: het valideren van een programma wordt vaker wel dan niet gedaan door het te testen op een redelijke verscheidenheid aan inputs. Wanneer een invoer niet de verwachte uitvoer oplevert, is de "bug" opgelost. Als we uiteindelijk voor elke geteste input de verwachte output krijgen, is er een redelijke overtuiging dat het programma geen fouten bevat. Dit is echter een tijdrovende validatiemethode en laat plaats voor niet-geteste invoer die zou mislukken. Het vinden van deze fouten nadat het programma is geïmplementeerd en in gebruik is genomen, kost nog meer middelen. Redeneren over programmacorrectheid met formele methoden is cruciaal voor kritieke systemen, omdat het een manier is om uitputtend te bewijzen dat een programma geen fouten bevat.

3.1 Hoare calculus

Om het soort principes van programma's te illustreren die door de regels in de Hoare-calculus zijn vastgelegd, volstaat het om er enkele te raadplegen. (NB: de regels betekenen dat als alle uitspraken boven de regelregel de premissen bevatten - dan geldt ook de verklaring onder de regelregel - de conclusie).)

{A} α 1 {B} {B} α 2 {C}	(regel van samenstelling)
{A} α 1; α 2 {C}

De compositieregel legt de elementaire sequentiële compositie van programma's vast. Als premisse hebben we twee aannames over de partiële correctheid van twee programma's α ₁ en α ₂. De eerste aanname is dat wanneer α ₁ wordt uitgevoerd in een toestand die aan A voldoet, het zal eindigen in een toestand die aan B voldoet, telkens wanneer het stopt. De tweede veronderstelling is dat wanneer α ₂ wordt uitgevoerd in een toestand die voldoet aan B, hij zal eindigen in een toestand die voldoet aan C, wanneer hij stopt. De conclusie van de regel gaat over de gedeeltelijke correctheid van het programma α ₁; α ₂ (dwz α ₁ sequentieel samengesteld met α ₂), dat volgt uit de twee veronderstellingen. We kunnen namelijk concluderen dat als α ₁; α ₂ wordt uitgevoerd in een toestand die voldoet aan A, het eindigt in een toestand die voldoet aan C, wanneer het stopt.

De iteratieregel is belangrijk omdat deze het essentiële vermogen van programma's vastlegt om een deel van de code herhaaldelijk uit te voeren totdat een bepaalde voorwaarde niet meer geldig is.

{A ∧ B} α {A}	(regel van iteratie)
{A} terwijl B niet α {Â B ∧ A}

Ten slotte zijn de twee consequentieregels van fundamenteel belang om een formele basis te geven voor een intuïtief heldere redenering met respectievelijk zwakkere postcondities en sterkere voorwaarden.

{A} α {B} B → C	(regel van gevolg 1)
{A} α {C}

C → A {A} α {B}	(regel van gevolg 2)
{C} α {B}

Uit het formalisme dat in Hoare [1969] wordt gepresenteerd, laten we de axioma-schema's weg omdat het een eerste-orde taal zou vereisen. Ten slotte worden in het daaropvolgende werk aan Hoare-logica vaak ook meer regels toegevoegd. Zie Apt [1979] voor een vroeg overzicht.

3.2 Hoare calculus en PDL

Dynamische logica komt van Pratts interpretatie van Hoare-triples en Hoare-calculus in het formalisme van modale logica. Met de modaliteit [α] kunnen we formeel uitdrukken dat alle staten die bereikbaar zijn door α uit te voeren voldoen aan de formule A. Dit doet u door [α] A te schrijven. Zo wordt de Hoare triple {A} α {B} eenvoudig vastgelegd door de PDL-formule

A → [α] B

Bovendien kunnen belangrijke programmeerconstructies gemakkelijk in PDL worden geïntroduceerd door een afkorting van definities:

• als A dan α anders β = _df ((A?; α) ∪ (¬ A?; β))
• terwijl A doen α = _df ((A?; α) *; ¬ A?)
• herhaal α tot A = _df (α; ((¬ A; α) *; A?))
• afbreken = _df 0?
• skip = _df 1?

Het lijkt er dus op dat we met PDL goed uitgerust zijn om logisch de juistheid van gestructureerde programma's te bewijzen. Afgezien van deze nogal met de hand zwaaiende verbinding tussen PDL en Hoare-calculus, is het misschien nog niet duidelijk hoe ze zich formeel verhouden. PDL is in feite een veralgemening van Hoare calculus in die zin dat alle regels van de Hoare calculus bewezen kunnen worden in het axiomatische systeem van PDL. (Rigoureus bevat de Hoare-calculus axioma's die de uitgebreide taal van eerste-orde dynamische logica zouden vereisen.) Dit is vrij opmerkelijk, dus we zullen hier de twee bovenstaande regels laten zien om als voorbeeld te dienen.

De bewijzen beginnen door uit te gaan van de premissen van de regels. Door vervolgens gebruik te maken van deze aannames, axioma's en regels van PDL, en niets anders, is het doel vast te stellen dat de conclusie van de regels logisch volgt. Daarom beginnen we voor de compositieregel met het aannemen van {A} α ₁ {B}, dat wil zeggen A → [α ₁] B in zijn PDL-formulering, en door aan te nemen {B} α ₂ {C}, dat is B → [α ₂] C. Het doel is om te bewijzen dat {A} α ₁; α ₂ {C}. Precies, we willen vaststellen dat A → [α ₁; α ₂] C ⊢ af te leiden is uit de reeks formules {A → [α ₁] B, B → [α ₂] C}.

1.	A → [α 1] B	aanname {A} α 1 {B}
2.	B → [α 2] C	aanname {B} α 2 {C}
3.	[α 1] B → [α 1] [α 2] C	Vanaf 2 met eentonigheid van [α 1]
4.	A → [α 1] [α 2] C	van 1 en 3 met propositioneel redeneren
5.	[α 1; α 2] C ↔ [α 1] [α 2] C	axioma schema (A1)
6.	A → [α 1; α 2] C	van 4 en 5 met propositioneel redeneren
-	{A} α 1; α 2 {C}

Het bewijs van de iteratieregel is iets meer betrokken.

1.	A ∧ B → [α] A	aanname {A ∧ B} α {A}
2.	A → (B → [α] A)	vanaf 1 met propositioneel redeneren
3.	[B?] [Α] A ↔ (B → [α] A)	axioma schema (A4)
4.	A → [B?] [Α] A	van 2 en 3 met propositioneel redeneren
5.	[B?; α] A ↔ [B?] [α] A	axioma schema (A1)
6.	A → [B?; Α] A	van 4 en 5 met propositioneel redeneren
7.	A → [(B?; Α) *] A	vanaf 6 met (I)
8.	A → (¬ B → (¬ B ∧ A))	propositionele tautologie
9.	A → [(B?; Α) *] (¬ B → (¬ B ∧ A))	van 7 en 8 met eentonigheid van [(B?; α) *] en propositioneel redeneren
10.	[¬ B?] (¬ B ∧ A) ↔ (¬ B → (¬ B ∧ A))	Axioma-schema (A4)
11.	A → [(B?; Α) *] [¬ B?] (¬ B ∧ A)	van 9 en 10 met eentonigheid van [(B?; α) *] en propositioneel redeneren
12.	[(B?; Α) *; ¬ B?] (¬ B ∧ A) ↔ [(B?; Α) *] [¬ B?] (¬ B ∧ A)	axioma schema (A1)
13.	A → [(B?; Α) *; ¬ B?] (¬ B ∧ A)	vanaf 12 met propositioneel redeneren
-	{A} terwijl B niet α {Â B ∧ A}

In het kader van PDL zijn de twee consequentieregels in feite bijzondere gevallen van de compositieregel. Om de eerste regel te verkrijgen, vervangt u α ₁ door α en α ₂ door overslaan. Om de tweede regel te verkrijgen, vervangt u α ₁ door overslaan en α ₂ door α. Het volstaat om het axioma-schema (A4) toe te passen en op te merken dat [α; overslaan] A ↔ [α] A en [α; overslaan] A ↔ [α] A zijn ook ⊢ aftrekbaar voor alle A en alle α.

3.3 Totale correctheid

Volgens Hoare zelf in Hoare [1979] was zijn oorspronkelijke calculus slechts een startpunt en had hij nogal wat beperkingen. In het bijzonder laat het alleen toe om te redeneren over gedeeltelijke correctheid. Dat wil zeggen, de waarheid van een verklaring {A} α {B} zorgt er alleen voor dat alle uitvoeringen van α die beginnen in een toestand die voldoet aan A, eindigen in een toestand die voldoet aan B, of niet stoppen. Dat wil zeggen dat een gedeeltelijk correct programma mogelijk niet-beëindigende uitvoeringen heeft. (In feite, een programma dat geen terminating uitvoering heeft altijd gedeeltelijk correct. Dit is het geval bijvoorbeeld van het programma , terwijl 1 kan overslaan. De formule A → [ terwijl 1 doen overspringen] B is aftrekbaar voor alle formules A en B.) De calculus biedt geen basis voor een bewijs dat een programma eindigt. Het kan worden gewijzigd om rekening te houden met de totale correctheid van programma's: gedeeltelijke correctheid plus beëindiging. Dit wordt bereikt door de iteratieregel te wijzigen. We presenteren het hier niet en verwijzen de geïnteresseerde lezer naar Apt [1981].

Laten we eerst opmerken dat men voor deterministische programma's al volledige correctheid kan vastleggen via dergelijke formules

A → B

De uitdrukking B betekent dat er een uitvoering van α is die eindigt in een toestand die voldoet aan B. Bovendien, als α deterministisch is, is deze mogelijke beëindigende uitvoering de unieke uitvoering van α. Dus als men voor het eerst erin slaagt te bewijzen dat een programma deterministisch is, werkt deze truc goed genoeg om de totale juistheid ervan te bewijzen.

Een algemene oplossing voor het probleem van totale correctheid bestaat op het gebied van PDL. Maar we moeten het een beetje uitbreiden. Pratt had in Pratt [1980b] al gezinspeeld dat PDL niet expressief genoeg is om de oneindige looping van programma's vast te leggen. In reactie daarop werd PDL met herhaling (RPDL) geïntroduceerd door Streett [1982]. Het bevat voor alle programma's α de uitdrukking Δα die staat voor een nieuwe propositie met semantiek

V (Δα) = {x: er bestaat een oneindige reeks x ₀, x ₁, … van toestanden zodat x ₀  = x en voor alle n ≥ 0, x _n R (α) x _{n +1} }

Streett [1982] vermoedde dat RPDL axiomatisch kan worden gemaakt door aan het bewijssysteem van PDL precies de volgende axioma-schema's toe te voegen.

(A6) Δα → Δα

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

Het bewijs van het vermoeden werd geleverd in Sakalauskaite en Valiev [1990]. (Een versie van het vermoeden in de variant van combinatorische PDL werd ook bewezen in Gargov en Passy [1988].)

Het is gemakkelijk te zien dat in de hierboven gepresenteerde Hoare-calculus niet-beëindiging alleen kan komen uit de iteratieregel. Analoog kan het niet beëindigen van een PDL-programma alleen komen door het gebruik van de onbegrensde iteratie. De uitdrukking Δα geeft aan dat α * kan uiteenlopen, en dit is precies het soort idee dat we nodig hebben. We kunnen nu inductief een predikaat ∞ definiëren, zodat voor een programma α de formule ∞ (α) precies waar zal zijn wanneer α een niet-afsluitende berekening kan invoeren.

∞ (π): = 0 waarbij π ∈ Π ₀

∞ (φ?): = 0

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

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

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

Ten slotte kan de totale correctheid van een programma worden uitgedrukt via dergelijke formules

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

wat letterlijk betekent dat als A het geval is, het programma α niet voor altijd kan worden uitgevoerd en elke succesvolle uitvoering zal eindigen in een toestand die aan B voldoet.

4. Enkele varianten

Resultaten met betrekking tot vergelijkingsvermogen, beslisbaarheid, complexiteit, axiomatisatie en volledigheid van een aantal varianten van PDL verkregen door uitbreiding of beperking van de syntaxis en semantiek vormen het onderwerp van een schat aan literatuur. We kunnen slechts zoveel zeggen en we zullen slechts een paar van deze varianten behandelen, waarbij grote delen van verder belangrijk werk in dynamische logica worden weggelaten.

4.1 PDL zonder tests

Het axioma schema [A?] B ↔ (A → B) lijkt aan te geven dat er voor elke formule C een gelijkwaardige testvrije formule C '-ie bestaat, er is een testvrije formule C' zodat ⊨ C ↔ C '. Het is interessant op te merken dat deze bewering niet waar is. Laat PDL ₀ de beperking zijn van PDL tot testvrije reguliere programma's, dat wil zeggen programma's die geen tests bevatten. Berman en Paterson [1981] overwogen de PDL-formule <(p?; Π) *; ¬ p?; Π; p?> 1, dat is

< terwijl p doen π> p

en bewezen dat er geen PDL _0- formule is die daarmee equivalent is. Daarom heeft PDL meer expressieve kracht dan PDL ₀. Hun argument kan in feite als volgt worden gegeneraliseerd. Laat PDL _{n +1} voor alle n ≥ 0 de subset van PDL zijn waarin programma's tests A kunnen bevatten? alleen als A een PDL _n- formule is. Voor alle n ≥ 0 beschouwden Berman en Paterson de PDL _{n +1} formule A _{n +1} gedefinieerd door

< Terwijl een _n do π _n > <π _n > A _n

waar A ₀  = p en π ₀  = π en bewees dat er voor alle n ≥ 0 geen PDL _n- formule is die equivalent is aan A _{n +1}. Daarom heeft PDL _{n +1} voor alle n ≥ 0 meer expressieve kracht dan PDL _n.

4.2 PDL met omgekeerde

CPDL is de uitbreiding van PDL met converse. Het is een constructie die al sinds het begin van PDL is overwogen. Laat α ^-1 voor alle programma's α staan voor een nieuw programma met semantiek

x R (α ^-1) y als f y R (α) x.

De omgekeerde constructie stelt ons in staat feiten uit te drukken over toestanden die aan de huidige voorafgaan en achterwaarts te redeneren over programma's. [Α ^-1] A betekent bijvoorbeeld dat voordat A α moest uitvoeren, A moest vasthouden. Wij hebben

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

De toevoeging van het omgekeerde construct verandert de eigenschappen van PDL op geen enkele significante manier. Door elk exemplaar van de volgende axioma-schema's toe te voegen:

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

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

volgens het bewijssysteem van PDL verkrijgen we een gezond en volledig afleidbaarheidspredikaat in de uitgebreide taal. Zie Parikh [1978] voor details. CPDL heeft de kleine modeleigenschap en (CPDL-SAT) is EXPTIME-compleet.

Het valt gemakkelijk op te merken dat CPDL meer zeggingskracht heeft dan PDL. Bekijk om dit te zien de CPDL-formule <π ^-1 > 1 en de LTS's M = (W, R, V) en M '= (W', R ', V') waar W = {x, y}, R (π) = {(x, y)}, W '= {y'}, R '(π) = ∅ en V (x) = V (y) = V' (y ') = ∅. Aangezien M, y zat <π ^-1 > 1, niet M ', y' zat <π ^-1 > 1, en omdat voor alle PDL-formules A het geval is dat M, y zat A iff M ', y' zat A, dan is het duidelijk dat geen enkele PDL-formule equivalent is aan <π ^-1 > 1.

4.3 PDL met herhalen en herhalen

We hebben de kracht van herhalen in paragraaf 3.3 al blootgelegd door RPDL te introduceren. Hier vatten we meer resultaten samen over RPDL en het verband met andere variaties op het idee van herhalende programma's.

Wat betreft de complexiteitstheorie van RPDL had Streett [1982] al vastgesteld dat RPDL de eindige modeleigenschap had; precies dat elke RPDL-bevredigende formule A bevredigend is in een model van grootte dat hoogst drievoudig exponentieel is in de lengte van A. Een automaat-theoretisch argument om te concluderen dat het probleem (RPDL-SAT) kan worden opgelost in deterministische drievoudige exponentiële tijd (3-EXPTIME). De kloof tussen deze bovengrens voor beslissen (RPDL-SAT) en de eenvoudige exponentiële tijdondergrens voor beslissen (PDL-SAT) was dus open. Het probleem was sterk verbonden met de groeiende interesse van informatici om de complexiteit van temporele logica vast te stellen, en meer specifiek van de (propositionele) modale μ-calculus (MMC) als gevolg van Kozen [1983], omdat RPDL een lineaire slag heeft vertaling naar MMC. Bovendien,Streett's argument schiep enigszins een precedent in het nu alomtegenwoordige gebruik van automaattechnieken om de computationele eigenschappen van logica's van programma's en van temporele logica te bewijzen. In Vardi en Stockmeyer [1985] werd een bovengrens in niet-deterministische exponentiële tijd getoond. In Emerson en Jutla [1988] en in zijn definitieve vorm in Emerson en Jutla [1999] werd aangetoond dat (MMC-SAT) en (RPDL-SAT) EXPTIME-compleet zijn. Als we de omgekeerde operator van sectie 4.2 toevoegen, verkrijgt men CRPDL. De complexiteit van (CRPDL-SAT) bleef een paar jaar open, maar het kan ook worden aangetoond dat het EXPTIME-compleet is. Dit wordt bereikt door de technieken van Emerson en Jutla [1988] en Vardi [1985] te combineren, zoals in Vardi [1998]. In Vardi en Stockmeyer [1985] werd een bovengrens in niet-deterministische exponentiële tijd getoond. In Emerson en Jutla [1988] en in zijn definitieve vorm in Emerson en Jutla [1999] werd aangetoond dat (MMC-SAT) en (RPDL-SAT) EXPTIME-compleet zijn. Als we de omgekeerde operator van sectie 4.2 toevoegen, verkrijgt men CRPDL. De complexiteit van (CRPDL-SAT) bleef een paar jaar open, maar het kan ook worden aangetoond dat het EXPTIME-compleet is. Dit wordt bereikt door de technieken van Emerson en Jutla [1988] en Vardi [1985] te combineren, zoals in Vardi [1998]. In Vardi en Stockmeyer [1985] werd een bovengrens in niet-deterministische exponentiële tijd getoond. In Emerson en Jutla [1988] en in zijn definitieve vorm in Emerson en Jutla [1999] werd aangetoond dat (MMC-SAT) en (RPDL-SAT) EXPTIME-compleet zijn. Als we de omgekeerde operator van sectie 4.2 toevoegen, verkrijgt men CRPDL. De complexiteit van (CRPDL-SAT) bleef een paar jaar open, maar het kan ook worden aangetoond dat het EXPTIME-compleet is. Dit wordt bereikt door de technieken van Emerson en Jutla [1988] en Vardi [1985] te combineren, zoals in Vardi [1998]. De complexiteit van (CRPDL-SAT) bleef een paar jaar open, maar het kan ook worden aangetoond dat het EXPTIME-compleet is. Dit wordt bereikt door de technieken van Emerson en Jutla [1988] en Vardi [1985] te combineren, zoals in Vardi [1998]. De complexiteit van (CRPDL-SAT) bleef een paar jaar open, maar het kan ook worden aangetoond dat het EXPTIME-compleet is. Dit wordt bereikt door de technieken van Emerson en Jutla [1988] en Vardi [1985] te combineren, zoals in Vardi [1998].

In paragraaf 3.3 hebben we een predikaat ∞ gedefinieerd, waarbij ∞ (α) betekent dat α een niet-afsluitende berekening kan hebben. We noemen LPDL de logica die wordt verkregen door PDL te vergroten met het predikaat ∞. Het is duidelijk dat RPDL minstens zo expressief is als LPDL; De inductieve definitie van ∞ (α) in de taal van RPDL is hiervan getuige. RPDL is in feite strikt expressiever dan LPDL. Dit werd getoond in Harel en Sherman [1982]. Zoals te vermoeden, hebben zowel RPDL als LPDL meer expressieve kracht dan PDL. Het is bewezen door te bewijzen dat sommige formules van RPDL en van LPDL geen gelijkwaardige expressie hebben in PDL. Het bewijs omvat de filtratietechniek die is ontworpen om een LTS ineen te storten tot een eindig model, terwijl de waarheid of onwaarheid van bepaalde formules onveranderd blijft. Voor een aantal PDL-formules X,het bestaat uit het groeperen in equivalentieklassen van de toestanden van een LTS die voldoen aan exact dezelfde formules in X. De aldus verkregen reeks equivalentieklassen van toestanden wordt de verzameling van toestanden van het filtraatmodel en er wordt op passende wijze een overgang overheen gebouwd.

Met een zorgvuldig gekozen set FL (A) die afhankelijk is van een PDL-formule A (de zogenaamde Fischer-Ladner-sluiting van de set subformules van A), levert een filtratie van een LTS M een eindig filtraat M 'op, zoals dat A bevredigend is in een wereld u in M, en alleen als het bevredigend is in de equivalentieklasse die u in het filtraat bevat. (Zie Fischer en Ladner [1979].)

We kunnen nu de filtraties van de LTS M = (W, R, V) waar beschouwen

• W = {(i, j): j en i positieve gehele getallen, 0 ≤ j ≤ i} ∪ {u}
• (i, j) R (π) (i, j -1) wanneer 1 ≤ j ≤ i
• u R (π) (i, i) voor elke i
• V (p) = ∅ voor elke p ∈ Φ ₀

In één zin, wat er in M gebeurt, is dat er vanuit de wereld u een oneindig aantal eindige π-paden met groeiende lengte is. We hebben zowel M, u zat ¬Δπ als M, u zat ¬∞ (π *). Toch hebben we voor elke PDL-formule A zowel Δπ als ∞ (π *) die voldoen aan de equivalentieklasse van u in het model verkregen door filtratie van M met FL (A). Inderdaad, de filtratie moet sommige staten van M doen instorten en enkele lussen creëren. Er bestaat dus geen PDL-formule die Δπ of ∞ (π *) kan uitdrukken. en toch zullen we zowel Δπ als ∞ (π *) hebben die voldoen aan de equivalentieklasse van u in een eindig filtraat van M. Dus Δπ noch ∞ (π *) kunnen worden uitgedrukt in PDL.

Er zijn andere manieren om de bewering mogelijk te maken dat een programma voor altijd kan worden uitgevoerd. Danecki [1984a] stelde bijvoorbeeld een predicaat sloep voor om programma's te kwalificeren die in sterke lussen kunnen deelnemen, dat wil zeggen:

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

Laten we SLPDL de logica noemen die is verkregen door PDL uit te breiden met sloep (α). RPDL en SLPDL zijn in wezen onvergelijkbaar: het predikaat Δ is niet definieerbaar in SLPDL en het predikaat sloep is niet definieerbaar in RPDL. SLPDL bezit niet de eindige modeleigenschap. Bijvoorbeeld de formule

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

is alleen bevredigend in oneindige LTS's. Desalniettemin heeft Danecki [1984a] de beslisbaarheid van (SLPDL-SAT) formules in deterministische exponentiële tijd vastgesteld.

4.4 PDL met kruispunt

Een ander construct is onderzocht: het snijpunt van programma's. Door kruising van programma's aan PDL toe te voegen, verkrijgen we de logische IPDL. In IPDL staat voor alle programma's α, β de uitdrukking α∩β voor een nieuw programma met semantiek

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

De beoogde lezing van A is bijvoorbeeld dat als we α en β in de huidige toestand uitvoeren, er een staat is die door beide programma's kan worden bereikt en die aan A voldoet. Als resultaat hebben we

⊨ A → A ∧ A

maar over het algemeen hebben we

niet ⊨ A ∧ A → A

Hoewel het snijpunt van programma's een belangrijke rol speelt bij verschillende toepassingen van PDL op kunstmatige intelligentie en informatica, bleven de bewijstheorie en de complexiteitstheorie van PDL met kruispunt enkele jaren onontgonnen. Wat betreft de complexiteitstheorie van IPDL, verschijnen er moeilijkheden wanneer men de eindige modeleigenschap beschouwt. In feite kan het construct sloep (α) worden uitgedrukt in IPDL. In propositionele dynamische logica met kruising is het equivalent aan 1. We kunnen dus de formule van IPDL van sectie 4.3 aanpassen, en we hebben dat

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

is alleen bevredigend in oneindige LTS's. Met andere woorden, IPDL bezit niet de eindige modeleigenschap. Danecki [1984b] onderzocht de complexiteitstheorie van IPDL en toonde aan dat beslissen (IPDL-SAT) kan worden gedaan in deterministische dubbele exponentiële tijd. (Een modern bewijs wordt gepresenteerd in Göller, Lohrey en Lutz [2007].) De complexiteitskloof tussen deze dubbele bovengrens van de exponentiële tijd om te beslissen (IPDL-SAT) en de eenvoudige ondergrens van de exponentiële tijd om te beslissen (PDL-SAT) verkregen door Fischer en Ladner [1979] bleef meer dan twintig jaar open. Lange [2005] stelde in 2004 de ondergrens van de exponentiële ruimte van (IPDL-SAT) vast. In 2006,Lange en Lutz [2005] gaven een bewijs van een dubbele exponentiële tijd-ondergrens van het bevredigingsprobleem voor IPDL zonder tests door een reductie van het woordprobleem van exponentieel ruimtegebonden alternerende Turing-machines. Bij deze reductie is de rol van het iteratieconstruct essentieel, aangezien volgens Massacci [2001] het bevredigingsprobleem voor iteratievrije IPDL zonder tests slechts PSPACE-compleet is. Als we het omgekeerde construct aan IPDL toevoegen, verkrijgen we ICPDL. Het bevredigingsprobleem van ICPDL is door Göller, Lohrey en Lutz [2007] 2-EXPTIME-compleet gebleken. Het bevredigingsprobleem van ICPDL is door Göller, Lohrey en Lutz [2007] 2-EXPTIME-compleet gebleken. Het bevredigingsprobleem van ICPDL is door Göller, Lohrey en Lutz [2007] 2-EXPTIME-compleet gebleken.

Wat betreft de bewijstheorie van IPDL, verschijnen er moeilijkheden wanneer we ons realiseren dat geen axioma-schema, in de taal van PDL met kruispunt, “correspondeert” met de semantiek x R (α∩β) y iff x R (α) y en x R (β) y van het programma α∩β. Dat is bijvoorbeeld niet op dezelfde manier dat de axioma-schema's (A1) en (A2) respectievelijk "corresponderen" met de semantiek van de programma's α; β en α∪β. Om deze reden was de axiomatisatie van PDL met kruising open tot het volledige proof-systeem ontwikkeld in Balbiani en Vakarelov [2003].

In een andere variant van PDL wordt, dankzij Peleg [1987] en verder bestudeerd door Goldblatt [1992b], de uitdrukking α∩β geïnterpreteerd als "do α en β parallel". In deze context zijn de binaire relaties R (α) en R (β) niet langer sets van paren van de vorm (x, y) met x, y-werelden, maar eerder sets van paren van de vorm (x, Y) met x een wereld en Y een verzameling werelden. Het is geïnspireerd op de Game Logic van Parikh [1985], een intepretatie van PDL met 'programma's als games'. Game Logic biedt een extra programmaconstructie die programma's dualiseert, waardoor het mogelijk wordt om het snijpunt van programma's te definiëren als het dubbele van de niet-deterministische keuze tussen programma's.

5. Conclusie

Dit artikel heeft zich geconcentreerd op propositionele dynamische logica en enkele van zijn significante varianten. Er zijn inmiddels een aantal boeken - Goldblatt [1982], Goldblatt [1992a], Harel [1979] en Harel, Kozen en Tiuryn [2000] - en onderzoeksdocumenten - Harel [1984], Kozen en Tiuryn [1990], Parikh [1983] Behandeling van PDL en gerelateerde formalismen. De hoeveelheid onderzoek naar PDL is zeker behulpzaam bij het ontwikkelen van veel logische theorieën over systeemdynamica. Deze theorieën vallen echter aantoonbaar buiten het bestek van dit artikel. Van Eijck en Stokhof [2006] is een recenter overzicht van onderwerpen die gebruik maken van dynamische logica en die verschillende thema's behandelen die voor filosofen van bijzonder belang zijn: bv. Dynamiek van communicatie of semantiek van natuurlijke taal. Recente boeken gaan in op veel details over nieuwere onderwerpen,zoals dynamische logica van kennis (dynamische epistemische logica) in Van Ditmarsch, Van Der Hoek en Kooi [2007], en de dynamische logica van continue en hybride systemen (differentiële dynamische logica) in Platzer [2010]. PDL is in de eerste plaats bedacht om te redeneren over programma's. Er zijn veel andere toepassingen van modale logica voor het redeneren over programma's. Algoritmische logica ligt dichter bij PDL, omdat je hiermee expliciet over programma's kunt praten. De lezer wordt uitgenodigd om het in Mirkowska en Salwicki [1987] bestudeerde werk te raadplegen. Tijdelijke logica is nu de belangrijkste logica in de theoretische informatica en staat in nauw verband met de logica van programma's. Ze laten toe om het temporele gedrag van transitiesystemen uit te drukken met een taal die abstraheert van de labels (vandaar de programma's). Zie bijvoorbeeld Schneider [2004] voor een overzicht van de grondslagen op dit onderzoeksgebied.

Bibliografie

• Apt, K., 1981, 'Tien jaar Hoare's logica: een enquête - Deel I', ACM Transactions on Programming Languages and Systems, 3 (4): 431–483.
• Balbiani, P., en D. Vakarelov, 2003, "PDL met kruising van programma's: een complete axiomatisatie", Journal of Applied Non-Classical Logics, 13: 231-276.
• van Benthem, J., 1998, "Programmaconstructies die veilig zijn voor bisimulatie", Studia Logica, 60: 311–330.
• Berman, F. en M. Paterson, 1981, "Propositionele dynamische logica is zwakker zonder tests", Theoretische informatica, 16: 321–328.
• Burstall, R., 1974, "Programma bewijzen als handsimulatie met een beetje inductie", Informatieverwerking 74: Proceedings of IFIP Congress 74, Amsterdam: North Holland Publishing Company, 308–312.
• Danecki, R., 1984a, "Propositionele dynamische logica met een sterk luspredikaat", in M. Chytil en V. Koubek, Mathematical Foundations of Computer Science, Berlin: Springer-Verlag, 573-581.
• –––, 1984b, "Niet-deterministische propositionele dynamische logica met kruispunt is beslissend", in A. Skowron (red.), Computation Theory, Berlin: Springer-Verlag, 34-53.
• De Giacomo, G. en F. Massacci, 2000, "Combineren van aftrek en modelcontrole in tableaus en algoritmen voor converse-PDL", Informatie en berekening, 160: 109–169.
• van Ditmarsch, H., W. van Der Hoek en B. Kooi, 2007, Dynamic epistemic logic, Dordrecht: Springer-Verlag.
• van Eijck, J., en M. Stokhof, 2006, "The Gamut of Dynamic Logics", in D. Gabbay en J. Woods (red.), The Handbook of History of Logic, Volume 7- Logic and the Modalities in the Twentieth Century, Amsterdam: Elsevier, 499–600.
• Emerson, E., en Jutla, C., 1988, "The Complexity of Tree Automata and Logics of Programs (Extended Abstract)", in Proceedings of the 29th Annual Symposium on Foundations of Computer Science, Los Alamitos, CA: IEEE Computer Society, 328–337.
• –––, 1999, “The Complexity of Tree Automata and Logics of Programs”, in SIAM Journal of Computing, 29: 132–158.
• Engeler, E., 1967, "Algoritmische eigenschappen van structuren", Mathematical Systems Theory, 1: 183–195.
• Fischer, M. en R. Ladner, 1979, "Propositionele dynamische logica van reguliere programma's", Journal of Computer and System Sciences, 18: 194–211.
• Floyd, R., 1967, "Betekenis toekennen aan programma's", Proceedings of the American Mathematical Society Symposia on Applied Mathematics (Volume 19), Providence, RI: American Mathematical Society, 19–31.
• Gargov, G. en S. Passy, 1988, "Determinism and looping in combinatory PDL", Theoretical Computer Science, Amsterdam: Elsevier, 259–277.
• Goldblatt, R., 1982, Axiomatising the Logic of Computer Programming, Berlijn: Springer-Verlag.
• –––, 1992a, Logics of Time and Computation, Stanford: Centrum voor de studie van taal- en informatiepublicaties.
• –––, 1992b, “Parallel Action: Concurrent Dynamic Logic with Independent Modalities”, Studia Logica, 51: 551–578.
• Göller, S., M. Lohrey en C. Lutz, 2007, "PDL met kruising en omgekeerd is 2EXP-compleet", Foundations of Software Science and Computational Structures, Berlin: Springer, 198–212.
• Harel, D., 1979, First-Order Dynamic Logic, Berlijn: Springer-Verlag.
• –––, 1983, “Terugkerende dominostenen: het zeer onbeslisbare hoogst begrijpelijk maken”, in M. Karpinski (red.), Foundations of Computation Theory, Berlin: Springer-Verlag, 177–194.
• –––, 1984, "Dynamic logic", in D. Gabbay en F. Guenthner (red.), Handbook of Philosophical Logic (Deel II), Dordrecht: D. Reidel, 497–604.
• Harel, D., D. Kozen en J. Tiuryn, 2000, Dynamic Logic, Cambridge, MA: MIT Press.
• Harel, D. en Sherman, R., 1982, 'Looping vs. Repeating in Dynamic Logic', Information and Control, 55: 175–192.
• Hoare, C., 1969, "Een axiomatische basis voor computerprogrammering", Communications of the Association of Computing Machinery, 12: 576–580.
• Kozen, D., 1983, 'Resultaten op de propositionele μ-calculus', Theoretische informatica, 27: 333–354.
• Kozen, D., en R. Parikh, 1981, "Een elementair bewijs van de volledigheid van PDL", Theoretische informatica, 14: 113–118.
• Kozen, D., en J. Tiuryn, 1990, "Logics of programmes", in J. Van Leeuwen (red.), Handbook of Theoretical Computer Science (Volume B), Amsterdam: Elsevier, 789–840.
• Lange, M., 2005, "A lagere complexiteit op weg naar propositionele dynamische logica met kruispunt", in R. Schmidt, I. Pratt-Hartmann, M. Reynolds en H. Wansing (red.), Advances in Modal Logic (Volume 5), Londen: King's College Publications, 133–147.
• Lange, M. en C. Lutz, 2005, "2-EXPTIME ondergrenzen voor propositionele dynamische logica met kruispunt", Journal of Symbolische logica, 70: 1072-1086.
• Lutz, C., 2005, "PDL met kruispunt en omgekeerde is beslissend". In L. Ong (red.), Computer Science Logic, Berlin: Springer-Verlag, 413-427.
• Massacci, F., 2001, "Beslissingsprocedures voor expressieve beschrijvingslogica met kruising, samenstelling, rollenwisseling en rolidentiteit", in B. Nebel (red.), 17e Internationale Gezamenlijke Conferentie over Kunstmatige Intelligentie, San Francisco: Morgan Kaufmann, 193–198.
• Mirkowska, G. en A. Salwicki, 1987, Algorithmic Logic, Dordrecht: D. Reidel.
• Nishimura, H., 1979, 'Sequentiële methode in propositionele dynamische logica', Acta Informatica, 12: 377–400.
• Parikh, R., 1978, "De volledigheid van propositionele dynamische logica", in J. Winkowski (red.), Mathematical Foundations of Computer Science, Berlin: Springer-Verlag, 1978, 403-415.
• –––, 1983, "Propositionele logica van programma's: nieuwe richtingen", in M. Karpinski (red.), Foundations of Computation Theory, Berlijn: Springer-Verlag, 347-359.
• –––, 1985, "The logic of games and its applications", Annals of Discrete Mathematics, 24: 111–140.
• Peleg, D., 1987, "Concurrent dynamic logic", Journal of the Association of Computing Machinery, 34: 450–479.
• Platzer, A., 2010, Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Berlin: Springer, 2010.
• Pratt, V., 1976, "Semantical considerations on Floyd-Hoare logic", in Proceedings of the 17th IEEE Symposium on Foundations of Computer Science, Los Alamitos, CA: IEEE Computer Society, 109–121.
• –––, 1978, "Een praktische beslissingsmethode voor propositionele dynamische logica", in Proceedings of the 10th Annual ACM Symposium on Theory of Computing, New York, NY: ACM, 326–337.
• –––, 1980a, “Een bijna optimale methode om te redeneren over actie”, Journal of Computer and System Sciences, 20: 231–254.
• –––, 1980b, “Toepassing van modale logica op programmeren”, Studia Logica, 39: 257–274.
• Sakalauskaite, J., en M. Valiev, 1990, "Compleetheid van propositionele dynamische logica met oneindig herhalen", in P. Petkov (red.), Mathematical Logic, New York: Plenum Press, 339–349.
• Salwicki, A., 1970, "Formalized algoritmic languages", Bulletin de l'Academie Polonaise des Sciences, Serie des sciences mathematiques, astronomiques et physiques, 18: 227–232.
• Segerberg, K., 1977, "Een volledigheidsstelling in de modale logica van programma's", Notices of the American Mathematical Society, 24: 522.
• Schneider, K., 2004, Verification of Reactive Systems, Berlin: Springer-Verlag.
• Streett, R., 1982, "Propositionele dynamische logica van looping en converse is elementair beslissend", Information and Control, 54: 121–141.
• Vakarelov, D., 1983, "Filtratiestelling voor dynamische algebra's met tests en inverse operator", in A. Salwicki (red.), Logics of Programs and their Applications, Berlin: Springer-Verlag, 314–324.
• Vardi, M., 1985, 'The Taming of Converse: Reasoning about Two-way Computations', in Lecture Notes in Computer Science (Volume 193), Berlin-Heidelberg: Springer, 413–423.
• –––, 1998, "Redeneren over het verleden met tweerichtingsautomaten", in Lecture Notes in Computer Science (Volume 1443), Berlin-Heidelberg: Springer, 628–641.
• Vardi, M., en Stockmeyer, L., 1985, "Verbeterde boven- en ondergrenzen voor modale logica van programma's: voorlopig rapport", in Proceedings of the 17th Annual ACM Symposium on Theory of Computing, New York, NY: ACM, 240 –251.
• Yanov, J., 1959, "On equivalence of operator plans", Problems of Cybernetic, 1: 1–100.

Academische hulpmiddelen

	Hoe deze vermelding te citeren.
	Bekijk een voorbeeld van de PDF-versie van dit item bij de Vrienden van de SEP Society.
	Zoek dit itemonderwerp op bij het Internet Philosophy Ontology Project (InPhO).
	Verbeterde bibliografie voor dit item op PhilPapers, met links naar de database.

Andere internetbronnen

[Neem contact op met de auteur voor suggesties.]