Logiki modalne i temporalne; część 1.pdf

(182 KB) Pobierz
64849289 UNPDF
Notatkidowyk“adu
Logikimodalneitemporalne
(semestrzimowy07/08)
EmanuelKiero«ski
Zgodniezobietnic¡przedstawiamlistƒwprowadzonychde nicjiitwierdze«.
1Jƒzykpodstawowejlogikimodalnej
Zak“adamy,»edysponujemyprzeliczalnymzbioremzmiennychzdaniowychV ar,oznaczanychzazwyczaj
literamip;q;ritp.Poni»szaregu“ade niujezbi ó rformu“podstawowejlogikimodalnej:
' ::= p j?j>j:' j '_' j '^' j ' ! ' j
3
' j
2
'
Wrzeczywisto–ciniekt ó rezpowy»szychkonstukcjis¡nadmiaroweidadz¡siƒzde niowa¢zapomoc¡
innych.Wszczeg ó lno–ci2
p ::= :
3
:'.Minimalnaregu“amo»ewygl¡da¢tak:
' ::= p j:' j '_' j
3
'
2Logikazdaniowa
De nicja1 (i)ModelemnazwiemyfunkcjƒM: V ar !f0; 1g
(ii)Formu“a'jestspe“nionawmodeluM...(tude nicjaindukcyjna)
(iii)Formu“ajestspe“nialna,gdyistniejemodel,wkt ó rymjestspe“niona
(iv)Formu“ajesttautologi¡je–lijestspe“nionawka»dymmodelu
Zwprowadzonymipojƒciamiwi¡»emynastƒpuj¡ceproblemyobliczeniowe:
De nicja2 (i)Wery kacjamodelu sprawdzi¢,czydanaformu“ajestspe“nionawdanymmodelu
(ii)Spe“nialno–¢ sprawdzi¢,czyistniejemodel,wkt ó rymformu“ajestspe“niona
(iii)Tautologie sprawdzi¢,czydanaformu“ajestspe“nionawka»dymmodelu
Twierdzenie3 (i)Problemwery kacjimodeludlalogikizdaniowejjestwP.
(ii)Problemspe“nialno–cidlalogikizdaniowejjestwNP.
(iii)Problembyciatautologi¡dlalogikizdaniowejjestcoNP-zupe“ny.
3StrukturyimodeleKripkego
De nicja4Struktur¡(ang.frame)dlapodstawowejlogikimodalnejnazywamyparƒF= (W;R),gdzie
Wjestniepustymzbiorem–wiat ó w(lubstan ó w),aRjestrelacj¡binarn¡naW.Modelemnazwiemyparƒ
M= (F;V ),gdzieFjeststruktur¡,aV : V ar ! P(W).
De nicja5Niechw 2 W,M= (W;R;V ).De niujemyindukcyjniepojƒcie: 'jestspe“nionewstaniew
('jestprawdziweww)modeluM,symbolicznie:M;w j= '.
M;w j= pi w 2 V (p)
M;w j= :'i niezachodziM;w j= '
M;w j=
3
'i dlapewnegov 2 W,tekiego»eRwvzachodziM;v j= '
M;w j=
2
'i dlaka»degov 2 W,takiego»eRwvzachodziM;v j= '
1
(...)
Dodatkowo,dlazbioruformu“,M;w j= ,gdyM;w j= 'dlaka»dego' 2 .
De nicja6Formu“ajestglobalnieprawdziwawmodeluM,Mj= ',gdyjestspe“nionawka»dymjego
stanie.
Przyk“ad7Przyk“ad1.22zestr.18
De nicja8 (i)Formu“a'jestprawdziwa(ang.valid)wstaniewstrukturyF,F;w j= ',gdyjest
prawdziewawtymstaniewka»dymmodelurozipƒtymnaF.
(ii)'jestprawdziwawF,Fj= ',gdyjestprawdziwawka»dymstanieF.
(iii)'jestprawdziwa(jesttautologi¡)wklasiestruktur F,gdyjestprawdziwawka»dejstrukturzeztej
klasy
(iv)'jestprawdziwa(albojesttautologi¡),gdyjestprawdziwawka»dejstrukturze.
Pojƒcieprawdziwo–ciwstrukturachznacz¡cor ó »nisiƒodpojƒciaprawdziwo–ci(spe“niania)wmodelach
przyk“adowo,je–li'_ jestspe“nionewstaniewmodeluM,to'jestspe“nionewwlub jestspe“nione
ww.Je–li'_ jestprawdziwewstaniewstrukturyF,towcalenieznaczy,»ekt ó ra–zpodformu“jestw
tymstanieprawdziwa.
Przyk“ad9 (i)3
(p _ q) ! (
3
p _
3
q)jestprawdziwawewszystkichstrukturach(inczejm ó wi¡cjest
pniejestprawdziwawewszystkichstrukturach.Jestzatoprawdziwawklasiestruktur
przechodnich.
p !
3
4Konsekwencjasemantyczna
De nicja10Niech,',Sbƒd¡odpowiedniozbioremformu“,formu“¡iklas¡modeli.M ó wimy,»e'jest
(lokalnie)semantyczn¡konsekwencj¡wklasieS(notacja: j= S '),gdydlaka»degomodeluMzklasyS
idlaka»degostanuw 2 W,je–liM;w j= ,toM;w j= '.
Przyk“ad11NiechSbƒdzieklas¡modeliprzechodnich.Wtedy:
f
33
pgj= S 3
p:
Oczywi–ciepowy»szyfaktniezachodzidlaSbƒd¡cegoklas¡wszystkichstrukur.
5Konstrukcjeniezmiennicze
5.1Sumyroz“¡cznemodeli
De nicja12NiechM i bƒdzierodzin¡modeli,M i = (W i ;R i ;V ).Zak“adamy,»emodeleniemaj¡wsp ó l-
nychstan ó w.Sumaroz“¡cznamodelide niowanajestnastƒpuj¡co: U i M i = (W;R;V ),gdzieWjestsum¡
Przyk“ad14Globalnegodiamentuniedasiƒzde niowa¢.M;w j= E'i M;v j= 'dlapewnegov.
5.2Generowanepodmodele
De nicja15M ó wimy,»eM 0 = (W 0 ;R 0 ;V 0 ) jestpodmodelemgdyM= (W;R;V ), W 0 W, R 0 jest
obciƒciemRdoW 0 iV 0 (p) = V (p)\W 0 .M 0 jestgenerowanympodmodelemM,gdydodatkowodlaka»dego
stanuw 2 Wzachodzi: w 2 W 0 iRwv,tov 2 W 0 .M ó wimy,»epodmodeljestgenerowanyprzezzbi ó r X
gdyjestnajmniejszymgenerowanympodmodelemzawieraj¡cymX.
Fakt16Je»eliM 0 jestgenerowanympodmodelemM,todlaka»degostanuwwM 0 zachodziM 0 ;w j=
'i M;w j= 'dladowolnego'.
Przyk“ad17Wstecznydiamentniejestde niowalny.
2
tautologi¡)
(ii)33
zbior ó wW i ,R sum¡relacjiR i ,aV (p) = U i V i (p).
Fakt13M i jakwy»ej.Dlaka»dego',ika»degostanuw 2 W i mamy U i M i ;w j= 'i M i ;w j= '.
5.3Mor zmyograniczone
De nicja18NiechM,M 0 bƒd¡modelami.Przekszta“cenief : W ! W 0 jestmor zmemograniczonym
(ang.boundedmorphism),gdy:
(i)wif(w)spe“niaj¡tesamezmiennezdaniowe
(ii)fjesthomomor zmem(Rwv ! R 0 f(w)f(v))
(iii)Je–liR 0 f(w)v 0 ,toistniejev 2 W,takie»eRwvorazf(v) = v 0
Przyk“ad19ModeleMiM 0 s¡zde niowanenastƒpuj¡co:
W = N ,Rmni n = m + 1,pspe“nionedlanparzystych
W 0 = fe;og,R 0 = f(e;o); (o;e),pprawdziwewe.
Mor zmograniczonyzMwM 0 :parzystenae,nieparzystenan.
Fakt20Je–lifjestmor zmemograniczonymzMwM 0 ,todladowolnego'zachodziM;w j= 'i M 0 ;f(w) j=
'.
6Bisymulacje
De nicja21BisymulacjapomiƒdzymodelamiM,M 0 totakaniepustarelacjaZ W W 0 ,»e:
(i)je–liwZw 0 ,towiw 0 spe“niaj¡tesamezmiennazdaniowe
(ii)(tam):je–liwZw 0 iRwvtoistniejetakiv 0 ,»eZvv 0 iR 0 w 0 v 0
(iii)(zpowrotem):je–liwZw 0 iR 0 w 0 v 0 ,toistniejetakiv,»eZvv 0 iRwv.
Notacja:M;w $ M 0 ;w 0 ;je–liistniejejakakolwiekbisymulacjatopiszemyczasem:M $ M 0
Twierdzenie22Je–liM;w $ M 0 ;w 0 ,towiw 0 spe“nij¡dok“adnietesameformu“y(modalformulasare
invariantunderbisimulation).
Twierdzenie23 (i)M i ;w $ U i M i ;w.
(ii)Je–liM 0 jestgenerowanympodmodelemM,todlaw 2 W 0 :M 0 ;w $ M;w.
(iii)Je–lifjestmor zmemograniczonymzMwM 0 ,toM;w $ M 0 ;f(w).
Twierdzenie24(Hennessy-Milner)NiechMiM 0 bƒd¡takimimodelami,»eka»dyichelementmatylko
sko«czeniewielenastƒpnik ó w.Wtedyw $ w 0 i w,w’spe“niaj¡dok“adnietesameformu“y.
7W“asno–¢modelusko«czonego
De nicja25M ó wimy,»elogikamodalnamaw“asno–¢modelusko«czonegowklasiemodeliM,gdyka»da
formu“aspe“nialnawMjestspe“nialnawpewnymmodelusko«czonymwM.
Twierdzenie26Logikamodalnamaw“ano–¢modelusko«czonego(wklasiewszystkichmodeli)
7.1Filtracja
Dow ó dtwierdzenia26przeprowadzimymetod¡ ltracji.
De nicja27M ó wimy,»ezbi ó rformu“ jestzamkniƒtynabraniepodformu“,gdy' 2 implikuje,»e
wszystkiepodformu“y'nale»¡r ó wnie»do.
De nicja28NiechM= (W;R;V )bƒdziemodelem,azbioremformu“zamkniƒtymnabraniepodformu“.
De niujemyrelacjƒr ó wnowa»no–ci nastanachmodeluMnastƒpuj¡co:
w w 0 zachodzi,gdydlawszystkich' 2 ;M;w j= 'i M;w 0 j= ':
Klasƒabstrakcjielementuwoznaczamyprzezjwj albopoprostuprzezjwj.Za“ ó »my,»emodelM f =
(W f ;R f ;V f )jesttaki,»e:
(a)W f = fjwj : w 2 Wg(zbi ó rklasabstrakcji)
(b)je–liRwv,toR f jwjjvj,
(c)je–liR f jwjjvj,todlaka»dejformu“y3
' 2 ,je–liM;v j= ',toM;w j=
3
'.
3
(d)V f (p) = fjwj :M;w j= pgdlappojawiaj¡cychsiƒw.
Takimodelnazywamy ltracj¡Mwzglƒdem.Czasem ltracj¡nazywamyte»sam¡relacjƒR f .
Fakt29FiltracjamodeluMwzglƒdemzamkniƒtegonapodformu“ymanajwy»ej2 jj stan ó w.
Twierdzenie30NiechM f bƒdzie ltracj¡modeluMwzglƒdemzamkniƒtegonapodformu“y.Wtedydla
ka»dego' 2 orazka»degow 2 Wzachodzi:M f ;jwjj= 'i M;w j= '.
Filtracjezawszeistniej¡.Dwiepodstawowede niowanes¡nastƒpuj¡co:
(i)najmniejsza ltracja: R s jwjjvji 9w 0 2jwj;v 0 2jvj Rwv
(ii)najwiƒksza ltracja: R l jwjjvji dlawszystkich3
' 2 :M;v j= 'implikujeM;w j=
3
'.
Lemat31Najwiƒkszainajmniejsza ltracjas¡rzeczywi–cie ltracjami.Wdodatkuka»da ltracjazawiera
najmniejsz¡izawierasiƒwnajwiƒkszej.
Twierdzenie32Logikamodalnamaw“asno–¢modelusko«czonego.Wdodatkuka»daspe“nialnaformu“a
'mamodelwielko–cinajwy»ej 2 m ,gdziemjestliczb¡podformu“'.
8Standardowyprzek“adnalogikƒpierwszegorzƒdu
De nicja33Rozwa»amysygnaturƒpierwszegorzƒduzawieraj¡c¡binarn¡relacjƒ Rorazunarnerelacje
P 1 ;P 2 ;:::,odpowiadaj¡cenaszymzmiennymzdaniowym.Dlazmiennejpierwszegorzƒduxstandardowy
przek“adST x zwracadlaformu“ymodalnejformu“epierwszegorzƒduzezmienn¡woln¡x:
ST x (p) = Px
ST x (:') = :ST x (')
ST x ('_ ) = ST x (') _ST x ( )
ST x (
3
') = 9y(Rxy^ST y ( ))
Wprzek“adziemo»emyograniczy¢siƒdou»ywanianazmianƒtylkodw ó chzmiennych: x;y.
Fakt34DlawszystkichmodeliMistan ó ww:M;w j= 'i Mj= ST x (')[w]
Wniosek:(podstawowa)logikamodalnajestfragmentamlogikipierwszegorzƒduFO.St¡d,mo»emywiele
wynik ó wdlaFOprzenie–¢dologikimodalnej.Przyk“adowo:zwarto–¢(compactness)-je–lika»dysko«czony
podzbi ó rpewnegozbioruformu“jestspe“nialny,toca“yzbi ó rr ó wnie»;dolnetw.L ö wenheima-Skolema:
ka»daspe“nialnaformu“amamodelprzeliczalny,itp.
Nale»yjednakpodkre–li¢,»elogikamodalnajestdo–¢ubogimframentemFO.Problemspe“nialno–cidla
FOjestnierozstrzygalny
Przyk“ad35Rxxniejestr ó wnowa»na»adnejformulemodalnej.
9De niowalno–¢w“asno–cistruktur
De nicja36Niech'bƒdzieformu“¡modaln¡,aKklas¡struktur.M ó wimy,»e'de niuje(lubcharake-
ryzuje)K,je–lidlaka»dejstrukturyF,F2 Ki Fj= '.Analogiczniedlazbioruformu“.
Przyk“ad37 (i)(T)p !
3
pde niujeklasƒstrukturzwrotnych.
(ii)(4)
33
p !
3
pde niujeklasƒstrukturprzechodnich.
(iii)(5)
3
p !
23
pde niujƒstrukturyzw“asno–ci¡eukliedsowo–ci.
pniemaodpowiednikawFO.
(1)Fakt:(L)de niujeklas¡struktur,wkt ó rychRjestprzechodnia,arelacjaodwrotnadoRdobrze
ufundowana(inaczejm ó wi¡cwRniemaniesko«czonego“a«cucha).
(2)Fakt:(L)niejestde niowalnawFO.
(
2
p ! p) !
2
Fakt39 (i)F;w j= 'i Fj= 8P 1 :::8P n ST x (')[w]
(ii)Fj= 'i Fj= 8P 1 :::8P n 8xST x (')
Fj= 8P 1 :::8P n 8xST x (')nazywamyczasemt“umaczeniem'naMSO(t“umaczeniemnapoziomiestruk-
tur).
4
Przyk“ad38Formu“aL ö ba(L):2
10Podej–cieaksjomatyczne,normalnelogikimodalne
De nicja40 K -dow ó dtosko«czonyci¡gformu“,zkt ó rychka»dajestaksjomatemlubpowstajezpoprzed-
nichpozastosowaniuregu“dowodzenia.Aksjomaty:
(PC)wszytkiepodstawieniatautologiilogikizdaniowej
(K)2(p ! q) ! (2p !
2q)
:p
Regu“ydowodzenia:
(1)(Modusponens):je–lidowiedli–my'oraz' ! ,tomo»emydowie–¢
(2)(Podstawienie):je–lidowiedli–my',tomo»emydowie–¢ ,je–li powstajez'przezjednorodne
podstawienieformu“zazmiennezdaniowe.
(3)(generalizacja):je–limamy',tomamy2
2
'.
Formu“a'jest K -dowodliwa(` K ')je–liistniejedow ó d,wkt ó rympojawiasiƒnako«cu.
Twierdzenie41[poprawno–¢systemuK]
(i)Ka»dyaksjomatjestprawdziwywklasiewszystkichmodeli.
(ii)Regu“ydowodzeniazachowuj¡prawdziwo–¢wklasiewszystkichmodeli.
Fakt42 (i)je–lidowiedli–my,tomo»emydowie–¢_.
(ii)je–lidowiedli–myi,tomo»emydowie–¢^.
Fakt43Poni»szeformu“ys¡dowodliwe(na¢wiczenia):
(a)(2^
2).
De nicja44 (i)'jestdowodliwezezbioruformu“ ( ` K ')gdyistniej¡takie 1 ;::: k 2 ,»e
` K ( 1 ^:::^ k ) ! '.
(ii)M ó wimy,»ezbi ó rformu“jestsprzecznyje–li ` K ?.Wprzeciwnymwypadkujestniesprzeczny.
(iii)jestmaksymalnymzbioremniesprzecznym(MCS),gdypodo“o»eniudoniegodowolnejformu“ystaje
siƒsprzeczny.
Fakt45 (i)niesprzecznyi ka»dyjegosko«czonypodzbi ó rniesprzeczny.
(ii):` K 'to:'niesprzeczne.
(iii)Je–lijestMCStodlaka»dego':dok“adniejednazformu“',:'nale»ydo.
(iv)ka»daformu“aniesprzecznajestzawartawpewnymMCS.
(v)je–liMCSi ` K ',to' 2 .
(vi)'_ 2 i ' 2 lub 2 .
(vii)'^ 2 i ' 2 i 2 .
(viii)je–li3
Twierdzenie46[Twierdzenieope“no–cidlalogikiK]
` K 'i j= '.
Dow ó dImplikacjawprawowynikaztwierdzenia41(opoprawno–ci).Wdrug¡stronƒwynikazlematu47.
2
Lemat47Ka»daformu“aniesprzecznamamodel.Wiƒcej:istniejemodelM= fW;R;Vg,wkt ó rymspe“-
nionajestka»daniesprzecznaformu“a.
Dow ó dKonstrukcjamodelukanonicznego.
2
De nicja48Normaln¡logik¡modaln¡nazwiemyzbi ó rformu“zamkniƒtynaoperacjesyntaktyczne(mo-
dusponens,podstawienieigeneralizacjƒ),zawieraj¡cyaksjomatysystemuK.Zazwyczajnormaln¡logikƒ
modaln¡de niujesiƒpodaj¡cpoprostudodatkoweaksjomaty.
Listaciekawychaksjomat ó w:
(4)33
3
p
5
(Dual)3p $:
3(^),
(b)2(^) $ (2^
3) !
'niesprzeczna,to'niesprzeczna.
p !

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin