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
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
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