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

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.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:

Wniosek7Problemspe“nialno–cidlaLTLjestPSPACE-trudny(azatem,dziƒkitwierdzeniu4,tak»ePSPACE-

zupe“ny).

=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).

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

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.

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika: