Logiki modalne i temporalne; część 3.pdf
(
183 KB
)
Pobierz
64848688 UNPDF
Notatkidowyk“adu
Logikimodalneitemporalne
(czƒ–¢trzecia-logikitemporalne)
(semestrzimowy07/08)
EmanuelKiero«ski
1LTL-(propositional)LinearTimeLogic
1.1Sk“adnia
Podobniejakwlogicemodalnejmamyzbi
ó
rzmiennychzdaniowychV ar.JƒzykLTLde
niujemynastƒpuj¡co:
'::=p j?j>j:' j '_' j '^' j ' ! ' j F' j G' j 'U j X'
Minimalnyzestaw:
'::=p j:' j '_' j 'U j X'
Skr
ó
ty: G'=:F:'; F'=>U'
1.2Semantyka
Napocz¡tekokre–lamysemantykƒwniesko«czonychmodelachliniowych.Dlauproszczeniazak“adamy,»e
dzidzin¡jestzbi
ó
r
N
.Modeltofunkcja
M
:
N
!2
Var
,czyliniesko«czonyci¡gP
0
;P
1
;:::podzbior
ó
wV ar.
De
niujemyprawdziwo–¢'wpunkciemodelui:
(i)
M
;i j=pi
p 2
M
(i)
(ii)
M
;i j=:'i
M
;i 6j='
(iii)
M
;i j='_ i
M
;i j='lub
M
;i j= ,
(iv)
M
;i j=X'i
M
;i+1j='
(v)
M
;i j='U i
9k i:
M
;k j= oraz8i j < k:
M
;j j='
Formu“ajestspe“nialnaje–liistniejemodel
M
orazpunkti,takie»e
M
;i j='.Poniewa»naszwariant
m
ó
witylkooprzysz“o–cimo»emy“atwozauwa»y¢,»e 'spe“nialnai
'spe“nialnawpunkcie0pewnego
modelu.
1.3AutomatyB
ü
chi’ego
De
nicja,przebieg,warunekakceptacji.Automatyuog
ó
lnione.
Twierdzenie1Problemniepusto–cidlaautomat
ó
w(uog
ó
lnionych)B
ü
chi’egojestwNLOGSPACE.
Dow
ó
d(szkic)Obserwujemy,»edowolnyprzebiegakceptuj¡cyautomatuA=(A;G
1
;:::;G
k
)nas“owie
wdajesiƒprzerobi¢na“adnyprzebiegakceptuj¡cy
0
,
0
=
1
2
2
2
:::na(by¢mo»e)innyms“owiew
0
.
1
to
fragmentdopierwszegowyst¡pieniastanuszG
1
pojawiaj¡cegosiƒniesko«czeniewielerazy.W
2
wystƒ-
pujepodci¡gs
2
;s
3
;:::;s
k
;s,taki»es
i
2 G
i
.Istnienie“adnegoprzebiegusprawdzasiƒniedeterministycznie
zgaduj¡ckolejnestany(pamiƒtamytylkodwakolejne, sorazinformacjƒ,kt
ó
regoG
i
terazpotrzebujemy).
2
Twierdzenie2Klasajƒzyk
ó
wrozpoznawalnychprzezautomatyB
ü
chi’egojestzamkniƒtanasumƒ,przekr
ó
j
idope“nianie.
Zamkniƒto–¢nadope“nieniejesttrudnymwynikiem.Niepodajemydowodu.
1
1.4Problemspe“nialno–cidlaLTL
Twierdzenie3Dlaka»dego'mo»nazbudowa¢automatuog
ó
lnionyB
ü
chi’egoA
'
,taki»ejƒzykakceptowany
przezA
'
sk“adasiƒzmodeli'.
Szczeg
ó
“owydow
ó
dtegotwierdzenia(wrazzinformacjamioautomatachB
ü
chi’ego)mo»naznale„¢w
notatkachMadhavanaMukunda:
http://www.cmi.ac.in/madhavan/papers/isical97.html
Konstrukcjaztwierdzenia3dajeautomatwielko–ciwyk“adniczejwzglƒdemj'j,awiƒc,dziƒkitwierdzeniu
1,mamyz“o»ono–¢EXPTIMEproblemuSAT(LTL).Zaobserwowali–myjednak,»etaknaprawdƒ,tonie
musimynigdziewypisywa¢ca“egoautomatu.Niepusto–¢A
'
mo»nasprawdzi¢konstruuj¡c–cie»kƒstan
ó
w.
Wystarczy,»eumiemysprawdzi¢(wpamiƒciwielomianowej),»ezgadniƒtyzbi
ó
rformu“jestatomem(czyli
stanem),sprawdzi¢,czymiƒdzykolejnymidwomastanamijestmo»liweprzej–cie,sprawdzi¢,czystannale»y
doG
i
,itp.Wszystkotownaszymprzypadkudajesiƒzrobi¢bezproblemu,st¡d:
Twierdzenie4Problemspe“nialno–cidlaLTLjestwPSPACE.
1.5LTLwmodelach
nieliniowych
imodelchecking
Pojƒciespe“nianiaformu“LTLmo»narozszerzy¢namodele,kt
ó
reniemusz¡by¢liniowe.Niech
M
=
fW;R;Lg,gdzieW-zbi
ó
rstan
ó
w,R-relacjaprzej–cia(zak“adamy,»e8w9vRwv),L:W !2
Var
.
‘
cie»k¡
w
M
nazywamyniesko«czonyci¡gw
0
;w
1
;:::element
ó
wW,taki»ew
i
Rw
i+1
dlawszystkichi.Foru“yLTL
na–cie»kachwyliczanes¡wnaturalnyspos
ó
b.
Rozwa»asiƒdwiewersjede
nicjispe“nianiaLTLw
M
:
(i)'spe“nionawpunkciew 2 W i
istnieje–cie»kazaczynaj¡casiƒww,kt
ó
raspe“nia';
(ii)'spe“nionawpunkciew 2 W i
ka»da–cie»kazaczynaj¡casiƒwwspe“nia';
Myprzyjmiemypierwsz¡wersjƒde
nicji.Zauwa»myjednak,»e'jestspe“nionawwwsensie(i)i
:'
niejestspe“nionawwwsensie(ii).
Zauwa»myr
ó
wnie»,»ezachodzinastƒpuj¡cyoczywistyfakt:
Fakt5Je–li'jestspe“nialna,to'jestspe“nialnawmodeluliniowym.
Problemmodelcheckingpoleganasprawdzeniudladanego
M
,wi',czy
M
spe“nia'wpunkciew.
Twierdzenie6ProblemmodelcheckingdlaLTLjestPSPACE-zupe“ny
Dow
ó
dGranicag
ó
rna:redukcjadoproblemuspe“nialno–ci.Pytamyospe“nianie 'wpunkcieumodelu
M
.Model
M
zakodujemy
wformule ibƒdziemypyta¢ospe“nialno–¢formu“y'^ .
WprowadzamynowezmiennezdanioweQ
w
dlaka»degoelementuw 2 W.DlaQ
w
piszemyformu“ƒ
w
,
kt
ó
ram
ó
wi:
(i)prawdziwo–cQ
w
poci¡gaprawdziwo–¢tychzmiennychz',kt
ó
renale»¡doL(w)oraznieprawdziwo–¢
tych,kt
ó
renienale»¡doL(w);
(ii)prawdziwo–¢Q
w
implikuje,»ewnastƒpnymstanieprawdziwejestjakie–Q
v
dlapewnegov,takiego»e
wRv.
Dodatkowom
ó
wimyformu“¡
0
,»ewka»dymstanieprawdziwejestdok“adniejednoQ
w
.Ostatecznie:
2
Wniosek7Problemspe“nialno–cidlaLTLjestPSPACE-trudny(azatem,dziƒkitwierdzeniu4,tak»ePSPACE-
zupe“ny).
2
=Q
u
^
0
^
V
w
G
w
.
Š
atwoterazpokaza¢,»eistnieje–cie»kaw
M
,zaczynaj¡casiƒwu,spe“niaj¡ca' i
'^ spe“nialna.
Granicadolna:kodowaniemaszynyTuringarozwi¡zuj¡cejproblemzPSPACE.Nawyk“adziepokazali–my
ideƒkonstrukcjiwykorzystuj¡cejtylkooperatoryX iF(orazdualnyG).Na¢wiczeniachzobaczymy,»e
PSPACE-trudnyjestte»wariantLTL-ajedyniezoperatoremU.
1.6LTL(F)
ZbadamyterazwariantLTL,wkt
ó
rymjedynymoperatoremtemporalnymjest F(mo»naoczywi–cieu»ywa¢
r
ó
wnie»dualnegodoniegoG).Udowodnimy:
Twierdzenie8Probelmspe“nialno–cidlaLTL(F)jestNP-zupe“ny
Dow
ó
dgranicyg
ó
rnejwponi»szymtwierdzeniuopierasiƒnaobserwacji,»eka»daformu“aspe“nialnama
modelliniowykszta“tuIRRRR:::,gdzieIorazRs¡wielko–ciliniowejwzglƒdemd“ugo–ci '(lub,inaczej
m
ó
wi¡c,modelsko«czonysk“adaj¡cysiƒze–cie»ki IorazcykluR).Konstrukcjajestnastƒpuj¡ca:
Niech
M
=s
0
;s
1
;s
2
;:::bƒdzieliniowymmodelem'.ZbioryL(s
i
)nazywa¢bedziemytypami.Poniewa»
interesuj¡nastylkozmiennepojawiaj¡cesiƒw'mamymaksymalniewyk“adniczodu»o(wzglƒdemj'j)
typ
ó
w.
Wyr
ó
zniamyw
M
dwapunkty: s
k1
-ostatniarealizajcatypuwystƒpuj¡cegow
M
sko«czeniewielerazy
(je–lika»dytypjestrealizowanyniesko«czeniewielerazy,tok=0);s
l
-takipunkt,»eprzedzia“s
k
;:::;s
l
zawierarealizacjewszystkichtyp
ó
wwystƒpuj¡cychniesko«czeniewielerazy.Fragment s
0
;:::s
k1
nazwiemy
fragmentempocz¡tkowym,fragments
k
;:::s
l
fragmentempowtarzanym.
Lemat9Je–lii;j k,towpunktachs
i
is
j
spe“nianes¡dok“adnietesameformu“yLTL(F).
Lemat10
M
0
=s
0
;:::;s
k1
;s
0
k
;:::;s
0
l
;s
1
k
;:::;s
1
l
;s
2
k
;:::s
2
l
;:::,wkt
ó
rymtyps
i
j
jesttakijaktyps
j
w
M
,
jestmodelem'.Cowiƒcej,zbi
ó
rformu“spe“nianychwpunkcies
i
j
wmodelu
M
0
jesttakisamjakspe“nianych
w
M
wpunkcies
j
(dlaj k).Zbioryformu“spe“nianewpunkcies
j
,dlaj < ks¡r
ó
wnie»wobumodelach
identyczne.
Okazujesiƒ,»ewci¡gupocz¡tkowymorazwci¡gupowtarzanymmo»nazostawi¢tylko–wiadk
ó
wdla
podformu“postaci F .Zapiszmy'wpostacinegacyjnejnormalnej(negacjezepchniƒtedozmiennych
zdaniowych).Uzyskujemywtenspos
ó
b'
0
.Dlaka»dejpodformu“y'
0
postaciF :je–liF jestspe“niona
wci¡gupocz¡tkowym,towybieramymaksymalne i < k,takie»e
M
;s
i
j=F ;je–li F jestspe“niona
wci¡gupowtarzanym,towybieramydowolnek i l,takie»e
M
;s
i
j=F .Elementyzfragment
ó
w
pocz¡tkowegoipowtarzanego(zwyj¡tkiemelementus
0
),kt
ó
reniezosta“ywybranewykre–lamy.Za“
ó
»my,
»epotejprocedurzewci¡gupocz¡tkowympozosta“ys
i
0
;s
i
1
;:::;s
i
m
,awpowtarzanym: s
i
n
;s
i
n+1
;:::;s
i
p
.
Lemat11
M
00
=s
i
0
;s
i
1
;:::;s
i
m
;s
0
i
n
;s
0
i
n+1
;:::;s
0
i
p
;s
1
i
n
;s
1
i
n+1
;:::;s
1
i
p
;:::,gdzietyps
i
j
jesttakisamjaktyp
s
j
w
M
,jestmodelem'.Cowiƒcej,zbi
ó
rpodformu“'spe“nianychwpunkcies
i
j
wmodelu
M
00
jesttakisam
jakspe“nianychw
M
wpunkcies
j
.Zbiorypodformu“spe“nianewpunkcies
j
s¡r
ó
wnie»wobumodelach
identyczne.
AlgorytmNPpolegateraznazgadniƒciuma“ychwersjifragmentupocz¡tkowegoifragmentupowtarza-
negoisprawdzeniuwczasiewielomianowym(lista11,zadanie3),czyrzeczywi–ciedaj¡onemodel '.
Twierdzenie12ProblemmodelcheckingdlaLTL(F)jestNP-zupe“ny.
Dow
ó
dGranicadolna:Kodowanie3-SAT.
Granicag
ó
rna(szkic):
Szukamy–cie»ki,nakt
ó
rejjestspe“nionanaszaformu“a'
Szukana–cie»kajestpostaci: IR
1
R
2
:::,gdzieIjestminimalnymfragmentemzawieraj¡cymwszystkie
stanypojawiaj¡cesiƒsko«czeniewielerazy,aR
i
s¡cyklamizaczynaj¡cymsiƒwtymsamympunkcie.
Zar
ó
wnoIjakiR
i
niemusz¡by¢proste.
Imo»emywybra¢kr
ó
tkie-wystrczy,»ezawiera–wiadk
ó
wdlapodformu“ F oraz“¡cz¡ceje–cie»ki
(proste!)-jestwiƒcmaksymalnied“ugo–ci jMjj'j.
Zbi
ó
rstan
ó
wRpojawiaj¡cychsiƒwR
i
generujesilniesp
ó
jn¡sk“adow¡modelu.Kolejno–¢tychstan
ó
w
na–cie»cejestnieistotna.Wystarczywiƒczgadn¡¢ I,Risprawdzi¢,czydaj¡onepoprawnymodel
(orazczys¡,odpowiednio,–cie»k¡isilniesp
ó
jn¡sk“adow¡)-todajesiƒzrobi¢wczasiewielomianowym
(Lista11,zad.3).
2
3
2Logikiczasurozga“ƒzionego
2.1De
nicjaCTL*iCTL
JakzwykleV ARjestzbioremzmiennychzdaniowych.Wyr
ó
»niamyformu“ystanoweoraz–cie»kowe.Sk“ad-
niaCTL*jestnastƒpuj¡ca:
Formu“ystanowe':
'::=V AR j '^' j '_' j:' j ' ! ' j E j A
Formu“y–cie»kowe :
::=' j ^ j _ j ! j X j U j F j G
WprzypadkuCTLformu“y–cie»kowes¡takie:
Formu“y–cie»kowe wCTL:
::=X' j 'U' j F' j G'
CTLjestzatemfragmentemCTL*.FragmentemCTL*jesttak»eLTL.
CTLmo»nazde
niowa¢te»poprostutak(tylkoformu“ystanowe):
'::=P j '^' j '_' j:' j EF' j EG' j AF' j AG' j E('U')j A('U')j EX' j AX'
Niekt
ó
rezformu“mo»natraktowa¢jakoskr
ó
ty.Przyk“adowyminimalnyzestaw(dlaCTL-a):
'::=V AR j '^' j:' j EG' j E('U')j EX'
SemantykaCTL*de
niowanajestwzglƒdemstrukturKripkego.Prawdziwo–¢formu“stanowychde
nio-
wanajestwstanach,a–cie»kowych
na–cie»kach(niesko«czonych).Niech
M
=(W;R;L)bƒdziestruktur¡
Kripkego.Zak“adamy,»e8w 2 W9w
0
2 W Rww
0
.Dla–ciezkiniesko«czonej =(s
0
;s
1
;:::)przez
i
oznaczamy–ciezkƒ(s
i
;s
i+1
;:::)
M
;s j=Pi
P 2 L(s)
M
;s j='^ i
M
;s j='oraz
M
;s j=
M
;s j=:' i
nieprawda,»e
M
;s j='
M
;s j=E'i
istniejeniesko«czona–cie»ka=(s;:::),taka»e
M
; j='
M
;s j=A'i
ka»daniesko«czona–cie»ka=(s;:::)spe“nia
M
; j='
M
; j='i
M
;s j='dla'stanowych
M
; j='^ i
M
; j='oraz
M
; j=
M
; j=:' i
nieprawda,»e
M
; j='
M
; j='U i
istniejei,takie»e
M
;
i
j= orazdlawszystkichj < i:
M
;
j
j='
M
; j=X'i
M
;
1
j='
Pozosta“eprzypadkianalogicznie.SemantykaLTLwstanach:formu“a'jestprawdziwawstanies,je–li
wszachodziA'(tymrazemnapotrzebykolejnegopodrozdzia“uprzyjmujemyinnywariantni»przyde
nicji
problemumodelcheckingdlaLTL).
2.2Por
ó
wnaniemocyCTL*,CTL,LTL
De
nition13M
ó
wimy,»edwieformu“y(stanowe)'i wCTL*s¡r
ó
wnowa»neje–lidlaka»degomodelu
M
ika»degopunktus:
M
;s j='i
M
;s j= .Formu“a(stanowa)CTL*'jestr
ó
wnowa»naformuleLTL,
gdydlaka»degomodelu
M
ika»degopunktus:
M
;s j='i
M
;s j=A .
Poka»emy,»eLTLiCTLs¡niepor
ó
wnywalne.
Przyk“adoweformu“ywCTL,kt
ó
reniemaj¡r
ó
wnowa»nychwLTL:
AFAGP
4
AF(P ^AXP)
AGEFP
Przyk“adoweformu“ywLTL,kt
ó
reniemaj¡r
ó
wnowa»nychwCTL:
FGP
F(P ^XP)
Przyk“adowaformu“aCTL*,kt
ó
raniemar
ó
wnowa»nejaniwCTLaniwLTL:
AFGP _AGEFQ
2.2.1KryteriumdlaLTL
Dla'wCTL*przez'
d
oznaczamyformu“ƒLTLpowsta“¡z'poprzezusuniƒciewszystkichkwanty
kator
ó
w
–cie»kowychEiA.
Twierdzenie14[Clarke,Draghicescu]Niech'bƒdzieformu“¡CTL*.Wtedy: 'jestr
ó
wnowa»nepewnej
formuleLTLi
'jestr
ó
wnowa»ne'
d
.
2.2.2KryteriumdlaCTL
Rozszerzymyde
nicjƒspe“nianiadostrukturKripkegozograniczeniami.Strukturamadodatkowyzbi
ó
rF
2
W
,
M
=(W;R;L;F).Dla–cie»kioznaczmyprzezinf()zbi
ó
rstan
ó
wwystƒpuj¡cychwniesko«czenie
wielerazy.Semantykƒograniczamydo–cie»ek,dlakt
ó
rychinf()2 F.Mo»emy(bezstratyog
ó
lno–ci)
przyj¡¢,»ewszystkiezbiorywFtworz¡nietrywialnesilniesp
ó
jnesk“adowew
M
.Silniesp
ó
jniesk“adowa
jesttrywialnatylko,gdyjestsingletonembezpƒtelki.
Twierdzenie15[Clarke,Draghicescu]Niech
M
=(W;R;L;F)bƒdziestruktur¡Kripkegozogranicze-
niami.Niech
M
0
=(W;R;L;F
0
)bƒdzietaka,»eF
0
=F[F
0
,gdzieF F
0
dlapewnegoF 2F.Wtedydla
ka»dejformu“yCTL'ika»degos 2 W:
M
;s j='i
M
0
;s j=':
2.3W“asno–¢modelusko«czonegodlaCTL
Twierdzenie16Ka»daspe“nialnaformu“aCTL'mamodelwyk“adniczywzglƒdemj'j.
Dow
ó
dtegotwierdzeniamo»naznale„¢wpracyEmersonaiHalperna.R
ó
»nisiƒonjednaktrochƒod
prezentowanegonawyk“adzie.
5
Plik z chomika:
jelonka72
Inne pliki z tego folderu:
zadanie hermeneutyki.rar
(19649 KB)
Feyerabend Paul - Jak być dobrym empirystą.doc
(168 KB)
Deleuze Gilles Guattari - Co to jest pojęcie (str22-42).pdf
(1737 KB)
m_bombik nowy eksperymentalizm.rar
(3558 KB)
M.Bombik - o definicji.rar
(2721 KB)
Inne foldery tego chomika:
H. Rasiowa
Logika
Logika dla opornych
Logika dla prawników
Logika formalna
Zgłoś jeśli
naruszono regulamin