Home

Federica EU

1/17

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} \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} \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.

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\ \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} True \in At \\ False \not\in At \\ p\in AP, p\in At & \mbox{implica} & \neg p \not\in At \\ p\in AP, \neg p\in At & \mbox{implica}& p \not\in At \\ \phi_1\wedge\phi_2 \in At & \mbox{implica}& \phi_1,\phi_2\in At \\ \phi_1\vee\phi_2 \in At & \mbox{implica}& \phi_1\in At \mbox{ o }\phi_2\in At\\ \phi_1\ U\ \phi_2 \in At & \mbox{implica}& \phi_2\in At \mbox{ o }\phi_1\in At\\ \phi_1\ R\ \phi_2 \in At & \mbox{implica}& \phi_2\in At \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' \\ \phi_1\ U\ \phi_2 \in At, \phi_2 \not\in At & \mbox{implica}& \phi_1\ U\ \phi_2 \in At'\\ \phi_1\ R\ \phi_2 \in At, \phi_1 \not\in At & \mbox{implica}& \phi_1\ R\ \phi_2 \in At' \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 ))\\ \phi_1\ R\ \phi_2 & \equiv & \phi_2 \wedge (\phi_1 \vee \bigcirc (\phi_1\ R\ \phi_2 )) \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 \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.

Automa di 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.

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$