CONTROLLER SYNTHESIS AND FORMAL BEHAVIOR INFERENCE IN AUTONOMOUS SYSTEMS
CONTROLLER SYNTHESIS AND FORMAL BEHAVIOR INFERENCE IN AUTONOMOUS SYSTEMS
Loading...
Files
Publication or External Link
Date
2021
Authors
Carrillo, Estefany
Advisor
Xu, Huan
Citation
DRUM DOI
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.