MVS - 07 - Restricted Computational Tree Logic
Lecture Info
Date:
In questa lezione abbiamo discusso del problema del formalismo logico introdotto nelle precedenti lezioni, e abbiamo poi discusso due particolari direzioni in cui estendere tale formalismo.
1 The Problem with CTL
La logica temporale è estremamente potente. La fregatura però sta nel fatto che la complessità computazionale nel verificare su un automa finito una proprietà di questa logica temporale diventa facilmente molto alta, in quanto possiamo combinare i vari operatori a nostro piacimento.
Questa complessità in particolare è P-space completa, ovvero lo spazio utilizzato è limitato da un polinomio rispetto al size iniziale. Dato che lo stato iniziale è fatto da tantissimi stati, già con un polinomio di quarto grado perdiamo ogni speranza di poter verificare in modo automatico le proprietà. Noi vorremmo invece un costo lineare rispetto al size.
Per cercare di eliminare questa complessità si introduce una restrizione della \(\text{CTL}^*\), che prende il nome di \(\text{CTL}\).
2 Restricted CTL
La CTL ristretta introduce la seguente restrizione: non è possibile avere un operatore temporale tipo \(X\), \(F\), \(G\), \(U\) se questo non è preceduto da un quantificatore esistenziale (\(E\)) o universale (\(A\)). Tale restrizione è quindi una restrizione principalmente di natura sintattico.
Nella CTL ristretta troviamo quindi i seguenti possibili operatori temporali:
\[\text{AX}, \text{AF}, \text{AG}, \text{AU}, \text{EX}, \text{EF}, \text{EG}, \text{EU}\]
Ricodiamo che per esprimere la fairness ad esempio possiamo utilizzare la seguente formula:
\[A G (R_a \implies F P_a)\]
Notiamo che tale formula non è ristretta. Per renderela ristretta abbiamo due possibili varianti:
\(A G (R_a \implies E F P_a)\)
\(A G (R_A \implies A F P_a)\)
Mentre la prima variante non esclude la possibilità di avere un cammino di starvation, e dunque non formalizza bene il concetto di fairness, la seconda invece esclude la possibilità di avere cammini di starvation, e dunque formalizza bene il concetto di fairness.
2.1 Example
Dall'esempio della fairness possiamo vedere come non sempre sia semplice trovare (se c'è) una formula ristretta equivalente ad una data. Andiamo adesso a vedere un esempio che non possiamo trasformare in una formula ristretta:
\[EGFP\]
questa formula è vera se e solo se esiste un cammino in cui infinite volte vale la proprietà P. Notiamo che tale formula non è ristretta, in quanto \(G\) è protetta da \(E\), ma \(F\) non è protetta da nessun quantificatore. Ricorando però che
\[\begin{split} F P &\equiv \neg G \neg P \\ A P &\equiv \neg E \neg P \\ \end{split}\]
osserviamo che una formula ristretta a quella precedentemente mostrata è la seguente
\[\neg A F \neg E F P \equiv E G E F P\]
2.2 The Locality of Restricted CTL
Nel passaggio da \(\text{CTL}^*\) a \(\text{CTL}\) ristretto anche se perdiamo di espressività guadagniamo una proprietà di località.
In particolare, se nella \(\text{CTL}^*\) per verificare una proprietà della forma \(\sigma, i \models \phi\) avevamo la dipendenza dal cammino \(\sigma\), nella CTL ristretta perdiamo la dipendenza dal cammino \(\sigma\), e possiamo verificare la proprietà guardando solo \(\sigma(i)\) e in modo ricorsivo i cammini che partono da \(\sigma(i)\).
3 Propositional Linear Temporal Logic (PLTL)
Un'altra restrizione che viene fatta è quella di linearizzare la logica temporale. La logica risultante è chiamata "Logica Temporale Lineare", o in inglese PLTL, che sta per "Propositional Linear Temporale Logic".
Questa restrizione consiste nel buttare via i quantificatori di cammino (\(A\)) ed (\(E\)). Al fine però di poter comunque impostare il problema di ricerca ci teniamo un solo quantificatore universale (\(A\) o \(E\)), che utilizzerò a partire dallo stato iniziale \(q_0\) dell'automa.
Ad esempio possiamo avere, a partire dallo stato iniziale \(q_0\):
\(EGFP\), o, equivalentemente, \(A\neg(G F P)\).
4 Summary so Far
La CTL è costruita con i seguenti elementi:
Proposizione atomiche (<=> Osservabili del sistema).
Operatori Booleani.
Operatori Temporali: X, F, G, U.
Quantificatori di cammino: E, A.
Se possiamo combinare tutti questi elementi come ci pare, il potere espressivo è enorme. In particolare si ritiene che CTL è in grado di esprimere tutte le proprietà di interesse in un problema di verifica. Ci sono dei teoremi che danno evidenza del potere espressivo della CTL.
Detto questo, la complessità di un possibile algoritmo di verifica è troppo alta. Infatti la complessità è P SPACE, nel senso che è polinomiale rispetto allo spazio dell'istanza. Notiamo che lo spazio dell'istanza è dato da
\[(\text{#Stati} + \text{#Transizioni}) \times (|\Phi|)\]
dove
il numero di transizioni è limitato dalla reachability analysis.
\(\Phi\) è la formula da verificare e \(|\Phi|\) è il numero di nodi dell'albero sintattico della formula.
Notiamo poi che siccome gli stati sono ingegnerizzati, abbiamo che il numero di transizioni non è troppo più grande del numero di nodi.
Abbiamo quindi introdotto le seguenti due restrizioni:
CTL ristretta, perdiamo qualche cosa ma non troppo (mi perdo F ).
PTLT (Propositional Linear Temporal Logic): Elimino i quantificatori di cammino A ed E (tranne un A per la verifica che tipicamente metto sullo stato iniziale).
Queste due restrizioni sono complementari tra loro.