Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis

1. Problema e Motivação

As Árvores de Comportamento (Behavior Trees - BTs) são amplamente utilizadas para projetar estratégias de controle hierárquicas e intuitivas para sistemas autônomos, oferecendo mecanismos robustos para falhas e fallbacks. No entanto, garantir a correção formal e a segurança dessas árvores durante a execução é desafiador.

Abordagens anteriores, como as Árvores de Comportamento Temporais (TBTs), utilizam lógica temporal (ex: STL - Signal Temporal Logic) para verificação e reparo de trajetórias (post hoc). Contudo, essas análises são limitadas a:

1. Análise post hoc: Verificação após a execução.
2. Lógica Binária: As TBTs tradicionais operam em lógica booleana (Verdadeiro/Falso), o que não captura adequadamente o estado "Em Execução" (Running) das BTs, onde o resultado ainda é indeterminado.
3. Incapacidade de Síntese: Dificuldade em usar TBTs diretamente para síntese de controle (gerar trajetórias ótimas que satisfaçam a especificação) devido à complexidade de codificar a lógica temporal sobre trajetórias parciais.

O problema central é como formular TBTs de modo que permitam a síntese de controle "correto por construção" para sistemas dinâmicos lineares, lidando com a incerteza de trajetórias parciais e o estado de execução indeterminado.

2. Metodologia

Os autores propõem uma reformulação das TBTs utilizando uma Lógica Ternária baseada na lógica forte de Kleene ($K_3$), combinada com codificações de programação linear inteira mista (MILP/MIQP).

A. Lógica Ternária ($K_3$)

Em vez da lógica booleana (0/1), o sistema utiliza três valores de verdade:

• Falso (F): Falha ou violação da especificação.
• Verdadeiro (T): Sucesso ou satisfação da especificação.
• Desconhecido (U): Estado intermediário (equivalente ao estado "Running" da BT ou quando a trajetória parcial não tem informação suficiente para decidir).

Isso permite que o sistema lide com trajetórias finitas e parciais, onde o horizonte de tempo da especificação pode exceder a trajetória atual, resultando em um valor "Desconhecido" em vez de falha imediata.

B. Semântica de STL sobre Trajetórias Parciais

A lógica STL é estendida para operar sobre trajetórias parciais com um horizonte definido ($t_2$).

• Predicados Ternários: Um predicado de sinal $f(x_t) \ge 0$ é avaliado como:
  • $T$ se $f(x_t) \ge \delta$
  • $F$ se $f(x_t) \le -\delta$
  • $U$ se $-\delta < f(x_t) < \delta$ (zona de incerteza).
• Operadores Temporais: Os operadores "Sempre" ($\square$) e "Eventualmente" ($\diamond$) são redefinidos para lidar com janelas de busca que podem exceder o horizonte da trajetória parcial. Se a janela excede o horizonte e não há "curto-circuito" (ex: um falso em uma conjunção), o resultado é $U$.

C. Codificação Inteira Mista (MILP/MIQP)

Para permitir a síntese de controle via otimização, as semânticas ternárias são codificadas em restrições lineares:

• Variáveis de Decisão: As variáveis de satisfação $z_t$ assumem valores em $\{-1, 0, +1\}$ (representando $F, U, T$).
• Operadores de BT (Seq e Sel):
  • Sequência (Seq): Exige que subfórmulas sejam satisfeitas sequencialmente. A codificação envolve uma disjunção sobre pontos de corte temporais ($\tau$) onde a primeira subfórmula termina e a segunda começa.
  • Seletor (Sel): Exige que pelo menos uma subfórmula seja satisfeita.
• Complexidade: A codificação introduz uma segunda dimensão temporal (o horizonte parcial), aumentando a complexidade para $O(T^{k+1})$ para árvores com $k$ subfórmulas, mas permitindo a resolução exata via otimização.

D. Formulação do Problema de Controle

O problema é formulado como um Programa Quadrático Inteiro Misto (MIQP):

• Objetivo: Minimizar o esforço de controle (função quadrática) para sistemas dinâmicos lineares discretos.
• Restrições: Dinâmica do sistema, limites de controle e a satisfação da fórmula TBT (codificada como restrições lineares mistas).

3. Contribuições Principais

1. Formalização Concreta: A concretização da formalização de BTs sobre a lógica ternária $K_3$, capturando rigorosamente o estado "Running".
2. Codificações Mistas: Introdução de codificações de programação linear inteira mista para STL e operadores de TBT (Seq e Sel) sobre lógica ternária.
3. Síntese de Controle: Demonstração da utilidade prática ao resolver problemas de controle ótimo linear discreto com restrições TBT, garantindo trajetórias que satisfazem especificações complexas de comportamento.

4. Resultados e Estudos de Caso

Os autores validaram a abordagem em dois cenários:

• Caso 1: Integrador Duplo Discreto (Robô Móvel):

  • Tarefa: Navegar para o objetivo A, verificar a bateria e, dependendo do nível, navegar para B (se >80%) ou C e depois B (se <80%), evitando obstáculos.
  • Resultado: O sistema sintetizou trajetórias ótimas em 97 segundos. O comportamento de fallback (ir para C se a bateria estiver baixa) foi gerado automaticamente pela lógica ternária do Seletor, sem necessidade de reescrita manual do plano.

• Caso 2: Planejamento Multiagente:

  • Tarefa: Três agentes devem trocar de objetivos sequencialmente (Seq), evitar obstáculos e manter uma distância mínima entre si.
  • Resultado: O sistema gerou trajetórias onde os agentes formaram uma "fila" (queuing) natural ao passar por corredores estreitos, demonstrando como as restrições de segurança estritas (distância mínima) interagem com a lógica temporal para gerar comportamentos emergentes seguros. O modelo foi resolvido em ~308 segundos.

5. Significado e Conclusão

Este trabalho representa um avanço significativo na interseção entre lógica formal e controle de sistemas autônomos.

• Ponte entre Verificação e Síntese: Transforma as TBTs de ferramentas de verificação offline em especificações diretas para síntese de controle online ou offline.
• Gestão de Incerteza: A lógica ternária oferece uma maneira matematicamente rigorosa de lidar com a indeterminação durante a execução, algo que a lógica booleana tradicional não consegue fazer sem simplificações excessivas.
• Escalabilidade: Embora a complexidade computacional aumente com o número de subfórmulas (devido à segunda dimensão temporal), os resultados mostram que problemas práticos de robótica móvel podem ser resolvidos globalmente em tempos razoáveis usando otimizadores comerciais (Gurobi).

Em suma, o artigo fornece um framework robusto para projetar controladores que são corretos por construção em relação a especificações de comportamento hierárquico e temporal complexas, essenciais para a autonomia segura de sistemas robóticos.