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 » 14.Model checking di LTL basato su automi


Temi della lezione

Introduzione all’approccio basato su automi per il Model Checking:

  • Definizione dell’approccio
  • Preliminari alla costruzione
    • Formule LTL in forma normale
    • Automi di Büchi con accettazione generalizzata
  • Riduzione del problema del model checking al problema del vuoto per un automa di Büchi
    • Costruzione dell’automa
    • Esempio di costruzione

Model checking per LTL

Si ricorda che data una struttura di Kripke K=(S,S_0,\Delta,AP,L) e una formula di LTL \phi il problema del model checking è decidere se per ogni AP-cammino \pi di K vale che

\pi,0 \models \phi (scritto in breve K \models \phi).

Un algoritmo di model checking è dunque una procedura di decisione che per una struttura di Kripke K e formula \phi restituisce:

Si se K \models \phi
No se non è il caso che K \models \phi e fornisce in questo secondo caso un controesempio che testimonia la violazione della proprietà.

In alternativa al provare che per ogni cammino \pi \pi,0 \models \phi, è preferibile considerare il problema duale e cercare un controesempio che violi la proprietà desiderata:

provare che esiste un cammino \pi tale che \pi,0 \models \neg \phi

Model Checking per LTL (segue)

Un AP-cammino è una sequenza di insiemi di simboli proposizionali in AP opportunamente sincronizzata con un cammino dell’LTS in K.

Per ogni formula \phi di LTL, è possibile definire un automa di Büchi
B_{\phi} \mbox{ sull'alfabeto } \Sigma = 2^{AP}
che accetta una sequenza infinita \alpha \in \Sigma^{\omega} se e solo se \alpha,0 \models \phi

In altri termini il linguaggio L(B_{\phi} ) è precisamente l’insieme dei modelli che soddisfano la formula \phi

Per verificare se un AP-cammino \pi di K è tale che \pi ,0 \models \phi occorre dunque vedere se:

  • \pi \in L(B_{\phi} ) (è un modello per la formula)
  • \pi è una sequenza sincronizzabile con un comportamento di K.

Model Checking per LTL (segue)

Se K ha un numero finito di stati può essere visto come un automa di Büchi B_{K}

La sincronizzazione tra B_K \mbox{ e } B_{\phi} indicata da
B_K \oplus B_{\phi} è ancora un automa di Büchi.

Il problema di verificare l’esistenza di un controesempio alla proprietà \phi in K è equivalente a verificare se l’automa di Büchi B_{K}<br /> \oplus B_{\neg \phi} ) accetta il linguaggio vuoto.

Il problema del model checking di LTL è dunque riconducibile alla risoluzione del problema del vuoto per un opportuno automa di Büchi.

Dal punto di vista della complessità

  • Il problema del vuoto è lineare nella taglia di B_{K}<br /> \oplus B_{\neg \phi}
  • Poiché B_{K}\oplus B_{\neg \phi} è sostanzialmente una variante dell’intersezione degli automi B_{K}\mbox{ e }B_{\neg \phi} la sua taglia è quadratica nelle taglie dei due operandi.
  • Purtroppo la taglia di B_{\neg \phi} è esponenziale nella dimensione della formula.

Riepilogo procedura decisione

Fig. 1 Algoritmo di decisione per il model checking di LTL basato su automi.

Fig. 1 Algoritmo di decisione per il model checking di LTL basato su automi.


Costruzione dell’automa di sincronizzaione: preliminari

Per la costruzione dell’automa di sincronizzazione è comodo utilizzare una variante degli automi di Büchi chiamata automi di Büchi generalizzati.

Rispetto alla definizione standard gli automi di Büchi generalizzati variano solo rispetto alla condizione di accettazione.

Un automa di Büchi generalizzato ha un insieme \overline{F}=F_1,\ldots , F_n di insiemi di stati di accettazione.

La condizione di accettazione impone che un comportamento sia accettato se per ogni insieme F_i, \mbox{ con } 1 \leq i \leq n esiste uno stato che occorre infinitamente spesso nella computazione.

La condizione di accettazione generalizzata non aggiunge capacità espressiva agli automi di Büchi.

Infatti, un automa di Büchi generalizzato
B=\langle\Sigma, Q, q_0, \delta,F_1, \ldots,F_n \rangle è equivalente alla seguente intersezione di automi di Büchi standard

\bigcap B_i \mbox{ con } B=\langle\Sigma, Q, q_0, \delta,F_i \rangle

Costruzione dell’automa di sincronizzaione: preliminari

La formula \phi deve essere espressa in una opportuna forma normale in cui la negazione coinvolge solo simboli di predicato.

Per semplicità non vengono considerati gli operatori temporali derivati.

La sintassi della forma normale è come segue.

\phi ::= True\ \mid\ False\ \mid\ p\ \mid\ \neg p\ \mid\ \phi \vee \phi\ \mid\ \phi \wedge \phi\ \mid\ \bigcirc\ \phi\<br /> \mid\ \phi\ U\ \phi\ \mid\ \phi\ R\ \phi

Con p\in AP.

Si osserva che per la forma normale sono necessari:
Entrambi i connettivi di congiunzione e disgiunzione
Entrambi gli operatori temporali Until e Release (uno il duale dell’altro)

Gli operatori \Diamond \mbox{ e } \Box sono invece derivabili.

Costruzione dell’automa di sincronizzazione: preliminari

Ogni formula di LTL può essere opportunamente riscritta in una formula equivalente che rispetta la forma normale utilizzando i seguenti schemi:

  • \neg(\phi_1 \vee \phi_2)\ \equiv\ \neg \phi_1 \wedge \neg \phi_2
  • \neg(\phi_1 \vee \phi_2)\ \equiv\ \neg \phi_1 \wedge \neg \phi_2
  • \neg \neg \phi\ \equiv\ \phi
  • \neg(\phi_1\ U\ \phi_2)\ \equiv\ \neg \phi_1\ R\ \neg \phi_2
  • \neg(\phi_1\ R\ \phi_2)\ \equiv\ \neg \phi_1\ U\ \neg \phi_2
  • \neg(\bigcirc\ \phi )\ \equiv\ \bigcirc\ \neg \phi

Per gli operatori derivati:

  • \phi_1\ \Longrightarrow\ \phi_2\ \equiv \ \neg \phi_1 \vee \phi_2
  • \Diamond\ \phi\ \equiv \ True\ U\ \phi
  • \Box\ \phi\ \equiv \ \neg (True\ U\ \neg \phi)\ \equiv False\ R\ \phi

Costruzione dell’automa di sincronizzazione: intuizione

Nella costruzione proposta i due passi elencati per la procedura di model checking:
Costruzione dell’automa per B_{\psi} con \psi la normalizzazione di \neg \phi
Costruzione dell’automa sincronizzato B_k \oplus B_{\psi}
Non verranno eseguiti in sequenza ma realizzati simultaneamente.

La costruzione proposta di seguito è quella dell’automa M=B_K \oplus B_{\psi}.

Idea della costruzione

Ogni stato s della struttura di Kripke K viene accoppiato con un insieme H di sottoformule di \psi garantendo che

Se (s,H) è uno stato di M, e \chi è una formula in H (sottoformula di \psi) deve esistere un cammino della struttura di Kripke K che parte da s e soddisfa \chi.

I simboli proposizionali in H devono essere compatibili con quelli associati allo stato s nella struttura di Kripke (cioè devono essere presenti in L(s)).
L’inserimento in H di una formula che coinvolge operatori temporali che parlano di stati futuri deve essere compatibile con l’etichettatura fatta da L di almeno un cammino che parta dallo stato s.

Costruzione dell’automa di sincronizzazione: preliminari

Data una formula \psi di LTL in forma normale si identifica con chiusura(\psi) l’insieme delle sottoformule di \psi.

Un sottoinsieme At \subseteq chiusura(\psi) si dice Atomo se rispetta dei vincoli di consistenza detti consistenza locale:

\begin{array}{lll}<br />
True \in At \\<br />
False \not\in At \\<br />
p\in AP, p\in At & \mbox{implica} & \neg p \not\in At \\<br />
p\in AP, \neg p\in At & \mbox{implica}& p \not\in At \\<br />
\phi_1\wedge\phi_2 \in At & \mbox{implica}& \phi_1,\phi_2\in At \\<br />
\phi_1\vee\phi_2 \in At & \mbox{implica}& \phi_1\in At \mbox{ o }\phi_2\in At\\<br />
\phi_1\ U\ \phi_2 \in At & \mbox{implica}& \phi_2\in At \mbox{ o }\phi_1\in At\\<br />
\phi_1\ R\ \phi_2 \in At & \mbox{implica}& \phi_2\in At<br />
\end{array}

L’insieme di atomi per una formula \psi \mbox{ e' indicato come } Atomi(\psi)

Un atomo è un insieme di sottoformule consistenti cioè che possono essere soddisfatte simultaneamente in un preciso istante temporale.
Un atomo è candidato ad essere associato ad uno stato s di K (se compatibile con L(s)).

Costruzione dell’automa di sincronizzazione: preliminari (segue)

I vincoli di consistenza locale riguardano solo la compatibilità (rispetto alla soddisfacibilità) di un insieme di formule relativamente ad un istante temporale (stato).

La presenza di operatori temporali che relazionano stati presenti con stati successivi impone di considerare regole di consistenza che devono essere rispettate quando due atomi At e At’ debbono essere associati a uno stato s e al suo successore s’.

Per due atomi At e At’ la relazione Succ(At,At’) vale se valgono i seguenti vincoli di consistenza di passo:

\begin{array}{lll}\bigcirc \phi \in At & \mbox{implica}& \phi \in At' \\<br />
\phi_1\ U\ \phi_2 \in At, \phi_2 \not\in At & \mbox{implica}& \phi_1\ U\ \phi_2 \in At'\\<br />
\phi_1\ R\ \phi_2 \in At, \phi_1 \not\in At & \mbox{implica}& \phi_1\ R\ \phi_2 \in At'<br />
\end{array}

Si osservi che i vincoli per Until e Release possono essere propagati al passo successivo nel rispetto delle seguenti equivalenze semantiche

\begin{array}{lll}\phi_1\ U\ \phi_2 & \equiv & \phi_2 \vee (\phi_1 \wedge \bigcirc (\phi_1\ U\ \phi_2 ))\\<br />
\phi_1\ R\ \phi_2 & \equiv & \phi_2 \wedge (\phi_1 \vee \bigcirc (\phi_1\ R\ \phi_2 ))<br />
\end{array}

Costruzione dell’automa di sincronizzazione

Sia una struttura di Kripke K=\langle S_0,S,\Delta, L \rangle \mbox { e } \chi una formula in forma normale, l’automa di sincronizzazione è un automa di Buchi generalizzato

B_K \oplus B_{\chi} = \langle Q,\Sigma,Q_0,\delta,\overline{F}\rangle

Q \subseteq S \times Atomi(\chi) con il vincolo,
(s,At) \in Q \mbox{ implica, per ogni } p \in AP \cap At \mbox{ vale } p\in L(s), \mbox{ e, per ogni } \neg p \in At \mbox{ vale } p\not\in L(s)

Q_0 \subseteq S_0 \times Atomi(\chi) con il vincolo,
(s,At) \in Q_0 \mbox{ implica, } \chi \in At

\delta \subseteq Q \times \Sigma \times Q è il seguente insieme di transizioni
\{\langle (s,At),a, (s',At') \rangle : \langle s,a,s'  \rangle \in \Delta, Succ(At,At')\}

Automa di sincronizzazione: condizione accettazione

La condizione di accettazione \overline F=F_1,\ldots, F_k deve risolvere un potenziale problema legato al soddisfacimento delle sottoformule della forma \psi_i=\phi_{1,i}\ U\ \phi_{2,i} \mbox{ con } i\in \{1,..,k\} della
formula \chi.

La regola di propagazione tra gli atomi successori

\phi_1\ U\ \phi_2 \in At, \phi_2 \not\in At \mbox{ implica } \phi_1\ U\ \phi_2 \in At'\\

Potrebbe propagare indefinitamente il vincolo di soddisfacimento al successore senza che la formula \phi_2 venga mai soddisfatta nel futuro come richiesto dalla semantica.

L’insieme di accettazione F_i = \{(s,At) : \mbox{ o } \phi_{2,i}\in At<br /> \mbox{ o } \psi_i \not\in At \}
esclude la possibilità di propagazione indefinita dell’Until.

Si osservi che ogni insieme di accettazione è in corrispondenza con una occorrenza di una formula Until

Esempio di model checking

Per esemplificare la costruzione dell’automa di sincronizzazione si considera la struttura di kripke in figura.

La formula da verificare è \chi = \Box \Diamond r_1

La formula per cui trovare il controesempio è

\neg (\Box \Diamond r_1)

La sua equivalente normalizzata è

\psi=True\ U\ (False\ R\ \neg r_1)

Sia \psi = False\ R\ \neg r_1


Fig.2  Struttura di Kripke.

Fig.2 Struttura di Kripke.


Automa di sincronizzazione

Fig.3  Automa sincronizzazione.

Fig.3 Automa sincronizzazione.


Automa di sincronizzazione: commenti

Per semplicità sono presentati solo gli stati con atomi minimali. Non sono state considerati atomi con combinazioni irrilevanti di proposizioni al fine del problema.

Tutti gli stati dell’esempio non sono di accettazione: gli stati di accettazione hanno un atomo che o contiene \phi o non contiene \psi (proprietà mai soddisfatta).
Si osserva che anche tutti gli stati non riportati hanno atomi in cui contengono \psi e non contengono \phi

L’automa accetta il linguaggio vuoto e dunque non esiste controesempio alla proprietà \chi che vale per tutte le computazioni.

Quindi K \models \chi

Fig.3 Automa sincronizzazione

Fig.3  Automa sincronizzazione.

Fig.3 Automa sincronizzazione.


Automa di sincronizzazione: commenti (segue)

Negli atomi associati agli stati s_0,s_1,s_2 la presenza della proposizione r_2 impedisce di comprendere nell’atomo la formula \phi che implicherebbe per consistenza la presenza anche di \neg r_2

Negli atomi associati agli stati s_3,s_4 la consistenza a passo impedisce di comprendere nell’atomo la formula \phi che, se presente, dovrebbe essere propagata anche all’atomo dello stato \neg s_1

Fig.3 Automa sincronizzazione

Fig.3  Automa sincronizzazione.

Fig.3 Automa sincronizzazione.


  • 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