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

Titolo: Codifiche Logiche Ternarie degli Alberi di Comportamento Temporali con Applicazione alla Sintesi del Controllo

1. Problema e Contesto

Gli Alberi di Comportamento (Behavior Trees - BT) sono diventati uno strumento popolare per la progettazione di strategie di controllo gerarchiche per sistemi autonomi, offrendo un'interfaccia grafica intuitiva e meccanismi di fallback robusti. Tuttavia, garantire la correttezza e la sicurezza di questi sistemi richiede modelli formali rigorosi.
Esistono approcci precedenti che utilizzano la Logica Temporale su Segnali (STL) per verificare gli alberi di comportamento (chiamati Temporal BTs o TBTs), ma questi metodi sono limitati all'analisi post hoc (dopo l'esecuzione) o alla riparazione delle tracce. Inoltre, la logica booleana classica (Vero/Falso) non è sufficiente per modellare lo stato "In Esecuzione" (Running) tipico dei BT, né per gestire l'incertezza nelle misurazioni o nei traiettorie parziali durante la sintesi del controllo.
Il problema centrale è quindi: come formulare i TBT in modo tale da permettere la sintesi di strategie di controllo "corrette per costruzione" (correct-by-construction) per sistemi dinamici lineari, gestendo stati intermedi e orizzonti temporali parziali?

2. Metodologia

Gli autori propongono un quadro teorico e computazionale basato su tre pilastri fondamentali:

• Logica Ternaria ($K_3$):
  Invece della logica booleana classica, il paper introduce l'uso della Logica Forte di Kleene ($K_3$), che introduce un terzo valore di verità: Sconosciuto (Unknown).

  • Vero (T): Corrisponde allo stato "Successo" (Success).
  • Falso (F): Corrisponde allo stato "Fallimento" (Failure).
  • Sconosciuto (U): Corrisponde allo stato "In Esecuzione" (Running) o a situazioni di incertezza dove la specifica non è né soddisfatta né violata (es. traiettorie parziali o predizioni future non ancora definitive).
    Questo permette di modellare formalmente la natura dinamica dei BT durante l'esecuzione.

• Semantica STL su Traiettorie Parziali:
  Viene estesa la semantica qualitativa della STL per operare su traiettorie parziali (sottosequenze contigue di una traiettoria infinita). Se l'orizzonte temporale della formula supera la lunghezza della traiettoria disponibile, il valore di soddisfazione non diventa indefinito, ma assume il valore "Sconosciuto" (U), a meno che non si verifichi un "corto circuito" logico (es. un'intersezione con un valore Falso rende immediatamente Falso l'intero operatore AND).

• Codifiche Miste-Interi (Mixed-Integer Encodings):
  Il contributo principale è la trasformazione delle semantica sopra descritte in vincoli di Programmazione Lineare Intera Mista (MILP/MIQP).

  • Le variabili decisionali non sono più binarie (0/1), ma ternarie (valori in $\{-1, 0, +1\}$), mappati su Falso, Sconosciuto e Vero.
  • Vengono definiti schemi di codifica specifici per gli operatori STL (Always $\square$, Eventually $\diamond$) e per gli operatori specifici dei TBT:
    • Sequence (Seq): Richiede che le sotto-formule siano soddisfatte in sequenza temporale. La codifica implica una disgiunzione su tutti i possibili punti di interruzione della traiettoria.
    • Selector (Sel): Richiede che almeno una sotto-formula sia soddisfatta (logica OR temporale).
  • Questi vincoli permettono di formulare il problema di controllo ottimo come un programma quadratico misto-intero (MIQP), dove l'obiettivo è minimizzare lo sforzo di controllo soggetto ai vincoli dinamici e alla soddisfazione del TBT.

3. Contributi Chiave

1. Formalizzazione Terna: Concretizzazione della formalizzazione dei BT sulla logica ternaria $K_3$, risolvendo la discrepanza tra lo stato "Running" dei BT e la logica booleana.
2. Codifiche Miste-Interi: Introduzione di codifiche MILP/MIQP per gli operatori STL e TBT su logica ternaria. Questo permette di gestire l'incertezza e le traiettorie parziali direttamente nel processo di ottimizzazione.
3. Sintesi del Controllo: Dimostrazione pratica della generazione di strategie di controllo "corrette per costruzione" per sistemi dinamici lineari discreti, garantendo che la traiettoria sintetizzata soddisfi le specifiche TBT.

4. Risultati e Studi di Caso

Gli autori hanno validato il framework risolvendo problemi di controllo ottimo in due scenari:

• Caso 1: Integratore Doppio Discreto (Robot Mobile Singolo):

  • Un robot deve navigare verso un obiettivo A, poi, a seconda del livello della batteria (stato di condizione), decidere se andare direttamente a B o prima a C (ricarica).
  • Il TBT gestisce il branching logico basato sulla batteria.
  • Il sistema è stato risolto globalmente in circa 97 secondi. I risultati mostrano che il robot segue percorsi ottimali diversi a seconda dello stato iniziale della batteria, rispettando vincoli di sicurezza (evitamento ostacoli) e la logica ternaria.

• Caso 2: Pianificazione Multi-Agente:

  • Tre agenti devono raggiungere obiettivi specifici in sequenza, evitando ostacoli e mantenendo una distanza minima reciproca.
  • La specifica TBT impone sequenze di compiti e vincoli di sicurezza collettivi.
  • Il sistema ha generato traiettorie in circa 307 secondi. Un risultato interessante è l'emergere di un fenomeno di coda (queuing): gli agenti si alternano nel passaggio attraverso un corridoio stretto per rispettare il vincolo di distanza minima, dimostrando la capacità del metodo di gestire interazioni complesse e vincoli di sicurezza rigidi.

5. Significato e Implicazioni

Questo lavoro rappresenta un passo significativo verso l'uso pratico degli Alberi di Comportamento nella sintesi automatica del controllo.

• Superamento dei limiti della Logica Booleana: L'uso della logica ternaria permette di trattare formalmente lo stato "Running" e l'incertezza, rendendo i modelli più fedeli alla realtà operativa dei sistemi autonomi.
• Sintesi "Correct-by-Construction": A differenza dei metodi di verifica post hoc, questo approccio garantisce che la traiettoria generata soddisfi le specifiche fin dall'inizio, riducendo il rischio di fallimenti in fase di esecuzione.
• Scalabilità e Complessità: Sebbene gli autori notino che la complessità computazionale cresce con la potenza $k$ (numero di sotto-formule) e il quadrato dell'orizzonte temporale ($O(T^{k+1})$) a causa della natura ricorsiva degli operatori TBT, il metodo è stato dimostrato efficace su problemi reali di dimensioni gestibili con solver moderni (Gurobi).
• Futuro: Il lavoro apre la strada all'applicazione di queste tecniche a sistemi non lineari e a scenari più complessi, generalizzando ulteriormente la classe di sistemi controllabili tramite specifiche formali basate su BT.

In sintesi, il paper fornisce un ponte solido tra la modellazione intuitiva degli alberi di comportamento e la rigorosa sintesi matematica del controllo, abilitando sistemi autonomi più sicuri, interpretabili e capaci di gestire scenari complessi e incerti.