Interpolazione nelle varie logiche

La costruzione di interpolanti ha molte applicazioni nell’ambito del model checking. Per cominciare, spieghiamo innanzitutto cosa è il model checking. Uno degli obiettivi principali dell’ambito di verifica software è capire come un sistema/software lavora. Per fare ciò, vengono utilizzati dei modelli matematici che permettono di ragionare sul sistema di riferimento, chiamati metodi formali. Il model checking è una tecnica che permette di automatizzare tali ragionamenti, in particolare modella il sistema da analizzare utilizzando insiemi di stati e relazioni di transizioni con lo scopo di determinare come un sistema cambia nel tempo. L’obbiettivo del model checking è verificare se un dato sistema possiede determinate proprietà. Gli interpolanti possono essere usati per determinare un invariante induttivo per un sistema di transizione [...] dove C è l’insieme delle configurazioni possibili, I l’insieme delle configurazioni iniziali e * una relazione su C chiamata appunto relazione di transizione). Più specificamente, possiamo utilizzare l’interpolante trovato per costruire un “operatore astratto” che può essere iterato in un punto fisso per ottenere un invariante. Tale invariante contiene solo quelle informazioni dedotte rifiutando controesempi alla proprietà assegnata in un numero fissato di passi. Ciò evita la complessità di computare il più forte invariante induttivo (come è stato fatto di solito per il model checking) ed evita l’utilizzo di un’euristica per determinare le informazioni rilevanti (e non) all’interno dell’invariante trovato. L’utilizzo degli interpolanti permettono quindi un procedimento di astrazione dell’operatore che non solo riduce la complessità ma si concentra prevalentemente sulle informazioni utili per la proprietà assegnata, ignorando le informazioni non utili.
Questo approccio restituisce una procedura completa per il model checking dei sistemi a stati finiti e ci permette di sfruttare nuove ricerche per i risolutori SMT nella fase di proof generation.