Model checking ( metodo )
Il model checking è un metodo di verifica di un sistema e di ragionamento logico. Si basa sull'analisi di tutti i modelli e di tutte le situazioni possibili, al fine di poter escludere quelle impossibili e quindi di concentrare l'attenzione su quelle attuabili. L'approccio model checking è utilizzato nei sistemi esperti e negli algoritmi di apprendimento e di ragionamento logico. Data una base di conoscenza ( KB ), composta da un sistema di regole ( formule o specifiche ), il metodo analizza tutti i vari modelli possibili ( stati del sistema ), eliminando quelli che non rispettano le regole di riferimento. Ad esempio, prendiamo in esame tre proposizioni logiche A, B e C, e una semplice regola di riferimento, in base al quale la proposizione A è vera se almeno una tra le proposizioni B o C è vera.
( B ∨ C ) ⇒ A
Il sistema formale è composto da 3 proposizioni atomiche (n=3) ognuna delle quali può assumere due stati ( b=2 ), lo stato vero ( T ) o falso ( F ). Le combinazioni del sistema sono bn ossia 23 stati ( 8 stati ). Da un punto di vista matematico il modello enumera tutte le possibili combinazioni dei valori alle variabili A, B e C.
Soltanto tre combinazioni x1, x2 e x3 soddisfano la regola ( B ∨ C ) ⇒ A. Tutte le altre possono essere eliminate poiché non rispettano le regole adottate dalla base di conoscenza. Nei modelli m(x1), m(x2) e m(x3) la proposizione A segue logicamente la formula ( B ∨ C ). Si tratta, pertanto, di una conseguenza logica. Nei modelli M(A) dalla base di conoscenza ( KB ) segue logicamente la proposizione logica A.
L'insieme delle combinazioni che rende vera la proposizione A può anche essere sinteticamente indicata con M(A). L'algoritmo model checking è molto semplice e può essere adottato quando le combinazioni da analizzare non sono molte e lo spazio dei modelli è finito e limitato. È invece un metodo poco efficiente quando lo spazio dei modelli è infinito ( n=∞ ) oppure è molto grande.
Complessità temporale. La complessità temporale del metodo model checking aumenta in modo esponenziale alle combinazioni da affrontare: O (bn). Ad esempio, ipotizzando che ogni combinazione richiede 1 secondo di elaborazione del processore, per analizzare due stati "vero" o "falso" ( b=2 ) e tre proposizioni logiche ( n=3 ) l'algoritmo deve analizzare 8 combinazioni ( 23 ) e, pertanto, impiega 8 secondi di elaborazione. Per analizzare una quarta proposizione aggiuntiva ( n=4 ) l'algoritmo deve analizzare 16 combinazioni ( 24 ) raddoppiando il tempo di esecuzione ( 16 secondi ) necessario. Per analizzare una quinta proposizione ( n=5 ) deve analizzare 32 combinazioni ( 25 ) e così via.
La complessità dell'algoritmo cresce in modo esponenziale. Il fenomeno è conosciuto come problema dell'esplosione combinatoria. In conclusione, nel model checking il tempo di esecuzione t dell'algoritmo ( complessità temporale ) cresce in modo esponenziale rispetto alla dimensione dei dati ( n ). È quindi un metodo di analisi inefficiente e poco adatto al ragionamento logico.
Complessità spaziale. La complessità spaziale del metodo model checking aumenta in modo lineare rispetto alle combinazioni da analizzare. L'algoritmo analizza una combinazione alla volta. Dopo aver analizzato una combinazione, l'algoritmo può svuotare la memoria temporanea, già utilizzata, e reimpiegarla per analizzare la combinazione successiva. La capacità di elaborazione e la memoria necessaria per analizzare una singola combinazione è pertanto pari a O(n). Ad esempio, per analizzare le tre proposizioni (n=3) la complessità spaziale è 3. Per analizzare una quarta proposizione aggiuntiva (n=4) la complessità spaziale è pari a 4, per una quinta proposizione (n=5) sarebbe pari a 5, e così via. In conclusione, in un algoritmo model checking la complessità spaziale ( memoria ) cresce in modo lineare rispetto alla dimensione del problema.
