Event

Ph.D. Dissertation Defense: Estefany Carrillo

Thursday, May 27, 2021
11:00 a.m.
Online Presentation

Controller Synthesis and Formal Behavior Inference in Autonomous Systems

Estefany Carrillo

Zoom: https://umd.zoom.us/j/9184185882pwd=M0ZmMEl1eHlJSWhRSHFJd3lHNXZ2QT09

Advisory Committee:

Professor Huan Xu, Chair/Advisor
Professor Robert Celi
Professor Michael Otte
Professor Robert Sanner
Professor Jeffrey Herrmann, Dean's Representative

Abstract

Autonomous systems are widely used in crucial applications such as surveillance, defense, firefighting, and search & rescue operations. Many of these applications require systems to satisfy user-defined requirements describing the desired system behavior. Given high-level requirements, we are interested in the design of controllers that guarantee the compliance of these requirements by the system. However, ensuring that these systems satisfy a given set of requirements is challenging for many reasons, one of which is the large computational cost incurred by having to account for all possible system behaviors and environment conditions. These computational difficulties are exacerbated when systems are required to satisfy requirements involving large numbers of tasks emerging from dynamic environments. In addition to computational difficulties, scalability issues also arise when dealingwith multi-agent applications, in which agents require coordination and communication to satisfy mission requirements. This dissertation is an effort towards addressing the computational and scalability challenges of designing controllers from high-level requirements by employing reactive synthesis, a formal methods approach, and combining it with other decision-making processes that handle coordination among agents to alleviate the load on reactive synthesis. The proposed framework results in a more scalable solution with lower computational costs while guaranteeing that high-level requirements are met. The practicality of the proposed framework is demonstrated through various types of multi-agent applications including firefighting, fire monitoring, rescue, search & rescue and ship protection scenarios. Our approach incorporates methodology from computer science and control, including reactive synthesis of discrete systems, metareasoning, reachability analysis and inverse reinforcement learning. This thesis consists of two key parts: reactive synthesis from linear temporal logic specifications and specification inference from demonstrations of formal behavior. First, we introduce the reactive synthesis problem for which the desired system behavior specifies the method by which a multi-agent system solves the problem of decentralized task allocation depending on communication availability conditions. Second, we present the synthesis problem formulated to obtain a high-level mission planner and controller for managing a team of agents fighting a wildfire. Third, we present a framework for inferring linear temporal logic specifications that succinctly convey and explain the observed behavior. The gained knowledge is leveraged to improve motion prediction for agents behaving according to the learned specification. The effectiveness of the inference process and motion prediction framework are demonstrated through a scenario in which humans practice social norms commonly seen in pedestrian settings.