Titlu CURS: SPECIFICAREA ŞI VERIFICAREA SISTEMELOR …masalagiu/pub/CAP_SPEC_LOG_2010.pdfE. W....

Titlu CURS: SPECIFICAREA ŞI VERIFICAREA

SISTEMELOR REALE

• Vom vorbi despre Specificarea şi verificarea sistemelor reale cu ajutorul logicii

E. W. Dijkstra• “Verificarea este o activitate intelectuală

incitantă care ajută cel puŃin programatorul să capete o înŃelegere mai profundă a programelor (proiect, sistem,…) sale. Ea este în acelaşi timp şi o activitate „nobilă”: provocatoare pentru probleme simple, dar cu „trucuri” şi obositoare pentru probleme mari şi previzibile”

• De aceea este bine să nu se intre în amănunte

Profesori:

• Prof. Dr. Cristian Masalagiu [email protected]://www.info.uaic.ro/~masalagiu/

• Asist. Vasile [email protected]://www.info.uaic.ro/~alaiba/

InformaŃii necesare

• „Totul” se găseşte pe paginile web menŃionate

• Slide-urile vor mai fi actualizate peparcurs în timp util (oricum, la „final”vor conŃine exact ceea ce vă cer)

CerinŃe

http://www.info.uaic.ro -> Membri

-> Personal Academic (pentru a cunoaşte şi alŃi profesori şi a naviga către paginile noastre)

http://www.info.uaic.ro -> StudenŃi-> Regulamente (+ Fişa disciplinei)

http://www.info.uaic.ro/~masalagiu/(CondiŃiile - în secŃiunea “Special Topics in Logic”)

ORAR

• MIERCURI, 8.00 – 10.00, CURS, C309• VINERI, 8.00 – 10.00,

LABORATOR/SEMINAR, C403(mai urmariŃi ORAR-ul, măcar în primele două săptămâni)

CURS 1- Prezentare generală

Logica - MOTIVA łIE 1• Logicile neclasice şi în special logicile

temporale sunt azi folosite eficient în studiul comportării sistemelor concurente reale (numite şi sisteme reactive)

• Timpul şi adevărul dependent de timp suntesenŃiale

• Sistemele reactive (sisteme reale, concurente, funcŃionează separat sau în conexiune cu mediul) au modele abstracteconvenabile

Logica - MOTIVA łIE 2

• Există aplicaŃii practice de anvergură,implementate în limbaje de programare comerciale specifice (printre care TLA+, SMV – symbolic model verifier, Spin, etc.)

• Există foarte multe site-uri privind acestelimbaje

• Voi cita doar câteva nume - K. McMillan, M. Dwyer, L.Dillon şi câteva UniversităŃi: Carnegie Mellon, Berkeley, North Carolina


• Metodele prezentate pot fi utilizate atât pentru a studia comportarea unui sistem deja existent cât şi pentru a proiecta noi sisteme care să funcŃioneze „în siguranŃă”

• Există sisteme reale având un înalt grad de risc în funcŃionare (numite Safety Critical/SCS sau Safety Risky/SRS ): domeniul militar, medicină, spaŃiul cosmic, afaceri, aplicaŃii (soft/hard) fără bug-uri, etc.


• Problema verificării este nedecidabilăadică nu exist ă algoritm care să aibă la intrare orice funcŃie recursivă (sau, un algoritm care o calculează) şi o proprietate nebanală pentru aceasta şi care să se termine întotdeauna, cu răspunsul „DA” dacă funcŃia satisface proprietatea şi „NU”în caz contrar


Contraargument• Cât de mult din activitatea de verificare poate fi

automatizat? • Cât de uşor de înŃeles şi de implementat sunt

metodele formale folosite?• Există şi „alte” tehnici: „baterii” de teste,

metodologii de proiectare coerente, etc.• Poate fi folosit şi alt cadru formal (algebra – e

static) precum şi alte logici (şi nu numai încontextul verificării)


• Problema este şi că nu putem verifica formal un program având mii sau chiar zeci/sute de mii de linii

• De aceea trebuie găsite metode simple pentru a dispune de un „cod scurt de cercetat”, precum şi de metode de verificare sigure şi fiabile

• Logica oferă astfel de posibilităŃi…


• Logica (temporală/modală „la origine”, …)posedă un cadru formal coerent, relativ simplu de înŃeles şi bogat în rezultate de anvergură

• Reprezentarea abstractă a sistemelor necesităun limbaj care să poată exprima proprietăŃi ale “paşilor” de evoluŃie şi nu numai cele legate, deexemplu, de un început şi un sfârşit; deşi chiar logica în sine poate constitui un asemenea limbaj…

• Dinamica în funcŃionare a sistemelor reale este esenŃial a fi „prinsă”


• E. M. Clarke: „Metodele formale au ajuns în sfâr şit la maturitate! Limbajele de specificare, demonstratoarele automate(ATP) şi model checker-ele (MC) încep să fie folosite în industrie ca proceduri de rutin ă. Logica este baza tuturor tehnicilor dezvoltate ”


• De ce nu s-au folosit „serios” până înprezent ?

• Pentru că „notaŃiile şi conceptele încorporate în aplicaŃiile soft majore sunt complicate şi nenaturale” ?

• Pentru că „beneficiile reale sunt minore” ?


Greşit (tot E. M. Clarke)• „Nu au existat texte corespunzătoare pentru

studenŃi sau începători în domeniu, prin care să se explice în mod simplu cum funcŃionează exact aceste tehnici”

• „Matematica din substrat nu este mai complicată decât, de exemplu, calculul diferenŃial şi integral”

• „Familiarizarea cu tehnicile formale de specificare/verificare trebuie să devină o parte esenŃială a muncii de zi cu zi a fiecăruiinformatician”


• „Făcând verificare”, putem contribui la crearea unei lumi mai bune şi mai sigure: evitarea pierderilor de vieŃi omeneşti, a pierderilor financiare inestimabile, etc.

• Logica are capacitatea de a fi importantă şi prin ceea ce poate „lăsa pe dinafară”, sugerând metode precise şi neambigue de a lucra cu SCS/SRS; adică sugerează şicum se pot repara greşelile


• Se pot obŃine câştiguri financiaredeosebite de către cei care stăpânesc domeniul cunoscut sub numele de Computer Aided Verification (CAV). În cadrul CAV sunt cuprinse, cel puŃin:-Authomated Theorem Proving (ATP) -Specificarea şi verificarea utilizând Model Cheching (MC)

PROIECT CONłINUT CURS• Recapitulare (Algebre Booleene)• Recapitulare (LP, SSSS-notaŃia…)• Recapitulare (LP1, etc.)• Recapitulare (Sisteme Deductive şi Teorii Logice;

teoreme de corectitudine şi completitudine)• Recapitulare (Programare Logică - tip PROLOG)• (O)BDD• Sisteme Formale Concurente, Sisteme TranziŃionale,

Automate (pe cuvinte infinite)• Logica modală• Logica temporală (LTL , CTL, CTL*)• Algoritmi de Model Checking• TLA , TLA+• Sisteme multiagent

CERCETARE

• Voi propune nişte teme de cercetare care să vă ajute atât la conceperea şi redactarea Lucrării de DizertaŃie, cât şi la obŃinerea de puncte suplimentare;

• Vezi paginile web amintite la început şi site-ul Grupului de Logică aplicată(http://profs.info.uaic.ro/~alg)

BDD 1

• Ştim ce înseamnă funcŃii booleene şireprezentarea lor cu ajutorul tabelelor de adevăr sau cu expresii (FNCP, de exemplu)

• O altă reprezentare a elementelor din FB se bazează pe diagramele de decizie binare (BDD)

• Alegerea celei mai „convenabile” reprezentări depinde de context

• Tot ceea ce putem menŃiona în acest moment este că în anumite cazuri o BDD poate fi mai „compactă” decât o tabelă de adevăr pentru o aceeaşi funcŃie (din cauza anumitor redundanŃe care pot fi exploatate)

BDD 2• Defini Ńie (diagram ă de decizie binar ă). Se numeşte

diagramă de decizie binară (BDD pe scurt) pesteX = {x1, x2, … , xn} un graf orientat, aciclic, etichetat (pe noduri şi pe arce) în care:

-există o unică rădăcină (nod în care nu intră nici un arc)-frunzele (nodurile din care nu iese nici un arc) sunt

etichetate cu 0 sau 1, iar celelalte noduri (inclusiv rădăcina) sunt etichetate cu elemente din X (se permit etichetări multiple, adică noduri diferite pot avea aceeaşietichetă)

-fiecare nod care nu este frunză are exact doi succesori imediaŃi, arcele care îi leagă fiind etichetate cu 0respectiv 1O subBDD (într-o BDD dată) este un subgraf generat de un nod fixat împreună cu toŃi succesorii săi

BDD 3

• De obicei, într-un desen care reprezintă o BDD, frunzele pot fi identificate (şi) prin pătrate (nu cercuri, ca restul nodurilor), orientarea arcelor este implicită („de sus în jos”), arcele etichetate 0 sunt linii punctate(„stânga”), iar cele etichetate 1 sunt linii continue („dreapta”)

• În exemplele care urmează grafurile suntchiar arbori

BDD 4

• (I) D0, D1 (peste ∅), Dx (peste X = {x}):

• (II) O BDD peste X = {x, y}

BDD 5• Observa Ńie. Orice BDD peste X = {x1,x2,… ,xn}

defineşte/reprezintă/calculează o unică funcŃie booleană f ∈ FB(n). Astfel, pentru α1,α2,…,αn∈B (considerate ca fiind valori asignate corespunzător „variabilelor” din X) se „porneşte” cu rădăcina (unică) şi se „parcurge” un drum (unic) în graf „până” la o frunză (să spunem, etichetată cu β ∈ B)

• La fiecare pas, plecând din nodul curent, se alege acel arc (prin urmare şi noul nod curent) căruia i se ataşează valoarea 0 sau 1 conform valorii α deja atribuite nodului curent x (în asignarea aleasă). Valoarea asignată lui β este chiar f(α1, α2, … , αn)

BDD 6

• În acest mod, BDD-ul din exemplul anterior reprezintă funcŃiaf(x, y) = x(bară) • y(bară)

• Este clar că putem proceda şi invers, adică pornind cu orice funcŃie f ∈ FB(n) dată printr-un tabel de adevăr, construim (măcar) un arbore (BDD) binar, complet şi având n nivele, notate 0- rădăcina, 1, … , n-1 – frunzele(alternativ, având adâncimea n) care calculează f, în modul următor:

BDD 7• se ordonează mulŃimea de variabile cu ajutorul căreia

este exprimată funcŃia, să zicem X = {x1, x2, … , xn}, sub forma <xk,1, xk,2, … , xk,n>, <k,1; k,2; … ; k,n> fiind o permutare pentru <1, 2, … , n>

• nodurile interioare (care nu sunt frunze) situate pe nivelul i -1 sunt etichetate (toate ) cu xk,i (i ∈ [n]); rădăcina esteetichetată cu xk,1 fiind (singurul nod de) pe nivelul 0

• cele două arce care ies din fiecare nod sunt etichetate cu 0 şi respectiv 1

• frunzele sunt etichetate cu 0 sau 1 conform tabelei de adevăr pentru f (drumul de la rădăcină la frunza corespunzătoare furnizează exact linia care trebuie aleasă din tabelă: eticheta fiecărui arc de pe drum reprezintă valoarea atribuită variabilei care este eticheta nodului din care iese arcul)

BDD 8

• Exemplu. Fie f ∈ FB(3) dată prin f(a, b, c) = (a ∨ b) ∧ (a ∨ b ∨ c), deci exprimată cu ajutorul lui X = {a, b, c}, <a, b, c> fiind şi ordinea impusă asupra variabilelor. Tabela sa de adevăr este (de făcut voi…)

• BDD-ul care calculează f după algoritmul sugerat anterior este (de verificat…):

BDD 10• După cum se observă imediat, construirea unui BDD care

calculează o funcŃie dată nu este un proces cu rezultat unic, fiind suficient să schimbăm ordinea

• Impunerea unei ordini asupra etichetelor nodurilor este însă şi un prim pas spre găsirea unor forme normale pentru BDD-uri

• Un alt aspect care trebuie avut în vedere pentru atingerea acestui scop este acela că reprezentarea ca arbore a unei BDD nu este deloc mai eficientă/compactă decât o tabelă de adevăr (nici decât, de exemplu, o FNC(P)): dacă f ∈ FB(n), atunci tabela sa de adevăr va avea 2n linii iar în reprezentarea BDD sugerată de noi (ca arbore, în care fiecare nivel este „destinat” unei variabile şi pe fiecare drum de la rădăcină la o frunză apar toate variabilele exact o dată) vor fi exact 2n+1 – 1 noduri

• Putem compacta o BDD dacă îi aplicăm următoarele procedee de reducere/optimizare (în cele de mai jos, când ne referim la nodul n, m, etc. nu ne referim la eticheta din X):

BDD 11C1 (înlăturarea frunzelor duplicat) . Dacă o BDD conŃine mai mult de o frunză

etichetată cu 0, atunci:-păstrăm una dintre ele-ştergem celelalte frunze etichetate cu 0, împreună cu arcele aferente, care de fapt se „redirecŃionează” spre singura 0-frunză rămasă (fiecare păstrându-şi nodul sursă)-se procedează în mod similar cu 1-frunzele. Admitem şi înlăturarea unei frunze dacă, în final, ea nu are nici un arc incident cu ea

C2 (eliminarea „testelor” redundante) . Dacă în BDD există un nod (interior) n pentru care atât 0-arcul cât şi 1-arcul au ca destinaŃie acelaşi nod m (lucru care se poate întâmpla doar dacă s-a efectuat măcar un pas de tip C1), atunci nodul n se elimină (împreună cu arcele sale care punctează spre m), iar arcele care înainte punctau spre n sunt „redirecŃionate” spre m

C3 (eliminarea nodurilor duplicat care nu sunt frun ze). Dacă în BDD există două noduri interioare distincte, să zicem n şi m, care sunt rădăcinile a două subBDD -uri identice (fiind identice, n şi m sunt şi pe acelaşi nivel), atunci se elimină unul dintre ele, să zicem m (împreună cu arcele care-l au ca sursă), iar arcele care punctau spre m se „redirecŃionează” spre n

BDD 12• Defini Ńie (diagrame de decizie binare reduse).

O BDD se numeşte redusă dacă provine dintr-o alta în urma aplicării uneia sau mai multor eliminări de tipul C1-C3 de mai sus. O BDD este maximal redusă dacă asupra ei nu se mai pot aplica nici una dintre transformările C1-C3

• Defini Ńie (diagrame de decizie binare echivalente). Două diagrame de decizie binare D şi D’ se numesc sintactic echivalente dacă una provine din cealaltă în urma efectuării uneia sau mai multor transformări de tipul C1-C3 (una este redusa celeilalte). D şi D’ se numesc semantic echivalente dacă reprezintă aceeaşi funcŃie

BDD 13

• Exemplu. Plecând de la BDD-ul din ultimul exemplu obŃinem succesiv (maiîntâi sunt transformări de tip C1, apoi de tip C3 şi, în sfârşit, de tip C2)

BDD 14

BDD 15

BDD 16

BDD 17

BDD 18

• Ultima BDD este maximal redusă• Desigur că ordinea în care se efectuează

eliminările de tipul C1-C3 poate influenŃa aspectul structural al unei BDD şi pot exista mai multe transformări distincte care să fie simultan admise pentru o aceeaşi structuri

• În schimb, nici o transformare nu modifică funcŃia booleană calculată

BDD 19

• Teorem ă (invarian Ńa transform ărilor). Fie D o BDD şi D’ orice BDD sintactic echivalentă cu ea. Atunci D şi D’ calculează aceeaşi funcŃie f ∈ FB(D şi D’ sunt şi semantic echivalente)

• Demonstra Ńie. Rezultă imediat din definiŃiafuncŃiei calculate de o BDD şi din faptul că nici una dintre transformările de tipul C1-C3 nu „strică” drumurile iniŃiale (de la rădăcină la frunze) în ceea ce priveşte valorile de adevăr atribuite variabilelor (valorile atribuite frunzelor oricum nu se modifică)

BDD 20• Concluzionând, BDD-urile pot fi uneori „convenabil de compacte”.

Mai mult, putem reformula anumite definiŃii ale funcŃiilor booleene pentru noua reprezentare, căpătând, de exemplu, idei noi pentru rezolvarea problemei SAT

• Defini Ńie (drumuri consistente şi satisfiabilitate). Fie o BDD D peste mulŃimea de variabile X, care calculează o funcŃie f ∈ FB. Se numeşte drum consistent pentru f în D, un drum (d) de la rădăcină la o frunză care satisface condiŃia că pentru fiecare x ∈ X, (d) conŃine doar arce reprezentate ca linii punctate sau doar arce reprezentate ca linii continue, care ies din fiecare nod etichetat cu x (acest lucru echivalează cu a stipula că pentru a afla valoarea de adevăr a lui f într-o asignare dată, unei variabile x nu i se pot atribui simultan valorile 0 şi 1, ceea ce este absolut normal). Atunci, f este satisfiabilă dacă şi numai dacă există o BDD D care o reprezintă şi un drum consistent pentru ea în D astfel încât el „leagă” rădăcina de o frunză etichetată cu 1 (similar cu LP se definesc noŃiunile de formulă validă şi contradicŃie)

BDD 21

• Cu toate aceste posibile avantaje, se pare totuşi că reprezentarea cu ajutorul BDD a funcŃiilor booleene nu este încă destul de „convingătoare”

• Nu sunt astfel „vizibili” algoritmi simpli pentru a testa echivalenŃa semantică a două BDD deja reduse dar diferite (ca în cazul tabelelor de adevăr) şi nici pentru a „compune” uşorBDD-urile (ca în cazul formelor normale din LP). Revenim atunci la ideea ordonării mulŃimii de variabile

OBDD 1

• Defini Ńie (diagrame de decizie binare ordonate). Fie X = {x1, x2, … , xn} o mulŃime de variabile considerată a fi deja total (strict) ordonată (X este de fapt lista < x1, x2, … , xn >) şi o BDD D peste X. Spunem că D are ordinea < x1, x2, … , xn > dacă şi numai dacă pentru fiecare drum (d) în D de la rădăcină la orice frunză şi fiecare apariŃie a etichetelor distincte xi şi xj pe noduri din (d), dacă xi apare înaintea lui xj atunci i < j

• O BDD D se numeşte ordonată (pe scurt, OBDD), dacă există o listă de variabile X (inclusiv lista vidă sau cea care conŃine un unic element) astfel încât D are ordinea X

OBDD 2

• Deşi esenŃiale pentru testarea satisfiabilităŃii unei formule date sunt doar variabilele care apar într-o BDD care o calculează, să notăm că nu am cerut în mod explicit ca lista să conŃină exact etichetele care apar într-o OBDD. Astfel, dacă un OBDD are ordinea <x, y, z> atunci ea are şi ordinea <u, x, y, v, z, w>, etc. Deoarece am presupus că ordinea este totală şi strictă, relaŃia respectivă „<” nu este reflexivă, este antisimetrică (în sensul că dacă x < y atunci nu putem avea şi y < x) şi tranzitivă

• Datorită acestor proprietăŃi, într-o OBDD nu există apariŃii multiple ale unei variabile pe un drum şi este clar că există măcar o BDD care nu este şi o OBDD:

OBDD 3

OBDD 4• Exemplele anterioare ne furnizează atât o

OBDD neredusă cât şi una maximal redusă

• Defini Ńie (ordini compatibile). Fie O1 şi O2 două ordini (totale, stricte) peste mulŃimile de variabile X şi respectiv Y (notăm Z = X U Y). O1 şi O2 se numesc compatibile dacă nu există variabilele distincte x, y ∈ Z astfel încât x precede y în O1 iar y precede x în O2

OBDD 5

• Restrângând clasa ordinilor posibile la ordinile compatibile, obŃinem imediat adevărul următoarei afirmaŃii:

• Teorem ă (unicitatea OBDD-urilor maximal reduse) . Fie f ∈ FB orice funcŃie booleană. Atunci OBDD-ul maximal redus care o reprezintă este unic via ordinile compatibile. Mai exact, fie D şi D’ două OBDD-uri maximal reduse care reprezintă f (adică semantic echivalente). Atunci D şi D’ coincid

OBDD 6• Din teorema precedentă rezultă că verificarea

echivalen Ńei semantice devine banal ă în acest context (într-o anumită implementare ar trebui să verificăm pur şi simplu egalitatea a doi pointeri). Mai rezultă şi faptul că indiferent de ordinea în care aplic ăm reducerile vom ob Ńine aceea şi diagram ă maximal redus ă

• Defini Ńie (forma canonic ă a diagramelor ordonate).Fie orice n ∈ N, orice f ∈ FB(n) şi orice mulŃime de „variabile” total şi strict ordonată X = <x1, x2, … , xn>. Fie D o OBDD peste X, care are ordinea X, este maximal redusă şi reprezintă f. Atunci D se numeşte (OBDD-)forma canonică a lui f

OBDD 7

• Am putea deduce că dimensiunea unei OBDD este independentă de ordinea aleasă. Din păcate acest lucru nu este valabil în general şi dependenŃa dimensiunii unei OBDD de ordinea aleasă este preŃul pe care îl plătim pentru avantajele pe care OBDD-rile le au faŃă de BDD-uri şi alte tipuri de reprezentări

OBDD 8

• În concluzie, chiar dacă nu trebuie să supraestimăm importanŃa OBDD-urilor şi a existenŃei reprezentărilor canonice pentru funcŃiile booleene, putem enumera următoarele avantaje ale utilizării acestora:

-Formele canonice sunt în multe cazuri reprezentări mai compacte decât cele folosite în mod uzual (tabele, forme normale)

OBDD 9

Formele canonice se pot construi efectiv şi în mod unic pornind de la alte reprezentări (şi reciproc)

-Nu conŃin apariŃii nenecesare de variabile. Dacă valoarea lui f ∈ FB(n) în <x1, x2, … , xn> nu depinde de un xi atunci forma canonică care reprezintă f nu va conŃine nici un xi-nod (nod etichetat cu xi)

-Dacă două funcŃii f, g ∈ FB(n) sunt reprezentate de Df respectiv Dg, OBDD-uri canonice cu ordini compatibile, atunci se poate decide simplu echivalenŃa semantică a lui Df şi Dg adică egalitatea f = g

OBDD 10• Putem testa dacă o funcŃie este satisfiabilă „lucrând” pe

forma sa canonică: forma canonică nu este D0. Validitatea/contradicŃia este la fel de simplu de testat: forma canonică a funcŃiei coincide cu D1/D0

• Putem testa dacă f „implică” g (f, g ∈ FB(n)), adică dacă pentru fiecare <a1, a2, … , an> ∈ Bn, din f(a1, a2, … , an) = 1 rezultă g(a1, a2, … , an) = 1. Asta înseamnă să calculăm forma canonică pentru f • g (bară)şi aceasta trebuie să coincidă cu D0 în cazul în care implicaŃia este adevărată

• Şi în cazul acestei reprezentări se pot defini, prin algoritmi eficienŃi, anumite operaŃii asupra OBDD-urilor (formelor canonice) prin care putem „construi” întreaga clasă a funcŃiilor booleene (şi nu numai), pornind cu anumite funcŃii de bază (elementare)

Specificarea şi “verificarea” sistemelorreale cu ajutorul logicii - MOTIVA łIE

FINAL• Model checking-ul ales de noi este o

tehnică de verificare formală (semi)automată, bazată pe modele şi având o abordare orientată pe verificarea proprietăŃilor (urmează)

• Util şi:• [email protected]• www.ivv.nasa.gov

Specificarea şi “verificarea” sistemelorreale cu ajutorul logicii – Metode de

verificare 1Orice tehnică formală de verificare este

alcătuită din trei părŃi distincte:(1)Un cadru general pentru specificarea

sistemelor reale cuprinzând un limbaj de descriere cât mai evoluat (sisteme concurente formale – FCS = sintaxa, sisteme tranziŃionale - TS = semantica(mai pot fi: procese secvenŃiale cooperante sau comunicante – CSP,algebre de proces, µ-calcul, reŃele Petri, reŃele workflow, etc.)

Specificarea şi “ verificarea ” sistemelorreale cu ajutorul logicii – Metode de

verificare 2

(2)Un limbaj pentru specificarea proprietăŃilor sistemelor reale (logica clasică, logica modală, logica temporală, logica liniară, etc.). Nu ar fi lipsit de interes ca cele două limbaje să coincidă (programare logică)

(3)O metodă/(semi)algoritm/metodologie prin care să se poate clar stabili dacă o anumită descriere a unui sistem satisface o anumită proprietate


verificare 3• Ne-am oprit asupra logicii (temporale)

şi FCS, TSTSTSTS din motivele menŃionate• O procedură/algoritm de tip model

checking (un model checker) va răspunde „DA” dacă MMMM ⊨ F şi „NU”altfel (MMMM - model “generat” de sistemulformalizat, F – proprietate/formulă)


verificare 4• Majoritatea model checker-elor

comerciale produc şi un istoric al comportamentelor unui sistem în caz de insucces – se poate deduce cetrebuie reparat (vezi şi TLC pt. TLA+ )

• Formulele pot “captura” diferiteaspecte din comportarea sistemelor(proprietăŃi, relaxare, etc.)


verificare 5Clasificarea metodelor:• (a) Bazate pe semantică/model/teorie logică sau bazate

pe sintaxă/demonstraŃie/sistem deductiv. Într-o abordare bazată pe sintaxă, descriem sistemul printr-o mulŃime de formule Г (într-o logică fixată) şi proprietatea printr-o formulă F (în aceeaşi logică). Metoda de verificare constă în a demonstra că Г ⊢ F, ceea ce implică aproape întotdeauna ATP şi o implicare deosebită din partea utilizatorului. Într-o abordare bazată pe semantică, sistemul este reprezentat printr-un model MMMM, proprietatea printr-o formulă F iar metoda de verificare constă din a demonstra MMMM ⊨ F. Ideal ar fi ca totul să fie automatizat, ca măcar un model să poată fi selectat aprioric şi să dispunem – în context – de o teoremă de completitudine şi corectitudine


verificare 6• (b) Gradul de „algoritmizare”. Aici este evident

că putem trece dintr-o extremă în alta: de la o algoritmică completă (în situaŃii particulare care permit acest lucru) la ceva complet „manual”. „În mijloc” ar fi tehnicile de tip CAV

• (c) Se verific ă o singură proprietate sau întregul comportament. Totul depinde de posibilitatea de a implementa metode eficiente


verificare 7• (d) Domeniul principal de aplicabilitate. Nu este

acelaşi lucru dacă ne gândim la hardware sau la software, la sisteme secvenŃiale sau concurente, la sisteme reactive (care „funcŃionează”permanent) sau care trebuie să-şi oprească funcŃionarea, etc.

• (e) Verificarea este destinată a fi aplicată pentru un sistem care există/funcŃionează deja sau înaintea proiectării acestuia. Singurul lucru pe care-l putem evidenŃia în plus aici este faptul că verificarea trebuie folosită cât mai devreme


verificare 8Concluzii (ce vom folosi noi, în special pentru punctele(1)-(3) de mai jos):

Metoda (VERIF)• Reprezentăm sistemul real ca un FCS, F• Reprezentăm proprietatea dorită a sistemului printr-o

formulă temporală, notată G• Construim sistemul tranziŃional ataşat lui F,TSTSTSTS. Limbajul

acceptat de acesta constituie modelele posibile pentru G, L(TSTSTSTS, F), unde condiŃia de acceptare F este aleasă corespunzător

• Construim automatul A, ataşat lui G (care ne furnizează modelele efective ale lui G) şi fie L(A, s0, F) limbajul acceptat (mulŃimea de stări finale F este, la rândul ei, aleasă corespunzător)

• Demonstrăm că L(TSTSTSTS, F) = L(A, s0, F)


verificare 9• Pentru a dispune de algoritmi performanŃi,

este posibil să nu cerem chiar aşa de multClase principale de algoritmi de verificare:• (1)Explorarea spaŃiului stărilor. Model

checking pentru logica temporală cu timp liniar (LTL )

• (2)Model checking pentru logica temporală cu timp ramificat (CTL)


verificare 10• (3)Algoritmi de verificare bazaŃi pe

ordini parŃiale• (4)Verificare simbolică• (5)Verificare compoziŃională• (6)Tratarea sistemelor cu un număr

infinit de stări


verificare 11Putem deduce structura generală a

Cursului:• (1)Automate, sisteme concurente formale,

sisteme tranziŃionale (şi: diagrame de decizie binare, logică modală, grafuri, limbaje formale, mulŃimi parŃial ordonate, topologie, statistică, algoritmică, decidabilitate şi complexitate, etc.)


verificare 12• (2)Logica temporală cu timp liniar. Logica

temporală cu timp ramificat• (3) Algoritmi de bază în verificareAlte nume de reŃinut: A. Pnueli, Z. Manna, E.

A. Emerson, J. Quielle, J. Sifakis, J. Halpern, A. Stoughton

Web site (artificial intelligence): www.cis.ksu.edu/~allen/research.html

Verificarea - vis şi realitate 1Cum s-a început?

-E.W. Dijkstra, gcd (greatest common divisor) –cel mai mare divizor comun . De la ce s-a plecat? În primul rând de la propriet ăŃile funcŃiei gcd şi apoi de la ideea că nu putem face o verificare serioasă dacă nu separăm informaŃia după nişte criterii specifice (date de intrare; date de ieşire; date intermediare, eventual diferite ca “locaŃii”)-Astfel, vom nota cu:

X – lista variabilelor de intrare; X = <X1, X2>Y – lista varibilelor de lucru; Y = <Y1, Y2>Z – variabila de ieşire

Verificarea - vis şi realitate 2

-gcd: Program care “calculează” cel mai mare divizor comun a două numere naturale (strict) pozitive.-ProprietăŃi utile ale funcŃiei gcd :

-gcd : N* × N* → N*

-gcd (x,y) = gcd (x-y, y) , dacă x ≥ y (similar pentru y)

-gcd (x,x) = x


• Schema logică:

Verificarea - vis şi realitate 4• Precondi Ńie

ϕ(X1, X2): X1 > 0 ∧ X2 > 0 ∧ X1 ∈ N ∧ X2 ∈ N

• InvariantI(X1, X2, Y1, Y2): X1 > 0 ∧ X2 > 0 ∧ Y1 > 0 ∧ Y2 > 0 ∧gcd (Y1,Y2) = gcd (X1,X2)

• Postcondi ŃieΨ(X1, X2, Z): Z = gcd (X1, X2)


• Ideea general ă este să arătăm că (un) program(ul) care satisface (o) Precondi Ńie la intrare, va satisface (o) Postcondi Ńie la ieşire, folosind, eventual, Invarian Ńi (pentru bucle)

(II) Ce “facem” cu terminarea ? FuncŃia (Colatz):

f : N* → N*n = 1

n - par

n - impar

1

nf(n)=

23n+1

CURS 2

• Formalizări (ceea ce nu „prea” este înWolper)

Automate şi limbaje 1

• Vom insista mai puŃin pe subiectul „automate şi limbaje pe cuvinte finite” acesta fiind (sperăm) unul destul de cunoscut

• Mai pe larg însă vom descrie formal noŃiunile de automat pe cuvinte infinite şi cea de automat pe arbori (finiŃi/infiniŃi), subliniind în acelaşi timp şi câteva dintre proprietăŃile lor generale


• Defini Ńie (automat) . Se va numi automat(determinist/nedeterminist, pe cuvinte finite sau infinite ), un 5-uplu A = <∑∑∑∑, S, δ, s0, F>, unde:-S este mulŃimea stărilor-δ : S × ∑∑∑∑ → S este funcŃia/relaŃia de tranziŃie (în cazul determinist), iar-δ : S × ∑∑∑∑ → 2S este funcŃia/relaŃia de tranziŃie (în cazul nedeterminist)-S0 ⊆⊆⊆⊆ S este mulŃimea stărilor iniŃiale (poate fi doar una)-∑∑∑∑ este alfabetul simbolurilor/simbolilor de intrare-F ⊆⊆⊆⊆ S este mulŃimea stărilor de acceptare sau finale


• MulŃimile S, ∑∑∑∑ şi F se presupun a fi nevide, disjuncte două câte două şi finite (în acest caz, automatul se va numi finit; de fapt, este suficient ca S să fie finită şi ΣΣΣΣ - cel mult numărabilă)

• Şi S0 este presupusă a fi nevidă. Este posibil uneori ca F să fie mai complicată (F ⊆ 2S, F ⊆ 2S × 2S, etc.)

Automate şi limbaje 4• Orice automat poate fi reprezentat ca un

(multi)graf orientat etichetat (atât pe noduri cât şi pe arce)

• În noduri vom avea stări iar pe arce – simboli de intrare. Un arc de la s1 la s2 etichetat cu a va indica faptul că s2 = δδδδ(s1, a) (cazul determinist; în acest caz vor putea apare arce multiple de la o stare la alta, sau, echivalent, un singur arc dar etichetat cu o mulŃime de simboli), respectiv s2 ∈ δδδδ(s1, a) (cazul nedeterminist; în acest caz vor putea exista şi arce multiple, dar şi mai multe arce care „ies” dintr-o stare şi având aceeaşi etichetă)


• Nodurile care conŃin o stare iniŃială vor fi indicate printr-un simbol special ataşat unei încercuiri simple iar cele care conŃin o stare finală – printr-o dublă încercuire

• Este posibil ca în cazul unor automate mai „stufoase” (Büchi generalizat, Rabin, Street) nodurile să capete şi nişte etichete suplimentare

Automate şi limbaje 6• Defini Ńie (cuvinte) . Un cuvânt finit (de lungime

n ∈ N) peste un alfabet Γ este o funcŃie

w : {0, 1, … , n – 1} → Γ. Aceasta poate fi reprezentată şi ca o listă/secvenŃă de „litere”(elemente ale lui Γ) w = w0•w1•...•wn-1 (simbolul „•” denotând de fapt operaŃia de concatenare, pe cuvinte de lungime 1; de obicei acesta se omite în scriere)

• wi este notaŃia prescurtată a lui w(i) (pentru orice i din domeniul lui w). Similar, un cuvânt infinitpeste Γ va fi privit ca o funcŃie w : N → Γ

Automate şi limbaje 7• MulŃimea cuvintelor finite peste un alfabet Γ se

notează cu Γ*, iar perechea < Γ*, •> este monoidul liber generat de Γ. Elementul neutru(sau cuvântul vid, fără nici o literă) se notează cu λ (λ : Ø →→→→ Γ)

• Concatenarea: dacă w1 = w11w12 … w1k şiw2 = w21w22 … w2m, atunci w1•w2 = w11w12 … w1k w21w22 … w2m (formal: cu funcŃii)

• MulŃimea cuvintelor infinite peste Γ se notează cu Γωωωω. Notăm mulŃimea tuturor cuvintelor peste Γprin Γ∞∞∞∞, adică Γ∞∞∞∞ = Γ* U Γωωωω

Automate şi limbaje 8• OperaŃiile specifice sunt legate de concatenare.

Dacă L1 şi L2 sunt limbaje peste ΓΓΓΓ, atunci punem L1•L2 = {w| w = w1•w2, w1 ∈ L1, w2 ∈ L2}. De asemenea, L[n] va nota concatenarea limbajului L cu el însuşi de n ori (concatenarea rămâne asociativă şi dacă este extinsă la limbaje). Vom pune şi L* = Un≥0L[n], limbaj care se va numi şi închiderea reflexivă şi tranzitivă a lui L

• Similar, Lω va denota concatenarea lui L cu el însuşi de o infinitate de ori. L[0] = {λ}. Prin inf(w) se înŃelege mulŃimea acelor litere (uneori, chiar subcuvinte) care apar de o infinitate de ori în cuvântul (infinit) w

Automate şi limbaje 9• În cazul cuvintelor infinite concatenarea rămâne

asociativă şi cuvântul vid rămâne λ. Informal, w1•w2 = w1 dacă w1 este cuvânt infinit (indiferent de caracterul lui w2). Dacă w1 este cuvânt finit, atunci w1•w2 va fi un cuvânt finit sau infinit (conform caracterului lui w2), avându-l ca prefix pe w1 (similar cu cazul cuvintelor finite)

• Orice submulŃime a lui Γ* (Γωωωω, Γ∞∞∞∞) se numeşte limbaj finitar/de cuvinte finite (respectiv, limbaj infinitar/de cuvinte infinite sau, simplu, limbaj ) peste ΓΓΓΓ. Cum limbajele sunt mulŃimi, operaŃiile generale cu acestea sunt cele cu mulŃimi (reuniune, intersecŃie, produs cartezian, etc.)

Automate şi limbaje 10• Intuitiv, un cuvânt finit w este acceptat de către

un automat A dacă există o secvenŃă (finită) de stări care începe cu un element din S0 şi se termină cu o stare finală/de acceptare (adică aparŃinând lui F), stări „obŃinute” prin „consumarea” simbolurilor de intrare prezente în w (se mai scrie şi …)

• În cazul cuvintelor infinite, acceptarea poate fi definită (tot intuitiv) prin faptul că într-o secvenŃă (infinită) de stări obŃinute ca mai înainte, anumite stări satisfac o anumită proprietate legată de F

Automate şi limbaje 11• Defini Ńie (limbaje de cuvinte finite acceptate de

automate). Fie automatul A = <∑∑∑∑, S, δ, S0, F>, F ⊆⊆⊆⊆ S şi cuvântul de lungime n, w = w0•w1•...•wn-1 peste ∑∑∑∑. Spunem că w este acceptat de A dacă există o listă/secvenŃă finită de stări (sau, cuvânt finit peste S) s: s0, s1, … , sn (se spune: compatibilă cu relaŃia de tranziŃie) astfel încât:-s(0) (adică s0) ∈ S0-(∀i, 0 ≤ i ≤ n-1)(si+1 = δδδδ(si, wi)) în cazul determinist şi (∀i, 0 ≤ i ≤ n-1)(si+1 ∈ δδδδ(si, wi)) în cazul nedeterminist

-sn ∈ F• MulŃimea tuturor cuvintelor acceptate de A se va numi

limbajul finitar (de cuvinte finite) acceptat de A (pornind cu S0 şi terminând cu F) şi va fi notat L(A, S0, F)

Automate şi limbaje 12• În cele de mai sus s-a folosit faptul că funcŃia

δ : S × ∑∑∑∑ →→→→ S (δ : S × ∑∑∑∑ →→→→ 2S) se poate extinde unic la δ* : S × ∑∑∑∑* →→→→ S(δ* : S × ∑∑∑∑* →→→→ 2S), prin δδδδ*(s, λ) = s şi δδδδ*(s, wa) = δδδδ(δδδδ*(s, w), a), pentru fiecare s ∈ S, w ∈ ΣΣΣΣ* şi a ∈ ΣΣΣΣ (în cazul determinist; nedeterminist: (Us’∈δδδδ*(s, w) δδδδ(s’, a))

• Deducem imediat şi proprietatea: δδδδ*(s, w1w2) = δδδδ*(δδδδ*(s, w1), w2). Acelaşi lucru va fi posibil şi în cazul ΣΣΣΣωωωω(e vorba de fapt de subcuvintele finite). Pentru simplitate, extensia se notează tot cu δδδδ

Automate şi limbaje 13• Se ştie că clasa limbajelor finitare acceptate de

automatele finite deterministe coincide cu clasa limbajelor finitare acceptate de automatele finite nedeterministe, aceasta numindu-se şi clasa limbajelor regulate

• Un limbaj regulat (adică acceptat de un automat finit, determinist sau nu) poate fi reprezentat prescurtat prin aşa numitele expresii regulate

• Expresiile regulate se definesc constructiv, similar cu expresiile aritmetice obişnuite. Constantele şi variabilele denotă limbaje (respectiv clase de limbaje) iar operatorii sunt de această dată: • (denotă concatenarea de limbaje), + (denotă reuniunea; câteodată în loc de + se foloseşte chiar U) şi * (denotă închiderea reflexivă şi tranzitivă)

Automate şi limbaje 14• Deşi există şi alte forme de acceptare (înafară de cea

„prin stări finale”), ele nu sunt relevante (în ceea ce priveşte clasa de limbaje care se poate obŃine); nicicard(s0)>1 nu e esenŃial

• Dacă la operatori mai adăugăm ωωωω, atunci vom vorbi de expresii (şi limbaje) ω-regulate. Astfel, expresia regulată b + a•b* reprezintă limbajul (finitar) L = {b, ab, ab[1], ab[2], …}, adică L = {b} U {a•b[n]| n ∈ N}(a înseamnă o prescurtare pentru L = {a})

• Dar expresia (puneŃi voi…)?• În cazul automatelor pe cuvinte infinite mulŃimea F poate

fi mai complicată, deşi este „alcătuită” tot din stări

Automate şi limbaje 15• Defini Ńie (limbaje de cuvinte infinite

acceptate de automate). Fie automatulA = <∑∑∑∑, S, δ, S0, F> şi cuvântul infinit w = w0•w1•...•wn-1• … peste ∑∑∑∑. Spunem că w este acceptat de A dacă există o listă/secvenŃă infinită de stări (cuvânt infinit peste S) s: s0, s1, … , sn, … (s : N →→→→ S) astfel încât:-s(0) (adică s0) ∈ S0.-s este compatibilă cu relaŃia de tranziŃie adică: (∀i, 0 ≤ i)(si+1 = δδδδ(si, wi)) în cazul determinist şi(∀i, 0 ≤ i)(si+1 ∈ δδδδ(si, wi)) în cazul nedeterminist

Automate şi limbaje 16• (a) F ⊆ S şi inf(s) ∩ F ≠ Ø: condiŃia de acceptare

Büchi (B). Sau:• (b) F ⊆ 2S, F = {F1, F2, … , Fm} şi inf(s) ∩ Fi ≠ Ø

pentru fiecare i ∈ [m]: condiŃia de acceptare Büchi generalizată (GB). Sau:

• (c) F ⊆ 2S × 2S, F = {<G1, B1>, <G2, B2>, … , <Gn, Bn>} astfel încât există măcar o pereche <G, B> ∈ F cu inf(s) ∩ G ≠ Ø şi inf(s) ∩ B = Ø: condiŃia de acceptare Rabin (R). Sau:

• (d) F ⊆ 2S × 2S, F = {<G1, B1>, <G2, B2>, … , <Gn, Bn>} şi pentru fiecare i ∈ [n] avem inf(s) ∩ Gi = Ø sau inf(s) ∩ B i ≠ Ø: condiŃia de acceptare Street (S)

Automate şi limbaje 17• MulŃimea tuturor cuvintelor infinite acceptate de

A va fi un limbaj infinitar (de cuvinte infinite) acceptat de A (pornind cu S0 şi depinzând de F) şi va fi notat LXωωωω(A, S0, F), unde

X ∈ {B, GB, R, S} (conform condiŃiilor de acceptare (a) – (d) de mai sus). Vom vorbi astfel de automate/limbaje Büchi, automate/limbaje Büchi generalizate, automate/limbaje Rabin sau automate/limbaje Street, deterministe sau nu

Automate şi limbaje 18• În privinŃa limbajelor acceptate de automatele pe

cuvinte infinite, lucrurile nu mai sunt atât de simple ca în cazul finit (aceasta şi datorită admiterii unor tipuri de acceptare esenŃial diferite). Astfel, dacă în cazul nedeterminist (indiferent de condiŃia de acceptare) se generează exact clasa limbajelor ω–regulate de forma Ui≥0L i(K i)ω, unde atât L i cât şi K i sunt limbaje regulate finitare, în cazul automatelor deterministe (pe cuvinte infinite) condiŃiile Büchişi Büchi generalizată sunt efectiv mai slabe decât celelalte două


• Exemplu. Fie automatul determinist

A = <∑∑∑∑, S, δ, S0, F>, unde ΣΣΣΣ = {a, b}, S = {s0}, S0 = {s0}, F = {s0}, δδδδ(s0, a) = s0, δδδδ(s0, b) = s0

LB ωωωω(A, S0, F) = ΣΣΣΣωωωω

Automate şi limbaje 20• Exemplu. Fie automatul determinist

A = <∑∑∑∑, S, δ, S0, F>, unde ΣΣΣΣ = {a, b}, S = {s0, s1}, S0 = {s0}, F = {s1}, δδδδ(s0, a) = s0, δδδδ(s0, b) = s1, δδδδ(s1, a) = s0, δδδδ(s1, b) = s1

LB ωωωω(A, S0, F) = {w ∈ ΣΣΣΣωωωω| b ∈ inf(w)}

Automate şi limbaje 21• Exemplu. Fie automatul determinist

A = <∑∑∑∑, S, δ, S0, F>, unde ΣΣΣΣ = {a, b}, S = {s0, s1}, S0 = {s0}, F = {s1},

δδδδ(s0, a) = s0, δδδδ(s0, b) = s1, δδδδ(s1, a) = s1, δδδδ(s1, b) = s1

Automate şi limbaje 22LB ωωωω(A, S0, F) = a*b(a + b)ω

• Exemplu. Fie automatul nedeterminist

A = <∑∑∑∑, S, δ, S0, F>, unde ΣΣΣΣ = {a, b}, S = {s0, s1}, S0 = {s0}, F = {s0},

δδδδ(s0, a) = {s0, s1}, δδδδ(s0, b) = {s0}, δδδδ(s1, a) = Ø, δδδδ(s1, b) = s0


LB ωωωω(A, S0, F) = {w ∈ ΣΣΣΣωωωω| ab ∈ inf(w)}

Automate şi limbaje 24• Un automat pe arbori este o generalizare a unui

automat pe cuvinte aşa cum un arbore (care poate fi privit şi ca un anumit tip de mulŃime parŃial ordonată) este o generalizare a unui cuvânt (mulŃime total ordonată). Pentru simplitate, ne vom limita pe moment doar la arbori binari (etichetaŃi) infiniŃi

• Defini Ńie (arbore binar infinit şi etichetat). Fie ΓΓΓΓ un alfabet (mulŃime finită şi nevidă). Un arbore binar orientat, infinit, etichetat peste ΓΓΓΓ este o funcŃie T : {0, 1}* → ΓΓΓΓ

Automate şi limbaje 25• Ideea definiŃiei precedente nu prea seamănă cu definiŃia

uzuală a unui arbore binar, este aceea că domeniul funcŃiei este constituit din toate drumurile posibile de la rădăcină la celelalte noduri

• Arcele care ies din fiecare nod sunt etichetate cu 0 („stânga”) sau 1 („dreapta”), ştiind că din fiecare nod „ies” cel mult două arce (dacă lipsesc nişte arce, funcŃia de mai sus este practic o funcŃie parŃială

• Nodurile au etichete din ΓΓΓΓ. Dacă w ∈ {0, 1}* şi T(w) = a ∈ ΓΓΓΓ, atunci w este un drum (unic identificabil!) de la rădăcină la un nod etichetat cu a

• T(λ) reprezintă eticheta rădăcinii. În desenul următor (nu am specificat etichetele tuturor nodurilor) este reprezentat în mod clasic un arbore peste ΓΓΓΓ = {a, b} (conform noii definiŃii ar trebui însă să „dăm complet”funcŃia T: T(λ) = a, T(0) = b, T(1) = a, T(00) = b, etc.)

Automate şi limbaje 27• Un automat pe arbori este tot un 5-uplu

A = <∑∑∑∑, S, δ, S0, F> (semnifica Ńia sintactic ă rămâne aceea şi) dar el trebuie desigur în Ńeles (semantic) ca o descriere a unei mul Ńimi de arbori (care va constitui limbajul acceptat în noul context) şi nu a unei mul Ńimi de cuvinte. Atunci ΣΣΣΣ, S, S0 şi F pot r ămâne la fel, dar δδδδ trebuie modificat. În cazul determinist vom avea δ : S × ∑∑∑∑ →→→→ S × S iar în cazul nedeterminist δ : S × ∑∑∑∑ →→→→ 2S × S

Automate şi limbaje 28• Defini Ńie (automate pe arbori infini Ńi). Se va

numi automat (determinist/nedeterminist, pe arbori infiniŃi), un 5-uplu A = <∑∑∑∑, S, δ, S0, F>, unde:-S este mulŃimea stărilor.-δ : S × ∑∑∑∑ → S × S este funcŃia/relaŃia de tranziŃie (în cazul determinist), iar δ : S × ∑∑∑∑ → 2S × S este funcŃia/relaŃia de tranziŃie(în cazul nedeterminist)-S0 ⊆⊆⊆⊆ S este mulŃimea stărilor iniŃiale.-∑∑∑∑ este alfabetul simbolurilor/simbolilor de intrare-F reprezintă mulŃimea stărilor finale, adică:F ⊆ S, sau F ⊆ 2S, sau F ⊆ 2S × 2S


• Daca arborii nu sunt binari, este posibil sa se mai adauge un element la 5-uplul anterior (stânga/dreapta este implicit)

• FaŃă de cuvinte, este mai dificil de a defini limbajul acceptat (semantica automatului). Arborii „candida Ńi la acceptare” vor fi desigur func Ńiile T : {0, 1}* →→→→ ΣΣΣΣ. Intuitiv, pentru ca un asemenea arbore s ă fie acceptat, trebuie urma Ńi urm ătorii pa şi:

Automate şi limbaje 30-Se eticheteaz ă (suplimentar) r ădăcina arborelui candidat cu o stare din S 0-Se „propag ă” această nouă etichetare (similar ă cu secven Ńa de st ări de la automatele pe cuvinte) la nodurile succesoare conform rela Ńiei de tranzi Ńie. În cazul determinist, dac ă un nod x (de fapt, identificat unic printr-un cuvânt w ∈∈∈∈ {0, 1}*) este etichetat cu a ∈∈∈∈ ∑∑∑∑ (T(w) = a) şi suplimentar cu starea s ∈∈∈∈ S şi avem în plus δδδδ(s, a) = <s 1, s2> atunci succesorii s ăi imedia Ńi, x0 – cel stâng (adic ă w0) şi x1 – cel drept (adic ă w1), vor fi eticheta Ńi suplimentar cu s 1respectiv s 2. În cazul nedeterminist ( şi în aceea şi situa Ńie de mai sus), vom avea δδδδ(s, a) = {<s 1, t1>, <s2, t2>, … , <sk, tk>} şi atunci x 0 va fi suplimentar etichetat cu {s 1, s2, … , sk} iar x 1 cu{t 1, t2, … , tk}

-Un arbore va fi acceptat (va face parte din limbaj ) dacă etichet ările suplimentare satisfac condi Ńia de acceptare

Automate şi limbaje 31• Defini Ńie (cale în automate pe arbori; arbori

accepta Ńi). Fie A = <∑∑∑∑, S, δ, S0, F> un automat pe arbori. O cale pentru un arboreT : {0, 1}* →→→→ ΣΣΣΣ este o func Ńie ρ : {0, 1}* →→→→ S, care satisface condi Ńiile:-ρ(λ) ∈∈∈∈ S0-ρ este compatibil ă cu rela Ńia de tranzi Ńie, adic ă:∀∀∀∀w ∈∈∈∈ {0, 1}*, <ρ(w0), ρ(w1)> = δ(ρ(w), T(w)) –în cazul determinist şi∀∀∀∀w ∈∈∈∈ {0, 1}*, <ρ(w0), ρ(w1)> ∈∈∈∈ δ(ρ(w), T(w)) –cazul nedeterminist


• Arborele T este acceptat de automatul A, pornind cuS0 şi depinzând de F (în sens Büchi, Büchigeneralizat, Rabin sau Street ) dacă exist ă o cale ρpentru care avem ( pentru fiecare d, drum infinit în T) respectiv:(a) F ⊆⊆⊆⊆ S şi inf(d) ∩ F ≠ Ø: Büchi (B)(b) F ⊆⊆⊆⊆ 2S, F = {F1, F2, … , Fm} şi inf(d) ∩ Fi ≠ Ø pentru fiecare i ∈∈∈∈ [m]: Büchi generalizată (GB)(c) F ⊆⊆⊆⊆ 2S ×××× 2S, F = {<G1, B1>, <G2, B2>, … , <Gn, Bn>} astfel încât exist ă măcar o pereche <G, B> ∈∈∈∈ F cu inf(d) ∩ Gi ≠ Ø şi inf(d) ∩ B i = Ø: Rabin (R)(d) F ⊆⊆⊆⊆ 2S ×××× 2S, F = {<G1, B1>, <G2, B2>, … , <Gn, Bn>} şi pentru fiecare i ∈∈∈∈ [n] avem inf(d) ∩ Gi = Ø sau inf(d) ∩ B i ≠ Ø: Street (S)

Automate şi limbaje 33• Mul Ńimea tuturor arborilor accepta Ńi de un

automat A = <∑∑∑∑, S, δ, S0, F> va constitui limbajul acceptat , notat LAX ωωωω(A, S0, F), unde X ∈∈∈∈ {B, GB, R, S} (conform condi Ńiilor de acceptare (a) – (d) de mai sus)

• Este evident c ă no Ńiunea de drum într-un arbore trebuie în Ńeleasă în sens clasic si c ă pentru orice pereche <T, ρ> drumurile (infinite) pot fi „gândite” drept cuvinte (infinite) peste S (nota Ńia având astfel sens)


Rezultate importante• Începem cu automatele pe cuvinte infinite. După cum am

mai precizat, vom lua în considerare doar automatele nedeterministe (care sunt mai generale) având S şi ΣΣΣΣfinite şi nevide.

• Teorem ă (închideri Büchi pe cuvinte). Clasa limbajelor Büchi este închisă la reuniune, intersecŃie, proiecŃie (pe subalfabete) şi complementariere (pe un acelaşi alfabet)

• Observa Ńie. DemonstraŃiile pentru reuniune, intersecŃie şi proiecŃie sunt aproape imediate în timp ce demonstrarea închiderii la complementariere nu este deloc trivială. Automatele „noi” construite în cursul demonstraŃiilor sunt uneori de tipul Büchi generalizat


• Se poate însă arăta uşor că pentru orice automat Büchi generalizat (nedeterminist) există un automat Büchi determinist care acceptă acelaşi limbaj

• Pentru ultima afirmaŃie din observaŃie vom furniza doar un exemplu. Automatul Büchigeneralizat A = <∑∑∑∑, S, δ, S0, F> este desenat mai jos, mulŃimile în cauză fiind uşor de identificat. Să precizăm totuşi că F = {F1, F2}, F1 = {s0}, F2 = {s1} (de aceea nodul s0 are şi eticheta suplimentară 1 iar nodul s1 are eticheta 2):

Automate şi limbaje 42• Problema (de decizie a) (ne)vidităŃii pentru o clasă de

automate se enunŃă în felul următor: „Există algoritm care având la intrare orice automat din clasa fixată se termină şi ieşirea este DA dacă limbajul acceptat de automat este vid şi NU în caz contrar?”

• Teorem ă (problema nevidit ăŃii Büchi pe cuvinte) . Problema vidităŃii pentru clasa automatelor Büchi este rezolvabilă (decidabilă) în timp liniar şi spaŃiu logaritmic nedeterminist

• În cursul demonstraŃiei teoremei precedente se folosesc alŃi algoritmi cunoscuŃi cum ar fi testarea faptului dacă o stare este accesibilă dintr-o altă stare (eventual iniŃială; inclusiv din ea însăşi) sau calcularea componentelor tare conexe ale unui graf orientat. AfirmaŃia din teoremă este valabilă (exceptând complexitatea) şi pentru automatele Rabin (timp polinomial) sau Street (timp exponenŃial). Ambele demonstraŃii folosesc faptul că pentru orice automat Rabin (Street) există un automat Büchiechivalent cu el (adică, automat care acceptă acelaşi limbaj)


• Continuăm cu câteva rezultate privind automatele pe arbori „clasice” (nealternate). Reamintim că lucrăm cu automate finite şi astfel anumite rezultate anterioare se pot păstra (de exemplu, pentru fiecare automat Büchi nedeterminist pe arbori, există unul determinist „echivalent”)

• Ca şi mai înainte, dacă nu facem alte precizări, vom folosi doar automate nedeterministe

• Teorem ă (închideri pentru limbaje Büchi pe arbori). Clasa tuturor limbajelor Büchi pe arbori este închisă la reuniune, intersecŃie şi proiecŃie. Această clasă nu este închisă la complementariere

Automate şi limbaje 44• Teorem ă (problema nevidit ăŃii Büchi pe arbori).

Problema (ne)vidităŃii pentru clasa limbajelor Büchi acceptate de automate pe arbori nedeterministe este decidabilă în timp pătratic (şi este PTIME-completă)

• Să observăm că (ne)viditatea este decidabilă şi pentru clasele Rabin (problema este însă NP-completă) şi Street (pentru aceasta nu există algoritm polinomial nici măcar nedeterminist). Ca o compensaŃie, clasele Rabin şi Street sunt închise la complementariere

• Teorem ă (închideri pentru automate alternate). Clasa limbajelor alternate este închisă la intersecŃie, reuniune, proiecŃie şi complementariere

• Închiderea la intersecŃie şi reuniune este imediată, precum şi închiderea la complementariere (dar nu pentru toate tipurile de acceptare). Închiderea la proiecŃie precum şi testarea (ne)vidităŃii implică algoritmi exponenŃiali chiar şi în cazul condiŃiei Büchi

CURS 3

• Viziunea asupra realităŃii

Sisteme reactive şi modele formale ale lor: sisteme concurente formale (FCS) şi

sisteme tranzi Ńionale (TS) 1• Informal, sistemele reactive sunt sisteme reale complexe

(implicând concurenŃa şi nedeterminismul) care interacŃionează în mod coerent şi continuu cu mediul

• Datorită complexităŃii lor şi (de cele mai multe ori a) gradului major de risc în funcŃionarea lor „corectă”, este de dorit să dispunem de o metodă credibilă, simplă, eficientă de a specifica şi verifica formal, cu ajutorul calculatorului (comportarea unor) asemenea sisteme (aprioric , adică înaintea proiectării definitive şi a punerii lor „în lucru”)

• Este implicit presupusă împărŃirea în subsisteme şi„reacŃia” sistemului la evoluŃia mediului

Sisteme reactive şi modele formale ale lor: sisteme concurente formale (FCS) şi

sisteme tranzi Ńionale (TS) 2

• Necesitatea unor asemenea modele abstracte credibile este evidentă în momentul în care alte tipuri de modele nu există sau pur şi simplu nu pot fi construite

• Să reŃinem că automatele sunt destinate reprezentării unor mulŃimi iar sistemele concurente formale şi sistemele tranziŃionale sunt dedicate reprezentării sintaxei şi semanticii sistemelor reactive

Sisteme concurente formale 1• Aşa cum este cazul cu majoritatea definiŃiilor formale

(datorită cerinŃelor legate de eficienŃă şi securitate), definiŃia care urmează nu este exhaustivă. Mai precis, se vor lua în considerare doar acele sisteme reale/reactive(numite şi procese nedeterministe concurente sau, simplu, procese) care:

-Au un număr fixat aprioric de componente „interne”distincte, numite procese (secvenŃiale); sistemele modelate nu sunt prin urmare scalabile

-Fiecare componentă are un număr finit de stări „de control” (numite şi locaŃii sau etichete). Dacă privim procesele ca fiind (în particular) programe, putem spune şi că am adoptat paradigma imperativă

Sisteme concurente formale 2-Procesele componente au acces la o memorie comună

(stare „internă”), reprezentată printr-un număr fixat aprioric de variabile (sau celule de memorie). Fiecare asemenea proces poate avea şi o memorie locală dar aceasta nu poate fi accesată direct de către celelalte

-„FuncŃionarea” sistemului se face prin realizarea unor „acŃiuni” de către componente. Efectul acŃiunilor asupra sistemului este descris cu ajutorul tranziŃiilor. TranziŃiile pot specifica: o schimbare a stării de control pentru unul sau mai multe procese (vom avea tranziŃii simple sau tranziŃii reunite); o condiŃie (gardă) asupra variabilelor (pentru ca acŃiunea descrisă să fie permisă şi tranziŃia să se efectueze, condiŃia trebuie să fie adevărată); o mulŃime de asignări simultane prin care se poate modifica memoria comună

Sisteme concurente formale 3• Defini Ńie (sisteme concurente formale). Un sistem

concurent formal (FCS) este un 3-uplu F = <P, M, T>, unde:

-P = {p1, p2, … , pn} este o mulŃime finită, nevidă, de procese (secvenŃiale). Fiecare p ∈ P are ataşată o mulŃime finită, nevidă, de stări de control (etichete, locaŃii) notată l(p) = {lp,0, lp,1, … lp,kp}. lp,0 se va numi locaŃia iniŃială a procesului p. Este satisfăcută condiŃia suplimentară (∀p, q ∈ P)(p ≠ q ⇒⇒⇒⇒ l(p) ∩ l(q) = ∅). Vom pune şi Up∈Pl(p) = L

-M = {x1, x2, … , xm} este memoria comună (mulŃime finită, nevidă de variabile, celule). Fără a preciza explicit codomeniul, presupunem şi existenŃa unei funcŃii J care atribuie o valoare iniŃială J(x) fiecărei variabile x ∈ M

Sisteme concurente formale 4

-T = {t1, t2, … , tk} este o mulŃime finită, nevidă de tranziŃii (acŃiuni). Fiecare tranziŃie t ∈∈∈∈ T este de fapt un 6-uplu t = <n(t), p(t), ls(t), ld(t), c(t), a(t)>, în care:

(a) n(t) este numele (identificatorul) tranziŃiei(b) p(t) ⊆⊆⊆⊆ P este mulŃimea proceselor care sunt

active pentru t (procesele inactive pentru t nu vor fi afectate de „producerea” tranziŃiei)

(c) ls(t) = {ls(t, pi) ∈ l(pi)| (∀∀∀∀i ∈ [n])(pi ∈ p(t)}, ceea ce înseamnă că fiecare tranziŃie t are o locaŃie sursă, notată ls(t, pi), pentru fiecare proces activ pentru ea, pi


(d) ld(t) = {ld(t, pi) ∈ l(pi)| (∀i ∈ [n])(pi ∈ p(t)}, ceea ce înseamnă că fiecare tranziŃie t are o locaŃie destinaŃie, notată ld(t, pi), pentru fiecare proces activ pentru ea, pi

(e) c(t) este o „condiŃie booleană aplicată unor predicate peste variabilele din M”;(f) a(t) este o mulŃime de asignări „operând asupra variabilelor”

Sisteme concurente formale 6• Vom putea astfel descrie complet o tranziŃie prin -t = nume, active : (surse, c → a, destinaŃii), unde nume =

n(t), active = p(t), surse = ls(t), destinaŃii = ld(t). În privinŃa condiŃiilor c(t), ele vor fi desigur formule din LP1(dar nu vom preciza cu exactitate limbajul logic peste care sunt construite). Asignările sunt multiple, adică de forma <v1, v2, … , vj> := <exp1, exp2, … , expj>. Ca şi în limbajele uzuale de programare, expresiile vor fi (simultan) evaluate (folosind valorile curente ale variabilelor) apoi rezultatele obŃinute vor fi atribuite corespunzător variabilelor. Exemplul de mai jos este o prezentare simplificată a binecunoscutului Algoritm al lui Dekker (de excludere mutuală) în cadrul formalismului tocmai introdus. Se consideră sistemul reactiv (programul, procesul concurent) p : : = p1 || p2, alcătuit din procesele (programele imperative) secvenŃiale p1 şi p2. Acestea nu fac altceva decât să modifice separat flag-urile c1 şi c2 cu ajutorul variabilei trn. Ele sunt reprezentate prin scheme logice şi pot fi făcute, uşor, mai complicate (şi numărul de procese poate fi mărit fără ca ideea generală să se schimbe)

Sisteme concurente formale 8• Să reprezentăm procesul anterior ca un FCS, FFFF = <PPPP, MMMM, TTTT>. Vom

pune succesiv:-P = {p1, p2} cu l(p1) = {lp1,0, lp1,1, …, lp1,7}, {lp2,0, lp2,1, …, lp2,7}-M = {c1, c2 , trn} cu J(c1) = 1, J(c2) = 1, J(trn) = 1. -TTTT = {t1, t2, … , t22}, unde t1, t2, … , t11 sunt respectiv (t1 este numită

rem1, t2 este t1,2, t4 este crit1, t5 este t1,5, t12 este rem2, etc.):• rem1, p1 : (lp1,0, true → () := (), lp1,1) (vezi şi „poza”…)• t1,2, p1 : (lp1,1, true → (c1) := (0), lp1,2)• t1,3, p1 : (lp1,2, c2 = 1 → () := (), lp1,6)• crit1, p1 : (lp1,6, true → () := (), lp1,7)• t1,5, p1 : (lp1,7, true → (trn, c1) := (2,1), lp1,0)• t1,6, p1 : (lp1,2, c2 = 0 → () := (), lp1,3)• t1,7, p1 : (lp1,3, trn = 1 → () := (), lp1,2)• t1,8, p1 : (lp1,3, trn = 2 → () := (), lp1,4)• t1,9, p1 : (lp1,4, true → (c1) := (1), lp1,5)• t1,10, p1 : (lp1,5, trn = 2 → () := (), lp1,5)• t1,11, p1 : (lp1,5, trn = 1 → () := (), lp1,1)

Sisteme concurente formale 9Iar t12, t13, … , t22 sunt (similar):• rem2, p2 : (lp2,0, true → () := (), lp2,1)• t2,2, p2 : (lp2,1, true → (c1) := (0), lp2,2)• t2,3, p2 : (lp2,2, c1 = 1 → () := (), lp2,6)• crit2, p2 : (lp2,6, true → () := (), lp2,7)• t2,5, p2 : (lp2,7, true → (trn, c1) := (1,1), lp2,0)• t2,6, p2 : (lp2,2, c1 = 0 → () := (), lp2,3)• t2,7, p2 : (lp2,3, trn = 2 → () := (), lp2,2)• t2,8, p2 : (lp2,3, trn = 1 → () := (), lp2,4)• t2,9, p2 : (lp2,4, true → (c1) := (1), lp2,5)• t2,10, p2 : (lp2,5, trn = 1 → () := (), lp2,5)• t2,11, p2 : (lp2,5, trn = 2 → () := (), lp2,1)


• În cele de mai sus, asignărilesimultane sunt „obişnuite” (exceptând t5 şi t16) , adică de forma x := exp(scris (x) := (exp)). Prin () := () vom înŃelege asignarea „vidă” (nu efectuează nici o transformare asupra variabilelor)

• Prin true vom înŃelege condiŃia adevărată permanent

Sisteme tranzi Ńionale 1• Sistemele tranziŃionale vor reprezenta semantica

operaŃională a sistemelor concurente formale şi, ca urmare, a sistemelor reactive. Aceasta deşi reprezintă, pentru început, tot un concept sintactic (similar cu cel de automat) având propria semantică

• Defini Ńie (sisteme tranzi Ńionale). Un sistem tranziŃional(TS) este un 4-uplu TS = <ΣΣΣΣ, S, s0, T>, unde

-Σ - este o mulŃime de etichete (alfabet – mulŃime finită şi nevidă)

-S – este o mulŃime de stări (nu neapărat finită)-s0 ∈ S – reprezintă starea iniŃială-T ⊆ S × ∑∑∑∑ × S – este o mulŃime (nevidă) de tranziŃii. O

tranziŃie va fi, în acest context, un triplet t = <s1, a, s2> în care s1 ∈ S este sursa, s2 ∈ S este destinaŃia iar a ∈ ΣΣΣΣeste o etichetă

Sisteme tranzi Ńionale 2• Asemănarea cu automatele este evidentă. Prin urmare,

dacă S este finită, un sistem tranziŃional va putea fi şi el reprezentat ca un digraf (graf orientat) etichetat. Fiecare stare este reprezentată printr-un nod (faŃă de automate, există o singură stare iniŃială si nu există stări finale) iar o tranziŃie printr-un arc etichetat cu o etichetă, de la starea sursă la starea destinaŃie (inclusiv acestea)

• Semantica „directă” (operaŃională) a unui sistem tranziŃional (aşa cum semantica unui automat era dată de limbajul acceptat), este dată de mulŃimea comportărilor sale (finite sau nu)

• O condiŃie suplimentară de acceptare se va adăuga atunci când va fi necesar

Sisteme tranzi Ńionale 3

• Defini Ńie (comport ările unui sistem tranzi Ńional). O comportare infinită σ a unui sistem tranziŃional TS = <ΣΣΣΣ, S, s0, T> este un cuplu de funcŃii σ = <σS, σT>, σS : N → S, σT : N → ΣΣΣΣ, astfel încât (elementele lui N se mai numesc şi momente, în acest context):

• σS(0) = s0 şi• (∀i ≥ 0)(<σS(i), σT(i), σS(i+1)> ∈ T) – grafic…• În mod similar se poate defini noŃiunea de

comportare finită

Sisteme tranzi Ńionale 4• O comportare (infinită) poate fi astfel reprezentată grafic

prin:σT(0) σT(1) σT(2)

σS(0) → σS(1) → σS(2) → …• La fiecare moment i, se mai spune că acŃiunea σT(i) a

fost permisă în starea σS(i) şi aleasă pentru execuŃie, sau, că tranziŃia <σS(i), σT(i), σS(i+1)> a fost (permisă şi) executată

• Vom nota cu Comp(TS) (respectiv Compf(TS)) mulŃimea comportărilor infinite (respectiv finite) ale sistemului tranziŃional TS

Sisteme tranzi Ńionale 5• Defini Ńie (sistemul tranzi Ńional ata şat unui sistem concurent

formal) . Fie FFFF = <PPPP, MMMM, TTTT> un sistem concurent formal. Sistemul tranziŃional ataşat lui F, TSF = <ΣΣΣΣ, S, s0, T>, este definit prin:

-ΣΣΣΣ = {n(t) | t ∈ T}-Dacă PPPP = {p1, p2, … , pn}, MMMM = {x1, x2, … , xm} şi pentru fiecare i ∈ [m]

mulŃimea valorilor admise pentru variabila xi este Vi, atunci S = l(p1)×… ×l(pn)×V1×… ×Vm. Cu alte cuvinte, o stare în TSFeste un n+m-uplu constând dintr-o stare de control (element din F) pentru fiecare proces (eticheta „instrucŃiunii” la care a ajuns „execuŃia” procesului respectiv, privit ca program imperativ) precum şi dintr-o valoare „curentă” pentru fiecare variabilă a memoriei comune (din F). Pentru fiecare stare s ∈ S, vom nota cu s(pi) locaŃia corespunzătoare pentru pi şi cu s(xj) valoarea curentă a variabilei xj(i ∈ [n], j ∈ [m]). Atunci o stare s ∈ S (în TSF) va avea forma s = <s(p1), …, s(pn), s(x1), …, s(xm)>

-Starea iniŃială a lui TSF va fi s0 = <lp1,0, lp2,0, …, lpn,0, J(x1), … , J(xm)>

Sisteme tranzi Ńionale 6-Pentru fiecare tranziŃie t ∈ T (t = <n(t), p(t), ls(t), ld(t), c(t), a(t)>) şi

pentru fiecare stare s ∈ S, vom spune că t este admisă (posibilă, permisă) în s dacă pentru fiecare proces pi care este activ pentru t avem s(pi) = ls(t, pi) şi condiŃia c(t) este satisfăcută pentru valorile s(x1), …, s(xm) (ale variabilelor în starea s). În această situaŃie, TSFva conŃine o tranziŃie t având eticheta n(t), sursa s ∈ S şi destinaŃia s’ ∈ S (t = <s, n(t), s’>), unde: -Pentru fiecare proces pi care nu este activ pentru t, punem s’(pi) = s(pi)-Pentru fiecare proces pi care este activ pentru t, punem s’(pi) = ld(t, pi)-Pentru fiecare variabilă xi care nu este modificată de a(t), punem s’(xi) = s(xi)

-Pentru fiecare variabilă xi pentru care a(t) îi asignează o expresie expi, punem s’(xi) = [expi]s unde [expi]s este valoarea expresiei expi în care valorile variabilelor sunt cele din S. Să observăm că date s ∈ Sşi t ∈ T, starea s’ este unică

Sisteme tranzi Ńionale 7• DefiniŃia anterioară poate fi interpretată ca semantica formală a unui

sistem reactiv reprezentat ca un FCS, F. Această semantică, Compf(TSF), imperativă, este de tip interleaving. Într-adevăr, toate comportările „intuitiv normale” (relativ la procesele componente) vor fi elemente ale lui Compf(TSF)

• Astfel, pentru a „progresa” într-o comportare, trebuie să „alegem”unul dintre procesele secvenŃiale active pentru o tranziŃie permisă la acel pas. Odată ce o tranziŃie permisă t ∈ T este selectată pentru a fi aplicată într-o stare s ∈ S, împreună cu un proces activ corespunzător p ∈ P, se poate unic determina (după cum am precizat) starea „următoare” (a comportării curente), s’ ∈ S

• Practic, se modifică doar valorile variabilelor şi locaŃiilor afectate de p şi t. Există însă (în general) mai multe astfel de procese/tranziŃii posibile de a fi alese la un anumit moment de „timp” în cursul unei comportări şi toate pot fi alese „pe rând”. Pentru a obŃine o comportare a sistemului se întrepătrund comportările proceselor secvenŃiale componente

• Unele dintre acestea sunt însă „inechitabile”: este posibil ca un anumit proces, deşi poate „progresa”, să fie permanent omis

Sisteme tranzi Ńionale 8• CondiŃiile de echitate reprezintă restricŃii calitative asupra

comportării sistemelor, impunând „avansarea”funcŃionării proceselor componente fără alte presupuneri de natură cantitativă. Ele ar putea fi gândite ca o abstractizare a politicilor particulare de gestionare a proceselor secvenŃiale, oricare ar fi ele

• În lipsa lor nu s-ar putea demonstra nici o proprietate a sistemelor concurente care necesită un „progres global”al unor componente

• Pentru a studia asemenea proprietăŃi generale ale FCS –urilor (cum ar fi echitatea) se va introduce noŃiunea de proces observator prin care putem „prinde”şi interacŃiunea unui sistem reactiv cu „mediul înconjurător”

• Un proces de tip observator este un proces secvenŃial suplimentar care „urmăreşte” comportările unui FCS (proces) fără a i le modifica (activitatea respectivă s-ar putea numi şi monitorizare)

CURS 4

• Logici temporale

Logici temporale 1• Logica temporală (mai corect: logicile

temporale) reprezintă o extensie a logicii clasice, timpul (interpretat discret şi nu continuu) fiind reprezentat implicit prin anumiŃi operatori sintactici şi apoi tratat explicit în semantică

• Logicile temporale se constituie într-un limbaj potrivit pentru a descrie proprietăŃi importante ale unor secvenŃe infinite (sau arbori infiniŃi), care pot reprezenta comportările unui sistem real

Logici temporale 2

• Logica temporală este, în acelaşi timp, un caz particular al logicii modale şi chiar al logicii dinamice, având şi implementări comerciale de succes

• În logica modală, principala idee este aceea că adevărul unei formule depinde de contextul în care aceasta apare

• Contextul îl poate reprezenta universul, timpul , sistemul de operare, mediul de programare, etc., şi este privit ca o mulŃime nevidă de stări care inter-relaŃionează

Logici temporale 3

• Structura/interpretarea unei formule în cazul unor asemenea logici neclasice (care, pentru „fragmentele” alese de noi, vor rămâne extensionale şi bivalente, bazate pe tertium non datur), va furniza o valoare de adevăr pentru fiecare stare dintr-un context dat

• Dacă dispunem şi de o relaŃie prin care se pot stabili legături între stări, atunci ne putem uşor imagina modalitatea prin care putem defini adevărul global al unei formule

• În logica dinamică relaŃia este generată de execuŃia unor „programe” (acŃiuni cumva externe universului considerat)

• Stare = situaŃie sistem; stări “corelate” = comportaresistem; formulă adevărată = proprietate satisfăcută

Logica temporală cu timp liniar 1• Vom începe cu o scurtă descriere a sintaxei şi semanticii

logicii temporale (propoziŃionale) cu timp liniar (LTL ), la nivel intuitiv

• Dacă ne gândim la sintaxa LP, formulele din LTL vor conŃine, înafara variabilelor propoziŃionale şi a conectorilor cunoscuŃi (∧,∨, ) cu ajutorul cărora se exprimă adevăruri generale, independente de timp, şi nişte operatori noi numiŃi operatori temporali (de viitor)

• Dintre aceştia (primii trei sunt unari iar ultimii doi, binari) amintim: ○ – circle /next (la_momentul_următor);□ - box /always (întotdeauna_în_viitor); ◊ - diamond /eventually (cândva_în_viitor); U – until (până_când); Ũ – releases (declanşează_în_viitor)

Logica temporală cu timp liniar 2• Din punct de vedere semantic se va schimba noŃiunea

de structură/interpretare. Formulele vor primi (gradual, constructiv) o valoare de adevăr (0 sau 1), posibil diferită, în funcŃie de secvenŃa aleasă, de valorile de adevăr ale variabilelor propoziŃionale în fiecare element al secvenŃei şi de operatorii care intră în componenŃa formulei

• Elementele unei secvenŃe (cuvânt infinit) se mai numesc stări, ele identificând (în mod uzual) anumite situaŃii la diversele locuri/momente de timp (elementele lui N). A alege o secvenŃă înseamnă de fapt a alege stările componente (identificate prin mulŃimea variabilelor propoziŃionale adevărate în ea) şi ordinea acestora. Să considerăm astfel secvenŃa următoare care conŃine stările s0, s1, s2, s3, s0, s1, s2, s3, … (respectiv pe poziŃiile/momentele 0,1, 2, 3, 4, 5, 6, 7, …)

Logica temporală cu timp liniar 3

unde s0 = {p, q}, s1 = { p, q}, s2 = { p, q} = s3 (p şi q fiind variabile

propoziŃionale):

Logica temporală cu timp liniar 4• Formulele F1 = p ∧ q şi F2 = ○(p ∧ q) sunt

adevărate în starea marcată iar F3 = □p este falsă în întreaga secvenŃă

• Dacă privim totul din punctul de vedere al logicii modale, universul ar fi constituit din clasa tuturor stărilor, relaŃia între stări fiind practic relaŃia totală pe univers (şi nu o succesiune temporală)

• Alegerea secvenŃelor drept „suport” al semanticii se încadrează în una dintre clasele particulare de modele pentru logicile modale

Logica temporală cu timp liniar 5• Pentru definiŃiile formale, vom porni cu

alfabetul logic L = A U Ā U P U C1 U C2, undeA = {p1, p2, …} este mulŃimea (nevidă, cel mult numărabilă) a variabilelor propoziŃionale (sau a literalilor pozitivi), Ā = {p1, p2, …} este mulŃimea negaŃiilor variabilelor propoziŃionale (a literalilor negativi), P = {( , )} este mulŃimea parantezelor, C1 = {∨, ∧} este mulŃimea conectorilor booleeni iar C2 = {○, U, Ũ} este mulŃimea operatorilor temporali

Logica temporală cu timp liniar 6• Pentru că nu am introdus aici şi

cuantificatorii, LTL este mai degrabă o extensie a LP decât a LP1. De aceea această mulŃime se mai numeşte şi logică temporală propoziŃională

• Faptul că este şi cu timp liniar va fi justificat de semantică (modalitatea de definire a unei structuri = obŃinere valori de adevăr pentru formule)

Logica temporală cu timp liniar 7• Defini Ńie (sintaxa LTL).Baza (formule atomice):(i) true , false sunt formule atomice şi elemente ale LTL(ii) Pentru fiecare p ∈A, atât p, cât şi p (∈ Ā) pot fi formule

atomice şi elemente ale LTL (nu simultan într-o aceeaşi stare – vezi semantica)

Pas constructiv (formule noi din formule vechi):(a) Dacă F1, F2 ∈ LTL , atunci (F1 ∧ F2), (F1 ∨ F2) ∈ LTL(b) Dacă F ∈ LTL , atunci (○F) ∈ LTL(c) Dacă F1, F2 ∈ LTL , atunci (F1 U F2), (F1 Ũ F2) ∈ LTL(d) Dacă F ∈ LTL , atunci (F) ∈ LTL(e) Nimic altceva nu mai este în LTL

Logica temporală cu timp liniar 8• Observa Ńie. FaŃă de cazul „clasic” am ales să

introducem (posibil) şi negaŃiile variabilelor propoziŃionale în mulŃimea formulelor atomice, dar negaŃia nu mai poate fi aplicată formulelor compuse

• După definirea semanticii vom vedea că acest dezavantaj poate fi eliminat (la fel ca şi absenŃa explicită a celorlalŃi operatori temporali amintiŃi, ◊şi □, care sunt „mai simpli”)

• Considerarea „constantelor” true şi false ca formule atomice este justificată de simplificarea exprimării unor rezultate

• Nicio astfel de modificare nu schimbă esenŃial rezultatele principale deja cunoscute

Logica temporală cu timp liniar 9• Dacă nu există confuzii, folosind priorităŃi pentru

operatori vom elimina anumite paranteze corespondente din scrierea formulelor. PriorităŃile acceptate în majoritatea cazurilor sunt: 0 – pentru cei unari, 1 – pentru ∧, ∨ şi 2 (şimai mare) – pentru restul

• Defini Ńie (drum /cale /structur ă). Se numeşte drum (cale, structură) pentru o logică LTL o funcŃie π : N → 2A. Pentru un drum π vom nota cu πi sufixul lui π obŃinut prin înlăturarea primelor sale i stări, adică funcŃia πi : N → 2A dată prin πi(j) = π(i+j), pentru fiecare j ∈ N

Logica temporală cu timp liniar 10• Defini Ńie (semantica LTL). Valoarea de adevăr pentru

formulele LTL într-o cale π se obŃine structural astfel:Baza:(i) π ⊨ true şi π ⊭ false(ii) π ⊨ p dacă şi numai dacă p ∈ π(0), şi π ⊨p dacă şi

numai dacă p ∉ π(0) (pentru fiecare p ∈ A)Pas constructiv:(a) π ⊨ (F1 ∧ F2) dacă şi numai dacă π ⊨ F1 şi π ⊨ F2, iar

π ⊨ (F1 ∨ F2) dacă şi numai dacă π ⊨ F1 sau π ⊨ F2

(b) π ⊨ (○F) dacă şi numai dacă π1 ⊨ F(c) π ⊨ (F1 U F2) dacă şi numai dacă există i ≥ 0 astfel încât

πi ⊨ F2 şi pentru fiecare 0 ≤ j < i avem πj ⊨ F1, iarπ ⊨ (F1 Ũ F2) dacă şi numai dacă pentru fiecare i ≥ 0 cu πi ⊭ F2, există 0 ≤ j < i astfel încât πj ⊨ F1

(d) π ⊨ (F) dacă şi numai dacă π ⊨ F

Logica temporală cu timp liniar 11• Intuitiv (şi…nu numai):-O formulă este adevărată într-o cale dacă şi numai dacă

ea este adevărată în starea iniŃială a căii respective-Dacă o variabilă propoziŃională nu aparŃine unei stări,

atunci implicit se consideră că „aparŃine” negaŃia ei (nu şi reciproc: dacă p ∉ s nu înseamnă că p ∈ s)

-Pentru nici o stare s şi atom p nu putem avea atât p ∈ s cât şi p ∈ s

-U: fie F2 este adevărată în toată calea, fie „de la un loc încolo”, dar în acest caz „până acolo” este mereuadevărată F1

-Ũ: pentru fiecare loc din cale „începând cu care” F2 nu este adevărată, există „un loc anterior” în care esteadevărată F1

Logica temporală cu timp liniar 12• Observa Ńie. Se pot adăuga explicit chiar la nivel

sintactic (în C1) alŃi conectori clasici, cum ar fi implicaŃia (→) sau echivalenŃa (↔), precum şi operatorul temporal (binar, de viitor, în C2) W – unless (doar_dacă_nu) cu semnificaŃia: π ⊨ F (F = (F1 W F2)) dacă şi numai dacă pentru fiecare i ∈ N avem πi ⊨ F1 U F2 sau πi ⊨ (□F1)

• (◊F) şi (□F) pot fi introduse acum drept prescurtări pentru (true U F) respectiv (false Ũ F) adică avem π ⊨ (◊F) dacă şi numai dacă π ⊨ (true U F) şi respectiv π ⊨ (□F) dacă şi numai dacă π ⊨ (false Ũ F)

• Intuitiv : -(◊F) este adevărată într-o cale dacă şi numai dacă există

un loc „în care” F este adevărată-(□F) este adevărată într-o cale dacă şi numai dacă F este

adevărată în fiecare loc (false nu poate fi adevărată înnici o poziŃie…)

Logica temporală cu timp liniar 13• Putem aplica astfel negaŃia şi formulelor

oarecare din LTL dacă Ńinem cont de adevărul afirmaŃiilor (mai bine, citit invers primele patru; şi „de la coadă la cap”):

- π ⊭ (F1 U F2) dacă şi numai dacă π ⊨ (F1) Ũ (F2)

- π ⊭ (F1 Ũ F2) dacă şi numai dacă π ⊨ (F1) U (F2)

- π ⊭ (○F) dacă şi numai dacă π ⊨ (○(F))

- π ⊨ (F) dacă şi numai dacă nu este adevărat că π ⊨ F, adică, dacă şi numai dacă avem π ⊭ F

Logica temporală cu timp liniar 14• Conform notaŃiilor şi convenŃiilor cunoscute,

π ⊨ F înseamnă că π este model pentru F (F este adevărată în π, F este satisf ăcut ă în π)

• Ideea (repetăm) este că o cale reprezint ă o structur ăşi că o formul ă este adev ărată într-o cale π dacă şi numai dacă ea este adevărată în starea ini Ńială a acelei c ăi

• De exemplu, (○F) este adevărată în π dacă şi numai dacă ea este adevărată în π(0), adică dacă şi numai dacă F este adevărată în π1, adică dacă şi numai dacă F este adevărată în π1(0), adică dacă şi numai dacă F este adevărată în π(1+0) = π(1), care este de fapt starea imediat succesoare lui π(0)

• Am folosit metodologia „clasică”:

Logica temporală cu timp liniar 15-Se porneşte cu o structură (asignare, interpretare) simplă

prin care se atribuie valori de adevăr variabilelor propoziŃionale. Practic, în cazul nostru, începem cu o mulŃime numărabilă (de fapt, cuvânt infinit) de stări, fiecare fiind element al lui 2A. Dacă s ∈ 2A şi p ∈ s, atunci p este adevărată în s (dacă p ∉ s, atunci negaŃiasa este adevărată în s, adică p este falsă în s)

-Se extinde structura la formule. Practic, ne interesează adevărul unei formule în anumite mulŃimi particulare de stări şi anume în drumuri. Adevărul unei formule într-un drum/cale este unic determinat de adevărul formulei în starea iniŃială a drumului, adevăr care (conform definiŃiei structurale) se reduce în final la adevărul, în anumite stări (de asemenea unic determinate) a variabilelor propoziŃionale componente

Logica temporală cu timp liniar 16• Transformările/prescurtările sintactice menŃionate nu

modifică puterea de exprimare a fragmentului de logică temporală ales. Acest lucru nu se mai întâmplă însă dacă adăugăm „întâmplare” la L variabile, simboluri funcŃionale/predicative şi cuantificatori (în sens clasic), sau (în C2) operatori temporali de trecut cum ar fi (primii trei sunt unari iar următorii doi – binari): ● – previously(imediat_anterior); ⊕⊕⊕⊕ - sofar (până_acum); �� - once(cândva); S – since (începând_cu); B – backto(înapoi_la). Nu precizăm pe moment semnificaŃiile exacte ale acestora deşi există suficiente indicaŃii de ordin intuitiv pentru ca ele să fie deduse; în acest cazsunt însă necesare şi anumite modificări formale (cum ar fi faptul că un drum este o funcŃie π : Z → 2A, etc.)

Logica temporală cu timp liniar 17• Exemplu. Fie p, q, r ∈ A variabile propoziŃionale şi

formulele F1 = □(p →(○q)), F2 = □(p → ○(q U r)), F3 = □(◊p), F4 = (p Ũ q). Atunci:

-F1 este satisfăcută în toate drumurile care satisfac condiŃia: fiecare stare a sa în care p este adevărată, este imediat urmată de o stare în care q este adevărată(altfel, p este falsă)

-F2 este satisfăcută în toate drumurile care satisfac condiŃia: dacă p este satisfăcută într-o stare a sa atunci, începând cu starea imediat următoare acesteia şi în următoarele, q este şi rămâne falsă şi acest lucru se întâmplă până când apare (ceea ce se întâmplă cu siguranŃă) o stare în care r este adevărată (altfel…)

-F3 este satisfăcută în toate drumurile care satisfac condiŃia: p este adevărată (în viitor) într-o infinitate de stări (altfel…)

-F4 este satisfăcută în toate drumurile care satisfac condiŃia: p este permanent adevărată, exceptând cazul în care această obligaŃie este exceptată prin faptul că p a fost deja adevărată într-o stare anterioară(declanşare…)

Logica temporală cu timp liniar 18• Din acest moment putem folosi în cadrul LTL toate

conceptele şi notaŃiile clasice, atât la nivel semantic cât şi sintactic (deşi n-am amintit nici un sistem deductiv specific, încă): formule satisfiabile (F este satisfiabilă dacă există o cale π astfel încât π ⊨ F), valide, contradicŃii; consecinŃă semantică; echivalenŃă tare şi slabă; axiomă, teoremă, consecinŃă sintactică; etc. Şi anumite rezultate cunoscute se menŃin

• Dar, esen Ńial este s ă privim o formul ă ca fiind dat ă printr-o mul Ńime de drumuri infinite şi anume acelea care constituie un model pentru ea . În acest mod vom putea „lega” formulele de automate, transferând problemele de tip SAT în altă „zonă” (de exemplu, testarea vidităŃii unor limbaje; intersecŃii, incluziuni, etc.)

Logica temporală cu timp liniar 19• Exemplu(reluat…). Fie formula F = (◊p), p ∈ A.

Conform definiŃiilor, avem π ⊨ (◊p) dacă şi numai dacă π ⊨ (true U p) adică dacă şi numai dacă există i ≥ 0 astfel încât πi ⊨ p şi pentru fiecare 0 ≤ j < i avem πj ⊨ true . Aceasta înseamnă că π ⊨ (◊p) dacă şi numai dacă există i ≥ 0 astfel încât πi ⊨ p. Prin urmare, F este adevărată în toate secvenŃele π pentru care p este adevărată măcar într-o stare

• Să construim un automat A = <∑∑∑∑, S, δ, S0, F> şi o condiŃie de acceptare X (X ∈ {B, GB, R, S}) astfel încât LXωωωω(A, S0, F) = {π : N → 2A | (∃i ≥ 0)(πi ⊨ p)}. łinând cont de codomeniul unui drum, evident că ∑∑∑∑ = 2A. Este de asemenea clar că S0 şi F trebuie să conŃină măcar o stare (să zicem s0 respectiv s1) şi că ele trebuie să fie distincte. Automatul de mai jos satisface egalitatea cerută (este nedeterminist, cu condiŃie de acceptare Büchi; deci LB ωωωω; desigur 2A = {Ø, {p}}):

Logica temporală cu timp liniar 20• Deci, automatul care acceptă doar

structurile π care sunt modele pentru F = (◊p) poate fi :

Logica temporală cu timp liniar 21• Generalizând, pentru a determina (folosind un

alt algoritm decât cel semantic) dacă o cale (cuvânt infinit) π : N → 2A satisface o formulă F ∈ LTL (este suficient să presupunem că AconŃine doar variabilele propoziŃionale peste care este construită F, prop(F)), vom începe prin a eticheta stările lui π cu subformule ale lui F în aşa fel încât etichetarea să fie compatibilă cu semantica LTL

• Pentru evitarea confuziilor, furnizăm una din definiŃiile formale (structurale) ale lui cl(F) (noi o notasem subf(F)), F ∈ LTL


• Defini Ńie (închiderea unei formule). Fie orice F∈ LTL .

Baza: F ∈ cl(F)Pas constructiv : (i) Dacă (F1 ○ F2) ∈ cl(F), unde

○ ∈ {∧,∨,U,Ũ}, atunci F1, F2 ∈ cl(F)(ii) Dacă (○G) sau (G) ∈ cl(F) atunci

G ∈ cl(F)• (iii) Nimic altceva nu mai este în cl(F)


• Evident că dacă am renunŃat la anumite paranteze corespondente (altfel obligatorii) dintr-o formulă, prin stabilirea unor priorităŃi asupra operatorilor (nu mai insistăm aici), acest lucru se va reflecta şi în conŃinutul închiderii. De exemplu, cl(◊ p) = {◊ p, p}

• Defini Ńie (etichetarea unui drum cu subformule).Fie F∈ LTL şi π : N → 2A, unde A conŃine doar variabilele propoziŃionale care apar în F. O etichetare viabilă a lui π cu elemente din cl(F) este o funcŃie τ : N → 2cl(F) care, pentru fiecare i ∈ N satisface condiŃiile:

(a) Fie orice p ∈ A. Dacă p ∈ π(i) atunci p ∈ τ(i) iar dacă p ∈ π(i) atunci p ∉τ(i)

(b) Dacă (F1 ∧ F2) ∈ τ(i) atunci F1 ∈ τ(i) şi F2 ∈ τ(i)(c) Dacă (F1 ∨ F2) ∈ τ(i) atunci F1 ∈ τ(i) sau F2 ∈ τ(i)


(d) Dacă (○F) ∈ τ(i) atunci F ∈ τ(i+1)

(e) Dacă (F1 U F2) ∈ τ(i) atunci fie F2 ∈ τ(i), fie (F1 ∈ τ(i) şi (F1 U F2) ∈ τ(i+1))

(f) Dacă (F1 Ũ F2) ∈ τ(i) atunci F2 ∈ τ(i) şi (fie F1 ∈ τ(i) fie (F1 Ũ F2) ∈ τ(i+1))

CURS 5

• Continuare LTL• Început CTL

Logica temporală cu timp liniar 25• Observa Ńie. Nu se poate ca la punctul (a) să

avem atât p ∈ τ(i) cât şi p ∈ τ(i) datorită definiŃiilor anterioare

• Dacă punctele (a)-(c) sunt absolut naturale (semantica operatorilor booleeni fiind o semantică locală, „de stare”) punctele următoare privesc operatorii temporali care au o semantică (globală) exprimată cu ajutorul unei întregi căi

• Şi acestea devin naturale dacă ne reamintim faptul că adevărul unei formule într-o cale se reduce în final la adevărul formulei (subformulelor) în anumite „stări iniŃiale”. Mai mult, sunt adevărate echivalenŃele:

-(i) (F1 U F2) ≡ F2 ∨ (F1 ∧ ○(F1 U F2))-(ii) (F1 Ũ F2) ≡ F2 ∧ (F1 ∨ ○(F1 Ũ F2))• O formulă de tipul (i) se va numi eventualitate

Logica temporală cu timp liniar 26• Defini Ńie (formule, satisfiabilitate şi etichet ări

viabile). O cale π : N → 2A satisface o formulă F∈ LTL dacă există o etichetare viabilă τ : N → 2cl(F) satisfăcând condiŃiile:

(a) F ∈ τ(0)(b) Pentru fiecare i ∈ N, dacă o eventualitate

(F1 U F2) ∈ τ(i) atunci există j ≥≥≥≥ i astfel încât F2 ∈ τ(j)

• Prin cele de mai sus am definit de fapt structural, pentru fiecare F∈ LTL un automat care acceptă exact mulŃimea acelor secvenŃe (drumuri, căi) care sunt modele pentru F

Logica temporală cu timp liniar 27• Defini Ńie (automatul pe cuvinte infinite ata şat unei

formule din LTL). Fie F∈ LTL. Se numeşte automat ataşat lui F automatul (nedeterminist, având asociată o condiŃie de acceptare de tip Büchi generalizată) AF = <∑∑∑∑, S, δ, S0, F>, unde:

-ΣΣΣΣ = 2A (simbolurile de intrare sunt mulŃimi de variabilepropoziŃionale; este suficient să considerăm doar acele variabile care apar în F)

-S = {s ∈ 2cl(F) | ((F1∧F2) ∈ s ⇒ F1 ∈ s şi F2 ∈ s) şi ((F1∨F2) ∈ s ⇒ F1 ∈ s sau F2 ∈ s)} (stările reprezintă posibile etichete viabile locale)

-δ : S × ∑∑∑∑ → 2S, funcŃia de tranziŃie, verifică dacă acele posibile etichete (booleene) locale sunt „potrivite” cu secvenŃa care ar trebui să fie acceptată ((1), (2)). De asemenea, sunt verificate şi condiŃiile asupra secvenŃei care „Ńin” de operatorii temporali ((3)-(5)). Mai exact, vom avea t ∈ δδδδ(s, a) dacă şi numai dacă următoarele afirmaŃii sunt adevărate:

Logica temporală cu timp liniar 28(1) Pentru fiecare p ∈ A, dacă p ∈ s atunci p ∈ a(2) Pentru fiecare p ∈ A, dacă p ∈ s atunci p ∉ a(3) Dacă (○F) ∈ s atunci F ∈ t(4) Dacă (F1 U F2) ∈ s atunci fie F2 ∈ s, fie

(F1 ∈ s şi (F1 U F2) ∈ t)(5) Dacă (F1 Ũ F2) ∈ s atunci F2 ∈ s şi (fie F1 ∈ s fie

(F1 Ũ F2) ∈ t)-S0 = {s ∈ S | F ∈ s} (stările iniŃiale sunt cele care conŃin

formula dată F)• Pentru a fixa condiŃia de acceptare, trebuie să mai

impunem ceea ce încă nu a fost făcut asupra secvenŃelor candidate, adică acele condiŃii de viabilitate legate de formulele din cl(F) care sunt eventualităŃi

Logica temporală cu timp liniar 29• Să presupunem astfel că o eventualitate (G U H) ∈ cl(F)

va fi notată cu eG(H) şi că toate eventualităŃile din cl(F) sunt eG1(H1), eG2(H2), … , eGm(Hm). Ştim deja (datorită relaŃiei de tranziŃie) că începând cu fiecare stare care conŃine eG(H), această formulă va continua să fie prezentă şi în toate stările care urmează, până la prima stare în care apare H

• Astfel, este suficient să cerem ca, pentru fiecare eventualitate eG(H) ∈ cl(F), secvenŃa candidat să conŃină fie o infinitate de apariŃii ale unei stări care nu conŃine pe eG(H), fie o infinitate de apariŃii ale unei stări care conŃine atât pe eG(H) cât şi pe H

• În concluzie, vom pune mulŃimea de stări finaleF = {Φ1, Φ2, … , Φm}, unde Φi = {s ∈ S | (eGi(Hi) şi Hi ∈ s) sau (eGi(Hi) ∉ s)}, pentru fiecare i ∈ [m]


• Deoarece este suficient să considerăm (în A) doar variabilele propoziŃionale care apar într-o formulă F şi numărul acestora este finit, rezultă că AF poate fi construit algoritmic. Problema satisfiabilităŃii unei formule din LTL se poate astfel reduce la problema apartenenŃei unui cuvânt (infinit) la un limbaj dat şi anume la limbajul acceptat de automatul ataşat formulei (demonstraŃia este imediată din definiŃiile anterioare)

Logica temporală cu timp liniar 31• Teorem ă (satisfiabilitate în LTL).

Fie F∈ LTL , AF = <∑∑∑∑, S, δ, S0, F> automatul ataşat, LGB ωωωω(AF, S0, F) limbajul acceptat de AF şi π : N → 2A

o cale (iar: este suficient să considerăm prop(F) în loc de întreg A). Atunci π ⊨ F dacă şi numai dacă

π ∈ LGB ωωωω(AF, S0, F)

Logica temporală cu timp liniar 32• Exemplu. Vom relua formula dintr-un exemplu

precedent, adică F = (◊p), p ∈ A, şi vom construi un (alt) automat care acceptă acelaşi limbaj, adică {π : N → 2A|(∃i ≥ 0)(πi ⊨ p)}, conform algoritmului sugerat de definiŃia anterioară

• Acest limbaj este LGB ωωωω(AF, S0, F), unde

F = {{1, 3, 4}} (care practic este chiar o condiŃie Büchi şi nu Büchi generalizată). Pe desen nu am inclus chiar toate tranziŃiile care ar trebui generate, ele nefiind importante (relativ la secvenŃele acceptate):

Logica temporală cu timp liniar 33Deci

Logica temporală cu timp liniar 34• Se observă că, deşi deja simplificat, automatul ataşat

este destul de „stufos” chiar pentru formule simple. Se pot aduce şi alte îmbunătăŃiri în construcŃia sa, vizând tot reducerea numărului de stări şi tranziŃii „inutile”, cum ar fi:

-Automatul se poate construi succesiv, pornind cu formula dată F, descompunând şi expandând operatorii temporali

-Stările care diferă doar prin variabilele propoziŃionale pot fi „comasate”, deoarece ele pot fi „reidentificate” datorită etichetelor tranziŃiilor (arcelor care intră în ele)

-Procesul de expandare poate fi oprit mai devreme de nivelul propoziŃional dacă se detectează cumva noduri care vor fi inutile


• Avem desigur (vezi rezultatele menŃionatela automate):

• Teorem ă (decidabilitatea SAT pentru LTL). Problema satisfiabilităŃii (validităŃii,nesatisfiabilităŃii) pentru clasa formulelor logicii (propoziŃionale) cu timp liniar este decidabilă

Logica temporală (propoziŃională) cu timp ramificat 1

• DiferenŃa principală faŃă de logica temporală (propoziŃională) cu timp liniar este faptul că timpul nu mai este considerat a fi liniar ci arborescent, adică, pentru fiecare stare curentă (moment) pot exista mai multe stări succesoare

• Această presupunere este naturală dacă ne gândim la nedeterminismul generat implicit de evoluŃia concurentă a proceselor

• Se schimbă din nou noŃiunea de structură, de la cuvânt infinit la arbore infinit

Logica temporală cu timp ramificat2

• Defini Ńie (structur ă Kripke, temporal ă). O structură Kripke temporală este un 6-uplu K = <A, W, R, w0, Π>, unde:

-A este mulŃimea variabilelor propoziŃionale (cel mult numărabilă)

-W este mulŃimea stărilor sau lumilor universului (nevidă; finită – dacă nu se precizează altfel)

-R ⊆ W × W este o relaŃie de trecere (sau, de accesibilitate), totală, adică satisface condiŃia (∀w ∈ W)(∃w’ ∈ W)(<w, w’> ∈ R)

-w0 ∈ W este starea iniŃială-Π : W → 2A este o funcŃie care va ataşa fiecărei stări

mulŃimea variabilelor propoziŃionale adevărate în acea stare


• Să observăm că datorită faptului că relaŃia R este totală, din fiecare stare w ∈ W „porneşte”un drum (secvenŃă infinită de stări) π = w0, w1, … care satisface proprietatea (∀i ≥ 0)(<wi, wi+1> ∈ R). Desigur că în definiŃia precedentă am pus w = w0 (nu neapărat w0!)

• Dacă identific ăm pentru un drum π elementul π(i) cu Π(w i), putem spune c ă din fiecare stare a unei structuri Kripke, K, “începe”(măcar) o structură (cale, drum; sequence, path) pentru LTL

• Vom spune că aceste structuri LTL sunt generate de K


• În acest mod, graful care prezintă structura (vezi mai jos) poate fi „expandat ” la un arbore cu rădăcina w0, din fiecare nod „pornind ” câte (m ăcar) o structură LTL

• O structură Kripke poate fi, la rândul ei, prezentată printr-un graf orientat etichetat în care noduri sunt stările lui W (etichetele sunt mulŃimi de variabile propoziŃionale reprezentând funcŃia Π) iar arcele reprezintă relaŃia R

• De exemplu, în cele de mai jos avem structura dată prin A = {p, q}, W = {w0, w1}, Π(w0) = {p}, Π(w1) = {q} iar Reste relaŃia totală adică R = {<p, p>,<p, q>,<q, p>,<q, q>} (în cerculeŃe trebuiau puse de fapt w0 respectiv w1 iar p şi/sau q trebuie puse dedesubt, între {}, corespunzător)


• De început trebuie însă să începem în mod obişnuit, adică cu sintaxa formală a noii (noilor) logici

• La alfabetul logic cunoscut, L = A U Ā U {true , false } U P U C1 U C2 se adaugă însă şi o mulŃime C3 = {E, A}, a cuantificatorilor (cuantorilor)de cale

• Vom pune L U C3 = Alf , deoarece transformarea anterioară este de aceeaşi „natură” cu trecerea de la LPla LP1

• Intuitiv, aceşti cuantificatori se vor aplica formulelor LTLcare vor deveni (în noul context) aşa-numitele formule de stare, formule care vor fi mai departe folosite pentru construcŃia formulelor de cale

• A se „citeşte” pentru fiecare iar E – există măcar - de unde şi denumirea de cuantori

• Spre deosebire de cuantorii din LP1 ei nu se aplică unor „variabile” ci unor formule, ceea ce face dificil de a aprecia unde este „locul exact” al CTL*/CTL în comparaŃie cu logicile clasice LP/LP1


• Defini Ńie (sintaxa CTL*). Fie Alf alfabetul logic menŃionat mai sus. MulŃimea formulelor logicii temporale (propoziŃionale, generalizate)cu timp ramificat (Computational Tree Logic – CTL* sau CTL*Alf ) este dată (bi)structural (imbricat) prin:

Formule de stareBaza_1 (formule atomice de stare)(i1) true , false sunt formule atomice (de stare) şi elemente ale CTL*(ii1) Pentru fiecare p ∈A, fie p, fie p (exclusiv ) sunt formule atomice

(de stare) şi elemente ale CTL* (vom scrie p sau p)Pas constructiv_1 (formule noi din formule vechi)(a1) Dacă F1, F2 ∈ CTL* sunt formule de stare, atunci (F1 ∧ F2) sau

(F1 ∨ F2) ∈ CTL* sunt formule de stare(b1) Dacă F ∈ CTL* este formulă de cale, atunci A(F) sau E(F) ∈ CTL*

sunt formule de stare(c1) Dacă F ∈ CTL* este formulă de stare, atunci (F) ∈ CTL* este

formulă de stare(d1) Nimic altceva nu mai este formulă de stare


Formule de caleBaza_2 (formule atomice de cale)(i2) Orice formulă de stare din CTL* este şi formulă

(atomică) de cale în CTL*Pas constructiv_2 (formule noi din formule vechi)(a2) Dacă F ∈ CTL* este formulă de cale, atunci

(○F) ∈ CTL* este formulă de cale(b2) Dacă F1, F2 ∈ CTL* sunt formule de cale, atunci

(F1 ∧ F2), (F1 ∨ F2) ∈ CTL* sunt formule de cale(c2) Dacă F1, F2 ∈ CTL* sunt formule de cale, atunci

(F1 U F2), (F1 Ũ F2) ∈ CTL* sunt formule de cale(d2) Dacă F ∈ CTL* este formulă de cale, atunci

(F) ∈ CTL* este formulă de cale(e2) Nimic altceva nu mai este formulă de cale


• Schimbându-se definiŃia sintactică, se va schimba şi definiŃia cl(F) pentru F ∈ CTL* (şi apoi pentru F ∈ CTL), într-un mod absolut evident. Am putea nota cu CTLS* mulŃimea formulelor de stare şi cu CTLC* mulŃimea formulelor de cale, dar de fapt identific ăm CTL* cu CTL S*, prin conven Ńie. Mai mult, vom lucra în principal cu o restricŃie a lui CTL*, notată CTL (logica liniară cu timp ramificat standard)

• Avem CTL ⊊ CTL*, condiŃia fiind aceea că orice operator temporal trebuie imediat precedat de un cuantificator de cale (deocamdată, la nivel sintactic)


• Defini Ńie (sintaxa CTL). DefiniŃia este identică cu cea anterioară (inclusiv, desigur, convenŃia şi înlocuind peste tot CTL* cu CTL) exceptând următoarele:

-În (a2), textul „Dacă F ∈ CTL* este formulă de cale , atunci(○F) ∈ CTL* este formulă de cale” se înlocuieşte cu:

(a2’) Dacă F ∈ CTL este formulă de stare , atunci(○F) ∈ CTL este formulă de cale

-În (c2), textul „Dacă F1, F2 ∈ CTL* sunt formule de cale , atunci (F1 U F2), (F1 Ũ F2) ∈ CTL* sunt formule de cale”se înlocuieşte prin:(c2’) Dacă F1, F2 ∈ CTL sunt formule de stare , atunci (F1 U F2), (F1 Ũ F2) ∈ CTL sunt formule de cale


• Exemplu. Sunt formule CTL* (de stare): A(p → (○E(□p)), A(□(◊p)), E(□(◊p)).

• Sunt formule CTL (de stare): A(□p), E(□p), A(□E(○p)), E(□E(◊p)).

• Dacă adoptăm priorităŃile clasice pentru operatori, formulele se vor putea scrie şi ca: A(p → ○E□p), A(□◊p), E(□◊p), respectiv A□p, E□p, A□E○p, E□E◊p

• În cele de mai sus, p ∈ A iar (din nou, clasic) F → G este o prescurtare pentru F ∨ G


• Defini Ńie (semantica CTL* /CTL).Fie K = <A, W, R, w0, Π> o structură Kripke. Adevărul formulelor CTL* în K se obŃine structural, în trei faze „imbricate”

(I) Adev ărul formulelor CTL* într-o stare oarecare din W:

Baza_I(iI) Pentru fiecare w ∈ W, w ⊨ true şi w ⊭ false(iiI) Pentru fiecare w ∈ W, w ⊨ p dacă şi numai dacă

p ∈ Π(w), şi w ⊨p dacă şi numai dacă p ∉ Π(w) (pentru fiecare p ∈ A)


• Pas constructiv_I(aI) Pentru fiecare w ∈ W, w ⊨ (F1 ∧ F2) dacă şi numai dacă

w ⊨ F1 şi w ⊨ F2 (pentru fiecare F1, F2 ∈ CTL*)(bI) Pentru fiecare w ∈ W, w ⊨ (F1 ∨ F2) dacă şi numai dacă

w ⊨ F1 sau w ⊨ F2 (pentru fiecare F1, F2 ∈ CTL*)(cI) Pentru fiecare w ∈ W, avem w ⊨ A(F) dacă şi numai

dacă pentru fiecare drum (structură LTL generată de K) începând cu w, π = w0, w1, … (w0 = w), este adevărat că π ⊨ F (pentru fiecare F ∈ CTL*)

(dI) Pentru fiecare w ∈ W, avem w ⊨ E(F) dacă şi numai dacă există un drum (structură LTL generată de K) începând cu w, π = w0, w1, … (w0 = w), astfel încât π ⊨ F (pentru fiecare F ∈ CTL*)


(II) Adev ărul formulelor CTL* /CTL într-un drum de st ări din W (privit ca structur ă LTL generat ă de K) :

Baza_II(iII) Fie F orice formulă de stare din CTL*/CTL şi

π = w0, w1, … orice secvenŃă infinită de stări din W (structură LTL geenerată de K). Atunci avem π ⊨ F dacă şi numai dacă w0 ⊨ F (din nou, o formulă este adevărată într-o structură LTLgenerată de K, dacă şi numai dacă ea este adevărată în starea iniŃială a acelei structuri)


• Pas constructiv_II(aII) Fie F1, F2 ∈ CTL* şi π o structură LTL generată de K.

Atunci π ⊨ (F1 ∧ F2) dacă şi numai dacă π ⊨ F1 şi π ⊨ F2

(bII) Fie F1, F2 ∈ CTL* şi π o structură LTL generată de K. Atunci π ⊨ (F1 ∨ F2) dacă şi numai dacă π ⊨ F1 sau π ⊨ F2

(cII) Fie F ∈ CTL* şi π o structură LTL generată de K. Atunci π ⊨ (○F) dacă şi numai dacă π1 ⊨ F

(dII) Fie F1, F2 ∈ CTL* şi π o structură LTL generată de K. Atunci π ⊨ (F1 U F2) dacă şi numai dacă există i≥0 astfel încât πi ⊨ F2 şi pentru fiecare 0≤ j< i avem πj ⊨ F1

(eII) Fie F1, F2 ∈ CTL* şi π o structură LTL generată de K. Atunci π ⊨ (F1 Ũ F2) dacă şi numai dacă pentru fiecare i≥0 cu πi ⊭ F2, există 0≤ j< i astfel încât πj ⊨ F1


(III) Adev ărul formulelor CTL* /CTL în K . O formulă F ∈ CTL* este adevărată într-o structură Kripke, K, dacă si numai dacă ea este adevărată în orice structură LTL , π, generată de K, care porneşte cu starea iniŃială w0 (adică K ⊨ F dacă şi numai dacă π ⊨ F, pentru fiecare π ca mai înainte)


• Ne vom ocupa în continuare de satisfiabilitateaformulelor CTL

• La fel ca în cazul LTL , ideea este să identificăm mai întâi o astfel de formulă cu mulŃimea structurilor Kripke care sunt model pentru ea şi apoi să „generăm” automatul pe arbori care acceptă ca limbaj exact mulŃimea acestor structuri

• Şi metodologia generală este similară, adică vom începe prin a eticheta o structură Kripke„candidat” cu subformule ale formulei date, Ńinând cont de anumite reguli semantice


• Defini Ńie (etichetarea unei structuri Kripke cu subformule). Fie F∈ CTL şi K = <A, W, R, w0, Π> o structură Kripke, unde AconŃine doar variabilele propoziŃionale care apar în F. O etichetare viabilă a lui K cu elemente dincl(F) este o funcŃie τ : W → 2cl(F) care, pentru fiecare w ∈ W satisface condiŃiile:

(a) Fie orice p ∈ A. Dacă p ∈ τ(w) atunci p ∈ Π(w) iar dacă p ∈ τ(w) atunci p ∉ Π(w)

(b) Dacă (F1 ∧ F2) ∈ τ(w) atunci F1 ∈ τ(w) şi F2 ∈ τ(w)

(c) Dacă (F1 ∨ F2) ∈ τ(w) atunci F1 ∈ τ(w) sau F2 ∈ τ(w)


(d) Dacă A(○F) ∈ τ(w) atunci pentru fiecare w’ cu <w, w’> ∈ R avem F ∈ τ(w’)

(e) Dacă E(○F) ∈ τ(w) atunci există w’cu <w, w’> ∈ R astfel încât F ∈ τ(w’)

(f) Dacă A(F1 U F2) ∈ τ(w) atunci fie F2 ∈ τ(w), fie (F1 ∈ τ(w) şi pentru fiecare w’ cu <w, w’> ∈ R avem A(F1 U F2) ∈ τ(w’))


(g) Dacă E(F1 U F2) ∈ τ(w) atunci fie

F2 ∈ τ(w), fie (F1 ∈ τ(w) şi există w’ cu <w, w’> ∈ R astfel încât E(F1 U F2) ∈ τ(w’))

(h) Dacă A(F1 Ũ F2) ∈ τ(w) atunci F2 ∈ τ(w) şi (fie F1 ∈ τ(w) fie, pentru fiecare w’ cu <w, w’> ∈ R avem A(F1 Ũ F2) ∈ τ(w’))

(i) Dacă E(F1 Ũ F2) ∈ τ(w) atunci F2 ∈ τ(w) şi (fie F1 ∈ τ(w), fie există w’ cu

<w, w’> ∈ R astfel încât E(F1 Ũ F2) ∈ τ(w’))


• Observa Ńie. Şi în acest caz punctele (a)-(c) sunt naturale (semantica operatorilor booleeni fiind o semantică locală, „de stare”) iar punctele următoare privesc operatorii temporali şi formulele de cale din CTL. Acestea au o semantică (globală) exprimată cu ajutorul structurilor (căilor, drumurilor) LTL generate de K. Ele devin la rândul lor naturale dacă folosim echivalenŃele (de demonstrat…):

-A(F1 U F2) ≡ F2 ∨ (F1 ∧ A(○A(F1 U F2)))-E(F1 U F2) ≡ F2 ∨ (F1 ∧ E(○E(F1 U F2)))-A(F1 Ũ F2) ≡ F2 ∧ (F1 ∨ A(○A(F1 Ũ F2)))-E(F1 Ũ F2) ≡ F2 ∧ (F1 ∨ E(○E(F1 Ũ F2)))


• În acest caz vom avea dou ă tipuri de eventualităŃi: A(F1 U F2) şi E(F1 U F2)

• Ca şi în cazul LTL , pentru aceste formule vor fi necesare nişte condiŃii suplimentare privind etichetările viabile

• În primul caz, F2 trebuie să apară în toate drumurile (structurilor LTL generate de K) care încep cu starea etichetată de eventualitatea respectivă, iar în al doilea F2 trebuie să apară măcar pe un drum pe care F1 este adevărată în toate stările care „preced” starea etichetată cu acea eventualitate


• Defini Ńie (formule, satisfiabilitate şi etichet ări viabile). O structură K = <A, W, R, w0, Π>, este model pentru o formulă F∈ CTL dacă există o etichetare viabilă τ : W → 2cl(F) satisfăcând condiŃiile:

(a) F ∈ τ(w0)(b) Pentru fiecare w ∈ W, dacă o eventualitate

A(F1 U F2) ∈ τ(w) atunci pentru fiecare drum (structură LTL generată de K) şi începând cu w, există pe acel drum un w’ (<w, w’> ∈ R) astfel încât F2 ∈ τ(w’)

(c) Pentru fiecare w ∈ W, dacă o eventualitate E(F1 U F2) ∈ τ(w) atunci există măcar un drum (structură LTL generată de K) şi începând cu w, astfel încât există pe drum un w’ (<w, w’> ∈ R) astfel încât F2 ∈ τ(w’) şi F1 este adevărată în stările de pe drum începând cu w până la w’


• Prin cele de mai sus am definit structural, pentru fiecare F∈ CTL, un automat care acceptă exact mulŃimea acelor arbori infiniŃi (structuri Kripke) care sunt modele pentru F

• Din păcate aceşti arbori nu sunt binari (gradul de ieşire pentru fiecare nod poate fi mai mare ca doi) şi suntem nevoiŃi să modificăm definiŃiile (deja cunoscute) relative la arbori oarecare (având gradele de ieşire/ramificare ale nodurilor într-o mulŃime D) şi automatele corespunzătoare


• Defini Ńie (arbori nebinari , infini Ńi, eticheta Ńi). Fie ΓΓΓΓ un alfabet (mulŃime finită şi nevidă) şi D ⊆ N (de fapt D se presupune a fi de forma {0, 1, … , k}, adică un segment iniŃial din N) mulŃimea gradelor maxime (de ieşire). Un arbore orientat, infinit, cu un grad variabil de ramificare, etichetat, peste ΓΓΓΓ este o funcŃie T : D* → Г

• Din nou, ca şi în cazul LTL , domeniul funcŃiei este constituit din toate drumurile posibile de la rădăcină la celelalte noduri. Arcele care ies dintr-un anumit nod vor fi etichetate respectiv cu 0, 1, … n-1 dacă gradul de ieşire al acelui nod este n ∈ D. Dacă D = {0, 1, … , k} şi n<k pentru măcar un nod, atunci T este o funcŃie parŃială

• Dacă w ∈ D* şi T(w) = a ∈ Г, atunci w este un drum (unic identificabil!) de la rădăcină la un nod etichetat cu a

• T(λ) reprezintă eticheta rădăcinii


• Defini Ńie (automatul alternat, pe arbori infini Ńi, ataşat formulelor din CTL). Fie F ∈ CTL. Se numeşte automat ataşat lui F automatul (determinist, având asociată o condiŃie de acceptare de tip Büchi pe arbori nebinari) ADF = <∑∑∑∑, D, S, δ, S0, F>, unde:

-ΣΣΣΣ = 2A (simbolurile de intrare sunt mulŃimi de variabile propoziŃionale; este suficient să considerăm doar acele variabile care apar în F)

-D este ca mai sus-S = cl(F) (este suficient, deoarece automatele alternate permit

etichetarea multiplă a nodurilor)-δ : S × ∑∑∑∑ × D → LPP1. Expresia (formula) din codomeniu face parte

(sintactic) dintr-o logică propoziŃională pozitivă (adică fără negaŃie, construită peste alfabetul A = N × S şi mulŃimea de conectori C = {∧, ∨}) şi fiind adevărată în „structurile convenabile” (similar cu ceea ce se întâmpla cu LP1=; am notat această logică prin LPP1)

-FuncŃia de tranziŃie “verifică” dacă acele posibile etichete booleene locale sunt „potrivite” cu secvenŃa care ar trebui să poată fi acceptată. Sunt verificate şi condiŃiile asupra secvenŃei care „Ńin” de operatorii temporali:


(1) Pentru fiecare p ∈ A, a ∈ 2A şi k ∈ D, dacă p ∈ a atunci δ(p, a, k) = true

(2) Pentru fiecare p ∈ A, a ∈ 2A şi k ∈ D, dacă p ∉ a atunci δ(p, a, k) = false

(3) Pentru fiecare p ∈ A, a ∈ 2A şi k ∈ D, dacă p ∉ a atunci δ(p, a, k) = true

(4) Pentru fiecare p ∈ A, a ∈ 2A şi k ∈ D, dacă p ∈ a atunci δ(p, a, k) = false

(5) Pentru fiecare F1, F2 ∈ CTL, a ∈ 2A şi k ∈ D, δ(F1 ∧ F2, a, k) = δ(F1, a, k) ∧ δ(F2, a, k)


(6) Pentru fiecare F1, F2 ∈ CTL, a ∈ 2A şi k ∈ D,δ(F1 ∨ F2, a, k) = δ(F1, a, k) ∨ δ(F2, a, k)

(7) Pentru fiecare F ∈ CTL, a ∈ 2A şi k ∈ D, δ(A(○F), a, k) = ∧c=0

k-1 <c, F>

(8) Pentru fiecare F ∈ CTL, a ∈ 2A şi k ∈ D, δ(E(○F), a, k) = ∨c=0

k-1 <c, F>

(9) Pentru fiecare F1, F2 ∈ CTL, a ∈ 2A şi

k ∈ D, δ(A(F1 U F2), a, k) = δ(F2, a,k) ∨ (δ(F1, a, k) ∧ ∧c=0

k-1 <c, A(F1 U F2)>)


(10) Pentru fiecare F1, F2 ∈ CTL, a ∈ 2A şi k ∈ D, δ(E(F1 U F2), a, k) = δ(F2, a, k) ∨ (δ(F1, a, k) ∧ ∨c=0

k-1 <c, E(F1 U F2)>)(11) Pentru fiecare F1, F2 ∈ CTL, a ∈ 2A şi k ∈ D,

δ(A(F1 Ũ F2), a, k) = δ(F2, a, k) ∧ (δ(F1, a, k) ∨ ∧c=0

k-1 <c, A(F1 Ũ F2)>)(12) Pentru fiecare F1, F2 ∈ CTL, a ∈ 2A şi k ∈ D,

δ(E(F1 Ũ F2), a, k) =δ(F2, a, k) ∧ (δ(F1, a, k) ∨ ∨c=0

k-1 <c, E(F1 Ũ F2)>)• S0 = {F}• F (mulŃimea de stări finale) conŃine toate formulele de

tipul AŨ şi EŨ din cl(F) (vezi (h), (i) din Defini Ńie)


• ADF poate fi construit algoritmic şi problema satisfiabilităŃii unei formule din CTL se poate reduce la problema apartenenŃei unui arbore (infinit) la un limbaj dat şi anume la limbajul acceptat de automatul ataşat formulei (demonstraŃia este imediată din definiŃiile anterioare):

• Teorem ă (satisfiabilitate în CTL). Fie F∈ CTL,ADF = <∑∑∑∑, D, S, δ, S0, F> automatul ataşat, LAB ωωωω(ADF, S0, F) limbajul acceptat de ADF şi K = <A, W, R, w0, Π> o structură Kripke. Atunci K ⊨ F dacă şi numai dacă K ∈ LAB ωωωω(ADF, S0, F)


• Exemplu. Fie formula

F = A(◊A(□p)) ∈ CTL, cu A = {p} şi D –oarecare. Atunci ADF = <∑∑∑∑, D, S, δ, S0, F> este dat de: ∑∑∑∑ = {{p}, Ø}, S = {F, A□p, p}, S0 = {F}, F = {A□p}. Pentru construcŃia lui S (adică a lui cl(F)), am eliminat parantezele şi am considerat doar „stările utile”, care sunt şi formule de stare

• FuncŃia de tranziŃie δ este dată tabelar prin:


q | δ(q, {p}, k) | δ(q, Ø, k)__________________________________p | true | falseA□p | ∧∧∧∧c=0

k-1 <c, A□p>) | falseF | ∧∧∧∧c=0

k-1 <c, A□p>) ∨∨∨∨ (∧∧∧∧c=0k-1 <c, F>) |

|∧∧∧∧c=0k-1 <c, F>


• Concluzionăm că logicile temporale pot fi „traduse” în automate, în sensul deja subliniat: mulŃimea structurilor care sunt model pentru o formulă coincide cu limbajul acceptat de un anumit automat, construit (sintactic, efectiv) din formula dată

• În acest mod, problema SAT pentru CTL (ca şi pentru LTL ) se reduce la o problemă privind apartenenŃa unui obiect la un limbaj dat

• „Dimensiunea” automatului ataşat pentru o formulă dată este exponenŃială în „dimensiunea” formulei (dacă ne referim la automatele nedeterministe ataşate unei formule LTL ) şi respectiv liniară în aceeaşi dimensiune (în ceea ce priveşte automatele alternate construite pentru formulele CTL)

• Amintim rezultatele principale privind SAT şi puterea (comparativă) de exprimare a logicilor implicate


• Teorem ă (decidabilitatea SAT pentru CTL). Problema satisfiabilităŃii (validităŃii, nesatisfiabilităŃii) pentru clasa CTL este decidabilă

• DemonstraŃia rezultatelor care urmează este simplă în cazul incluziunilor (ceea ce nu mai este cazul cu găsirea exemplelor/contraexemplelor adecvate)


• Teorem ă (putere de exprimare comparativ ă). Sunt adevărate afirmaŃiile:

(i) CTL ⊊ CTL*(ii) LTL ⊊ CTL*(iii) LTL ⊈ CTL(iv) CTL ⊈ LTL

(v) CTL ∩ LTL ≠ Ø

CURS 6

• Logica modală şi nu numai…(alternative la logicile anterioare; o variantă estereprezentată de TLA /TLA+ )

Logica modală 1• Deşi logicile temporale pot fi privite, a şa

dup ă cum am sugerat, drept cazuri particulare ale unor logici modale, ele au în acest moment o existen Ńă şi o evolu Ńie/aplicabilitate „în sine”

• Diverse logici modale (mai generale) au, de asemenea, o evolu Ńie individualizat ă în anumite ramuri ale informaticii legate în mod direct de concuren Ńă, cum ar fi cunoa şterea în sistemele multiagent

• Astfel, modalit ăŃile principale ale logicii modale de baz ă (clasice , standard ) nu sunt ○, U şi Ũ, ci □ (box) şi ◊ (diamond)

Logica modală 2• În func Ńie de diferitele „nuan Ńe” ( moduri ) de adev ăr

(în afar ă de adevărat în viitor din logica temporală studiat ă deja, mai putem avea şi adevărat în mod necesar , crezut a fi adev ărat , corespunde cuno ştin Ńelor agentului Q, etc.) ele nu se mai citesc întotdeauna_în_viitor/cândva_în_viitor ci necesar/posibil , crezut_de_to Ńi/crezut_de_cineva , agentul_Q_ ştie_sigur_c ă/din_ceea-_ce_ ştie-_agentul_Q, etc.

• Vom nota cu Ф mul Ńimea formulelor logicii modale de bază, definit ă constructiv peste alfabetul L = A U P U C1 U C2, unde A = {p1, p2, …} este mul Ńimea variabilelor propozi Ńionale (a literalilor pozitivi), P = {( , )} este mul Ńimea parantezelor, C1 = {, ∨∨∨∨, ∧∧∧∧, →→→→, ↔↔↔↔} este mul Ńimea conectorilor booleeni iar C 2 = {□, ◊} este mul Ńimea operatorilor modali

Logica modală 3

• Ā = {p1, p2, …} va denota mul Ńimea nega Ńiilor variabilelor propozi Ńionale (a literalilor negativi)

• Nu vom introduce explicit în L mul Ńimea{true, false} (posibil a fi nota Ńi în continuare şi prin ⊤, respectiv ⊥⊥⊥⊥). De asemenea, defini Ńiile structurale pot fi prezentate mai succint dac ă utiliz ăm nota Ńia Backus-Naur

Logica modală 4• Defini Ńie (sintaxa logicii modale de baz ă). Baza (formule atomice).

(i) true , false ∈ Ф(ii) Pentru fiecare p ∈ A, p ∈ Ф

Pas constructiv (formule noi din formule vechi).(a) Dacă F ∈ Ф, atunci (F) ∈ Ф(b) Dacă F1, F2 ∈ Ф, atunci (F1 ∧ F2),

(F1 ∨ F2), (F1 → F2), (F1 ↔ F2) ∈ Ф(c) Dacă F ∈ Ф, atunci (□F), (◊F) ∈ Ф(d) Dacă F ∈ Ф, atunci (F) ∈ Ф(e) Nimic altceva nu mai este în Ф

Logica modală 5• Conform celor deja amintite, am putea înlocui

definiŃia precedentă cu:Ф ::= ⊤ | ⊥ | (p) | ( Ф) | (Ф ∧ Ф) | (Ф ∨ Ф) | (Ф → Ф) | (Ф ↔ Ф) | (□ Ф) | (◊ Ф), unde p ∈ A

• Înainte de a furniza şi semantica, să precizăm că diferenŃele faŃă de logica temporală sunt minore la nivel sintactic, cea mai importantă fiind posibilitatea de a aplica negaŃia oricărei formule, încă de la început

• Însă nu ne vom ocupa de probleme de genul „care este numărul minim de conectori astfel încât nici unul să nu poată fi exprimat (semantic) cu ajutorul celorlalŃi” (echivalent, „care sunt bazele minimale pentru o logică”)

Logica modală 6• Defini Ńie (structuri Kripke modale). O structură

Kripke modală este un 5-uplu K = <A, W, R, Π>, unde:

-A este mulŃimea variabilelor propoziŃionale(nevidă, cel mult numărabilă)

-W este mulŃimea stărilor sau lumilor universului(nevidă)

-R ⊆ W × W este o relaŃie de trecere (sau, de accesibilitate)

-Π : W → 2A este o funcŃie care va ataşa fiecărei stări mulŃimea variabilelor propoziŃionale adevărate în acea stare

Logica modală 7• Defini Ńie (semantica Ф).

Fie K = <A, W, R, Π> o structură Kripke modală. Adevărul formulelor din Ф, în K, se obŃine în două faze:

(I) Adev ărul formulelor într-o lume oarecare .

Baza.(i) Pentru fiecare w ∈ W, w ⊨ true şi

w ⊭ false(ii) Pentru fiecare w ∈ W, w ⊨ p dacă şi numai dacă p ∈ Π(w), pentru fiecare p ∈ A

Logica modală 8Pas constructiv .(a) Pentru fiecare w ∈ W, w ⊨ ( F) dacă şi numai

dacă w ⊭ F, fiecare F ∈ Ф(b) Pentru fiecare w ∈ W, w ⊨ (F1 ∧ F2) dacă şi

numai dacă w ⊨ F1 şi w ⊨ F2, pentru fiecare F1, F2 ∈ Ф

(c) Pentru fiecare w ∈ W, w ⊨ (F1 ∨ F2) dacă şi numai dacă w ⊨ F1 sau w ⊨ F2, pentru fiecare F1, F2 ∈ Ф

(d) Pentru fiecare w ∈ W, w ⊨ (F1 → F2) dacă şi numai dacă, (dacă w ⊨ F1 atunci w ⊨F2), pentru fiecare F1, F2 ∈ Ф

Logica modală 9(e) Pentru fiecare w ∈ W, w ⊨ (F1 ↔ F2) dacă şi numai

dacă, (dacă w ⊨ F1 atunci w ⊨F2 şi reciproc), pentru fiecare F1, F2 ∈ Ф

(f) Pentru fiecare w ∈ W, w ⊨ (□F) dacă şi numai dacă avem (w’ ⊨ F pentru fiecare w’ ∈ W care satisface

<w, w’> ∈ R), pentru fiecare F ∈ Ф(g) Pentru fiecare w ∈ W, w ⊨ (◊F) dacă şi numai dacă

avem (există w’ ∈ W care satisface <w, w’> ∈ R astfel încât w’ ⊨ F), pentru fiecare F ∈ Ф

(II) Adev ărul formulelor în structura dat ă. O formulă F ∈ Ф este adevărată într-o structură Kripke, K, dacă şi numai dacă ea este adevărată în orice lume w ∈ W (adică avem K ⊨ F dacă şi numai dacă w ⊨ F, pentru fiecare w ∈ W)

Logica modală 10• Să notăm mai întâi că peste tot în cele de mai sus ar fi

trebuit să scriem w ⊨KF sau K, w ⊨F. Apoi, că şi în definiŃiile semantice modificările de suprafaŃă sunt minore. Aceste mici transformări (faŃă de logiciletemporale) pot avea însă nişte efecte profunde şi nebănuite asupra înŃelegerii corecte a noŃiunii de adevăr a unei formule

Observa Ńie. (1)RelaŃia R nu mai este presupusă a fi totală (din acest

motiv îşi pierde relevanŃa şi presupunerea „temporală” că există o stare iniŃială). Pot exista lumi w care nu mai au succesori. Pentru ele avem, de exemplu, w ⊭ (◊F), pentru fiecare F ∈ Ф (inclusiv pentru F = true ). Şi asta pentru că semantica impunea să existe măcar o lume „legată” de w (prin R), ceea ce nu se întâmplă aici. Dual, avem w ⊨ (□F), pentru fiecare F ∈ Ф (inclusiv pentru F = false ), deoarece afirmaŃia „avem (w’ ⊨ F pentru fiecare w’ ∈ W care satisface <w, w’> ∈ R)” este adevărată „prin lipsă”

Logica modală 11• (2) Expresia „lumea w’ este legată de lumea w” (în K,

prin R) trebuie desigur înŃeleasă prin aceea că <w, w’> ∈ R. Aceasta ne sugerează în primul rând faptul că logica modală de bază are o interpretare (ca mod de adevăr) pentru □/◊ de genul în_toate_lumile_legate /pentru_m ăcar_o_lume_legat ăceea ce face ca într-adevăr această logică să poată fi privită ca o generalizare a tuturor celor deja sugerate, inclusiv a logicilor temporale (totul depinzând de semnificaŃia atribuită cuvântului „legată”). În al doilea rând, ar părea natural ca în lipsa „totalităŃii” relaŃia R să fie măcar reflexivă şi tranzitivă

• Şi alte proprietăŃi pentru R pot fi luate în considerare, lucru care poate conduce la rezultate surprinzătoare faŃă de cele „standard”

• (3) Operatorii □ şi ◊ „seamănă” atât cu cuantificatorii din LP1 cât şi cu cuantificatorii de cale din CTL, dar este evident că diferenŃele determină o clară „separare” în ceea ce priveşte problemele de decizie legate de semantică din logicile respective

Logica modală 12• Exemplu. Fie structura Kripke K = <A, W, R, Π>

A = {p, q}; W = {w1, w2, w3, w4, w5, w6};

R = {<w1, w2>, <w1, w3>, <w2, w3>, <w2, w2>, <w3, w2>, <w4, w5>, <w5, w4>, <w5, w6>};

Π(w1) = {q}, Π(w2) = {p, q}, Π(w3) = {p}, Π(w4) = {q}, Π(w5) = Ø, Π(w6) = {p}), avem w1 ⊨ q, w1 ⊨ (◊q), w1 ⊭ (□q), w5 ⊭ (□p), w5 ⊭ (□q), w5 ⊭ (□p ∨ □q), w5 ⊨ □(p ∨ q).

Lumile care satisfac formula F = (□p → p) sunt exact w2, w3, w4, w5, w6

Logica modală 13• Deşi definiŃiile privind satisfiabilitatea sunt cunoscute din

cazul clasic (sau se pot uşor generaliza), există anumite probleme legate de definirea constructivă „în trepte”. Pentru că nu am insistat în cazul logicilor temporale, considerăm util să facem nişte precizări în acest cadru mai general

• Defini Ńie (consecin Ńă semantic ă şi echivalen Ńe în logica modal ă de bază). Fie F ⊆ Ф, G ∈ Ф şi K = <A, W, R, Π> o structură Kripke. Spunem că G este consecinŃă semantică din F în K (pe scurt, F ⊨K G) dacă şi numai dacă din w ⊨K F (pentru fiecare F ∈ F) avem w ⊨K G şi aceasta pentru fiecare w ∈ W. Două formule F şi G din Ф sunt tare echivalente în K (F ≡K G) dacă şi numai dacă {F} ⊨K G şi {G} ⊨K F

Logica modală 14• FaŃă de echivalenŃele cunoscute deja din logica

propoziŃională, putem observa că ele se păstrează pentru Ф, deoarece putem substitui orice formulă modală într-o schemă de echivalenŃă din LP fără a o „distruge”

• Gândindu-ne la interpretarea lui □ şi ◊ drept cuantificatori „pe lumi”, nici relaŃiile care urmează nu sunt surprinzătoare

• Teorem ă (echivalen Ńe în Ф). Fie K = <A, W, R, Π> ostructură Kripke şi F, G ∈ Ф. Atunci:

• (i) □F ≡K ◊ F şi ◊F ≡K □ F• (ii) □(F ∧ G) ≡K □F ∧ □G şi ◊(F ∨ G) ≡K ◊F ∨ ◊G• (iii) Nu avem □(F ∨ G) ≡K □F ∨ □G şi nici

◊(F ∧ G) ≡K ◊F ∧ ◊G• (iv) □⊤ ≡K ⊤ dar nu şi ◊⊤ ≡K ⊤

• (v) ◊⊥ ≡K ⊥ dar nu şi □⊥ ≡K ⊥• (vi) ◊⊤ ≡K □F → ◊F

Logica modală 15• Defini Ńie (formule valide în logica modal ă de bază).

Fie K = <A, W, R, Π> o structură Kripke şi F ∈ Ф. F este validă în K dacă avem w ⊨K F pentru fiecare w ∈ W. F se va numi validă (⊨F) dacă este validă în fiecare structurăKripke

• Desigur că putem găsi imediat câteva formule valide pornind de la echivalenŃele de mai sus (de exemplu, □F ↔ ◊ F este o formulă validă)

• O altă formulă validă (schemă de axiome care poate fi folosită pentru construcŃia unui sistem deductiv) este □(F → G) → (□F → □G) (numită şi K, după S. Kripke)

• Încep însă să apară probleme dacă ne gândim că pentru o anumită modalitate de adevăr adoptată ar trebui ca anumite formule care în logica modală de bază sunt doar satisfiabile (şi pot fi privite ca „ipoteze suplimentare”) să fie chiar valide. Sau, anumite scheme nu ar trebui să fie valide pentru toate formulele

Logica modală 16• De exemplu schema □F → F ar trebui să fie validă

pentru fiecare F în cazul în care □ este interpretat drept necesar , dar nu şi dacă □ este interpretat drept crezut_de_to Ńi. Putem vorbi astfel de ceva ce s-ar putea chema o „inginerie a logicilor ” şi unde „se poate umbla”, ca şi în situaŃia logicilor clasice, este la noŃiunea de structură (Kripke, în acest context)

• Mai exact, ideea este de a impune satisfacerea anumitor propriet ăŃi de c ătre rela Ńia R (reflexivitate, tranzitivitate, simetrie, antisimetrie, totalitate, etc.). Astfel, în cazul necesar faptul că <w, w’> ∈ R ar însemna că „w’ poate fi accesată/posibilă datorită informaŃiei prezente în w” iar în cazul crezut_de_to Ńi faptul că <w, w’> ∈ R înseamnă că „w’ poate fi privită drept acceptabilă/de_crezut datorită informaŃiei furnizate de w”(de unde se va putea deduce ce proprietate este de dorit pentru R)

Logica modală 17• Lucrurile se complică şi mai mult dacă ne

propunem să tratăm logici „mixte” (în ceea ce priveşte modalitatea de adevăr adoptată pentru anumite scheme)

• Toate aceste complicaŃii se reflectă până la urmă în „uşurinŃa” de a testa satisfiabilitatea formulelor

• În bibliografia sugerată sunt furnizate exemple practice, concrete, pentru diverse astfel de tipuri de logici, inclusiv sisteme deductive corecte şi complete

CURS 7• Descrierea mai în detaliu a claselor principale de

algoritmi de verificare (conform slide-urilor 25-27)

• În funcŃie de timp vom prezenta şi câŃivaalgoritmi particulari

• Este vorba desigur de algoritmi PRACTICI de bază în model cheching - MC (desigur, bazaŃi pelogică)

• Teoria sperăm că este deja clară (ceea ce am făcut se numeşte “automata theoretical approach” – conform metodei (VERIF))

MC pentru LTL 1

• Este o metodă de tip „explorarea spaŃiuluistărilor”, urmând în general linia indicatăde Metoda (VERIF) (slide 25)

• Partea centrală a procesului de verificareeste de a obŃine sistemul tranziŃionalataşat sistemului concurent formal care trebuie analizat

• Avem practic nevoie doar să găsim stărileaccesibile ale acestui sistem

MC pentru LTL 2• ProprietăŃile generale cerute pot fi apoi

verificate prin examinarea sistemului, maiexact prin examinarea mulŃimii stăriloraccesibile (este o anumită stare accesibilă?, există blocaj?, etc.)

• Problema cea mai importantă este aceeacă sistemul tranziŃional este de obicei de o dimensiune foarte mare

• Este nevoie de tehnici speciale de optimizare pentru a obŃine toate stărileaccesibile, chiar dacă nu simultan

MC pentru LTL 3• Fie F = <P, M, T> un sistem concurent formal şi

TSF = <ΣΣΣΣ, S, s0, T> sistemul tranziŃional ataşat luiF. Algoritmul următor, care, având ca intrare Ffurnizează (ceea ce interesează din) TSF la ieşire, foloseşte o stivă (Stack) şi o tabelă hash(H) pentru a memora mulŃimea curentă a stărilor vizitate (accesibile din starea iniŃială)

• FuncŃia enabled(s) va returna tranziŃiile din Tcare sunt permise în starea s ∈ S

• Pentru fiecare s ∈ S şi t ∈ T, funcŃia succ(s, t) va returna starea s’ ∈ S astfel încât <s, n(t), s’> ∈ T

MC pentru LTL 4

• łinând cont că sistemele tranziŃionale pot fi privite şi ca grafuri, procedura următoare este de tip căutare în adâncime (DFS)

• Folosirea stivei (prin „istoricul” pe care-l reŃine) este foarte utilă pentru a înŃelege de ce o stare eronată/neconvenabilă este accesibilă (ideal ar fi ca asemenea stări care fac ca o anumită proprietate să nu fie satisfăcută, nici să nu poată fi atinse)

• Desigur că prin adăugarea de procese observator pot fi verificate simultan mai multe proprietăŃi exprimate prin formule de logică temporală

• Se observă că T nu este memorată (returnată) înansamblul său, astfel încât putem spune că verificarea folosind acest algoritm se face on-the-fly

MC pentru LTL 5• Algoritm DFS• procedure DFS ()• begin• s := top (Stack)• Tr := enabled(s)• for all t ∈ Tr• begin• s’ := succ(s, t)• if s’ ∉ H then• begin• insert s’ in H;• push s’ onto Stack;• DFS()• end• end• pop (Stack);• end• Stack := <s0>; H := {s0};• DFS();

MC pentru LTL 6• Pentru a verifica dacă un sistem tranziŃional (de

tip TSF , adică obŃinut dintr-un sistem concurent formal) satisface o formulă G ∈ LTL , avem de fapt de verificat că toate comportările sale (infinite) satisfac (sunt modele pentru; sunt admisibile pentru) G

• Reformulând (VERIF) şi construind automatul care generează toate modelele lui G (ceea ce ar putea eventual reduce numărul de comportări), putem spune că ideea principal ă este de a utiliza automatul ca observator pentru sistem

MC pentru LTL 7

• Totuşi, în acest mod (Ńinând cont şi de faptul că automatul este nedeterminist şi că acceptă „la modul existenŃial”) ajungem la necesitatea de a stabili că pentru toate comportările sistemului tranziŃional există măcar un calcul de acceptare pentru observator , ceea ce este destul de problematic

• Trucul este de a nega G. Mai exact, pentru a dispune de un algoritm de tip model checking pentru (testarea propriet ăŃilor sistemelor reprezentate ca FCS-uri şi exprimate în) LTL, trebuie urma Ńi urm ătorii paşi, în ipoteza că dispunem de F = <P, M, T>, un sistem concurent formal (ca reprezentare a unui sistem real) şi formula G ∈ LTL (ca reprezentare a unei proprietăŃi de verificat a sistemului real):

MC pentru LTL 8Metoda (VERIF-LTL)

• Construim un automat pe cuvinte infinite, notat AG care acceptă exact toate secvenŃele infinite care nu satisfac G

• AG este adăugat ca un observator la F. Dacă este necesar, se pot adăuga şi alŃi observatori (de exemplu, cei legaŃi de condiŃiile de echitate)

• Se generează sistemul tranziŃional ataşat, TSF = <ΣΣΣΣ, S, s0, T>, conform DFS (condiŃia de acceptare este de tip Büchi generalizată)

• Se verifică dacă limbajul acceptat de TSF este sau nu vid (orice cuvânt infinit acceptat de TSF reprezintă o comportare a sistemului iniŃial care nu este model pentru G)

MC pentru LTL 9• Problema legată de algoritmul de mai sus este

legată în principal de eficienŃă/complexitate: cum verificăm dacă TSF acceptă un limbaj (ne)vid prin DFS, fără a apela la algoritmii complicaŃi cunoscuŃi (de exemplu cei legaŃi de găsirea componentelor tare conexe ale unui graf)

• Dimensiunea unei reprezentări (sistem tranziŃional, sistem concurent formal, formulă LTL ) poate fi gândită în sensul dimensiunii unui graf (număr de noduri plus, eventual, număr de arce; sau număr de nivele în cazul unui arbore sau a unui graf orientat ordonat)

MC pentru LTL 10• Teorem ă (complexitatea unui LTL model

checker). Fie sistemul concurent formal F = <P, M, T>, sistemul tranziŃional ataşat TSF = <ΣΣΣΣ, S, s0, T>, şi formula G ∈ LTL . Complexitatea unui model checker construit după Metoda (VERIF-LTL) , în ipoteza unor implementări corespunzătoare, este:

-Liniară în dimensiunea sistemului tranziŃional (NLOGSPACE )

-ExponenŃială în dimensiunea sistemului concurent formal (PSPACE)

-ExponenŃială în dimensiunea formulei G (PSPACE)

MC pentru LTL 11• Exemplu (propriet ăŃi de siguran Ńă). Să ne imaginăm o

proprietate G ∈ LTL pentru care automatul ataşat ar avea o condiŃie de acceptare vidă. Atunci AG va accepta practic orice, singura posibilitate de neacceptare fiind ajungerea într-o situaŃie în care nu mai este posibilă nici o tranziŃie. Mai exact, AG va avea o singură stare de acceptare, începând cu care (odată ce ea este „atinsă”) toate cuvintele infinite vor fi acceptate, indiferent ce se petrece ulterior. În acest mod, AG este practic un automat pe cuvinte finite. Mai mult, anumite condiŃii de echitate devin nenecesare iar testul de viditate pentru limbajul acceptat de TSF devine banal (revine la un test de accesibilitate)

• Am putea chiar trage concluzia că un automat fără nici o condiŃie de acceptare defineşte o proprietate de siguranŃă

MC pentru LTL 12

• SiguranŃă/safety: „tot ceea ce se petrece în sistem se desfăşoară conform unui plan prestabilit”

• PermanenŃă/liveness: „sistemul are un scop spre care tinde şi acest scop va fi cu siguranŃă atins”

• Anumite formule generale din logica temporală (de exemplu □(F → ○(G)), care este o aşa-numită formulă de tranziŃie) pot exprima clase întregi de proprietăŃi

• Pentru a intra în alte amănunte este nevoie de cunoştinŃe suplimentare de statistică, topologie şicomplexitate, aşa că…

• De exemplu, se poate arăta (într-un cadru adecvat, bazat pe noŃiunea de topologie) că orice proprietate „naturală” a sistemelor reale poate fi reprezentată ca fiind intersec Ńia dintre o proprietate de siguran Ńă şi una de permanen Ńă

MC pentru CTL 1• Reamintim că CTL ⊊ CTL* şi poate fi definită direct prin:

Formule de stare (CTLS)Baza (formule atomice de stare)(i) true , false ∈ CTLS

(ii) Pentru fiecare p ∈A, fie p, fie p (exclusiv ) ∈ CTLS(vom scrie p sau p)

Pas constructiv (formule de stare noi din formule vechi)(a) Dacă F1, F2 ∈ CTLS, atunci (F1 ∧ F2) sau

(F1 ∨ F2) ∈ CTLS sunt formule de stare(b) Dacă F ∈ CTLC, atunci A(F) sau E(F) ∈ CTLC sunt

formule de stare(c) Dacă F ∈ CTLS, atunci (F) ∈ CTLS

(d) Nimic altceva nu mai este formulă de stare

MC pentru CTL 2Formule de cale (CTLC) Pe scurt, (○F) şi (F1 U F2) sau (F1 Ũ F2) ∈ CTLC,

unde F1, F2 ∈ CTLS. De asemenea, Dacă F ∈ CTLC, atunci (F) ∈ CTLC şi nimic altceva nu mai este formulă de cale

• Reamintim şi că atunci când vorbim de CTLvorbim de fapt de CTLS

• Folosirea lui sau (exclusiv) în cele de mai sus se explică prin folosirea lui „iniŃială” în (ii), lucru la rândul lui necesar datorită modalităŃii de a construi semantica

MC pentru CTL 3• Este tot o metodă de tip „explorarea spaŃiului

stărilor” (altă „concretizare” (VERIF))• Se dau din nou F = <P, M, T>, un sistem

concurent formal, şi TSF = <ΣΣΣΣ, S, s0, T> sistemul tranziŃional ataşat lui F, adică o mulŃime de comportări care constituie limbajul acceptat

• Obs. : Această mulŃime de comportări este înacest caz o structură KripkeK = <A, W, R, w0, Π>

• Se mai dă şi o formulă F ∈ CTL, prin care se exprimă proprietatea dorită a sistemului (real, iniŃial, formalizat prin …)

MC pentru CTL 4• Sarcina unei metode MC este de verifica dacă K

satisface (este model pentru) F

• Obs. : deoarece mulŃimea de comportări esteprivită ca o structură Kripke (drumurile π sunt„strânse” într-o asemenea structură), nu maieste nevoie să spunem (ca la LTL ) că „toatecomportările trebuie să satisfacă formula”

• Această sarcină poate rezolvată (după cum ştim), folosind o metodă de etichetare

• Mai exact, trebuie să verificăm dacă stareainiŃială w0 poate fi etichetată cu F, respectândsemantica CTL

MC pentru CTL 5• După cum ştim, aceasta înseamnă să găsim o

etichetare τ : W → 2cl(F) care să satisfacă un număr de 10 condiŃii (la care se adaugă faptulcă toate elementele din cl(F) care sunteventualităŃi trebuie să fie adevărate în K)

• Cum construcŃia lui τ este standard, pentru a transforma verificarea faptului că toate condiŃiilesunt adevărate într-un algoritm, vom începe prina eticheta pe W cu elemente din cl(F) într-oordine compatibilă o ordine „standard” pesubformule (adică începând cu subformulele„cele mai din interior”, adică de tip p/ p)

MC pentru CTL 6

• Structura generală a algoritmului va fi:

(1)Alege o formulă G ∈ cl(F) ale cărei (toate) subformule au fost deja procesate (etichetate); iniŃial, nimic nu este procesat şi un asemenea G nu poate fi decât de tipul p/ p

(2)Se consideră fiecare w ∈ W. Aceasta se vaeticheta cu G dacă şi numai dacă acest lucrueste permis de către regulile de etichetare

(3)Paşii anteriori se reiau până când G = F

• Pasul (1) devine determinist dacă stabilimefectiv o ordine „standard” strictă pe cl(F)

MC pentru CTL 7• Să detaliem Pasul (2):

-Pentru formulele G de forma (G1 ∧ G2),(G1 ∨ G2), A(○H), E(○H) este evident că trebuiesă ne uităm doar la etichetarea curentă (dacăsatisface condiŃiile)

-Pentru restul formulelor G (adică de forma A(G1 U G2), A(G1 Ũ G2), E(G1 U G2), E(G1 Ũ G2) trebuie făcut mai mult deoarecepentru U şi Ũ etichetarea este recursivă; în plus, în cazul U trebuie să avem garantat faptul că G2va fi şi ea satisfăcută de K

MC pentru CTL 8

-Pentru G = A(G1 U G2) vom folosi următoareleobservaŃii

(i)O stare w ∈ W (nod în graful care reprezintă K) care este deja etichetată cu G2, poate finecondiŃionat etichetată şi cu G

(ii)Dacă pentru toate stările w’ cu <w, w’> ∈ R, w’este necondiŃionat etichetată cu G iar w este(deja) etichetată cu G1, atunci (şi) w poate fietichetată necondiŃionat şi cu G

-ObservaŃiile precedente conduc la următorulsubalgoritm al Pasului (2):

MC pentru CTL 9(2.1)EtichetaŃi toate nodurile deja etichetate cu G2,

şi cu A(G1 U G2)(2.2)Se consideră fiecare w ∈ W. Dacă pentru

fiecare w’ cu <w, w’> ∈ R, w’ este dejaetichetată cu A(G1 U G2) şi w este dejaetichetată cu G1, atunci w se etichetează şi cu A(G1 U G2)

(2.3)Pasul (2.2) se repetă până când nici un nod nu mai poate fi etichetat

-Pentru formulele G de tipul A(G1 Ũ G2) situaŃiaeste cumva duală, adică se porneşte cu o etichetare „optimistă maximal” şi apoi se înlăturădin mulŃimea de etichete cele incorecte

MC pentru CTL 10-ObservaŃii:(i)Un nod w deja etichetat cu G2, se va

eticheta provizoriu şi cu A(G1 Ũ G2)(ii) Se consideră fiecare w ∈ W. Dacă w nu

este etichetat cu G1 şi există un nod w’ cu <w, w’> ∈ R care nu este etichetatprovizoriu cu A(G1 Ũ G2), atunci se înlătură A(G1 Ũ G2) din mulŃimea de etichete ale lui w

-ObservaŃiile se „traduc” în subalgoritmul:

MC pentru CTL 11(2.1’)Se etichetează nodurile deja etichetate cu

G2, şi cu A(G1 Ũ G2)(2.2’)Pentru fiecare nod w ∈ W, dacă w nu este

etichetat cu G1 şi există w’ astfel încât

<w, w’> ∈ R şi w’ nu este etichetat cu A(G1 Ũ G2), atunci se înlătură A(G1 Ũ G2) din mulŃimea de etichete ale lui w

(2.3’)Se repetă pasul anterior până când nu maitrebuie înlăturată nici o etichetă

-Subproceduri similare se deduc pentru formulelede tipul E(G1 U G2), E(G1 Ũ G2) (puteŃi voi?)

MC pentru CTL 12• Din aceleaşi motive (lipsă de timp; cunoştinŃe

suplimentare, etc.), nu mai insistăm; totuşi:• Teorem ă.-Algoritmul de etichetare are complexitateaOOOO(card(W)2) (aceasta se poate reduce chiar la OOOO(card(W)) dacă se evită „munca duplicat”); pentru a avea această complexitate, trebuie să„marcăm” toate nodurile în care formula F esteadevărată printr-o singură parcurgere a grafuluipentru K

-Complexitatea MC pentru CTL esteOOOO(card(W) × lung(F))

Ordini parŃiale 1• Să punctăm câteva dintre ideile principale care

stau la baza creării unor algoritmi de verificarebazaŃi pe ordini parŃiale

(1)Semantica „de intercalare” (interleaving) folosităde noi pentru a descrie execuŃia concurentă a unor procese secvenŃiale, reprezintă o mulŃimede comportări (tot ce se poate obŃine prinintercalarea comportărilor individuale)

(2)Comportările din această mulŃime sunt „legate”astfel încât pentru a verifica o anumităproprietate, de obicei, nu sunt toate necesare

Ordini parŃiale 2(3)Ar trebui astfel să se poată verifica anumite

proprietăŃi ale unor sisteme folosind doar unelecomportări din fiecare execuŃie concurentă

(4)Comportările esenŃiale alese s-ar putea sădepindă de proprietatea de verificat

• Se porneşte cu un sistem (program) P reprezentat ca un sistem concurent formal F P = <P, M, T>

• Ca şi până acum, scopul este de a exploraspaŃiul de stări al sistemului tranziŃional asociatlui P (acesta se va numi sistemul tranziŃionalglobal, STG, stările sale numindu-se stăriglobale)

Ordini parŃiale 3• Ideea este de a explora doar o parte

„mică” a (mulŃimii stărilor) lui STG pentru a răspunde întrebărilor legate de comportamentul lui P

• NotaŃia s →t s’ va indica faptul că <s, t, s’> este în mulŃimea T a tranziŃiilor lui STG

• NotaŃia s ⇒t1…tks’ va indica faptul putem„ajunge” de la starea s la starea s’ în STGprin aplicarea succesivă a tranziŃiilort1, t2, …,tk

Ordini parŃiale 4• Defini Ńie. Două tranziŃii t1 şi t2 se numesc

independente dacă sunt satisfăcute următoareledouă condiŃii pentru fiecare stare s:

(1)Dacă t1 (t2) este permisă în s şi s →t1 s’(s →t2 s’), atunci t2 (t1) este permisă în s dacă şinumai dacă t2 (t1) este permisă în s’ (tranziŃiileindependente nu se pot „interzice” una pe alta)

(2)Dacă t1 şi t2 sunt permise în s, atunci există o unică stare s’ astfel încât avem atât s ⇒t1t2 s’ câtşi s ⇒t2t1 s’ (comutativitatea tranziŃiilorindependente)

• În caz contrar, tranziŃiile se numesc dependente

Ordini parŃiale 5• Nu este practic ca aceste proprietăŃi să se

verifice pentru toate perechile de tranziŃii şiîn toate stările

• Există însă condiŃii suficiente (de naturăsintactică) pentru testa dacă două tranziŃiit1 şi t2 sunt independente (uşor de verificat), de exemplu:

-MulŃimea de procese care „participă” în t1 este disjunctă de cea care „participă” în t2

-MulŃimile de variabile folosite în t1 şi t2 suntdisjuncte

Ordini parŃiale 6• Defini Ńie. Două secvenŃe de tranziŃii sunt

echivalente ddacă ele pot fi obŃinute una din altaprin permutări de tranziŃii independente alăturate

• Pornind astfel cu o relaŃie de independenŃă, relaŃia anterioară pe mulŃimea secvenŃelor de tranziŃii este o relaŃie de echivalenŃă (în sensalgebric) şi atunci aceste secvenŃe pot fi grupateîn clase de echivalenŃă

• O asemenea clasă se va numi urmă (trace); o clasă cu reprezentantul w = t1t2…tk se va nota [w]

Ordini parŃiale 7• Este evident că dacă s ⇒w1 s1,

s ⇒w2 s2 şi [w1] = [w2] rezultă s1 = s2, adică „două secvenŃe de tranziŃii care pornesc din aceeaşi stare şi aparŃinaceleiaşi urme conduc la aceeaşi stare”

• Astfel, pentru a determina dacă o stare este accesibilă printr-o mulŃime de secvenŃe făcând parte din aceeaşi urmă, este suficient să luăm în considerare doaro secvenŃă din acea acea urmă

Ordini parŃiale 8• Pentru un algoritm de „căutare selectivă”, ideea

de bază este de a face o căutare clasică; însă, în loc de a executa în mod sistematic toatetranziŃiile permise în fiecare stare găsită întimpul căutării, se vor executa doar unele dintreele (nu-I mai dăm forma generală; o găsiŃi înWolper, p.191)

• Prin urmare, se explorează doar un subgraf al grafului stărilor globale

• Există mai multe tipuri de mulŃimi de tranziŃiicare ar trebui selectate; dintre ele amintimmulŃimile persistente/rezistente (persistent) şicele sleep (inactive, amorŃite)

Ordini parŃiale 9• Defini Ńie. O mulŃime de tranziŃii T, permise

în starea s, se numeşte persistentă în s ddacă pentru fiecare t ∉ T pentru care există o secvenŃă în STG, s=s0→t0 s1→t1 s2…→tn-1 sn→tn=tsn+1, care include doar tranziŃii ti neincluse în T, iar teste independentă în raport cu fiecaretranziŃie din T („orice s-ar face pornind cu s dar rămânând înafara lui T, aceasta nu interacŃionează şi nici nu afectează T”)

• Obs. : MulŃimile persistente evită blocajul

Ordini parŃiale 10• Există mai multe strategii de a folosi mulŃimile

persistente în algoritmii de căutare selectivă (nu intrăm în amănunte)

• Nici una dintre ele nu elimină posibilitatea a selecta simultan mai multe tranziŃii independente

• Pentru a atinge acest scop (evitarea explorării, nenecesare, a unor posibile alăturări prinintercalare a unor tranziŃii independente) s-au introdus mulŃimile inactive

• O mulŃime inactivă este ataşată fiec ărei stări s în care ajunge căutarea

Ordini parŃiale 11• MulŃimea inactivă asociată cu starea iniŃială este

mulŃimea vidă• MulŃimea asociată cu s este o mulŃime de

tranziŃii (cea mai mare, de obicei) care suntpermise în s dar niciodat ă executate

• Cu ajutorul mulŃimilor inactive se pot înlăturadoar tranziŃii (arce), nu şi stări (noduri); bine şiaşa…

• „Combinând” mulŃimile inactive cu celepersistente putem înlătura şi stări şi putempreveni ajungerea în stări care să generezeblocaj

Ordini parŃiale 12

• Există generalizări pentru a testa într-un mod similar şi alte proprietăŃi generale ale sistemelor

• Din păcate analiza complexităŃii în modul clasic(„worst case”) nu ne ajută prea mult în aceastăsituaŃie şi nici informaŃiile obŃinute din studiereaexemplelor „academice” (gen „cina filozofilor”)

• Pentru a fi evaluate, metodele de tip „ordiniparŃiale” trebuie să fie implementate şi testate „lagreu” pe exemple reale, complexe (industriale)

Verificare simbolică 1• Recapitulând (din nou) şi reformulând:

-scopul este de a verifica faptul că un sistemreactiv satisface anumite proprietăŃi generale, exprimate printr-o formulă F (să pp. că F ∈ CTL, pt. că este mai natural)

-sistemul reactiv este formalizat în final printr-un sistem tranziŃional TS (care este un cazparticular de automat), de fapt prin mulŃimeacomportărilor acestuia (limbajul acceptatconform anumitor condiŃii)

-grupând comportările, această mulŃime poate fiprivită ca o structură Kripke K=<A, W, R, w0, Π>

Verificare simbolică 2-în loc de a verifica prin metode deja

cunoscute că K este model pentru F, esterezonabil să presupunem că am puteadeduce acest lucru studiind(meta)proprietăŃile generale ale lui K

-am putea astfel şti, de exemplu, „cam care”ar fi formulele care au şanse să fie satisfăcute de K (poate F este printre ele)

• Ideea este de a reprezenta K simbolic, prin (meta)formule şi de a cerceta aceste(meta)formule pentru a deduce (meta)proprietăŃile lui K

Verificare simbolică 3• Să presupunem că lucrăm doar cu structuri

Kripke având un număr finit de stări (A estemulŃimea variabilelor propoziŃionale, W este mulŃimea stărilor, R ⊆ W × W este totală, w0 ∈ W, iar Π : W → 2A); să pp. căcard(W) = m < 2n (n fiind cel mai mic nr. cu această proprietate)

• Fiecare stare w ∈W va putea fi astfel codificatăprintr-un cuvânt (vector) de lungime n, w = b1b2…bn, bi ∈ B (este desigur vorba de ordonarea lui W şi de reprezentarea binară peexact n poziŃii a numerelor 1, 2, … ,m)

Verificare simbolică 4

• Fiecare W’ ⊆W va putea fi reprezentată astfelprin funcŃia sa caracteristică cW’ : W → B, cW’(w) = 1 ddacă w ∈W’; mai mult, dacă

w = b1b2…bn, atunci cW’ poate fi considerată ca o funcŃie din FB(n) (b1b2…bn este identificat cu lista <b1, b2, … ,bn>)

• Ca exemplu, printr-o asemenea funcŃiebooleană se poate reprezenta, pentru fiecarep ∈ A, mulŃimea stărilor w astfel încât p ∈ Π(w) (adică cele în care variabila propoziŃională p este considerată a fi adevărată)

Verificare simbolică 5• Similar, şi relaŃia R se poate reprezenta

printr-o funcŃie cR din FB(2n), (2n)cR(w, w’) = 1 ddacă <w, w’>∈ R

• ProprietăŃile lui K vor fi studiate lucrând cu aceste funcŃii din FB

• Mai direct, Ńinând cont de cele spuse, ne putem pune următoarele întrebări:

(1)Cum se pot verifica (meta)proprietăŃileunei structuri Kripke, date printr-o mulŃimede funcŃii booleene, şi ce algoritmi suntnecesari?

Verificare simbolică 6(2)Cum se reflectă aceşti algoritmi prin

operaŃii asupra funcŃiilor booleene?(3)Care este cea mai bună reprezentare a

funcŃiilor booleene care să permită o implementare simplă a operaŃiilor găsiteanterior?

• Obs. : La punctul (3) am răspuns deja: este vorba despre OBDD-uri

• Pentru a răspunde la punctul (1) , se introduce mai întâi un (meta)limbaj logic pentru „reprezentarea” structurilor Kripke;

Verificare simbolică 7• Mai exact, o formulă F în acest limbaj (ceva

destul de complicat ca aspect, între LP1= şi LP2, dar decidabil) va avea ca semantică o structurăKripke K (formula fiind în acelaşi timp o reprezentare simbolică a structurii) împreun ă cu o interpretare similară cu cea pentru LP1

• Limbajul permite exprimarea prin astfel de formule a majorităŃii lucrurilor importante care ne interesează în legătură cu structurile, cum ar fimulŃimea stărilor accesibile din starea iniŃială(ceea ce, după cum am văzut, este „nucleul”testării unor proprietăŃi generale cum ar fi celede siguranŃă)

Verificare simbolică 8• Verificarea efectivă a validităŃii proprietăŃilor

implică operaŃii logice cu asemenea formule şiimplicit operaŃii cu funcŃiile booleene care reprezintă structura Kripke („imagine” a sistemului real)

• Putem astfel reveni la punctul (2) de maiînainte, punctând faptul că avem nevoie de implementări simple pentru urmatoarele operaŃiicu funcŃii booleene: +, ¯, i, →, etc.

• Acestea există în cazul OBDD-urilor• Să facem şi observaŃia că MC simbolic, bazat pe

OBDD-uri, este aplicat cu succes pentruverificarea circuitelor hard; în cazul aplicaŃiilorsoft ajungem rapid la un nr.incontrolabil de mare de stări

Verificare compoziŃională 1• Toate metodele de verificare descrise până

acum operează pe descrierea completă a unuisistem, care este de cele mai multe ori de dimensiune foarte mare

• Scopul verific ării compozi Ńionale este de a considera pe rând fiecare proces în parte

• Ne-am putea gândi că procedeul ar fi următorul: pentru a verifica dacă P1║P2 satisfaceproprietatea (formula) F, trebuie găsite F1, F2astfel încât P1 satisface F1, P2 satisface F2 şiF1∧ F2 → F

• De fapt, acesta nu „merge” sub această formădin mai multe motive:

Verificare compoziŃională 2-Procesul P1 ar putea satisface F1 dacă s-ar

executa singur, dar nu şi în prezenŃa lui P2; de fapt, am verifica faptul că P1 satisface F1, indiferent de ceea ce face P2, ceea ce este o cu totul altă problemă de verificare decât ceatratată până în prezent (ce se întâmplă dacă P1foloseşte o variabilă care poate fi modificată de către P2?)

-Limbajul în care se exprimă formulele poate să nu aibă o putere de exprimare suficientă pentru ca verificarea compoziŃională să fie posibilă (nicilogicile temporale propoziŃionale, fie LTL , fie CTL, nu pot exprima satisfăcător toateproprietăŃile sistemelor cu un nr. finit de stări; nici TLA…)

Verificare compoziŃională 3-ConjuncŃia poate să nu fie cel mai potrivit

corespondent semantic al concurenŃei (săne gândim la echitate)

• Pentru a elimina problemele de mai sus, ar trebui să ne fixăm un obiectiv mai puŃinambiŃios

• Pt. a verifica dacă P1║P2 satisface F, procedăm astfel:

-Se înlocuieşte P1 cu un proces „echivalent”mai „simplu” P1’

Verificare compoziŃională 4-Se înlocuieşte P2 cu un proces „echivalent” mai

„simplu” P2’

-Se verifică dacă P1’║P2’ satisface F• Aici cuvântul „echivalent” trebuie înŃeles ca

„echivalent în contextul oricărui alt proces”• Nu intrăm în prea multe amănunte; să precizăm

totuşi că mai întâi se restricŃionează clasa de procese secvenŃiale, la procese care nu folosescvariabile (ele fiind de fapt sisteme tranziŃionalecu tranziŃii etichetate) şi interacŃionând doar printranziŃii partajate (shared) adică prinrendez-vous

Verificare compoziŃională 5• Se defineşte compunerea de procese

concurente, apoi echivalenŃa lor (ideea este ca două procese echivalente să aibă aceeaşicomportare, indiferent de context, adicăindiferent de procesele cu care mai suntcombinate), noŃiunea de bisimulare (este o echivalenŃă tare cu câteva proprietăŃisuplimentare) precum şi cea de echivalenŃăobservaŃională (este o bisimulare mai slabă)

• Cu o alegere atentă a structurilor de date folosite, algoritmul de testare a bisimulării poatefi implementat în timp OOOO(card(P1) x card(P2)), sau chiarOOOO((card(P1) + card(P2))log(card(P1) +card(P2)))

Verificare compoziŃională 6• Faptul că P1’ este mai „simplu” decât P1

trebuie înŃeles în sensul că P1’ este o abstractizare a lui P1 (sau, o specificare), P1 fiind o implementare (mai concretă) a lui P1’ (sau, o instanŃă)

• P1 este astfel „permis” de P1’, nu totdeauna şi reciproc

• RelaŃiile de bisimulare şi echivalenŃăobservaŃională nu sunt în acest sens preacorecte; se introduc astfel versiunile lorasimetrice: simulare şi simulareobservaŃională

Verificare compoziŃională 7

• O problemă tipică la care se poate aplica cu succes tehnica de faŃă este de a verifica un sistem în care un acelaşi proces poate apare de oricâte ori (de exemplu, un protocol în care numărul de participanŃi nu este fixat aprioric)

• Obs. : Metoda verifică o familie de sisteme, fiecare din ele fiind de tip finite-state, dar nu esteimpusă nici o margine superioară globală asupranumărului de stări

• Aceasta conduce la următoarea (şi ultima) metodă (n-am tratat însă nici o metod ăsintactic ă de verificare, bazată pe sistemedeductive …)

Număr infinit de stări 1

• Chiar de la început se putea observa că dacă un sistem concurent formal are variabile al cărordomeniu nu este finit, nu există nici o garanŃie căspaŃiul stărilor va fi finit

• Atunci când spaŃiul stărilor este cu adevăratinfinit, el nu poate fi controlat prin tipul de căutare enumerativă folosit până în prezent

• ExcepŃia ar putea-o constitui verificareasimbolică, în care spaŃiul stărilor ar putea fidescris finitar (printr-o formulă) chiar dacă esteinfinit


• Din păcate, chiar dacă limbajul în care sunt exprimate formulele este decidabil(problema SAT este decidabilă), lucru de altfel absolut necesar, s-ar putea ca spaŃiul stărilor tot să nu poată fi controlat(„calculat”), deoarece proprietăŃilenebanale ale acestuia sunt în general nedecidabile

• Există două strategii importante pentru a trata rezonabil situaŃia expusă:


(1)Se consideră (identifică) doar acele subclase de sisteme cu un spaŃiu infinit al stărilor pentru care acesta poate fi controlat (mulŃimea stărilor esterecursivă) – sisteme „decidabile”

(2)Se consideră şi clase „nedecidabile” (mulŃimeastărilor este recursiv enumerabilă), dar atuncirenunŃăm la ideea de a avea la dispoziŃie numaialgoritmi pentru „tratamentul” lor, ci şisemialgoritmi

• Nu mai insistăm, din motivele deja cunoscute…

CURS 8 – reamintiri…• Ce este de învăŃat…• Mai sunt greşeli…• Cele 90 puncte la „proiecte” – cf. celor stabilite cu mine

şi cu V. Alaiba• Cele 30 puncte de la examen sunt împărŃite câte 5 pe

cele 3 subiecte, pe fiecare lucrare (fiecare de câte 15 puncte)

• Nu se promoveaz ă fără măcar 40 puncte• Aceste slide-uri cuprind tot ceea ce am făcut şi ceea ce

vă cer; nu uitaŃi că aveŃi acces şi la articolul lui L. Lamport (The Temporal Logic of Actions – măcar primele 17 pagini), precum şi la cartea lui M. Huth şi M. Ryan (Logic in Computer Science – măcar paginile legate de logica modală şi sistemele multiagent)

Logica temporală a acŃiunilor 1• „Mergem” pe ideea că orice sistem real poate fi

gândit până la urmă ca un algoritm concurent (program concurent, process format din programe secvenŃiale)

• Demonstrarea corectitudinii procesului via o proprietate dorită este esenŃială

• Abordarea noastră se bazează pe faptul că atât algoritmul cât şi proprietatea pot fi specificate într-o unică logică

• Corectitudinea algoritmului va însemna că formula prin care se prezintă specificaŃiilealgoritmului implic ă formula care descrie proprietatea (e vorba de implicaŃia logică obişnuită)

Logica temporală a acŃiunilor 2

• TLA (Temporal Logic of Actions) reprezintă astfel o metodă pentru a descrie şi a raŃiona despre procese

• Pentru a vedea „cum lucrează” TLA cu algoritmi reali, avem nevoie de TLA+/TLC (laborator…)

• TLA combină de fapt două logici: o logicăa acŃiunilor (Lamport) şi o logică temporală (liniară) standard

Logica temporală a acŃiunilor 3

• Răspunsul la întrebarea „De ce să înlocuim un limbaj de programare obişnuit cu logica ?” am dat-o în altă parte a cursului ( a se consulta şi bibliografia, atent …)

• Pentru a avea o alternativă practică a limbajelor de programare „obişnuite”, o logică trebuie să fie simpl ă şi expresiv ă

• Toate formulele TLA pot fi exprimate în termenii unor operatori temporali de viitor cunoscuŃi (cum ar fi ∧; desigur, şi cei din logica propoziŃională clasică; plus ∃∃∃∃), precum şi simbolul nou ´(prim )

TLA - Variabile, valori şi stări 1

Sisteme multiagent 1• Postulate fundamentale (nu are rost să încercăm să le

demonstrăm formal; J. Gall):-ORICE ESTE UN SISTEM-ORICE SISTEM ESTE PARTE A UNUI SISTEM MAI VAST-UNIVERSUL POATE FI ÎMPĂRłIT ÎN (SUB)SISTEME ÎNTR-O INFINITATE DE MODURI, ATÂT „DE JOS ÎN SUS”(SISTEME „MAI MARI”), CÂT ŞI DE SUS ÎN JOS (SISTEME „MAI MICI”)-TOATE SISTEMELE SUNT INFINIT DE COMPLEXE; ILUZIA SIMPLITĂłII PROVINE DIN FAPTUL CĂ ATENłIA A FOST FOCALIZATĂ ASUPRA UNOR COMPONENTE

Sisteme multiagent 2• Sistem multiagent : o mulŃime de agen Ńi care

interacŃionează• Agent : entitate într-un sistem multiagent

• Exemple :-Un joc de poker poate fi modelat ca un sistem multiagent; un agent aici poate fi

numit şi jucător-Un sistem concurent (distribuit) constând

din procese/site-uri (alt agent!) şi dezvoltat într-o reŃea care utilizează un anumit protocol

Sisteme multiagent 3• Trebuie să acceptăm că sistemele care ne interesează

sunt deosebit de complexe• Este f. greu să raŃionăm despre un singur agent în parte,

d-apoi despre o multitudine de agenŃi care interacŃionează

• Am putea urma următorii paşi (pentru a stăpâni complexitatea):

(1)Ne îndreptăm atenŃia doar asupra a câtorva detalii, sperând că acestea vor acoperi tot ceea ce este relevant pentru ceea ce ne interesează(2)Trebuie depistate situaŃiile care generează o complexitate mare şi trebuie găsite modalităŃi de abordare eficiente pentru a le micşora complexitatea

Sisteme multiagent 4• Normal, pentru o tratare generală şi

precisă a acestor chestiuni, avem nevoie de un model formal pentru noŃiunea de sistem multiagent

• Un asemenea cadru trebuie desigur să fie suficient de general pentru exprimarea tuturor trăsăturilor importante ale sistemelor multiagent, dar fără a intra în amănunte plictisitoare şi greu de manipulat

Sisteme multiagent 5• O decizie cheie va fi aceea că dacă privim un

sistem ca fiind urmărit de noi, la momente (discrete, de timp), fiecare agent se va afla într-o anumită stare (locală)

• Va exista, evident, şi o stare globală pentru un asemenea sistem

• Dar, dacă starea locală va încapsula întreagainformaŃie la care un agent are acces, nu vom face (în modelul general) nici o precizare suplimentară asupra stării globale

Sisteme multiagent 6• De exemplu, dacă modelăm un joc de poker,

starea pentru un jucător poate fi constituită din cărŃile pe care le deŃine la momentul respectiv, „pariurile” făcute de către ceilalŃi jucători, cărŃile deja văzute (şi alte informaŃii de natură personala, cum ar fi „ştiu că Andrei trişează”

• După cum se observă, deja este o chestie netrivială „CE punem” într-o stare

• Odată ce am decis ce punem într-o stare, trebuie să decidem CUM REPREZENTǍM ceea ce am introdus

Sisteme multiagent 7• Odată ce ne-am decis că, la fiecare moment

(discret) de timp pe care îl urmărim, fiecare agent este într-o anumită stare (locală), este uşor de imaginat că întregul sistem se va afla la momentul respectiv într-o anumită stare (globală)

• Ideea iniŃială ar fi ca starea globală să fie de forma <s1, s2, … , sn>, unde si este starea în care se află agentul i

• Din păcate, pentru a analiza „corect” comportarea unui sistem, este de multe ori insuficient să facem apel doar la starea agenŃilor

Sisteme multiagent 8• De exemplu, dacă studiem un sistem concurent

bazat pe „message-passing” (în care procesele au memorie locală şi comunică doar prin mesaje, prin anumite canale), am putea dori să cunoaştem mesajele aflate în tranzit la momentul respectiv, sau dacă un anumit canal este disponibil „în sus sau în jos”

• Astfel, din punct de vedere conceptual, un sistem va fi împărŃit de la început în două componente: agenŃii şi mediul (=orice altceva care este relevant)

Sisteme multiagent 9• Deşi este clar că mediul joacă un rol diferit faŃă

de un agent „obişnuit”, acesta poate fi privit totuşi ca un agent suplimentar

• Astfel, vom defini starea globală a unui sistem cu n agenŃi ca fiind un (n + 1)–tuplu, de forma <se, s1, s2, … ,sn>, unde si este starea în care se află agentul i, iar se este starea mediului

• Pentru a trece la restul amănuntelor de modelare, trebuie să remarcăm că avem multe alternative

Titlu CURS: SPECIFICAREA ŞI VERIFICAREA SISTEMELOR …masalagiu/pub/CAP_SPEC_LOG_2010.pdfE. W....

Documents

Transcript of Titlu CURS: SPECIFICAREA ŞI VERIFICAREA SISTEMELOR …masalagiu/pub/CAP_SPEC_LOG_2010.pdfE. W....