CONTROLLER SYNTHESIS AND FORMAL BEHAVIOR INFERENCE IN AUTONOMOUS SYSTEMS

Abstract

Autonomous systems are widely used in crucial applications such as surveillance,defense, reghting, and search & rescue operations. Many of these application require systems to satisfy user-dened 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 diculties are exacerbated when systems are required to satisfy requirements involving large numbers of tasks emerging from dynamic environments. In addition to computational diculties, scalability issues also arise when dealing with multi-agent applications, in which agents require coordination and communication to satisfy mission requirements. This dissertation is an eort towards addressing the computational and scalability challenges of designing controllers from highlevel 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 reghting, re 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 specications and specication inference from demonstrations of formal behavior. First, we introduce the reactive synthesis problem for which the desired system behavior species 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 ghting a wildre. Third, we present a framework for inferring linear temporal logic specications that succinctly convey and explain the observed behavior. The gained knowledge is leveraged to improve motion prediction for agents behaving according to the learned specication. The eectiveness of the inference process and motion prediction framework are demonstrated through a scenario in which humans practice social norms commonly seen in pedestrian settings.