Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

Adriano Peron » 12.Specifica di proprietà in Logica Temporale Lineare


Temi della lezione

Introduzione a un Linguaggio logico di specifica delle proprietà

  • Logica Temporale in Tempo Lineare (LTL)
  • Sinatssi
  • Semantica
  • Esempi di proprietà

Verifica in LTL

Elementi essenziali

Il sistema da verificare è descritto da un LTS (S,S_0,\Delta);
Le asserzioni elementari sono espresse da un insieme AP di proposizioni atomiche;
Gli stati dell’LTS sono decorati con un insieme di proposizioni atomiche mediante una funzione L: S \longrightarrow 2^{AP}

Se p \in L(s) l’asserzione p vale nello stato s;
Se p \not\in L(s) l’asserzione p non vale nello stato s.

La struttura che ne deriva è chiamata struttura di Kripke ed ha la forma (S,S_0,\Delta,AP,L).

Esempio: struttura di Kripke

LTS di un arbitro che soddisfa le richieste di accesso ad una risorsa condivisa per due processi richiedenti.

Alfabeto transizioni:
Req_i (richiesta dell’iesimo processo)
Grt_i (assegnazione all’iesimo processo)
Ret_i (rilascio dell’i-esimo processo)

Proposizioni atomiche:
R_i (iesimo processo inattivo)
W_i (iesimo processo in attesa)
P_i (i-esimo processo con risorsa assegnata)

Fig.1 Esempio di struttura di Kripke.

Fig.1 Esempio di struttura di Kripke.


Verifica in LTL

Un cammino della struttura di Kripke K è la struttura su cui viene valutata una formula \phi di LTL.

Un cammino è un comportamento dell’LTS (specifica del sistema);
Un cammino è una sequenza di insiemi di proposizioni atomiche;
La formula \phi descrive una proprietà del sistema di cui si vuole verificare il soddisfacimento.

Esempio di cammino (si omettono gli archi delle transizioni):

\begin{array}{ccccccccc}S_0 & S_3 & S_4 & S_0 & S_1 & S_2 & S_0 & S_3 & \ldots\\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

Il cammino considerato soddisfa la seguente proprietà (informale):

Se il processo 1 è in stato di attesa, successivamente avrà assegnata la risorsa.

Verifica in LTL

Model checking

La struttura di Kripke K verifica la proprietà \phi (K \models \phi) se ogni cammino di K (a partire dallo stato iniziale) è un modello per la proprietà.

Il modello di Kripke verifica la seguente proprietà (informale).

Per ogni stato, se il processo 1 è in stato di attesa (w_1 è vera), nello stato successivo avrà assegnata la risorsa (p_1 è vera).

Il modello di Kripke non verifica la seguente proprietà (informale).

Esiste un punto della computazione in cui il processo 1 avrà assegnata la risorsa.

La proprietà non è verificata perché il cammino che attraversa ciclicamente i soli stati s_0,s_1,s_2 non soddisfa la proprietà.

LTL: sintassi

Insieme AP di proposizioni atomiche AP=\{p_0,p_1,\ldots p_n\}

Formule

  • Ogni proposizione atomica p \in AP è una formula LTL;
  • Se \phi, \phi_1, \phi_2 sono formule LTL;
  • \neg \phi, \phi_1\ \vee\ \phi_2, \phi_1\ \wedge\ \phi_2 sono formule LTL;
  • \bigcirc\ \phi (operatore “next”) è una formula LTL;
  • \Diamond\ \phi (operatore “future”) è una formula LTL;
  • \Box\ \phi (operatore “global”) è una formula LTL;
  • \phi_1\ U\ \phi_2 (operatore “until”) è una formula LTL.

LTL: Semantica

Il soddisfacimento di una formula è valutato rispetto ad una sequenza (infinita) \pi \in (2^{AP})^{\omega}:

Sequenza infinita di sottoinsiemi di AP;
E’ la sequenza di etichette associati agli stati di un cammino iniziale di una struttura di Kripke.

Notazione:

\pi(i) \mbox{ con } i\geq 0 indica il sottoinsieme di AP associato all’i-esima posizione della sequenza

(insieme di proposizioni atomiche vere nell’i-esimo stato del cammino della struttura di kripke).

Ogni formula è valutata in un punto specifico della sequenza \bf \pi,i \models \ldots

Semantica LTL

\phi  :: {\bf p}\ | \phi \vee \phi \ |\phi \wedge \phi \ | \neg \phi \ |  \bigcirc \phi \ | \Diamond \phi \ | \Box \phi \ | \phi\ U\ \phi

\pi , i \models p \mbox{ con } p\in AP \mbox{ se } p \in \pi(i)

\begin{array}{ccccccccc} \pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6) \pi(7) & \ldots \\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

\pi , 0 \models r_1

\pi, 1\models w_1

\pi, 2 \models p_1

Semantica LTL

\phi  :: p \ |{\bf  \phi \vee \phi \ |\phi \wedge \phi \ | \neg \phi} \ |  \bigcirc \phi \ | \Diamond \phi \ | \Box \phi \ | \phi\ U\ \phi

\pi , i \models \phi_1 \vee \phi_2 \mbox{ se } \pi,i \models \phi_1 \mbox{ o } \pi,i \models \phi_2

\pi , i \models \phi_1 \wedge \phi_2 \mbox{ se } \pi,i \models \phi_1 \mbox{ e } \pi,i \models \phi_2

\pi , i \models \neg\phi \mbox{ se non \'e il caso che } \pi,i \models \phi

\begin{array}{ccccccccc} \pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6) & \pi(7) & \ldots \\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

\pi , 0 \models \neg w_1 \wedge \neg p_1

\pi, 1\models w_1 \vee r_1

\pi, 2 \models (p_1 \wedge r_2) \wedge (\neg w_1 \wedge \neg r_1)

Semantica LTL

\phi  :: p \ | \phi \vee \phi \ |\phi \wedge \phi \ | \neg \phi\ | {\bf \bigcirc \phi} \ | \Diamond \phi \ | \Box \phi \ | \phi\ U\ \phi

Operatore temporale NEXT (Successore)

\pi , i \models \bigcirc (\phi) \mbox{ se } \pi,i+1 \models \phi

\begin{array}{ccccccccc} \pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6) &\pi(7) & \ldots \\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

\pi , 0 \models  w_1 \wedge \bigcirc p_1

\pi, 0 \models \bigcirc \bigcirc p_1 \wedge \neg \bigcirc p_1

\pi, 1 \models \bigcirc p_1 \wedge  \neg p_1

Semantica LTL

\phi  :: p \ | \phi \vee \phi \ |\phi \wedge \phi \ | \neg \phi\ | \bigcirc \phi \ | {\bf \Diamond \phi} \ | \Box \phi \ | \phi\ U\ \phi

Operatore temporale Future (Nel futuro si verifica la proprietà)

\pi , i \models \Diamond (\phi) \mbox{ se }\exists j \geq i\  :\ \pi,j \models \phi

\begin{array}{ccccccccc}\pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6) & \pi(7) & \ldots \\\{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots\end{array}

\pi , 0 \models  \Diamond (p_1 \wedge r_2)

\pi, 2 \models p_1 \wedge r_2

Semantica LTL

\phi  :: p \ | \phi \vee \phi \ |\phi \wedge \phi \ | \neg \phi\ |  \bigcirc \phi \ | \Diamond \phi \ | {\bf \Box \phi} \ | \phi\ U\ \phi

Operatore temporale Globally (la proprietà si verifica sempre)

\pi , i \models \Box (\phi) \mbox{ se } \forall j \geq i\  :\ \pi,j \models \phi

\begin{array}{ccccccccc} \pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6) & \pi(7) & \ldots \\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

\pi , 0 \models  \Box (r_1 \vee r_2)

Uno dei due processi è sempre inattivo

\pi, 0 \models \Box (\neg w_1 \vee \bigcirc p_1)

Dopo aver raggiunto lo stato di attesa si accede in un passo alla risorsa

Semantica LTL

\phi  :: p \ | \phi \vee \phi \ |\phi \wedge \phi \ | \neg \phi\ |  \bigcirc \phi \ | \Diamond \phi \ | \Box \phi \ | {\bf \phi\ U\ \phi}

Operatore temporale Untile (nel futuro deve valere \phi_2 e nel frattempo deve valere con continuità \phi_1)

\pi , i \models \phi_1\ U\ \phi_2 \mbox{ se } \exists j \geq i\  :\ \pi,j \models \phi_2\ \wedge \forall i \leq k < j\ : \ \pi,k \models \phi_1

\begin{array}{ccccccccc} \pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6)&\pi(7) & \ldots \\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

\pi , 0 \models  r_2\ U\ w_2

Il secondo process sarà ad un certo punto in attesa e nel frattempo è inattivo.

LTL: operatori derivati

Connettivi standard derivati:

True è abbreviazione per
p \vee \neg p per qualche p\in AP

\phi_1 \wedge \phi_2

È abbreviazione per
\neg (\neg \phi_1 \vee \neg \phi_2)

\phi_1 \supset \phi_2

È abbreviazione per
(\neg \phi_1 \vee \phi_2)

Operatori temporali derivati:

\Diamond \phi è abbreviazione per  True\ U\ \phi

\Box \phi è abbreviazione per  \neg \Diamond \neg \phi

LTL: operatori derivati (segue)

Altri operatori temporali:

\phi_1\ B\ \phi_2 (Before)

\phi_2 non può essere osservato senza che prima sia osservato \phi_1

\pi , i \models \phi_1\ B\ \phi_2 \mbox{ se }

se\ \exists j \geq i\  :\ \pi,j \models \phi_2\
allora\ \exists i \leq k < j\ : \ \pi,k \models \phi_1

È esprimibile con
\neg (\neg \phi_1\ U\ \phi_2)

\begin{array}{ccccccccc} \pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6) & \pi(7) & \ldots \\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

\pi , 0 \models  r_2\ U\ p_2

LTL: operatori derivati (segue)

Altri operatori temporali:

\phi_1\ W\ \phi_2 (Unless)

Sempre \phi_1 a meno che non si osservi \phi_2

È esprimibile con
\Box\ \phi_1 \vee  (\phi_1\ U\ \phi_2)

Si osservi che \Box\ \phi È esprimibile con   \phi\  W\ \neg\ True

\begin{array}{ccccccccc} \pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6) &\pi(7) & \ldots \\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

\pi , 0 \models  r_2\ W\ w_2

LTL: operatori derivati (segue)

Altri operatori temporali:

\phi_1\ R\ \phi_2 (Releases)

Sempre \phi_2 a meno che non si osservi prima \phi_1

È esprimibile con
\neg (\neg \phi_1\ U\ \neg \phi_2)

Si osservi che Releases è l’operatore duale di Until

\begin{array}{ccccccccc} \pi(0) & \pi(1) & \pi(2) & \pi(3) & \pi(4) & \pi(5) & \pi(6) & \pi(7) & \ldots \\ \{r_1,r_2\} & \{w_1,r_2\} & \{p_1,r_2\} & \{r_1,r_2\} & \{r_1,w_2\} & \{r_1,p_2\} & \{r_1,r_2\} & \{w_1,r_2\} & \ldots \end{array}

\pi , 0 \models  w_2\ R\ r_2

Model Checking

Sia K=(S,S_0,\Delta,AP,L) una struttura di Kripke e \phi una formula di LTL.

Un AP-cammino di K è una sequenza

L(s_0),L(s_1),L(s_2),\ldots,L(s_i),\ldots

Dove s_0,s_1,s_2,\ldots,s_i,\ldots sono la sequenza di stati di un comportamento originato dallo stato iniziale.

(sequenza di insiemi di proposizioni atomiche che etichettano un comportamento dell’LTS)

K \models \phi (problema del model checking)

Se per ogni AP-cammino \pi vale che \pi,0 \models \phi.

Esempio: model checking

Non può mai capitare che entrambi i processi possano avere la risorsa allo stesso tempo
K \models \Box \neg (p_1 \wedge p_2)

Se in stato di attesa avrà la risorsa
K \models \Box  (w_i \supset \diamond p_i)

Ogni processo è infinitamente spesso inattivo
K \models \Box \Diamond (r_i)

Ogni processo se è infinitamente spesso in attesa, infinitamente spesso avrà la risorsa
K \models (\Box \Diamond (w_i)) \supset (\Box \Diamond (p_i))

Non vale però
K \models (\Box \Diamond (r_i)) \supset (\Box \Diamond (p_i))

Fig.2 Esempio di struttura di Kripke K.

Fig.2 Esempio di struttura di Kripke K.


  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion