Resumo Técnico: Análise de Robustez Neurosimbólica para Sistemas Discretos com Respecto a Desvios de Transição

Declaração do Problema

No controle supervisório de sistemas de eventos discretos (DES), controladores são sintetizados para impor especificações em um modelo de planta. Embora os métodos clássicos forneçam garantias de "corretude por construção", essas garantias dependem estritamente da precisão do modelo da planta. Na prática, desalinhamentos decorrentes de dinâmicas não modeladas, ruído de sensores ou erros de abstração fazem com que o sistema real desvie de seu modelo nominal, podendo comprometer a segurança.

Trabalhos recentes abordaram isso definindo a robustez discreta como o conjunto de todos os possíveis desvios de transição (transições adicionais adicionadas à planta nominal) contra os quais um supervisor mantém a segurança. No entanto, essa abordagem baseada em transições enfrenta duas limitações críticas:

1. Escalabilidade: O espaço de possíveis desvios cresce exponencialmente com os espaços de estados e ações, tornando a enumeração exaustiva computacionalmente intratável para todos, exceto os sistemas menores.
2. Conservadorismo: A grande maioria dos desvios matematicamente possíveis é fisicamente inviável (por exemplo, uma máquina gerando espontaneamente uma peça sem entrada). Incluir esses desvios inviáveis infla o espaço de busca e produz resultados de robustez que não refletem fielmente o comportamento do mundo real.

Tentativas existentes para filtrar desvios inviáveis usando restrições formais do sistema ($P_{sys}$) exigem que especialistas do domínio codifiquem manualmente leis físicas em especificações formais, criando uma carga significativa e adicionando sobrecarga ao pipeline de análise.

Metodologia

O artigo propõe um framework de computação neurosimbólica para abordar esses desafios de escalabilidade e viabilidade. A abordagem desacopla o raciocínio sobre a viabilidade física da computação formal das garantias de robustez, utilizando um processo de dois estágios:

1. Filtragem de Viabilidade Neural (Camada de LLM)

O primeiro estágio utiliza Grandes Modelos de Linguagem (LLMs) para inferir um subconjunto de transições de desvio fisicamente viáveis ($D$).

• Entrada: O framework ingere modelos LTS formais da planta e do supervisor, descrições em linguagem natural de estados e eventos do sistema, especificações de segurança e conhecimento de domínio referente a leis físicas (ex: "uma peça não pode estar em dois lugares ao mesmo tempo").
• Processo: Um template de prompt estruturado guia o LLM para raciocinar sobre essas entradas. O LLM é incumbido de identificar transições que representem falhas ou desvios realistas consistentes com a semântica do sistema e as restrições físicas.
• Saída: Um conjunto reduzido de desvios viáveis $D \subseteq (Q_E \times Act_E \times Q_E) \setminus R_E$, significativamente menor que o espaço de transição completo.

2. Verificação de Robustez Simbólica (Camada Simbólica)

O segundo estágio realiza a verificação formal no conjunto reduzido $D$.

• Processo: Um algoritmo de força bruta (Algoritmo 1) itera através de todos os subconjuntos dos desvios viáveis $D$. Para cada conjunto de desvio candidato $d$, ele utiliza model checking padrão para verificar se o sistema desviado $E_d$ controlado pelo supervisor $S$ satisfaz a propriedade de segurança $P$ (ou seja, $E_d/S \models P$).
• Refinamento: O algoritmo extrai apenas os desvios de robustez maximais (aqueles não contidos dentro de outros desvios robustos) para formar o conjunto de robustez final $\Delta_f$.
• Garantia: Como a verificação é realizada simbolicamente em um sistema de transição formalmente definido, as garantias de robustez resultantes permanecem matematicamente corretas em relação ao conjunto $D$ inferido.

Principais Contribuições

O artigo delineia duas contribuições primárias:

1. Um Framework Neurosimbólico: Uma arquitetura inovadora que combina LLMs para inferir modelos de desvio fisicamente viáveis com métodos simbólicos para computar garantias de robustez. Esta abordagem automatiza a extração de restrições físicas a partir de linguagem natural e conhecimento de domínio, removendo a necessidade de codificação formal manual de $P_{sys}$.
2. Protótipo e Avaliação: A implementação de uma ferramenta protótipo e sua avaliação experimental em três estudos de caso distintos: um sistema de manufatura, a interface de terapia de radiação Therac-25 e o Protocolo de Bit Alternado (ABP).

Resultados Experimentais

O framework foi avaliado em três estudos de caso utilizando LLMs (GPT-5.2 e Claude 3.5 Sonnet) para filtragem de viabilidade e um verificador simbólico baseado em Python.

• Sistema de Manufatura: O LLM identificou 18 desvios viáveis (de um espaço teórico de 108). A camada simbólica encontrou um conjunto de desvio robusto maximal, confirmando que o sistema é robusto contra 15 transições específicas, mas vulnerável a falhas específicas de descarga de buffer.
• Therac-25: A análise identificou 9 desvios viáveis. O sistema mostrou-se robusto contra pressões repetidas de "enter" pelo operador, mas vulnerável à condição de corrida específica envolvendo a seleção da terapia de elétrons, capturando com precisão a falha de design histórica.
• Protocolo ABP: O LLM identificou 16 desvios viáveis. A análise confirmou a robustez contra perda, duplicação e corrupção de mensagens, alinhando-se com a intenção de design do protocolo.

Achados Quantitativos:

• Redução de Viabilidade: Os LLMs reduziram significativamente o espaço de busca. A redução variou de 67% (Therac-25) a 99% (ABP) em comparação com o espaço de transição total.
• Precisão de Viabilidade: Para o exemplo de manufatura, 89% das transições geradas pelo GPT eram fisicamente viáveis, comparado a 54% para o Claude. Em sistemas mais complexos como o ABP, as taxas de viabilidade caíram para ambos os modelos (63% e 36%, respectivamente), indicando a necessidade de melhoria na engenharia de prompt ou ontologias de domínio.
• Equivalência de Robustez: Apesar de operar em um conjunto reduzido de desvios, o framework produziu garantias de robustez comparáveis às obtidas através da análise baseada em transição total nos casos avaliados.

Significância e Alegações

O artigo alega que este abordagem neurosimbólica aborda com sucesso o equilíbrio entre escalabilidade e a inclusão de desvios inviáveis na análise de robustez discreta. Ao utilizar LLMs para filtrar o espaço de soluções com base no entendimento semântico e físico, o método torna a análise de robustez tratável para sistemas onde a enumeração exaustiva é impossível.

Os autores enfatizam que, embora o componente de LLM introduza um elemento probabilístico na identificação de desvios viáveis, a subsequente verificação simbólica garante que as garantias de robustez finais sejam formalmente corretas em relação ao conjunto $D$ inferido. O trabalho demonstra que é possível recuperar análises de robustez comparáveis aos métodos de espaço total operando em um subconjunto de desvios drasticamente menor e fisicamente significativo.

O artigo conclui modestamente, observando que a implementação atual do algoritmo de força bruta requer otimização para sistemas maiores e que trabalhos futuros focarão em melhorar a engenharia de prompt, incorporar ontologias de domínio para aumentar a precisão do LLM e investigar loops de refinamento interativo onde resultados simbólicos guiam consultas de LLM.