L3. Logica Temporala Liniara

Logica propozitionala

Inainte de a prezenta formalismul Logicii Temporale Liniare (LTL), trebuie prezentate conventiile logicii clasice (i.e. propozitionale), care vor fi utilizate si in cadrul LTL.
Pornind de la o multime de propozitii atomice AP, numite uneori simboluri propozitionale, se va defini multimea formulelor logicii propozitionale peste AP, pe scurt formule, prin urmatoarele reguli:

1. adevarat (true) este o formula
   
2. orice propozitie atomica a ∈ AP este o formula
   
3. daca Φ, Φ₁ si Φ₂ sunt formule, atunci si (¬Φ) si (Φ₁ ^ Φ₂) sunt formule
   
4. nimic altceva nu este o formula.
   

In sintaxa abstracta, se pot rescrie regulile de mai sus astfel:
Formulele descriu propozitii care ar putea fi valide sau nu, in functie de valoarea de adevar a propozitiilor atomice care trebuie sa fie adevarate. In mod intuitiv, formula a implica presupunerea ca propozitia atomica a este valida.
Simplificarea formulelor logice se poate face prin intermediul operatorilor derivati si declarând o regula de precedenta a operatorilor.
Regula de precedenta a operatorilor atribuie operatorului unar de negare o prioritate mai mare decât a operatorului conjunctie. De exemplu, formula ((¬a) ^ b) se poate scrie pe scurt ¬a ^ b.
Se pot defini urmatorii operatori derivati:
Pentru a formaliza sensul intuitiv al formulelor propozitionale, este necesara o definitie precisa a contextului in care se hotaraste care propozitii atomice sunt valide si care nu. Aceasta se realizeaza cu ajutorul unei evaluari care atribuie valorile de adevar 0 (fals) sau 1 (adevarat) fiecarei propozitii atomice. Formal, o evaluare pentru AP este o functie μ : AP → { 0, 1 }.
Semantica logicii propozitionale este specificata printr-o functie (relatie) de satisfactie ⊨ indicând evaluarile μ pentru care o formula Φ este adevarata. Formal, ⊨ este o multime de perechi (μ, Φ), unde μ este o evaluare, iar Φ o formula.Se scrie:
μ ⊨ Φ in locul (μ, Φ) ∈ ⊨
In consecinta, μ ⊭ Φ inseamna (μ, Φ) ∉ ⊨. Intuitiv, μ ⊨ Φ inseamna ca formula Φ este adevarata sub evaluarea μ.
Relatia de satisfactie a logicii propozitionale se defineste astfel:

μ ⊨ true
μ ⊨ a		⇔		μ(a) = 1
μ ⊨ ¬Φ		⇔		μ ⊭ Φ
μ ⊨ Φ1 ^ Φ2		⇔		μ ⊨ Φ1 si μ ⊨ Φ2

Logica Temporala Liniara

In cadrul sistemelor reactive (sisteme care interactioneaza in mod continuu cu mediul din care fac parte) corectitudinea depinde de executia sistemului, nu doar de intrarile si rezultatele unor calcule. Logica temporala este un formalism pentru specificarea proprietatilor(cerinte) de corectitudine ale sistemelor folosind atribute temporale.
Logica temporala extinde logica propozitionala intr-un mod care permite referirea la comportamentul infinit al sistemelor reactive. Aceasta ofera o notatie precisa pentru exprimarea relatiei dintre starile unei executii. Chiar daca logica temporala a fost studiata inca din antichitate in domenii precum filozifia, aplicarea acesteia in verificarea sistemelor reactive a fost propusa la sfârsitul anilor '70 de Pnuelli.
Principalele relatii temporale, prezente in majoritatea logicilor temporale, includ operatorii:

◊		“eventual”		(cândva in viitor)
□		“mereu”		(acum si in toate starile viitoare)

Natura logicii temporale poate fi de doua feluri: liniara sau arborescenta. Dintr-o perspectiva liniara, exista un singur succesor, in timp ce dintr-o perspectiva arborescenta, pot exista cai alternative in fiecare moment de timp. Perspectiva liniara este abordata in cadrul Logicii Temporale Liniare, formalism care sta la baza lucrarii de fata.
In cadrul procesului de validare, relatia de timp are un sens abstract. Desi termenul sugereaza o relatie de timp intre evenimente, acesta se refera la ordinea acestora, dar nu si la momentele de timp in care acestea se produc. Acest lucru implica o privire discreta asupra relatiei de timp. Prin formalismul logicii temporale pot fi verificate conditii precum „evenimentul X se va produce doar dupa Y”, sau „exenimentul X se produce infinit de des.”
Formulele Logicii Temporale Liniare pot fi descrise astfel:
φ ::= true| a | φ₁ ^ φ₂ | ¬φ |     O φ | φ₁ U φ₂ , unde a apartine multimii propozitiilor atomice AP.
Formalismul LTL preia operatorii logicii clasice, carora le adauga cei doi operatori temporali de baza   O ( urmator - next) si U (pâna când - weak until).
Formula   O φ este valida in momentul de fata doar daca φ este valida la momentul urmator.
Formula φ₁ U φ₂ este valida doar daca φ₁ este adevarat pâna când φ₂ devine si el adevarat.
Trebuie facuta observatia ca operatorul until prezinta asociativitate de dreapta. De exemplu, φ₁ U φ₂ U φ₃ este echivalent cu φ₁ U (φ₂ U φ₃).
Prin utilizarea operatorilor negatie si conjunctie, pot fi definiti aceiasi operatori derivati ca si in cazul logicii propozitionale.
In plus, pot fi obtinuti si operatorii eventual si mereu, astfel:

◊		φ		=		true U φ
□		φ		=		¬ ◊ ¬φ

Formula ◊ φ ne asigura ca φ va fi adevarat cândva in viitor, in timp ce □ φ semnifica necesitatea ca φ sa fie mereu adevarata, incepând din acest moment. Este acelasi lucru cu a spune ca nu este permisa eventualitatea ca φ sa fie fals in viitor.
Semnificatile acestor operatori temporali sunt ilustrate in cadrul figurii de mai sus. In partea stânga sunt trecute formulele LTL corespunzatoare operatorilor, iar in dreapta, secvente de stari (executii). Deasupra fiecarei stari sunt trecute conditiile logice care trebuie sa fie adevarate pentru ca formulele sa fie valide.
Prin compunerea operatorilor □ si ◊ pot fi obtinute noi relatii temporale:

□◊		„infinit de des φ”
◊□		„eventual mereu φ” - eventual, φ devine si ramâne adevarata pâna la sfârsit.

Ca exemplu al descrierii proprietatilor sistemelor prin logica temporala, putem considera problema excluziunii mutuale a doua procese concurente, P1 si P2. Executia proceselor poate trece prin trei stagii: o sectiune non-critica, in care procesele nu interactioneaza in nici un fel si lucreaza cu multimi distincte de variabile, o sectiune critica, reprezentând faza accesului la o resursa comuna si o faza de asteptare, prin care procesele trebuie sa treaca inainte de a intra in sectiunea critica. Presupunem ca se poate verifica daca un proces i se afla in asteptare sau in sectiunea critica prin intermediul propozitiilor wait_i, respectiv crit_i.
Proprietatea de siguranta a mecanismului de excluziune mutuala impune ca: in orice moment maxim un proces se poate afla in sectiunea critica. Se obtine formula:
□ ¬ (crit_a ^ crit_b ) care se poate rescrie:
□ (¬crit_a ∨ ¬crit_b ) Formula exprima conditia ca in orice moment (mereu □ ) cel putin unul dintre procese nu se afla in sectiunea critica.
Pentru ca algoritmul de excluziune mutuala sa functioneze, ori de câte ori un proces intra in asteptare, trebuie sa aiba eventual acces la sectiunea critica. Proprietatea se modeleaza prin formula:
(□◊wait_a → □◊crit_a) ^ (□◊wait_b → □◊crit_b) Aceste formule se refera doar la locatii (valori ale contorului de program) prin intermediul propozitiilor atomice wait_i si crit_i. Propozitiile se pot referi, de asemenea, si la valorile unor variabile.
NOTA: principiile verificarii formulelor LTL se bazeaza pe teoria automatelor pe cuvinte infinite, sau pe scurt a ω-automatelor.
Cuvinte infinite peste alfabetul Σ sunt secvente infinite A₀, A₁, A₂, ... de simboluri A_n ∈ Σ. Σ^ω reprezinta multimea tuturor cuvintelor infinite peste Σ.
Fie φ o formula LTL peste AP. Proprietatea de timp liniar introdusa de φ este:
Words (φ) = { σ ∈ AP^ω | σ ⊨ φ } , unde satisfactia relatiei ⊨ ⊆ AP^ω × LTL este cea mai mica functie cu proprietatile:

σ ⊨ true
σ ⊨ a		⇔		a ∈ A0 ( A0 ⊨ a )
σ ⊨ φ1 ^ φ2		⇔		σ ⊨ φ1 si σ ⊨ φ2
σ ⊨ ¬φ		⇔		σ ⊭ φ
σ ⊨  O Φ2		⇔		σ[1...] = A1 A2 A3 … ⊨ φ
σ ⊨ φ1 U φ2		⇔		∃j ≥ 0 a.i. σ[j...] ⊨ φ2 si σ[i...] ⊨ φ2 , ∀ 0 ≤ i < j

Aici, σ = A₀, A₁, A₂, ... ∈ AP^ω , iar σ[j...] = A_j, A_j+1, A_j+2, ... este sufixul lui σ care porneste de la al (j+1)-lea simbol A_j.
Daca definim notiunea fragment de cale pentru un sistem de tranzitii TS, ca fiind o secventa finita de stari s₀, s₁, s₂, ... s_n unde s_i ∈ Post ( s_i-1 ), un fragment infinit de cale π va fi secventa infinita de stari s₀, s₁, s₂, ... unde s_i ∈ Post ( s_i-1 ), ∀ i > 0 . In aceste conditiile, vom numi o cale de executie a sistemului de tranzitii TS un fragment initial, maxim de cale (analog definitiei 2.6 - lab2).
Vom spune ca un sistem de tranzitii TS satisface propozitia temporala φ daca toate secventele sale de executie satisfac aceasta relatie. Practic, pentru a demonstra acest lucru se aplica principiul reducerii la absurd si se va cauta daca exista o singura secventa care nu verifica formula φ.

Logica temporala in SPIN

Sintaxa expresiilor LTL in SPIN este urmatoarea:

ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl

Operanzi(opd):
true, false, nume definite de utilizator care incep cu o
litera mica, sau expresii incapsulate intre acolade
ex: { a + b > n}
 

Operatori Unari (unop):
[] 	(operatorul temporal mereu)
<> 	(operatorul temporal eventual)
! 	(operatorul logic de negare)


Operatori Binari (binop):
U 	(operatorul temporal pâna când)
V 	(dualul operatorului U): (p V q) ≡ !(!p U !q))
&& 	(operatorul logic si)
|| 	(operatorul logic sau)
/\ 	(forma alternativa pentru &&)
\/ 	(forma alternativa pentru ||)
-> 	(operatorul pentru implicatie logica)
<-> 	(operatorul pentru echivalenta logica)
X 	(operatorul temporal next)

Versiunea 6 a validatorului SPIN permite specificarea propozitiilor temporale in doua moduri: fie inline, in cadrul modelelor, fie prin traducerea expresiei intr-o clauza temporala si includerea acesteia in model.
Cea mai buna varianta este aceea a definirii inline, astfel:

ltl [ nume ] '{' formula '}'

Utilizarea numelui este optionala, dar recomandata atunci când se doreste specificarea mai multor proprietati logice.
NOTA: operatorul next este dezactivat in mod implicit, fiind incompatibil cu algoritmul de reducere partiala a ordinului (POR).
Spre exemplu, clauza temporala (sub forma unui automat Büchi) creata de SPIN pentru operatorul Until (propozitia a U b ) este urmatoarea:

never until { /* !((a) U (b)) */
accept_init:
T0_init:
	if
	:: (! (b)) -> goto T0_init
	:: (! (a) && ! (b)) -> goto accept_all
	fi;
accept_all:
	skip
}

Pentru a fi utilizata in verificare, expresia temporala trebuie negata (se face automat in cazul specificarii inline). Daca automatul modelat prin aceasta constructie fie isi incheie executia fie cicleaza in mod infinit printr-o stare marcata cu o eticheta accept, validatorul considera ca a identificat o eroare (exista o cale de executie care nu satisface propozitia temporala).
NOTA: daca intr-un moment al executiei nu este posibila nici o tranzitie in clauza temporala, se considera ca propozitia temporala este satisfacuta pentru orice stare ulterioara, iar validatorul va trece la verificarea urmatoarei cai.

Specificarea clauzelor temporale

Sintaxa:

never { secventa }

Clauzele temporale sunt utilizate pentru specificarea unui comportament de interes al sistemului modelat. De regula specifica un comportament care NU trebuie sa fie posibil.
In timpul validarii, pentru fiecare tranzitie din cadrul modelului principal va fi executata o instructiune in clauza never (ruleaza in "lockstep"), daca este posibil. Daca se ajunge la sfarsitul clauzei never, se considera ca s-a identificat un comportament nedorit.
NOTA: in timpul procesului de validare poate fi utilizata o singura clauza temporala, dar pot fi specificate mai multe.

Aplicatie - algoritm de excluziune mutuala

Fie un algoritm care foloseste o variabila globala (un fanion) pentru semnalizarea dizponibilitatii zonei critice. Fie codul (fisierul 40.pml) :

mtype={wait, crit, done}
mtype statusa = wait;
mtype statusb = wait;

bool flag = true;


active proctype A() {
    (flag) ->
        statusa = crit;
        flag = false;
        
        skip;		//zona critica
        
        statusa = done;
        
}

active proctype B() {
    (flag) ->
        statusb = crit;
        flag = false;
        
        skip;		//zona critica
        
        statusb = done;
        flag = true;
}

Algoritmul este unul exemplificativ si nu are nici o utilitate practica. Evident, acesta nu asigura excluziunea mutuala a accesului la zona critica. Conditia de excluziune mutuala este: □ ¬ ( statusa==crit ^ statusb==crit ) Aceasta se traduce in conditia LTL (se adauga la sfarsitul fisierului 40.pml):

ltl p0 { []( ! (statusa==crit && statusb==crit) ) }

In urma validarii a fost identificata o incalcare a clauzei temporale: A doua conditie de buna functionare a algoritmului de excluziune mutuala este ca ambele procese sa aiba acces eventual la zona critica: (□◊crit_a) ^ (□◊crit_b) ,care se traduce in

ltl p1 { ([]<> (statusa==crit)) && ([]<> (statusb==crit)) }

Adaugati si aceasta clauza temporala in modelul anterior si validati.
NOTA: deoarece noul model are doua clauze temporale, trebuie specificat la validare care dintre acestea va fi utilizata(argumentul -N):

Aplicatie interactiva - algoritm de sincronizare a ceasului logic cu timp scalar

Fie modelul [Lamport, 1978] unui ceas logic orientat pe evenimente (care se incrementeaza cu δ > 0 la fiecare eveniment; de regula, δ = 1). Vom nota t_i ceasul logic al procesului i. Consideram eveniment:

• receptia, transmisia unui mesaj sau
• alte evenimente interne procesului curent

Algoritmul functioneaza astfel:

1. daca evenimentul este unul de receptie, se actualizeaza ceasul intern cu noua valoare, daca este cazul
   t_i < t_rec => t_i = t_rec
2. la alte evenimente se incrementeaza ceasul logic intern, cu o valoare δ
3. inainte de transmisia unui mesaj se incrementeaza ceasul logic cu δ, si se transfera impreuna cu mesajul