The complexity of being monitorable

Resumo Técnico: A Complexidade de Ser Monitorável

Enunciado do Problema
A Verificação em Tempo de Execução (Runtime Verification - RV) baseia-se na síntese de monitores para determinar se as execuções de um sistema satisfazem ou violam uma especificação. Um desafio central é a monitorabilidade: a propriedade de que uma especificação permite a síntese de um monitor capaz de eventualmente alcançar um veredito (satisfação ou violação) com base em observações de execuções. Embora a monitorabilidade seja frequentemente estudada sintaticamente para linguagens de especificação específicas, Diekert e Leucker [DL14] propuseram uma abordagem semântica e topológica. Neste framework, os comportamentos do sistema são pontos em um espaço topológico $X$, e as observações são conjuntos abertos. Uma propriedade (um subconjunto $A \subseteq X$) é monitorável se, para cada observação aberta não vazia $U$, for possível refiná-la para um $V \subseteq U$ aberto e não vazio que esteja inteiramente contido em $A$ ou inteiramente em seu complemento.

O artigo aborda a complexidade da teoria dos conjuntos descritiva da família de conjuntos monitoráveis, denotada por $M(X)$, vista como um subconjunto do conjunto das partes $\mathcal{P}(X)$. Especificamente, os autores investigam o quão difícil é determinar se um subconjunto arbitrário de um espaço enumerável $X$ é monitorável. Eles analisam a posição de $M(X)$ na hierarquia de Borel e na hierarquia projetiva, dependendo das propriedades topológicas de $X$.

Metodologia
Os autores empregam ferramentas da teoria dos conjuntos descritiva [Kec95] e redutibilidade de Wadge.

1. Configuração Topológica: Eles identificam $\mathcal{P}(X)$ com o espaço de Cantor $2^X$ (via funções características) dotado da topologia do produto. Como $X$ é enumerável, $\mathcal{P}(X)$ é um espaço de Polish.
2. Caracterização da Monitorabilidade: Eles utilizam a caracterização de que um conjunto $A$ é monitorável se, e somente se, o interior de sua fronteira é vazio ($\text{Int}(\text{Fr}(A)) = \emptyset$). Isso é equivalente a dizer que $A$ não é simultaneamente denso e codenso em qualquer conjunto aberto não vazio.
3. Análise de Complexidade: Eles classificam $M(X)$ determinando se pertence a classes de pontos específicas ($\Sigma^0_\alpha, \Pi^0_\alpha, \Sigma^1_1, \Pi^1_1$) e se é completo para essas classes. Isso envolve a construção de reduções contínuas de conjuntos conhecidos como difíceis (ex: conjuntos completos para $\Sigma^0_3$ ou $\Pi^1_1$) para $M(X)$.
4. Distinção de Casos: A análise é dividida em dois casos primários:
   • Espaços de Segunda Contagem: Onde $X$ possui uma base enumerável.
   • Espaços Não de Segunda Contagem: Onde $X$ é enumerável, mas carece de uma base enumerável.

Principais Contribuições e Resultados

1. O Caso de Segunda Contagem
Para um espaço topológico enumerável e de segunda contagem $X$, a família $M(X)$ é sempre um subconjunto $\Pi^0_3$ de $\mathcal{P}(X)$. O artigo fornece uma classificação precisa das complexidades possíveis que $M(X)$ pode atingir:

• $\Delta^0_1$ (Clopen): Ocorre se $M(X) = \mathcal{P}(X)$, o que acontece se, e somente se, o conjunto de pontos isolados for denso em $X$.
• $\Sigma^0_2$-completo: Ocorre em espaços como a topologia cofinita em um conjunto enumerável.
• $\Pi^0_3$-completo: Ocorre em espaços como a topologia de Alexandrov em $\mathbb{N}^2$ com uma ordem parcial específica.
• Resultados de Impossibilidade: Os autores provam que, para espaços de segunda contagem, $M(X)$ não pode ser $\Sigma^0_1$-completo, $\Delta^0_2$-agudo (sharp) ou $\Pi^0_2$-completo.

Um critério operacional crucial é derivado (Observação 3.15): $M(X)$ é $\Pi^0_3$-completo se, e somente se, após remover a união de todos os conjuntos abertos mínimos não vazios, o interior restante contiver infinitos subconjuntos abertos disjuntos entre si. Caso contrário, $M(X)$ é $\Sigma^0_2$.

2. Aplicação a Relações de Transição
Os autores aplicam esses resultados a topologias induzidas por relações de transição em um conjunto enumerável de estados (modelando sistemas de tempo de ramificação/branching-time). Eles definem $R_0$ como o conjunto de relações de transição que induzem uma família de conjuntos monitoráveis $\Sigma^0_2$, e $R_1$ como aquelas que induzem uma família $\Pi^0_3$-completa.

• Teorema 3.18: Tanto $R_0$ quanto $R_1$ são subconjuntos de Borel no espaço de todas as relações de transição. Além disso, $R_0$ é comensurável (residual), significando que "a maioria" das relações de transição (no sentido da categoria de Baire) induz uma família de conjuntos monitoráveis topologicamente simples ($\Sigma^0_2$).

3. O Caso Não de Segunda Contagem
O artigo demonstra que a restrição a espaços de segunda contagem é essencial.

• Exemplo: Os autores constroem um espaço enumerável, não de segunda contagem (baseado na topologia de Scott para sequências finitas com um elemento $\infty$).
• Resultado: Para este espaço, a família de conjuntos monitoráveis $M(X)$ é $\Pi^1_1$-completa (completa coanalítica). Isso representa um salto significativo de complexidade em comparação ao caso de segunda contagem, mostrando que, sem a segunda contagem, o problema de determinar a monitorabilidade pode ser tão difícil quanto o problema da bem-fundação de árvores.

Significância
O artigo fornece um framework unificado e independente de sintaxe para compreender a monitorabilidade. Ao mapear o problema para a teoria dos conjuntos descritiva, estabelece que:

1. No cenário padrão de espaços de segunda contagem (que inclui muitos modelos de verificação em tempo de execução), a complexidade de determinar a monitorabilidade é limitada dentro da hierarquia de Borel, especificamente no nível $\Pi^0_3$.
2. Existe um critério estrutural claro (relacionado a conjuntos abertos mínimos e disjunção) que determina se um modelo de sistema específico gera um problema de monitorabilidade "simples" ($\Sigma^0_2$) ou "complexo" ($\Pi^0_3$-completo).
3. A suposição de segunda contagem é crítica; relaxá-la permite uma complexidade arbitrariamente alta (até $\Pi^1_1$-completa), destacando a importância das restrições topológicas na análise teórica da verificação em tempo de execução.

O trabalho não propõe novos algoritmos para a síntese de monitores, mas sim delineia os limites teóricos e as propriedades estruturais do problema de decisão da monitorabilidade através de diferentes modelos topológicos.