Visualising CTL Witnesses and Counterexamples -- Extended Version

1. Problema e Motivação

O artigo aborda uma lacuna fundamental na verificação de modelos (model checking) de lógicas temporais, especificamente na comparação entre LTL (Linear Temporal Logic) e CTL (Computation Tree Logic).

• O Contexto: Em LTL, a noção de contraexemplo é intuitiva e fácil de visualizar: trata-se de uma única trilha (trace) que viola a propriedade. Isso facilita a compreensão humana de por que um sistema falha.
• A Dificuldade no CTL: O CTL é uma lógica de "tempo ramificado" (branching time). A não satisfação de uma propriedade CTL não pode ser explicada apenas por uma única trilha, pois a estrutura de ramificação do modelo é essencial. Além disso, no CTL, a não satisfação de uma propriedade $\phi$ é equivalente à satisfação de sua negação $\neg\phi$. Portanto, focar apenas em "contraexemplos" para propriedades violadas é limitado; é necessário considerar tanto testemunhas (witnesses) para propriedades satisfeitas quanto contraexemplos para propriedades violadas.
• O Desafio: Como definir uma noção unificada de "evidência" (evidence) que capture a razão precisa para a satisfação ou violação de uma fórmula CTL arbitrária, e como visualizar essa evidência de forma que seja compreensível para humanos, especialmente em modelos complexos?

2. Metodologia

O autor propõe uma abordagem formal baseada em submodelos e estados fechados (closed states) para caracterizar a evidência mínima.

• Definição de Modelo e Evidência:

  • O trabalho utiliza modelos baseados em grafos dirigidos com estados rotulados por fórmulas.
  • Introduz-se o conceito de estados fechados ($C \subseteq S$). Um estado é "fechado" se todas as suas transições de saída no modelo original estão presentes no submodelo de evidência. Isso é crucial para representar a ausência de caminhos (informação negativa) sem precisar enumerar todos os caminhos inexistentes.
  • Evidência: Um submodelo $M'$ é evidência para uma afirmação $(s, \phi, b)$ se, para qualquer supermodelo sonoro $N$ que contenha $M'$, a afirmação permanece verdadeira. Se $b=1$, é uma testemunha; se $b=0$, é um contraexemplo.

• Caracterização Sintática e Semântica:

  • O artigo define condições sintáticas ($wts$ para testemunhas e $ctr$ para contraexemplos) que garantem que um modelo é uma evidência.
  • Para fórmulas cujos subcomponentes não são "constrangidos" (unconstrained), essas condições são necessárias e suficientes.
  • São definidas condições para evidência mínima ($minwts$e$minctr$), que buscam o menor submodelo (em relação à ordem de submodelo $\sqsubseteq$) que ainda serve como evidência.

• Visualização e Prova:

  • Uma prova é definida como um conjunto de evidências para todas as afirmações compostas de um modelo.
  • Para melhorar a compreensão, são introduzidos conceitos de evidência natural (que inclui a satisfação de todos os filhos em estados não terminais, evitando ambiguidades) e evidência combinada (que funde as evidências de todas as estados para uma única fórmula em um único modelo).
  • A visualização é baseada em Árvore de Sintaxe Abstrata (AST) sobreposta ao modelo de estados, usando codificação de cores (verde para verdadeiro, vermelho para falso, cinza para indefinido) e padrões de hachura para estados fechados.

3. Principais Contribuições

1. Modelo Formal de Evidência: A definição formal de evidência que unifica testemunhas e contraexemplos no contexto do CTL, utilizando a noção de estados fechados para capturar a estrutura de ramificação necessária.
2. Caracterização de Evidência Mínima: A identificação das condições exatas para a evidência mínima para cada operador temporal do CTL ($EX$, $EU$, $EG$, e seus negados). O artigo prova que, para fórmulas não constrangidas, essas condições são necessárias e suficientes.
3. Conceitos de "Evidência Natural" e "Evidência Combinada":
   • Evidência Natural: Resolve o problema de que a evidência estritamente mínima pode ser contra-intuitiva para humanos (ex: omitir informações locais óbvias). A evidência natural preenche essas lacunas para maior clareza.
   • Evidência Combinada: Demonstra que é possível consolidar as evidências de todos os estados de um modelo para uma única fórmula em um único modelo combinado, reduzindo a fragmentação visual.
4. Implementação e Visualização: Desenvolvimento de um demonstrador interativo que gera e visualiza essas evidências, permitindo ao usuário selecionar pares (estado, subfórmula) para inspecionar a prova local.

4. Resultados

• Teoremas de Minimalidade: O artigo estabelece teoremas (como o Teorema 14 e o Corolário 15) que provam que as condições definidas nas tabelas do artigo caracterizam exatamente os mínimos da ordem de submodelo para testemunhas e contraexemplos.
• Análise de Exemplos: O uso de um exemplo de jogo simples (um tabuleiro com estados de vitória, derrota e lançamento de dados) ilustra como a evidência mínima para fórmulas como $E \neg d1 \ U \ win$ (existe um caminho para ganhar sem lançar 1) é construída. A visualização mostra claramente quais estados são fechados e quais caminhos são bloqueados.
• Validação Prática: A ferramenta demonstrada consegue gerar provas completas e visualizações combinadas, mostrando que a abordagem é viável na prática e superior a abordagens puramente baseadas em trilhas lineares para o CTL.

5. Significado e Impacto

• Compreensão Humana: O trabalho avança significativamente na área de "diagnóstico de verificação de modelos". Ao fornecer uma visualização estruturada e minimalista (mas natural) de por que uma propriedade é verdadeira ou falsa em um sistema ramificado, torna o processo de depuração de sistemas complexos mais acessível.
• Generalização do Conceito de Contraexemplo: Ao tratar testemunhas e contraexemplos como duas faces da mesma moeda (evidência), o artigo oferece uma estrutura teórica mais robusta para lógicas de tempo ramificado, superando a limitação de apenas buscar trilhas de falha.
• Uso de Estados Fechados: A introdução de estados fechados como mecanismo para representar a ausência de transições é uma inovação técnica que permite representar a negação de propriedades existenciais de forma compacta e precisa, algo que seria difícil apenas com grafos de estados abertos.
• Futuro: O trabalho abre caminho para a aplicação dessas técnicas em lógicas mais expressivas (como CTL*) e para o refinamento de relações de simulação que levem em conta a estrutura de fechamento dos estados.

Em resumo, o artigo fornece a base teórica e prática para transformar resultados booleanos de verificação de modelos CTL em explicações visuais ricas e compreensíveis, preenchendo a lacuna entre a complexidade computacional da lógica e a necessidade humana de intuição sobre o comportamento do sistema.