Algorithms for autonomous urban navigation with formal specifications

Abstract

This thesis addresses problems in planning and control of autonomous agents. The central theme of this work is that integration of "low-level control synthesis" and "high-level decision making" is essential to devise robust algorithms with provable guarantees on performance. We pursue two main directions here. The first part considers planning and control algorithms that satisfy temporal specifications expressed using formal languages. We focus on task specifications that become feasible only if some of the specifications are violated and compute a control law that minimizes the level of unsafety of the system while guaranteeing that it still satisfies the task specification. Examples in this domain are motivated from an autonomous car navigating an urban landscape while following road safety rules such as "always travel in the left lane" and "do not change lanes frequently" or an electric vehicle in a mobility-on-demand scenario. The second part of the thesis focuses on multi-agent control synthesis, where agents are modeled as dynamical systems and they interact with each other while sharing the same road infrastructure - all the while respecting the same road driving rules expressed as LTL specifications. We discuss algorithms that identify well-defined notions in the game theory literature such as Stackelberg equilibria and non-cooperative Nash equilibria under various information structures. This work builds upon ideas from three different fields, viz., sampling-based motion-planning algorithms to construct efficient concretizations of general, continuous time dynamical systems, model checking for formal specifications that helps guarantee the safety of a system under all scenarios, and game theory to model the interaction between different agents trying to perform possibly conflicting tasks.