Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity

Sintesi Tecnica: Model Checking Spaziale di Immagini tramite Modelli Minimi e Bisimilarità di Branching

Problematica
Il model checking spaziale consiste nella verifica automatica di proprietà espresse in logiche spaziali (specificamente la Logica Spaziale per gli Spazi di Chiusura, SLCS) su ogni punto di un modello spaziale. Sebbene strumenti come VoxLogicA abbiano applicato con successo questi metodi a immagini digitali (rappresentate come modelli di chiusura quasi-discreti, QdCM), le dimensioni enormi delle moderne immagini mediche e digitali — che spesso contengono milioni di pixel o voxel — pongono sfide significative in termini di efficienza temporale e di spazio. Il model checking diretto su tali modelli estesi può essere computazionalmente costoso. Il presente articolo affronta la necessità di procedure efficaci di minimizzazione del modello che riducano le dimensioni del modello senza perdere la capacità di verificare le proprietà spaziali, accelerando così il processo di verifica.

Metodologia
La metodologia proposta si basa su una codifica teorica di Modelli di Chiusura (CM) finiti in Sistemi di Transizione Etichettati (LTS) per sfruttare gli algoritmi di minimizzazione esistenti e altamente efficienti per la bisimilarità di branching.

1. Fondamento Teorico (CoPa-Bisimilarità): Il lavoro si basa sulla bisimilarità "Compatible Paths" (CoPa), una relazione di bisimilarità spaziale per i QdCM. A differenza delle bisimilarità precedenti che si basano strettamente sulla raggiungibilità a un passo (appartenenza alla chiusura), la CoPa-bisimilarità si basa sulla compatibilità dei percorsi. Due percorsi sono compatibili se possono essere decomposti nella stessa quantità di "zone" (sequenze di punti) tali che i punti nelle zone corrispondenti siano correlati dalla bisimilarità. Questa relazione è caratterizzata logicamente dalla Logica di Raggiungibilità Compatibile Infinitaria (ICRL), che presenta modalità di raggiungibilità condizionale diretta ($\vec{\zeta}$) e inversa ($\overleftarrow{\zeta}$).
2. Codifica in LTS: Il contributo tecnico centrale è una codifica di un QdCM finito $M = (X, C, V)$ in un LTS.
   • Per i QdCM generali (non simmetrici), ogni punto $x$ è mappato in due stati nell'LTS: uno stato diretto $\vec{x}$ e uno stato inverso $\overleftarrow{x}$. Le transizioni includono auto-anelli per le proposizioni atomiche, transizioni $\tau$ per punti con valutazioni identiche raggiungibili nella chiusura, transizioni $ch$ per punti con valutazioni differenti, e transizioni specifiche $cv$ (converse) e $dr$ (direct) che collegano gli stati diretti e inversi.
   • Per i QdCM simmetrici (tipici delle immagini digitali con adiacenza a 8), viene utilizzata una codifica più compatta in cui ogni punto mappa un singolo stato, con transizioni $\tau$ e $ch$ che rappresentano le relazioni di chiusura.
3. Correttezza: L'articolo dimostra che la CoPa-bisimilarità nel QdCM originale coincide esattamente con la bisimilarità di branching nell'LTS codificato. Di conseguenza, il modello minimo rispetto alla CoPa-bisimilarità può essere calcolato minimizzando l'LTS codificato utilizzando algoritmi di bisimilarità di branching.
4. Toolchain (VoxMinX): È stata sviluppata una toolchain prototipo, VoxMinX, per validare questo approccio. Essa esegue i seguenti passaggi:
   • Converte un'immagine digitale in un QdCM e poi in un LTS.
   • Minimizza l'LTS utilizzando il minimizzatore di bisimilarità di branching del toolset $mCRL2$.
   • Trasforma l'LTS minimo nuovamente in un QdCM minimo.
   • Esegue il model checking spaziale sul modello minimo utilizzando GraphLogicA.
   • Proietta i risultati sull'immagine originale, preservando la relazione tra le classi di equivalenza e gli insiemi originali di pixel.

Contributi Chiave

• Codifica Teorica: L'articolo introduce una codifica formale di modelli di chiusura finiti in LTS che preserva la CoPa-bisimilarità tramite la bisimilarità di branching. Ciò consente l'applicazione di tecniche efficienti di riduzione dello spazio degli stati dalla algebra dei processi al model checking spaziale.
• Dimostrazioni di Correttezza: Sono fornite dimostrazioni dettagliate, inclusa una nuova induzione basata sulla "profondità" degli stati in un LTS, dimostrando che la codifica riflette correttamente la Coppa-bisimilarità.
• Implementazione Pratica: Lo sviluppo di VoxMinX, una toolchain che integra elaborazione di immagini, codifica LTS, minimizzazione e proiezione dei risultati.
• Validazione Sperimentale: L'approccio è valutato su tre famiglie di immagini benchmark (labirinti, pattern monoscopio e scene di Pac-Man) a varie risoluzioni, confrontando le prestazioni con lo stato dell'arte, il checker non minimizzato VoxLogicA.

Risultati
I risultati sperimentali indicano un significativo incremento della velocità nel model checking quando si utilizzano i modelli minimizzati, particolarmente per le immagini più grandi:

• Immagini Labirinto: Gli incrementi di velocità sono variati da circa 3.3x per immagini piccole (128x128) a oltre 17x per immagini grandi (8192x8192). La dimensione del modello minimo è rimasta costante (7 stati) indipendentemente dalla risoluzione di input, poiché la struttura spaziale era identica.
• Immagini Monoscopio: Per immagini con proprietà di raggiungibilità annidate complesse, gli incrementi di velocità hanno superato le 25x per la risoluzione più grande (4320p). La dimensione del modello minimo variava con la risoluzione a causa della perdita di dettagli fini durante il downscaling.
• Immagini Pac-Man: È stato osservato un incremento di velocità di circa 3x fino a 7x. Il modello minimo conteneva costantemente 35 stati attraverso tutte le risoluzioni.
• Overhead: L'articolo nota che, sebbene i passaggi di minimizzazione e codifica introducano un overhead (tempi di I/O e conversione), la riduzione del tempo di model checking sul modello minimo (usando GraphLogicA) supera questo costo per le immagini più grandi. Gli autori riconoscono che VoxLogicA è altamente ottimizzato per le immagini, mentre GraphLogicA è un checker di grafi generale; pertanto, i miglioramenti riportati sono stime conservative.

Significatività e Rivendicazioni
L'articolo sostiene che il metodo proposto offre un "promettente incremento di velocità" per il model checking spaziale di immagini di dimensioni realistiche. La significatività risiede nel dimostrare che la minimizzazione della bisimilarità spaziale è una strategia valida per gestire dati spaziali su larga scala, come le immagini mediche (ad esempio, scansioni MRI con milioni di voxel).

Gli autori sottolineano che l'approccio preserva la verità logica del modello originale, permettendo di visualizzare i risultati direttamente sull'immagine originale (ad esempio, evidenziando i pixel che soddisfano una proprietà). Sebbene l'attuale prototipo serva come studio di fattibilità, i risultati suggeriscono che l'integrazione dei componenti della toolchain potrebbe produrre un'efficienza ancora maggiore. Il lavoro si pone come un passo verso la rendere il model checking spaziale più pratico per applicazioni del mondo reale, specialmente nell'imaging medico dove i dataset comuni sono di grandi dimensioni. Gli autori inquadrano modestamente il lavoro come una base per la ricerca futura, notando che la tecnica di minimizzazione potrebbe anche servire come forma di compressione lossless per le proprietà spaziali.