SE PhD Prospectus Defense of Alphan Ulusoy

TITLE: Optimal Temporal Logic Control of Autonomous Systems ABSTRACT: Temporal logics, such as Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), are extensions of propositional logic that can capture temporal relations. Even though temporal logics have been used in model checking of finite systems for quite some time, they have gained popularity as a means for specifying complex mission requirements in path planning and control synthesis problems only recently. The proposed thesis focuses on methods and algorithms for optimal path planning and control synthesis for autonomous systems where a global high-level mission specification expressed in LTL (or a fragment of LTL) must be satisfied. In a nutshell, after obtaining a discrete representation of the overall system, ideas and tools from formal verification and graph theory are leveraged to synthesize provably correct and optimal control strategies. The main research objectives of the proposed thesis can be summarized as follows: - Optimal planning for multi-agent systems in static environments: This part will focus on automatic planning of optimal paths for a group of robots that must satisfy a common high level mission specification. The effect of slight deviations in traveling times on the behavior of the team will be analyzed and methods that are robust to bounded non-determinism in traveling times will be proposed. Most centralized planning approaches typically suffer from the so-called state-space explosion problem. We will also look at ways to alleviate this issue. - Optimal control synthesis for agents interacting with external probabilistic agents. This part will focus on the case where an autonomous agent is required to satisfy a high-level mission specification in the presence of other probabilistic agents that we cannot control. Efficient methods to synthesize control policies that maximize the probability of satisfaction of the mission specification will be presented. - Optimal control synthesis for agents in non-deterministic environments: The main focus of this part will be the problem where an autonomous agent is required to satisfy a high-level mission specification in a non-deterministic environment that we know only partially. Methods for synthesizing control policies that can guarantee the satisfaction of the mission specification, while simultaneously minimizing the worst-case cost defined with respect to some relevant metric, will be presented. We will also investigate receding horizon like approaches that make use of the local information provided by the sensors in addition to the a priori information about the environment. - Implementation and validation: For all of the automatic planning and control synthesis problems that are considered, the proposed algorithms will be implemented and validated through experiments and/or simulations. COMMITTEE: Advisor: Calin Belta, ME/SE; John Baillieul, ME/ECE; Sean Anderson, ME/SE; Mac Schwager, ME/SE