Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity

Resumo Técnico: Verificação de Modelos Espaciais de Imagens via Modelos Minimizados e Bisimilaridade de Ramificação

Definição do Problema
A verificação de modelos espaciais envolve a verificação automática de propriedades expressas em lógicas espaciais (especificamente, a Lógica Espacial para Espaços de Fechamento, SLCS) em cada ponto de um modelo espacial. Embora ferramentas como o VoxLogicA tenham aplicado com sucesso esses métodos a imagens digitais (representadas como modelos de fechamento quase-discretos, QdCMs), o tamanho colossal das imagens médicas e digitais modernas — que frequentemente contêm milhões de pixels ou voxels — impõe desafios significativos de eficiência de tempo e espaço. A verificação direta de modelos em modelos tão grandes pode ser computacionalmente dispendiosa. O artigo aborda a necessidade de procedimentos eficazes de minimização de modelos que reduzam o tamanho do modelo sem perder a capacidade de verificar propriedades espaciais, acelerando assim o processo de verificação.

Metodologia
A metodologia proposta baseia-se em uma codificação teórica de Modelos de Fechamento (CMs) finitos em Sistemas de Transição de Estados Rotulados (LTSs) para aproveitar algoritmos de minimização existentes e altamente eficientes para bisimilaridade de ramificação.

1. Fundamentação Teórica (CoPa-Bisimilaridade): O trabalho baseia-se na bisimilaridade de "Caminhos Compatíveis" (CoPa), uma relação de bisimilaridade espacial para QdCMs. Diferente de bisimilaridades anteriores que dependem estritamente de alcançabilidade de um passo (pertencimento ao fechamento), a CoPa-bisimilaridade baseia-se na compatibilidade de caminhos. Dois caminhos são compatíveis se puderem ser decompostos no mesmo número de "zonas" (sequências de pontos) de tal forma que os pontos nas zonas correspondentes sejam relacionados pela bisimilaridade. Esta relação é caracterizada logicamente pela Lógica de Alcançabilidade Compatível Infinitária (ICRL), que apresenta modalidades de alcançabilidade condicional direta ($\vec{\zeta}$) e inversa ($\vec{\zeta}$).
2. Codificação para LTS: A principal contribuição técnica é uma codificação de um QdCM finito $M = (X, C, V)$ em um LTS.
   • Para QdCMs gerais (não simétricos), cada ponto $x$ é mapeado para dois estados no LTS: um estado direto $\vec{x}$ e um estado inverso $\vec{x}$. As transições incluem auto-loops para proposições atômicas, transições $\tau$ para pontos com avaliações idênticas alcançáveis dentro do fechamento, transições $ch$ para pontos com avaliações diferentes, e transições específicas $cv$ (conversa) e $dr$ (direta) ligando os estados direto e inverso.
   • Para QdCMs simétricos (típicos de imagens digitais com adjacência de 8), uma codificação mais compacta é utilizada, onde cada ponto mapeia para um único estado, com transições $\tau$ e $ch$ representando as relações de fechamento.
3. Corretude: O artigo prova que a CoPa-bisimilaridade no QdCM original coincide exatamente com a bisimilaridade de ramificação no LTS codificado. Consequentemente, o modelo minimal com relação à CoPa-bisimilaridade pode ser computado minimizando o LTS codificado usando algoritmos de bisimilaridade de ramificação.
4. Cadeia de Ferramentas (VoxMinX): Uma cadeia de ferramentas protótipo, VoxMinX, foi desenvolvida para validar esta abordagem. Ela realiza as seguintes etapas:
   • Converte uma imagem digital em um QdCM e, em seguida, em um LTS.
   • Minimiza o LTS usando o minimizador de bisimilaridade de ramificação do conjunto de ferramentas $mCRL2$.
   • Transforma o LTS minimal de volta em um QdCM minimal.
   • Executa a verificação de modelo espacial no modelo minimal usando o GraphLogicA.
   • Projeta os resultados de volta na imagem original, preservando a relação entre as classes de equivalência e os conjuntos originais de pixels.

Principais Contribuições

• Codificação Teórica: O artigo introduz uma codificação formal de modelos de fechamento finitos em LTSs que preserva a CoPa-bisimilaridade via bisimilaridade de ramificação. Isso permite a aplicação de técnicas eficientes de redução de espaço de estados da álgebra de processos para a verificação de modelos espaciais.
• Provas de Corretude: Provas detalhadas são fornecidas, incluindo uma indução inovadora baseada na "profundidade" dos estados em um LTS, demonstrando que a codificação reflete corretamente a Coapa-bisimilaridade.
• Implementação Prática: O desenvolvimento do VoxMinX, uma cadeia de ferramentas que integra processamento de imagem, codificação de LTS, minimização e projeção de resultados.
• Validação Experimental: A abordagem é avaliada em três famílias de imagens de referência (labirintos, padrões de monoscópio e cenas de Pac-Man) em várias resoluções, comparando o desempenho com o estado da arte, o verificador não minimizado VoxLogicA.

Resultos
Os resultados experimentais indicam uma aceleração significativa nos tempos de verificação de modelos quando se utilizam os modelos minimizados, particularmente para imagens maiores:

• Imagens de Labirinto: As acelerações variaram de aproximadamente 3,3x para imagens menores (128x128) a mais de 17x para imagens grandes (8192x8192). O tamanho do modelo minimal permaneceu constante (7 estados) independentemente da resolução de entrada, pois a estrutura espacial era idêntica.
• Imagens de Monoscópio: Para imagens com propriedades de alcançabilidade aninhadas complexas, as acelerações ultrapassaram 25x para a maior resolução (4320p). O tamanho do modelo minimal variou com a resolução devido à perda de detalhes finos durante a redução de escala.
• Imagens de Pac-Man: Observou-se uma aceleração de aproximadamente 3x a 7x. O modelo minimal continha consistentemente 35 estados em todas as resoluções.
• Sobrecarga (Overhead): O artigo observa que, embora as etapas de minimização e codificação introduzam sobrecarga (tempos de I/O e conversão), a redução no tempo de verificação do modelo (usando o GraphLogicA) compensa esse custo para imagens maiores. Os autores reconhecem que o VoxLogicA é altamente otimizado para imagens, enquanto o GraphLogicA é um verificador de grafos geral; portanto, as acelerações relatadas são estimativas conservadoras.

Significância e Alegações
O artigo afirma que o método proposto oferece uma "aceleração promissora" para a verificação de modelos espaciais de imagens de tamanho realista. A significância reside em demonstrar que a minimização de bisimilaridade espacial é uma estratégia viável para lidar com dados espaciais de grande escala, como imagens médicas (ex: exames de RM com milhões de voxels).

Os autores enfatizam que a abordagem preserva a verdade lógica do modelo original, permitindo que os resultados sejam visualizados diretamente na imagem original (ex: destacando pixels que satisfazem uma propriedade). Embora o protótipo atual sirva como um estudo de viabilidade, os resultados sugerem que a integração mais profunda dos componentes da cadeia de ferramentas poderia gerar ainda mais eficiência. O artigo posiciona este trabalho como um passo para tornar a verificação de modelos espaciais mais prática para aplicações do mundo real, particularmente em imagens médicas onde grandes conjuntos de dados são comuns. Os autores enquadram modestamente o trabalho como uma fundação para pesquisas futuras, observando que a técnica de minimização também pode servir como uma forma de compressão sem perdas para propriedades espaciais.