STLCG

Conjunto de ferramentas JAX para robustez diferenciável de Signal Temporal Logic

Licença

BSD-2-Clause

Visão geral

STLCG (distribuído como a biblioteca JAX stljax) é um conjunto de ferramentas para computar a robustez de fórmulas de Signal Temporal Logic (STL) usando grafos de computação. STL é uma linguagem formal para expressar requisitos espaço-temporais como "entrar na região-alvo em até 10 segundos e permanecer por 5 segundos", e sua medida de robustez quantifica o quão fortemente um sinal satisfaz ou viola uma especificação. O stljax reimplementa em JAX o stlcg PyTorch original de 2019 do Stanford ASL, substituindo a avaliação recorrente sequencial por uma formulação totalmente paralelizável baseada em mascaramento que roda até ~1000x mais rápido na GPU. Como todo o pipeline é diferenciável, especificações STL podem ser incorporadas diretamente em otimização de trajetória baseada em gradiente, modelagem de recompensa para aprendizado por reforço (RL) e mineração de parâmetros. Publicado no IEEE Robotics and Automation Letters (RA-L) 2025; instalável via pip como stljax.

O stljax permite que engenheiros de robótica transformem especificações de missão em lógica temporal legíveis por humanos em termos de objetivo e restrição diferenciáveis. Você constrói fórmulas STL a partir de Expressions e Predicates, avalia sua robustez ao longo de um sinal ou trajetória e — como tudo é implementado em JAX — obtém avaliação em lote via vmap e gradientes exatos para uso dentro de otimizadores e laços de aprendizado. A principal escolha de projeto é uma reformulação baseada em mascaramento dos operadores temporais (Always/Eventually/Until) que paraleliza o que antes era uma computação recorrente sequencial, proporcionando acelerações de ordem de magnitude ao mesmo tempo em que distribui corretamente os gradientes por todas as operações de min/max.

Por que importa

Signal Temporal Logic dá à robótica uma forma precisa e legível por humanos de especificar requisitos temporais e espaciais de missão, mas por anos sua computação de robustez foi sequencial, lenta e difícil de diferenciar — mantendo a STL fora dos pipelines modernos de aprendizado e otimização. O stljax remove essa barreira: uma implementação paralelizada e nativa de autodiff torna a STL rápida o suficiente para controle em tempo real e treinamento em grandes lotes, de modo que especificações podem atuar diretamente como objetivos de planejador, recompensas de RL ou sinais de verificação.

Problema que resolve

Ferramentas anteriores de robustez STL dependiam de computação recorrente sequencial, que era lenta e difícil de diferenciar, o que limitava o uso de especificações formais de lógica temporal dentro de otimização de trajetória baseada em gradiente e aprendizado.

Pontos principais

• Robustez STL paralela baseada em mascaramento, até ~1000x mais rápida que métodos recorrentes na GPU
• Nativo em JAX: lotes via vmap e gradientes exatos, com distribuição correta de gradiente por min/max
• APIs de Expression e Predicate para construir fórmulas Always/Eventually/Until
• Especificações diferenciáveis utilizáveis como objetivos/restrições em otimização de trajetória e RL
• Instalável via pip (stljax); RA-L 2025; sucessor do stlcg PyTorch do Stanford ASL

Para quem é

• Pesquisadores de planejamento de movimento e otimização de trajetória
• Pesquisadores de controle e métodos formais
• Projetistas de recompensa de aprendizado por reforço
• Engenheiros de autonomia segura e verificação

Limitações

• Exige familiaridade com Signal Temporal Logic para criar especificações úteis
• A suavização/aproximação da função de robustez introduz compromissos de precisão/gradiente
• Dependência de JAX e sua cadeia de ferramentas
• Uma biblioteca de avaliação de especificações — não inclui um planejador ou controlador em si