Resumo Técnico: Um Guia Pragmático para a Construção de Abstrações Discretas Conservadoras de Sistemas Ciber-Físicos

Declaração do Problema

Sistemas ciber-físicos (CPS) operam em ambientes críticos de segurança onde falhas podem ameaçar vidas e propriedades. Embora a verificação de modelos simbólicos seja um método eficaz para verificar propriedades complexas de lógica temporal, ela requer um modelo de estados finitos. No entanto, os CPS do mundo real evoluem sobre espaços de estados contínuos. Para aplicar a verificação de modelos, engenheiros devem discretizar essas dinâmicas contínuas em uma abstração de estados finitos.

O desafio central reside em garantir a consistência (soundness): as garantias de verificação derivadas do modelo abstrato devem transferir-se para o sistema concreto. Isso exige que a abstração seja uma sobre-aproximação conservadora do espaço de estados e dos comportamentos concretos. Na prática, os construtores de modelos frequentemente encontram quatro armadilhas que comprometem a consistência ou introduzem pessimismo excessivo:

1. Subcobertura (Under-covering) do espaço de estados concreto.
2. Subaproximação da relação de transição (omissão de comportamentos viáveis).
3. Poda não consistente (unsound pruning) de comportamentos "degenerados" (ex: remoção de auto-loops sem certificação).
4. Elevação de especificação imprópria (improper specification lifting), falhando em preservar a implicação lógica da satisfação abstrata para a satisfação concreta.

Esses problemas frequentemente levam a contraexemplos "espúrios", onde o modelo abstrato viola uma especificação que o sistema concreto de fato satisfaz, tornando a verificação inútcia.

Metodologia

O artigo propõe um fluxo de trabalho modular de quatro etapas para construir abstrações discretas conservadoras. O fluxo de trabalho é "conservador por construção", o que significa que a consistência é mantida em cada etapa por meio de garantias matemáticas específicas.

Etapa 1: Abstração do Espaço de Estados

O espaço de estados contínuos $X$ é particionado em um conjunto finito de estados abstratos $\hat{X}$ usando uma grade retilínea uniforme. Uma função de quantização $\psi: X \to \hat{X}$ mapeia estados concretos para células abstratas. O mapeamento inverso $\Psi(\hat{x})$ define a região concreta (preimagem) de cada estado abstrato. Esta etapa garante que todo estado concreto e condição inicial tenha um representante no modelo abstrato.

Etapa 2: Construção de Transição Conservadora

O artigo apresenta três métodos intercambiáveis para computar a relação de transição $\hat{f}$ (ou seja, determinar quais estados abstratos podem seguir outros), garantindo que toda transição concreta seja representada no modelo abstrato:

• Caixa Delimitadora Alinhada aos Eixos (AABB - Axis-Aligned Bounding Box): Computa a caixa delimitadora da imagem de uma célula concreta sob a dinâmica do sistema. Qualquer célula abstrata que intercepte esta caixa é adicionada como sucessora. Este método é computacionalmente eficiente, mas pode ser excessivamente conservador para sistemas não lineares.
• Propagação de Polítopo: Utiliza um polítopo (invólucro convexo) para sobre-aproximar a imagem da célula concreta. É mais estrito que o AABB para dinâmicas não lineares, mas computacionalmente mais caro. Emprega o descarte por AABB para filtrar candidatos antes de realizar testes de interseção de polítopos mais custosos.
• Amostragem com Certificados PAC: Para sistemas de caixa-preta ou altamente não lineares, as transições são descobertas por amostragem do espaço de estados. Em vez de uma garantia determinística, este método fornece uma garantia Provavelmente Aproximadamente Correta (PAC - Probably Approximately Correct). Ele certifica que, com alta confiança ($1-\delta$), a relação de transição construída inclui todas as "transições significativas" (aquelas que ocorrem com probabilidade $\ge \beta$), limitando a "massa perdida" de transições não observadas.

Etapa 3: Mitigação de Comportamentos Degenerados

Abstrações conservadoras frequentemente introduzem transições espúrias (transições impossíveis no sistema concreto) e auto-loops (transições de um estado para si mesmo). Estes podem causar falsos negativos na verificação, particularmente para propriedades de vivacidade (liveness).

• Transições Espúrias: São tratadas via Refinamento de Abstração Guiado por Contraexemplo (CEGAR - Counterexample-Guided Abstraction Refinement). Se um trajeto de contraexemplo é encontrado no modelo abstrato, o algoritmo o valida contra a dinâmica concreta. Se o trajeto for espúrio (o conjunto alcançável torna-se vazio), o espaço de estados é refinado (dividido) para eliminar a falsa transição.
• Auto-loops: São tratados via Remoção de Auto-loop Certificada. Um auto-loop é removido apenas se puder ser certificado que todo trajeto concreto partindo daquela célula escapa dentro de um número finito de passos ($K$). Isso é verificado através da propagação do conjunto alcançável ou via uma estratégia de amostragem com uma garantia PAC.

Etapa 4: Elevação Consistente de Especificações LTL

Para verificar o modelo abstrato, a especificação LTL $\phi$ definida no espaço concreto deve ser elevada para uma especificação abstrata $\hat{\phi}$. O artigo emprega semântica de "pode" e "deve" (may-must semantics):

• Predicados "deve" (must): Uma proposição atômica é válida em um estado abstrato apenas se ela for válida para todos os estados concretos naquela célula.
• Predicados "pode" (may): Uma proposição atômica é válida se ela for válida para pelo menos um estado concreto.
  O operador de elevação $\rho$ transforma $\phi$ em $\hat{\phi}$ ao fortalecer proposições atômicas para "deve" (para segurança) ou enfraquecê-las para "pode" (conforme apropriado para a estrutura lógica), garantindo que $\hat{s} \models \hat{\phi} \implies s \models \phi$.

Principais Contribuições

1. Um Fluxo de Trabalho Pragmático: Um pipeline unificado de quatro etapas que integra partição de estado, construção de transição, mitigação de comportamento degenerado e elevação de especificação em um único framework consistente.
2. Sub-rotinas Intercambiáveis: A metodologia suporta múltiplas abordagens para construção de transição (AABB, Polítopo, Amostragem) e remoção de comportamento degenerado (CEGAR, Erasure Certificada), permitindo que os usuários equilibrem custo computacional com rigor da abstração.
3. Garantias PAC para Amostragem: Introduz uma abordagem baseada em dados para construção de transição que fornece certificados de cobertura probabilística rigorosos (via estimador Good-Turing e limites de McAllester-Schapire) para sistemas onde a sobre-aproximação analítica é intratável.
4. Tratamento Sistemático de Degenerescência: Aborda explicitamente a remoção de auto-loops e transições espúrias através de apagamento certificado e CEGAR, prevenindo o pessimismo que tipicamente afeta as abstrações conservadoras.

Resultados Experimentais

Os autores avaliaram o pipeline em três estudos de caso: um sistema linear sintético, o benchmark Mountain Car (não linear, política aprendida) e um Uniciclo Autônomo (modelo de Dubins).

• Construção de Transição: Métodos baseados em amostragem geralmente produziram relações de transição mais esparsas, com menos auto-loops e menor variabilidade na contagem de sucessores em comparação aos métodos AABB e Polítopo, particularmente para sistemas não lineares. Isso levou a Taxas de Verdadeiros Positivos (TPR) mais altas na verificação.
• Erasure de Auto-loops: A remoção de auto-loops melhorou significativamente os resultados de verificação. Para o caso do Uniciclo, a TPR aumentou de ~0,19 para ~0,63 após a remoção. No caso do Mountain Car, a TPR melhorou de ~0,83 para ~0,93.
• CEGAR: Embora o CEGAR tenha aumentado substancialmente o tamanho do modelo e o tempo de construção, ele consistentemente reduziu a proporção de auto-loops (SLP). Ele produziu melhorias pronunciadas de TPR para o sistema Mountain Car, mas teve impacto mínimo no Uniciclo, onde uma alta SLP foi atribuída a contraexemplos triviais difíceis de eliminar sem erasure direcionada.
• Granularidade: Granularidades mais finas do espaço de estados consistentemente produziram TPRs mais altas, confirmando o compromisso entre o tamanho do modelo e a precisão da verificação.

Significância

O artigo afirma sua importância como um guia pragmático para engenheiros e pesquisadores que constroem abstrações para CPS. Ele aborda a lacuna entre técnicas de abstração teórica e implementação prática ao:

• Oferecer um fluxo de trabalho consistente por construção que evita erros comuns que levam à verificação inconsistente.
• Oferecer ferramentas modulares que permitem aos praticantes escolher entre métodos determinísticos (AABB/Polítopo) e probabilísticos (Amostragem) com base na complexidade do sistema e nos recursos computacionais disponíveis.
• Demonstrar que a mitigação de comportamentos degenerados (transições espúrias e auto-loops) não é meramente uma otimização, mas um passo crítico para alcançar resultados de verificação significativos, particularmente para propriedades de vivacidade.

Os autores concluem que, embora a verificação de modelos simbólicos seja poderosa, sua utilidade para CPS depende inteiramente da qualidade da abstração. Este fluxo de trabalho fornece um framework rigoroso e adaptável para alcançar essa qualidade, equilibrando o pessimismo com a tratabilidade.