Post on 30-Oct-2019
SISTEMUL DE AXIOME ȘI REGULI DE INFERENȚĂ PENTRU
LOGICA BAN; EXEMPLE (NSS) ȘI (WMF)
PROTOCOL (ABSTRACT) DE SECURITATE
Este o secvență (finită) de mesaje text (tranzacții; șabloane de comunicare), reprezentând
comunicarea între două entități (privită ca o sesiune de comunicare distinctă de altele,
posibile), în mediu internautic, având trimițătorul (U) și receptorul (V) precizați în mod
explicit:
U V: text (U îi transmite lui V informația/datele precizate în text)
Porțiunile distincte de text sunt separate prin virgulă, iar aceste porțiuni individualizate pot
reprezenta texte reale (sau chiar obiecte mai complexe), dar și diverse prescurtări, extensii,
mnemonice, codificări, criptări, etc. ale acelor texte reale.
Ca (sub)porțiuni de text, putem identifica:
-(grupuri de) agenți (participanți la comunicare; mai sunt numiți și principali, servere (în care
orice participant se poate încrede), mașini, dispozitive)
-chei de criptare/decriptare (simetrice, în general); divizate/împărțite, publice, secrete
(corespunzătoare celor publice) și folosite pentru algoritmii (cifruri, criptosisteme) de
criptare/decriptare a textului sursă într-un text cifrat; se încearcă astfel împiedicarea finalizării
uor atacuri (în special al celor prin revenire, care folosesc informațiile vehiculate într-o sesiune
de comunicare anterioară) ale unor intruși/atacatori/adversari/persoane rău
intenționate/corupte; de obicei, textele cifrate apar delimitate de acolade (indicându-se și cheia
folosită)
-mesageri/co-fondatori/nonces, care sunt numere (pseudo)aleatoare, prin care se identifică
sesiunea curentă a unei comunicări (prospețimea informației)
-timpul curent de transmitere a text-ului, pentru transmițător
-o marcă (suplimentară) de timp, folosită de participanții la comunicare pentru idenficarea mai
sigură a sesiunii de proveniență (curentă sau nu) a (părții de) text în care apare
-formule (BAN), care, practic, adnotează anumite (sub)porțiuni de text
OPERATORI (BINARI, apoi UNARI) CARE POT APARE ÎN
FORMULELE BAN
Apărând în formulele BAN, operatorii vor apare și în textele din cadrul tranzacțiilor unei sesiuni
de comunicare printr-un anumit protocol. Iată lista lor (sperăm ca ea să fie exhaustivă pentru
înțelegerea acestei logici; a se vedea și sintaxa formală, din Curs/slide-uri):
⫢: believes/crede
| : has jurisdiction over/are control, jurisdicție, autoritate asupra lui
|~ : said/spune, trimite, a spus cândva, a trimis cândva
: sees/vede
↔K : communicate/comunică (printr-o cheie K; sau, o cheie publică +K, sau o
cheie secretă matching/corespunzătoare cheii publice +K, adică -K)
key/cheie(K, • ↔ •), notație alternativă pentru ↔K (sau +K/-K); o vom folosi des
K : from/de la (luând în considerare cheia K; sau +K/-K)
<•,•> : (con)catenation/concatenare (alăturare textuală de mesaje)
{•}K : encryption/criptare (cu cheia K, +K, -K)
#(•) : fresh/proaspăt, nou, recent, actual
K(•) : has, posesses/are, deține cheia K (+K, -K)→׀
Observație. Simbolurile care sunt indici inferiori (dreapta) pentru operatori, pot apare și/sau
deasupra operatorului respectiv.
AXIOMELE (FORMULELE ELEMENTARE ALE) LOGICII BAN
(desigur că ele sunt scheme de axiome)
1A. P crede X (P ⫢ X)
2A. P are control asupra lui X (P | X)
3A. P spune/trimite X (P |~ X)
4A. P vede X (P X)
5A. {X}K (putem avea desigur și ceva de genul {Kpq}Kqs , sau {P ↔K Q}Kqs): mesajul X este
criptat cu cheia K
6A. nou(X) (#(X)): aceasta este, uneori, o alternativă pentru P spune X
7A. cheie(K, P ↔ Q) (sau P ↔K Q, sau...): se aplică de obicei presupunerea că secretele sunt
protejate în mod implicit în modelul Dolev-Yao, deci nu vom folosi ipoteze suplimentare pentru
acest lucru în demonstrații; de asemenea implicit, presupunem că operatorul este comutativ, în
sensul că dacă P ↔ Q atunci vom avea și Q ↔ P, şi reciproc; această formulă poate fi un mesaj
8A. P deține cheia K (׀→K(P)): se presupune implicit că cheia K nu va putea niciodată fi
descoperită de către niciun alt agent; cu excepţia desigur a lui P, sau a altuia în care P are
încredere (exprimată explicit)
Observație.
(i)În general: P este agent, S este server, X este mesaj, K este cheie, etc. (ceea ce înseamnă că
schemele sunt valabile „pentru fiecare...”). Dar pot fi și excepții, sau cazuri particulare, după cum
deja am amintit mai sus.
(ii)Axiomele BAN sunt în realitate formulele elementare, atomice. Sistemul în sine (să-l numim
SD-BAN) este, până la urmă, un sistem de tip deducție naturală în calculul cu secvențe. Ceea
ce se adaugă pentru a începe o demonstrație sunt de fapt ipotezele suplimentare, care transcriu
un anumit protocol (ca secvență de tranzacții) ca formule BAN, inclusiv anumite presupuneri
implicite care se explicitează (rezultând SD-BAN+) și care, în cazul clasic, se elimină pe
parcurs.
REGULILE DE INFERENȚĂ ALE LOGICII BAN
(desigur că și acestea sunt de fapt scheme de reguli)
Regulile vor fi redactate sub forma:
Dacă premize atunci concluzii (premizele/concluziile vor fi separate prin și).
Vă revine sarcina de a le rescrie sub formă arborescentă și folosind exprimarea simbolică.
1I. (MM1) Dacă (P crede (cheie(K, P ↔ Q))) şi (P vede {X}K), atunci (P crede (Q spune X))
Reamintim că în general, regulile de tip Message Meaning privesc interpretarea mesajelor
autentificate printr-o criptare care utilizează chei private sau divizate. Astfel, regula poate fi
redată prin:
1I’. Dacă (P crede (cheie(K, P ↔ Q))) şi (P vede {X}K, dar provenienţa nu este de la P),
atunci (P crede (Q spune X))
Anticipând, în logica GNY se va introduce simbolul (operatorul unar) „” pentru a se specifica
faptul că o (sub)componentă „nu își are originea în acel loc”, ceea ce ar face ca presupunerea
anterioară să devină internă logicii şi regula să arate sub forma:
1I’’. (MM2) Dacă (P crede (׀→K (Q))) şi (P vede {X}-K), atunci (P crede (Q spune X))
2I. (NV) Dacă (P crede (Q spune X)) şi (P crede (nou(X))), atunci (P crede (Q crede X))
Această regulă, Nonce Verification, mai are variante numite mai jos (FR) (de la Freshness
Rule).
În plus, pentru aceste prime reguli de inferenţă, să reamintim că, condiţia de aplicabilitate
exprimată prin formula (c1): P crede (nou(X)) este câteodată admisă ca fiind valabilă implicit.
În asemenea situații, sunt însă posibile atacuri prin reluare.
3I. (J) Dacă (P crede (Q are control asupra lui X)) şi (P crede (Q crede X)),
atunci (P crede X)
4I. (SG) Dacă (P crede (Q spune <X, Y>)) atunci
((P crede (Q spune X)) şi (P crede (Q spune Y)))
Numele anterior provine de la Sees Group. Continuăm cu:
5I. Se poate și „invers”, adică vom admite de fapt corectitudinea schemelor (mnemonicul
provine de la BElief) :
5Ia. (BE1) Dacă ((P crede X) şi (P crede Y)) atunci (P crede <X, Y>)
5Ib. (BE2) Dacă (P crede <X, Y>) atunci ((P crede X) şi (P crede Y))
5Ic. (BE3) Dacă (P crede (Q crede <X, Y>))
atunci ((P crede (Q crede X)) şi (P crede (Q crede Y)))
5Id. (BE4) Dacă (P crede (Q crede X)) şi
(P crede (Q crede Y)) atunci (P crede (Q crede <X, Y>))
6I. Reamintim că, mai jos, presupunem implicit că agentul P cunoaşte cheile necesare
(mnemonicul provine de la Sees Part):
6Ia. (SP1) Dacă (P vede <X, Y>) atunci ((P vede X) şi (P vede Y))
6Ib. (SP2) Dacă (P vede {X}K ) şi (P crede (cheie(K, P ↔ Q))) atunci (P vede X)
Reamintim și că regula imediat anterioară ar putea fi, câteodată, înlocuită de:
6Ib’. (SP2’) Dacă ((P vede {X}K ) şi (P vede K)) atunci (P vede X)
6Ib’’. (SP2’’) Dacă P crede (cheie(K, P ↔ Q)) atunci (P vede K)
7I. Revenind la prospețime, vom introduce:
7Ia. (FR1) Dacă (P crede (#(X))) atunci (P crede (#(<X, Y>))), pentru fiecare Y
7Ib. (FR2) Dacă (P crede (#(X))) atunci (P crede (#({X}K)))
Următoarea regulă este uneori acceptată implicit (mesajele criptate cu ajutorul cheilor publice,
K/+K, pot fi decriptate doar folosind cheile private, -K):
8I. (SP3) Dacă ((P vede {X}+K) şi (P crede ׀→+K(P)) atunci (P vede X)
Penultima schemă este opţională în BAN (dar, câteodată este bine ca cineva care deţine o
anumită cheie publică, să poată descifra orice mesaj criptat cu o cheie privată):
9I. (SP4) Dacă ((P vede {X}-K) şi (P crede (׀→+K(Q)) atunci (P vede X)
Regula (SG), (dată la 4I.), poate fi, în acest moment, reformulată prin:
10I. (SG) Dacă (P crede (Q spune <X, Y>)) atunci (P crede (Q spune X))
Observație recapitulativă.
(i)Ca și în cazul axiomelor, în general, P, Q sunt agenți (S este server...), X, Y sunt mesaje,
K/+K/-K/Kxy sunt chei, etc. (ceea ce înseamnă, din nou, că schemele sunt valabile „pentru
fiecare...”), dar pot fi și excepții/particularizări
(ii)Într-o deducție SD-BAN (sau SD-BAN+) privind activitatea protocoalelor concrete, mai pot
fi uneori utilizate, ca ipoteze/axiome suplimentare, și alte formule. Acestea fie că adnotează în
mod implicit tranzacțiile protocolului respectiv (și câteodată sunt aduse, pentru siguranță,
explicit „în scenă”), fie că „traduc direct în logică” anumite tranzacții (ne)introduse inițial în
protocol, fie sunt presupuneri „venite” din (meta)modelul Dolev-Yao (în mod uzual, acceptate ca
fiind „adevărate” în mod implicit).
(iii)Concluziile trase asupra corectitudinii funcționării unui protocol (via specificații, deși date și
ele, cam mereu, într-un mod ambiguu, adică în limbaj natural) sunt reflectate ca teoreme în
sistemul deductiv (SD-BAN, poate și BAN/SD în slide-uri) sugerat mai sus. Aceste teoreme sunt
astfel presupuse ca fiind afirmații adevărate privind protocolul în cauză (a se vedea „lipsa
semanticii formale”, distanța eventual „probabilistă”, K - B, etc.). Urmăriți cu atenție exemplele.
PROTOCOLUL NEEDHAM-SHRöDER, CU CHEI DIVIZATE
(NSS)
În comunicare sunt implicate trei entități: principalii (agenții) P (Alice) și Q (Bob), precum și
serverul de încredere S. P este cel care inițiază comunicarea. Admitem că P este competent
(cunoscând, de exemplu, întrega problematică privind criptosistemele) și că are încredere nu doar
în S, dar și în Q. De asemenea, se admite că cei trei sunt disponibili și doritori de a comunica (cel
puțin într-o primă fază). Cheia Kas este simetrică, generată înainte de P (sau de către S), împărțită
între P și S și cunoscută (cumva) doar de aceștia. Similar, pentru Kqs (deși se acceptă, uzual,
faptul că cheia este generată de S și făcută cumva cunoscută lui Q). Transmiterea lor adresanților
se face astfel prin alte mijloace de comunicare. Și Kpq este o cheie simetrică, divizată, generată
de către S. Ea este cheia sesiunii curente de comunicare dintre P și Q, fiind cunoscută doar de S,
P, Q (presupunere, belief...). Np și Nq sunt nonces, adică mesagerii de identificare generați pentru
sesiunea curentă de P, respectiv Q.
Inițierea unei sesiuni de comunicare între P și Q folosind (NSS) înseamnă, pentru început,
trimiterea unui set de mesaje standard între entități urmând succesiv șabloanele O1. – O5.:
P îi trimite un prim mesaj lui S, prin care se identifică (cumva) pe sine, ca emițător și pe Q,
ca receptor. Simultan, P generează și trimite Np:
O1. P → S: P, Q, Np
Serverul S îi răspunde lui P, efectuând de fapt, în prealabil, următoarele acțiuni: generează
Kpq (eventual, tot acum, și cheia Kqs, pe care i-o comunică lui Q prin alte metode), precum
și o copie a ei pentru P, criptată cu Kqs, deja cunoscută (această copie va fi trimisă, imediat,
prin O3., de P lui Q; copia va include desigur și numele lui P). Mesajul O2. va conține, de
asemenea, pe Np, deoarece s-ar putea ca, în decursul sesiunii, P să mai solicite chei și pentru
a comunica cu alți indivizi; prezența lui Np îl asigură pe P că mesajul primit de la S este
proaspăt, S răspunzând astfel chiar la O1. și nu la vreun mesaj având altă origine sau care
este un duplicat. Se va include în acest răspuns și numele lui Q, pentru ca P să știe sigur că
persoana cu care va împărți cheia Kpq este cea dorită. Prin urmare, S va trimite lui P toate
aceste informații, adică Np, Q, Kpq, {Kpq, P}Kqs, criptate însă, pentru siguranță, cu cheia Kps:
O2. S → P: {Np, Q, Kpq, {Kpq, P}Kqs}Kps
După cum am precizat deja, după ce primește O2. de la S, P îi va trimite lui Q cheia de
sesiune, divizată între ei, Kpq, de-abia primită de la S, împreună cu numele său (pentru
siguranță), totul criptat cu Kqs (al cărei corespondent va putea fi folosit pentru decriptare
de către Q):
O3. P → Q: {Kpq, P}Kqs
Normal, Q îi va răspunde imediat lui P, confirmându-și identitatea atât prin trimiterea lui
Nq, cât și prin criptarea acestuia cu Kpq, de-abia primită de la P:
O4. Q → P: {Nq}Kpq
Ultimul mesaj, de la P la Q, este necesar pentru o ultimă confirmare a faptului că P deține
cu adevărat cheia comună Kpq de comunicare, pentru sesiunea curentă, și că este „în viață”
(adică încă își dorește continuarea comunicării cu Q). Înainte de a trimite mesajul, P
efectuază o operație simplă asupra lui Nq (cunoscută cumva, aprioric, și de Q; de fapt, se
cunoaște aprioric toată secvența de tranzacții O1. – O5., la nivel de șablon, de către toate
părțile implicate), rezultatul expediind-ul criptat cu Kpq:
O5. P → Q: {Nq - 1}Kpq
Evident, sesiunea va/poate continua cu secvența de comunicare efectivă.
În Curs se demonstrează, utilizând SD-BAN, anumite afirmații privind utilizarea și
funcționarea acestui protocol.
Ca un corolar, să amintim că una dintre problemele majore legate de acest protocol este că e
vulnerabil la un atac prin replicare (sugerat de Denning și Sacco). Pe scurt, dacă un atacator
folosește o valoare mai veche pentru Kpq (creată într-o sesiune anterioară de comunicare între P
și Q), el poate înlocui practic O3. cu ceva deja compromis. Q îl va accepta, deoarece nu va ști că
cheia Kpq nu este proaspătă. Există suficiente variante pentru „repararea” acestei situații
neplăcute (sesizată accidental, în mod informal; același lucru se întâmplă frecvent și cu alte
vulnerabilități), printre care utilizarea protocolului Kerberos ((NSS) modificat; nu insistăm).
Situații similare se întâlnesc și în legătură cu protocolul Needham-Schröder cu chei publice,
„reparat” prin Needham-Schröder-Löwe, etc.
Ceea ce trebuie însă să reținem, este că trebuie să dispunem de metode formale de a depista
vulnerabilitățile protocoalelor, înainte de a le „pune în funcțiune”. Aici intervin logicile de
încredere (BAN, pentru început), în cadrul cărora putem discuta despre analiza unui protocol,
despre corectitudinea în ceea ce privește funcționarea lor conform specificațiilor sau (in)existența
vulnerabilităților.
Exemplele de demonstrații din Curs sunt, sperăm, edificatoare și comentate suficient acolo.
Pentru uniformitate, vom prezenta în continuare și protocolul wide-mouth-frog, în același mod
ca pe (NSS), deși ceea ce există deja în slide-uri este perfect suficient.
PROTOCOLUL (DIDACTIC) WIDE-MOUTH(ED)-FROG (WMF)
Protocolul a fost propus în 1990 de către Burrows, Abadi, Needham ca exemplu pentru
necesitatea introducerii BAN.
Este un protocol de autentificare în rețele, creat cu scop didactic și permițând entităților implicate
în comunicare (A, B, S) să-și dovedească (una alteia și pe ansamblu) propria identitate, evitând,
în același timp (pe cât posibil), interceptarea mesajelor și atacurile prin replicare. Ca și până
acum, cei doi agenţi/principali (A și B) doresc să comunice via un server sigur S. Față de
protocolul menționat anterior, nonces nu sunt implicate, dar se vor folosi explicit mărcile de timp
TA și TS, numere înregistrate la momentul primei emiteri a mesajului în care apar. Se presupune
în plus că ceasurile (t) ale participanților sunt mereu sincronizate. Aceasta în primul rând datorită
faptului că A nu știe cu siguranță că B chiar există, sau dacă acesta este mereu disponibil.
Comunicarea ar putea fi deci oprită (periodic, în timp) și S trebuie să se „descurce” în aceste
cazuri. Mai presupunem implicit (ca mai înainte) că se folosește și o anumită formă de
criptare/autentificare prealabilă a mesajelor. Tot ca la protocolul anterior, cheile folosite sunt
chei simetrice (partajate), Kas fiind cunoscută doar de A și S (similar pentru Kbs). Cheia Kab
(cheia de sesiune), este generată și complet determinată de „competentul” A, care poate chiar
relua mesaje (folosind această cheie), în perioada pentru care nu se schimbă mărcile de timp.
Această descriere poate fi considerată ca fiind specificarea informală (în limbaj natural) a
(funcționării) protocolului.
Folosind notaţia standard, protocolul poate fi prezentat prin patru tranzacții (în Curs, doar
primele două sunt introduse de la început; următoarele sunt cumva „deduse” odată cu
dezvoltarea demonstrației afirmației (*) enunțate aici la finalul demersului).
Mai întâi, A îi transmite lui S un mesaj prin care: se identifică pe sine (într-un mod deja
stabilit), apoi îi comunică lui S marca sa de timp (aceasta se poate și autogenera, în
momentul emisiei), cheia (împărțită) de sesiune Kab, pe care a creat-o și o va folosi în
comunicarea cu B, precum și identitatea lui B (aceste ultime trei informații, criptate cu
cheia cunoscută, Kas):
1Ex1. A → S: A, {TA, Kab, B}Kas
În continuare, S va comunica cu B prin trimiterea: mărcii sale, a cheii de sesiune primite de
la A, precum și identitatea lui A (totul criptat cu cheia stabilită Kbs):
2Ex1. S → B: {TS, Kab, A}Kbs
Necesitatea continuării protocolului prin mesajul (următor) trimis de A lui S, devine
imperativă în urma considerentelor privind reușita demonstrării (în Curs) a lui (*). Astfel,
A (își) citeşte ceasul obţinând timpul curent t, şi apoi trimite (lui S) mesajul format din t și
cheia (sigură) de sesiune, Kab, totul criptat din nou cu cheia sa privată de autentificare
pentru server, Kas:
3Ex1. A → S: {t, cheie(Kab, A ↔ B)}Kas
Se poate demonstra chiar, în particular (SD-BAN, vezi slide-urile din Curs), că S crede și el că
mesajul anterior nu a fost preluat/citit de către vreun atacator care l-ar fi putut captura (cândva în
trecut), deoarece A crede așa ceva.
Ca urmare, bazându-se pe această certitudine (A crede (cheie(Kab, A ↔ B))), S va putea
(re)trimite cheia de comunicare Kab către B, de data aceasta cheia fiind cu adevărat sigură;
mesajul corespunzător va mai conține timpul sincronizat t, precum și identitatea lui A,
totul criptat cu Kbs, adică putem introduce în protocol:
4Ex1. S→B: {t, A, A crede (cheie(Kab, A ↔ B))}Kbs
Sesiunea curentă va/poate continua cu secvența de comunicare efectivă dintre A și B, chiar
eliminând din protocol primele două mesaje, acestea putând fi practic înlocuite de următoarele
două, fără ca acest lucru să împieteze asupra lui (*).
(*) Ceea ce demonstrăm (detaliat, în Curs, în SD-BAN la care se adaugă niște ipoteze
suplimentare) este, într-un final, afirmația că, folosind protocolul descris prin 1Ex1. – 4Ex1.
(mai exact, doar prin 3Ex1. și 4Ex1.), B va putea contacta (oricând) pe A în mod direct și în
siguranță, cu ajutorul cheii Kab, care este sigură și proaspătă.
Putem analiza și ce s-ar întâmpla dacă am renunţa la ipoteza ceasurilor sincronizate. Acest lucru
îl facem tot în slide-urile de Curs, concluzia fiind că ipoteza ceasurilor sincronizate este esențială
pentru corectitudinea protocolului (funcționarea acestuia conform specificației inițiale).
Am încheiat astfel parțial demonstrația formală a corectitudinii specificării, precum și
analiza (și a) protocolului (WMF).
Arbori versus text (de pus în continuare, aici sau separat, „pozele” respective).
Urmează aici și descrierea protocolului Needham-Schröder(-Löwe) cu chei publice,
folosit în explicarea legăturii logici de încredere – Isabelle (vezi slide-urile finale din Curs).
LOGICI MODALE ȘI TEMPORALE
(selecție din materie)
Sintaxa logicii modale de bază (MD).
Baza (formule atomice).
(i) true, false Ф.
(ii) Pentru fiecare p A, avem 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 Ф.
______________________________________________________________________________
Structură Kripke modală. O structură Kripke modală este un 4-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ă, cel mult numărabilă)
-R W W este o relaţie de trecere (sau, de accesibilitate/legătură între lumi)
-Π : W 2A este o funcţie care va ataşa fiecărei stări mulţimea variabilelor propoziţionale
adevărate în acea stare
-Se mai poate adăuga o mulțime de stări inițiale, W0 W (și atunci K devine un 5-uplu); în
acest caz, de obicei, card(W0) = 1.
______________________________________________________________________________
Semantica MD. 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 modale într-o lume/stare oarecare.
Baza.
(i) Pentru fiecare w W, w true şi w false.
(ii) Pentru fiecare w W, w p ddacă p Π(w), pentru fiecare p A.
Pas constructiv.
(a) Pentru fiecare w W, w ( F) ddacă w F (pentru fiecare F Ф).
(b) Pentru fiecare w W, w (F1 F2) ddacă w F1 şi w F2 (pentru fiecare F1, F2 Ф).
(c) Pentru fiecare w W, w (F1 F2) ddacă w F1 sau w F2 (pentru fiecare F1, F2 Ф).
(d) Pentru fiecare w W, w (F1 F2) ddacă: dacă w F1 atunci w F2 (pentru fiecare F1,
F2 Ф).
(e) Pentru fiecare wW, w (F1 F2) ddacă: dacă w F1 atunci w F2 şi reciproc (pentru
fiecare F1, F2 Ф).
(f) Pentru fiecare w W, w (□F) ddacă avem:
w’ F pentru fiecare w’ W care satisface <w, w’> R (pentru fiecare F Ф).
(g) Pentru fiecare wW, w (◊F) ddacă avem: există w’W care satisface <w, w’> R astfel
încât w’ F (pentru fiecare F Ф).
(II) Adevărul formulelor modale într-o structură dată. O formulă F Ф este adevărată într-o
structură Kripke, K, ddacă ea este adevărată în orice lume w W (adică avem K F ddacă
w F, pentru fiecare w W).
Putem scrie și (convențional) K(F) = 1 (sau chiar w(F) = 1, sau S(F) = 1, ...)
Putem pune, în situațiile care o cer, K F ddacă w F, pentru fiecare w W0.
Să notăm că, în cele de mai sus, era mai corect de scris w K F sau <K, w> F.
Observaţie. Relaţia R nu este presupusă a fi totală. Pot astfel exista lumi w care nu mai au
succesori și pentru care avem, de exemplu, w (◊F), pentru fiecare F Ф (inclusiv pentru
F = true); 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ă.
În continuare se presupune că R este reflexivă și tranzitivă (exceptând exemplele concrete), dar
nu este (neapărat) totală.
______________________________________________________________________________
Sintaxa logicii temporale (propoziționale) cu timp liniar (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 ( Ā) sunt 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.
Drum. Se numeşte drum (cale, urmă, rută, traseu, structură, secvență, cuvânt) pentru o
logică LTL (peste A) orice funcţie π : N 2A.
Pentru un drum π vom nota cu πi sufixul său obţinut prin înlăturarea primelor i elemente, adică
funcţia πi : N 2
A dată prin π
i(j) = π(i+j), pentru fiecare j N, i N*. Orice valoare π(i) (de
fapt, orice submulțime w a lui A), se numește stare. π(0) va fi starea inițială a căii π. Vom spune,
în definiția semanticii (urmează), ce înseamnă că o formulă F este adevărată într-o cale π, dar
admitem de pe acum că F este adevărată în π (π F) ddacă ea este adevărată în starea iniţială a
căii respective (adică în π(0) A). Prin convenție, admitem mai sus și cazul i = 0, adică π0, care
va denota pe π.
Putem adăuga în sintaxă definițiile explicite pentru box și diamond, dar putem pune și direct,
semantic, π (◊F) π (true U F) şi respectiv π (□F) π (false Ũ F). A se vedea și
echivențele (tari) din final (inclusiv descrierile intuitive).
„Trăgând cu ochiul” la logica modală (la semantica operatorilor de mai sus), și stabilind, prin
convenție, că orice stare w este și succesorul său „implicit” (nu imediat!) putem spune că:
π (□F) ddacă π(0) (□F), adică ddacă πi F (pentru fiecare i 0); similar pentru (◊F)
(înlocuind „pentru fiecare i”, cu „există măcar un i”).
______________________________________________________________________________
Semantica LTL. Valoarea de adevăr pentru formulele LTL, într-o cale π, se obţine structural
astfel:
Baza.
(i) π true şi π false, pentru fiecare π.
(ii) π p ddacă p π(0), şi π p ddacă p π(0) (pentru fiecare p A) (pentru fiecare π).
Pas constructiv.
(a) π (F1 F2) ddacă π F1 şi π F2, iar π (F1 F2) ddacă π F1 sau π F2 (pentru
fiecare π).
(b) π (F) ddacă π1 F (pentru fiecare π).
(c) π (F1 U F2) ddacă există i 0 astfel încât πi F2 şi pentru fiecare 0 j < i avem π
j F1,
iar π (F1 Ũ F2) ddacă pentru fiecare i 0 cu πi F2, există 0 j < i astfel încât π
j F1 (pentru
fiecare π).
(d) π (F) dacă şi numai dacă π F (pentru fiecare π).
Observație. Intuitiv, pentru a obține semantica unei formule LTL, se procedează succesiv, după
cum urmează:
-Se porneşte, ca în metodologia generală, cu o structură (asignare, interpretare...) simplă, prin
care se atribuie valori de adevăr variabilelor propoziţionale. În cazul nostru, începem cu o
mulţime numărabilă (de fapt, cuvânt infinit) de stări, fiecare stare fiind element al lui 2A. Dacă
w 2A şi p w, atunci p este adevărată în w. Dacă p w, atunci negaţia sa este adevărată în w,
p w, adică p este falsă în w (dacă p w, nu vom pune însă p w).
-Se extinde apoi structura anterioară la formule. Adică, ne va interesa 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, adică la (ne)apartenența lor la starea corespunzătoare.
După cum am mai remarcat, o cale π poate fi privită ea însăși ca o structură Kripke modală
(acum, temporală), dacă se face cu o mai mare exactitate paralela cu relația R și funcția Π,
pornind de la mulțimea stărilor, W). Ideea ar fi ca, mai jos, să avem și Kπ F în caz că π F.
Mai precis, dată orice cale π : N 2A , și notăm π w0w1... (unde wi A și π(i) = wi)),
componentele rămase a fi precizate ale structurii Kripke (modale) atașate acestui drum, și notată
Kπ = <A, Wπ, Rπ, Ππ>, sunt:
-mulțimea lumilor, adică Wπ = {π0, π
1, π
2,...};
-<s, s’> Rπ ddacă s = πi și s’ = π
i+1 (pentru fiecare s, s’ Wπ , adică pentru fiecare i N);
-în final, funcția Ππ : W 2A , va fi dată prin Ππ(π
i) = π
i(0) = π(i) (nu uităm că π
0 este de fapt
π).
Se arată ușor, prin inducție structurală (este suficient să considerăm că F este de forma true,
( F), (F1 F2), (□F) și (◊F)), că este adevărată afirmația (π)(P(π)), unde:
P(π): (F LTL)(π F atunci Kπ F)
Înainte de a ne ocupa de logica mai evoluată CTL*/CTL, să remarcăm că putem proceda și
invers, adică putem „trece” de la MD la LTL.
Dacă pornim cu o structură Kripke modală K = <A, W, R, Π>, și considerăm DK ca fiind
mulțimea tuturor „drumurilor Kripke, infinite” din K, putem spune că K F ddacă avem π F,
pentru fiecare π DK. În mod natural, vom pune π DK ddacă π = w0w1... , și <wi, wi+1> R,
pentru fiecare i N.
Mulțimea subformulelor lui F LTL, notată cl(F) (și numită închidere), va fi, posibil, utilă
pentru model-checking sau pentru demonstrarea automată.
______________________________________________________________________________
Închiderea unei formule temporale propoziționale. Fie orice F LTL.
Baza. F cl(F).
Pas constructiv.
(a) Dacă (F1 * F2) cl(F), unde * {, , U, Ũ}, atunci F1, F2 cl(F).
(b) Dacă (G) sau (G) cl(F) atunci G cl(F).
(c) Nimic altceva nu mai este în cl(F).
Aici, înțelegem de fapt că procesul de construcție al lui cl(F) se încheie imediat după ce
introducem toate formulele atomice care apar în F.
______________________________________________________________________________
La alfabetul logic cunoscut, L = A U Ā U {true, false} U P U C1 U C2, se adaugă şi o mulţime
C3 = {E, A}, a cuantificatorilor (cuantorilor) de cale. Vom pune L U C3 = Alf.
Sintaxa CTL*. Mulţimea formulelor logicii temporale cu timp ramificat peste Alf, CTL* (sau
CTL*Alf) este dată (bi)structural, imbricat, prin:
Formule de stare
Baza_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, în sensul de la LTL) sunt formule atomice (de
stare) şi elemente ale CTL*.
Pas constructiv_1 (formule noi din formule vechi).
(a1) Dacă F1, F2 CTL* sunt formule de stare, atunci (F1 F2), (F1 F2) CTL* sunt
formule de stare.
(b1) Dacă F CTL* este formulă de cale, atunci A(F), 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 cale
Baza_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.
De obicei se lucrează cu o parte mai restrânsă a lui CTL*, notată CTL, și numită logica liniară
standard cu timp ramificat.
______________________________________________________________________________
Sintaxa CTL. Definiţia sintaxei CTL este identică cu definiția CTL*, exceptând următoarele
(înlocuim acolo, peste tot, CTL* cu CTL):
Î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.
Desigur că, schimbându-se definiţia sintactică se va schimba şi definiţia lui cl(F) pentru
F CTL* (şi apoi pentru F CTL).
Vom nota cu CTLS* - mulţimea formulelor de stare şi cu CTLC* - mulţimea formulelor de
cale. Când vom folosi „F CTL*, vom înțelege însă „F CTLS*” (prin convenţie).
Procedăm similar și cu CTL.
______________________________________________________________________________
Structură Kripke temporală ramificată. O structură Kripke temporală ramificată este un
5-uplu K = <A, W, R, w0, Π>, unde (nu prea sunt lucruri efectiv noi):
-A este mulţimea variabilelor propoziţionale (cel mult numărabilă).
-W este mulţimea stărilor/lumilor universului (nevidă; finită, dacă nu se precizează altfel).
-R W W este relaţia de trecere/accesibilitate, presupusă a fi totală, adică satisface condiţia:
(w W)(w’ W)(<w, w’> R).
-w0 W este starea iniţială.
-Π : W 2A este funcţia care ataşează fiecărei stări mulţimea variabilelor propoziţionale
adevărate în acea stare.
Datorită faptului că relaţia R este totală, din fiecare stare w W „porneşte” (măcar) un drum
(secvenţă infinită de stări) π = w0w1… (π(i) = wi) care satisface (i 0)(<wi, wi+1> R);
desigur că aici am pus w = w0 (care nu coincide neapărat cu w0).
Astfel, dacă identificăm pentru un drum π, elementul π(i) cu Π(wi), putem spune că din fiecare
stare a unei structuri Kripke ramificate K, „începe” (măcar) o structură/cale/drum pentru
LTL (adică, după cum am arătat, o structură Kripke liniară). Vom spune că aceste „structuri
pentru LTL-uri” sunt generate de K (și pot fi gândite, în final, ca formând împreună niște
arbori pentru K). În acest mod, legăturile CTL*/CTL cu LTL și MD (și reciproc) sunt acum
clarificate.
Putem reprezenta o structură ramificată K printr-un graf orientat etichetat în care nodurile sunt
stările lui W, etichetele lor sunt mulţimi de variabile propoziţionale reprezentând valorile
funcţiei Π, iar arcele descriu relaţia R.
______________________________________________________________________________
Semantica CTL*/CTL. Fie K = <A, W, R, w0, Π> o structură Kripke temporală ramificată.
Adevărul formulelor CTL* în K se obţine structural, în trei faze imbricate:
(I) Adevărul formulelor CTL* într-o stare oarecare w din W.
BazaI.
(iI) Pentru fiecare w W, w true şi w false.
(iiI) Pentru fiecare w W, w p ddacă p Π(w), pentru fiecare p A şi w p ddacă
p Π(w), pentru fiecare p A (sau, direct, pΠ(w)).
Pas constructivI.
(aI) Pentru fiecare w W, w (F1 F2) ddacă w F1 şi w F2, pentru fiecare F1, F2 CTL*.
(bI) Pentru fiecare w W, w (F1 F2) ddacă w F1 sau w F2, pentru fiecare
F1, F2 CTL*.
(cI) Pentru fiecare w W, avem w A(F) ddacă pentru fiecare drum (structură LTL generată
de K) începând cu w, adică π = w0w1… (w0 = w), este adevărat că π F; și asta pentru fiecare
F CTL*.
(dI) Pentru fiecare w W, avem w E(F) ddacă există un drum (structură LTL generată de K)
începând cu w, π = w0, w1, … (w0 = w), astfel încât π F; și asta pentru fiecare F CTL*.
(II) Adevărul formulelor CTL*/CTL într-un drum/cale π, de stări din W (π privit ca structură
LTL generată de K).
BazaII.
(iII) Fie deci F orice formulă de stare din CTL*/CTL şi π = w0w1… o secvenţă infinită de stări
din W (structură LTL generată de K). Atunci avem π F dacă şi numai dacă w0 F (știm deja
că o formulă este adevărată într-o structură LTL generată de K, ddacă ea este adevărată în starea
iniţială a acelei structuri).
Pas constructivII (pentru fiecare F, F1, F2 CTL*/CTL și fiecare π, cale, ca mai sus).
(aII) Fie F1, F2 CTL*/CTL și π, cale. Atunci π (F1 F2) ddacă π F1 şi π F2.
(bII) Fie F1, F2 CTL*/CTL și π, cale. Atunci π (F1 F2) ddacă π F1 sau π F2.
(cII) Fie F CTL*/CTL și π, cale. Atunci π (F) ddacă π1 F.
(dII) Fie F1, F2 CTL*/CTL și π, cale. Atunci π (F1 U F2) ddacă există i 0 astfel încât
πi F2 şi pentru fiecare 0 j i avem π
j F1.
(eII) Fie F1, F2 CTL*/CTL și π, cale. Atunci π (F1 Ũ F2) ddacă pentru fiecare i 0,
cu πi F2, există 0 j i astfel încât π
j F1.
(III) Adevărul formulelor CTL*/CTL într-o structură Kripke ramificată K. O formulă
F CTL*/CTL este adevărată în K, ddacă ea este adevărată în orice structură LTL, π, generată
de K și care porneşte cu starea iniţială w0. Adică K F ddacă π F, pentru fiecare π având
π(0) = w0 = w0.
EXPLICAȚII SUPLIMENTARE ASUPRA MODALITĂȚILOR
Urmează, tot ca un „remember”, definițiile semantice directe (adevăr într-o cale dată, π) ale
operatorilor temporali mai des folosiți, în trei moduri: intuitiv (a)), formal (b)) și grafic (c)).
1. Next: π (F)
a) În pasul/momentul (imediat) următor (de timp), F (trebuie să fie) este adevărată
b) π1 F
c) ○ ○ ○ ○ ... (F este adevărată în starea înnegrită; în rest, nu contează)
2. Until: π (F U G)
a) F trebuie să rămână adevărată până când G devine adevărată (lucru care se și întâmplă, cu
siguranță)
b) Există i N astfel încât πi G, și, pentru fiecare 0 k i (trebuie să) avem π
k F
c) ... ○ ○ ○ ... (F este adevărată în stările înnegrite și G este falsă în ele; G devine
adevărată în starea înroșită, care este prima pusă în evidență și poate fi și prima din secvență; în
rest, nu contează)
3. Release: π (F Ũ G) (cumva dual față de U)
a) G trebuie să rămână adevărată până când se întâmplă ca F să devină adevărată (lucru care
poate să nu se întâmple niciodată)
b) Pentru fiecare i N cu πi G, există 0 k i astfel încât π
k F
c) ... (F este falsă mereu deci și G rămâne mereu adevărată), sau,
... ○ ○ ○ ... (G este adevărată în stările înnegrite și F este falsă ele; în starea
înroșită, F devine adevărată iar G rămâne și ea adevărată; în rest, nu contează)
4. Always: π (□F)
a) F trebuie să fie adevărată la fiecare pas/moment/stare a(l) căii
b) Pentru fiecare i N, avem πi F
c) ... (F este adevărată în toate stările)
5. Eventually: π (◊F)
a) Există măcar un moment de timp în care F este (va fi) adevărată
b) Există i N astfel încât avem πi F
c) ○ ○ ... ○ ○ ○ ○ ... (F este adevărată în starea înnegrită, care poate fi și prima; în stările de
dinaintea ei, F este falsă, iar în cele care urmează, nu contează)
6. Unless (weak until): π (F W G)
a) F trebuie să rămână adevărată până când G devine adevărată (ceea ce poate să nu se întâmple
niciodată)
b) Dacă există i N astfel încât πi G, atunci pentru fiecare 0 k i avem π
k F
c) ... (G este permanent falsă), sau
... ○ ○ ○ ... (F este adevărată în stările înnegrite, G este falsă în acestea, iar în
starea înroșită, G este adevărată; în rest, nu contează)
ECHIVALENȚE IMPORTANTE ÎN LOGICILE MODALE ȘI
TEMPORALE
Continuăm, tot ca un „remember”, cu listarea câtorva echivalențe. Este vorba despre echivalența
tare a unor formule din LTL (în primul rând; majoritatea lor sunt valabile și în MD, fără
transformări esențiale, dar π de mai jos se înlocuiește cu structura modală K, adică F K G
ddacă: K F ddacă K G). Ca definiție a acestui tip de echivalență, în acest contex, folosim:
F G ddacă: π F ddacă π G, pentru fiecare cale π
Mai concret, pentru fiecare F, G LTL, p A avem:
(I) Echivalențe clasice:
-F G ( F G)
-F G F G
-F G (F G) (G F)
-true p p
-false true
(II) Echivalențe legate de exprimarea unor operatori temporali în funcție de alții (vezi și
(III) (b)):
-(F Ũ G) ( F U G)
-(F W G) (F U G) (□F) F U (G (□F)) G Ũ (G F)
-(F U G) (◊G) (F W G)
-(F Ũ G) G W (G F)
-(◊F) true U F (□( F))
-(□F) false Ũ F (◊( F))
Este adevărat și faptul că formula F U G ◊G este validă (pentru fiecare F).
(III) Alte echivalențe utile:
(a) Distributivitate
-(F G) (F) (G)
- (F G) (F) (G)
-(F U G) (F) U (G)
-◊(F G) (◊F) (◊G)
-□(F G) (□F) (□G)
-H U (F G) (H U F) (H U G)
-(F G) U H (F U H) (G U H)
(b) Propagarea negației
- (F) ( F)
- (□F) ◊( F)
- (◊F) □( F)
- (F U G) ( F Ũ G)
- (F Ũ G) ( F U G)
(c) Proprietăți temporale speciale (primele 3: idempotență; următoarele 5: expansiune;
ultimele 2: absorbție)
-◊F ◊(◊F)
-□F □(□F)
-F U G F U (F U G) (F U G) U G
-F U G G (F (F U G))
-F W G G (F (F W G))
- F Ũ G G (F (F Ũ G))
-□F F (□F)
-◊F F (◊F)
- ◊(□(◊F)) □(◊F)
- □(◊(□F)) ◊(□F)
(IV) Să amintim și câteva echivalențe care implică (și) cuantificatorii de cale (bineînțeles că
aici totul se relativizează la CTL*/CTL, inferent că este vorba despre formule, modalități, sau
noțiunea de echivalență tare):
(a) A(◊F) E(□( F))
(b) A(□F) E(◊( F))
(c) A(F) E(( F))
(d) A(◊F) A(true U F)
(e) E(◊F) E(true U F)
(f) A(□F) E(true U ( F))
(g) E(□F) A(true U ( F))
EXEMPLE UTILE PRIVIND LOGICILE MODALE ȘI TEMPORALE
(majoritatea au fost făcute împreună)
Începem cu câteva exemple pentru MD, LTL, CTL*/CTL.
Exemplu. Fie structura Kripke modală K = <A, W, R, Π>, unde:
-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}
Să se construiască graful care reprezintă R. Este relația reflexivă ? Este adevărat că avem:
w1 q, w1 (◊q), w1 (□q), w5 (□p), w5 (□q), w5 (□p □q), w5 □(p q) ?
Care sunt lumile care satisfac formula F = ((□p) p) ? Avem K F ? Dar în nedeterminismul
angelic ?
______________________________________________________________________________
Exemplu. Fie p, q, r A variabile propoziţionale şi formulele LTL:
F1 = □(p (q)), F2 = □(p ( q U r)), F3 = □(◊p), F4 = (p Ũ q). Avem π Fi, i [4],
după cum urmează:
-F1 este satisfăcută în toate drumurile π care satisfac condiţia: fiecare stare (w, element din π) în
care p este adevărată/satifăcută (p w), este imediat urmată de o stare în care q este adevărată.
-F2 este satisfăcută în toate drumurile π care satisfac condiţia: dacă p este satisfăcută într-o stare,
atunci, începând cu starea (imediat) următoare acesteia (precum şi în următoarele), fie r este
adevărată (mereu), fie q este şi rămâne falsă până când apare (ceea ce se întâmplă cu siguranţă) o
(altă) stare în care r este adevărată (și apoi, r rămâne adevărată până „la sfârșit”).
-F3 este satisfăcută în toate drumurile π care satisfac condiţia: p este adevărată într-o infinitate de
stări.
-F4 este satisfăcută în toate drumurile π care satisfac condiţia: q este mereu adevărată de la
început, sau măcar o dată falsă, dar nu mereu începând cu acel loc; dacă se întâmplă totuși așa
ceva, atunci există măcar un loc anterior celui în care q este falsă și în care p este adevărată.
______________________________________________________________________________
Exemplu. Fie formula F = A((E(p) Ũ A(((p (q)) U r)))). Să se „deseneze” arborele care o
reprezintă. Apoi să se găsească cl(F) și să se identifice formulele din CTL*/CTL, de stare și de
cale (p, q, r A).
______________________________________________________________________________
Exemplu.
Sunt formule CTL* (de stare): A E(□p)), A(□(◊p)), E(□(◊p)) (?)
Sunt formule CTL (de stare): A(□p), E(□p), A(□E E(□E(◊p)) (?)
În cele de mai sus, desigur că p A.
______________________________________________________________________________
Iată și câteva exemple privind demonstrarea unor echivalențe.
Exemplu.
Să demonstrăm că (◊F) true U F, adică, pentru fiecare drum π avem:
π (◊F) ddacă π true U F.
Dar, π (◊F) ddacă există k N, cu πk adică ddacă există k N, cu
(πk i pentru fiecare 0 j k, avem π
j true) (deoarece true este adevărată în orice stare a
drumului π) și, în sfârșit, ddacă π true U F (din definiția lui U).
______________________________________________________________________________
Exemplu.
Să demonstrăm și (□F) (◊( F)), adică, să arătăm că pentru fiecare drum π, avem:
π (□F) ddacă π (◊( F)).
Dar, π (□F), ddacă pentru fiecare i N avem πi F (din definiția lui □), adică ddacă nu este
adevărat că există i N, astfel încât (nu avem πi F) (legătura dintre oricare și există în LP1),
adică (vom folosi acum definițiile negației) ddacă nu este adevărat că (există i N, astfel încât
πi F), adică ddacă nu este adevărat că (π ◊( F)), adică, în sfârșit, ddacă π (◊( F)) (din
nou am folosit definiția negației).
______________________________________________________________________________