Resumo Técnico: STLSat—Um Tableau Melhorado para Verificação de Satisfatibilidade de Fórmulas de Lógica Temporal de Sinais

Problema

A Lógica Temporal de Sinais (STL) é o padrão de fato para especificar propriedades temporais de sinais de valores reais em sistemas ciber-físicos (CPS). Em domínios de segurança crítica, as especificações frequentemente consistem em grandes coleções de fórmulas STL. Um grande gargalo de engenharia surge na verificação da consistência desses conjuntos de requisitos (garantir que existe um sinal que satisfaça todas as fórmulas) e na identificação de redundância (determinar se uma fórmula é implicada por outras). Ambas as tarefas reduzem-se ao problema de satisfatibilidade de STL.

Embora os procedimentos baseados em tableau sejam uma abordagem natural para este problema, os autores identificam uma falha crítica no único tableau de forma de árvore existente para STL de tempo discreto limitado (proposto por Melani et al. [30]). A otimização "JUMP" original, projetada para pular etapas de tempo repetitivas, foi considerada insound (não íntegra): em fórmulas com operadores temporais aninhados, as regras de salto poderiam pular instantes de tempo onde conflitos são introduzidos, levando o procedimento a aceitar incorretamente fórmulas insatisfatíveis. Além disso, as ferramentas existentes carecem de implementações maduras e de alto desempenho que integrem a extração de núcleo insatisfatível para depuração.

Metodologia

1. Algoritmo de Tableau Corrigido

A principal contribuição teórica é um tableau de forma de árvore, íntegro e completo para STL de tempo discreto limitado.

• Tableau Básico: Os autores mantêm as regras de expansão básicas (decomposição de operadores lógicos e temporais) e a regra STEP (avanço de tempo por uma unidade) do trabalho anterior, que são íntegras e completas.
• A Falha: A regra JUMPO original permitia pular etapas de tempo baseando-se em limites de intervalo, mas falhava ao não considerar conflitos gerados por partes "invariantes" de operadores temporais (por exemplo, o lado esquerdo de um operador Until) durante o intervalo pulado.
• A Correção: Os autores introduzem uma nova regra JUMP que comprime com segurança sequências de aplicações de STEP. Para garantir integridade e completude, o tamanho do salto $k$ é calculado como o mínimo de três limites distintos:
  1. Limite de Limites ($k$): Impede o salto além da ativação ou expiração de operadores sem pais ativos.
  2. Limite de Integridade ($k^*_{sound}$): Garante que proposições "invariantes" emitidas por operadores temporais ativos durante o intervalo pulado não conflitem com proposições de outros operadores ativos ou não ativos. Isso é computado analisando os Intervalos de Validade de Proposições ($T(\phi)$), que mapeiam os instantes de tempo onde proposições atômicas podem aparecer.
  3. Limite de Completude ($k^*_{comp}$): Garante que um ramo satisfatível não seja perdido ao pular um passo de tempo onde uma proposição "alvo" (por exemplo, o lado direito de um Until) poderia ser satisfeita.
• Corretude: Os autores fornecem provas formais (Teoremas 2 e 3) demonstrando que o novo tableau é tanto íntegro (aceita apenas fórmulas satisfatíveis) quanto completo (aceita todas as fórmulas satisfatíveis).

2. Implementação da Ferramenta STLSat

Os autores implementaram o STLSat, uma biblioteca open-source em Rust que atua como um solver de portfólio, executando três procedimentos de decisão complementares em paralelo:

• Mecanismo de Tableau: Implementa a regra JUMP corrigida. Inclui uma fase de simplificação sintática leve (achatamento, fusão de intervalos) e utiliza uma pilha explícita para gerenciar a memória de forma eficiente. Também apresenta um novo mecanismo de extração de núcleo insatisfatível que agrega conflitos locais de ramos rejeitados para identificar o subconjunto mínimo de requisitos conflitantes.
• Mecanismo de Lógica de Primeira Ordem (FOL): Um codificação otimizada inspirada por Li et al. [28], traduzindo fórmulas STL para FOL onde os sinais são funções de inteiros para valores reais/booleanos. Utiliza traduções ad-hoc para operadores F e G para reduzir o tamanho da fórmula.
• Mecanismo SMT Sem Quantificadores: Codifica STL como um problema SMT sem quantificadores sobre aritmética real linear, semelhante aos métodos usados para controle preditivo baseado em modelo e verificação de modelo limitada.

Principais Contribuições

1. Algoritmo de Tableau Corrigido: Um novo conjunto de regras para a otimização JUMP que garante formalmente a integridade e a completude para STL de tempo discreto limitado, corrigindo a falha na otimização da STLTree.
2. Ferramenta STLSat: Uma implementação de alto desempenho em Rust do STLSat, fornecendo um portfólio de solvers (Tableau, FOL, SMT).
3. Extração de Núcleo Insatisfatível: Um método dedicado integrado ao mecanismo de tableau para extrair subconjuntos mínimos de requisitos inconsistentes, facilitando a depuração de especificações.
4. Codificações Melhoradas: Codificações FOL e SMT de semântica qualitativa aprimoradas para STL.
5. Suíte de Benchmarks: O lançamento de uma extensa suíte de benchmarks pública cobrindo fórmulas tanto de STL quanto de Lógica Temporal Linear de Tempo de Missão (MLTL), incluindo instâncias do mundo real e geradas aleatoriamente.

Resultados Experimentais

Os autores avaliaram o STLSat contra o STLTree (a implementação original de tableau) e o MLTLSAT (um solver de FOL de última geração para MLTL) através de diversos benchmarks.

• Desempenho: Nenhuma técnica única dominou todos os instâncias.
  • O mecanismo FOL destacou-se no benchmark NASA-Boeing (requisitos de aviação do mundo real), resolvendo 62/63 instâncias rapidamente, em grande parte porque estas fórmulas dependem fortemente dos operadores F e G em vez de U.
  • O mecanismo de Tableau teve o melhor desempenho em fórmulas geradas aleatoriamente com amplos intervalos de tempo, aproveitando a regra JUMP para pular etapas redundantes de forma eficiente.
  • O mecanismo SMT geralmente teve um desempenho inferior em comparação aos outros dois.
• Abordagem de Portfólio: Executar os três mecanismos em paralelo rendeu o melhor desempenho geral, igualando ou superando ferramentas de última geração enquanto preservava as garantias de integridade do tableau íntegro.
• Depuração: Em um exemplo de execução envolvendo um controlador de irrigação, o STLSat identificou o conjunto de requisitos como insatisfatível em uma fração de segundo e extraiu corretamente o núcleo insatisfatível $\{\phi_1, \phi_2\}$, apontando o conflito entre os requisitos de taxa de fluxo e os limites de segurança.

Significância

O artigo afirma que o STLSat aborda uma lacuna crítica na verificação de sistemas ciber-físicos ao fornecer um verificador de satisfatibilidade íntegro onde ferramentas anteriores de última geração continham otimizações não íntegras. Ao combinar uma base teórica corrigida com uma ferramenta prática de alto desempenho que suporta a extração de núcleo insatisfatível, o STLSat permite a mineração de especificações, eliminação de redundância e depuração automatizada de forma eficaz. Os autores enfatizam que seu trabalho transforma conjuntos brutos de restrições potencialmente inconsistentes em modelos de requisitos concisos e rastreáveis, uma capacidade anteriormente ausente em solvers dedicados maduros.