Hybrid dynamical type theories for navigation

TL;DR

This paper introduces a hybrid dynamical type theory designed to formalize and verify safety in navigation algorithms, integrating linear dependent types with hybrid system categories and exploring temporal logic embeddings.

Contribution

It combines existing type-theoretic frameworks with hybrid systems to enhance formal safety verification and proposes a novel embedding of temporal logic for controller synthesis.

Findings

Successfully organized and proved safety properties for obstacle-avoiding navigation algorithms

Proposed a conjectural embedding of linear-time temporal logic into the type theory

Outlined potential extensions for model-physical space conjugacies and hierarchical relationships

Abstract

We present a hybrid dynamical type theory equipped with useful primitives for organizing and proving safety of navigational control algorithms. This type theory combines the framework of Fu--Kishida--Selinger for constructing linear dependent type theories from state-parameter fibrations with previous work on categories of hybrid systems under sequential composition. We also define a conjectural embedding of a fragment of linear-time temporal logic within our type theory, with the goal of obtaining interoperability with existing state-of-the-art tools for automatic controller synthesis from formal task specifications. As a case study, we use the type theory to organize and prove safety properties for an obstacle-avoiding navigation algorithm of Arslan--Koditschek as implemented by Vasilopoulos. Finally, we speculate on extensions of the type theory to deal with conjugacies between model and physical spaces, as well as hierarchical template-anchor relationships.