Orientação de Rota para Especificações de Lógica Temporal Satisfatórias sobre o Movimento de Aeronaves

Uma nova técnica para orientação de rotas de aeronaves sujeita a especificações de lógica temporal linear é apresentada. A abordagem proposta é baseada na partição do espaço de trabalho e se apoia na ideia dos chamados gráficos elevados. Resumidamente, as arestas em um gráfico elevado são sucessões de arestas adjacentes no gráfico topológico associado à partição do espaço de trabalho. As arestas do gráfico elevado estão associadas a certas propriedades de alcançabilidade do modelo de aeronave. O principal resultado deste artigo é a caracterização precisa de rotas aceitáveis (ou seja, sequências de células) que são garantidas para serem atravessáveis por trajetórias de estado admissíveis do modelo de aeronave enquanto satisfazem as especificações dadas de lógica temporal linear. A abordagem proposta incorpora restrições cinemáticas não holonômicas, não requer controle completo na presença de restrições do espaço de trabalho e não exige linearização do modelo de aeronave. Métodos numéricos para implementar o algoritmo de planejamento de rotas proposto são discutidos. O algoritmo proposto é ilustrado com exemplos de simulação numérica que refletem a importância prática das especificações de lógica temporal linear na orientação de aeronaves.