Motion Planning and Controls with Safety and Temporal Constraints

Motion planning, or trajectory planning, commonly refers to a process of converting high-level task specifications into low-level control commands that can be executed on the system of interest. For different applications, the system will be different. It can be an autonomous vehicle, an Unmanned Aerial Vehicle(UAV), a humanoid robot, or an industrial robotic arm. As human machine interaction is essential in many of these systems, safety is fundamental and crucial. Many of the applications also involve performing a task in an optimal manner within a given time constraint. Therefore, in this thesis, we focus on two aspects of the motion planning problem. One is the verification and synthesis of the safe controls for autonomous ground and air vehicles in collision avoidance scenarios. The other part focuses on the high-level planning for the autonomous vehicles with the timed temporal constraints. In the first aspect of our work, we first propose a verification method to prove the safety and robustness of a path planner and the path following controls based on reachable sets. We demonstrate the method on quadrotor and automobile applications. Secondly, we propose a reachable set based collision avoidance algorithm for UAVs. Instead of the traditional approaches of collision avoidance between trajectories, we propose a collision avoidance scheme based on reachable sets and tubes. We then formulate the problem as a convex optimization problem seeking control set design for the aircraft to avoid collision. We apply our approach to collision avoidance scenarios of quadrotors and fixed-wing aircraft. In the second aspect of our work, we address the high level planning problems with timed temporal logic constraints. Firstly, we present an optimization based method for path planning of a mobile robot subject to timed temporal constraints, in a dynamic environment. Temporal logic (TL) can address very complex task specifications such as safety, coverage, motion sequencing etc. We use metric temporal logic (MTL) to encode the task specifications with timing constraints. We then translate the MTL formulae into mixed integer linear constraints and solve the associated optimization problem using a mixed integer linear program solver. We have applied our approach on several case studies in complex dynamical environments subjected to timed temporal specifications. Secondly, we also present a timed automaton based method for planning under the given timed temporal logic specifications. We use metric interval temporal logic (MITL), a member of the MTL family, to represent the task specification, and provide a constructive way to generate a timed automaton and methods to look for accepting runs on the automaton to find an optimal motion (or path) sequence for the robot to complete the task.

Antonio Salieri's La calamita de' cuori (1774): Sources, Form, Context

Antonio Salieri’s La calamita de’ cuori (1774) warrants musicological attention for what it can tell us about Salieri’s compositional craft and what it reveals about the development of form in Viennese Italian-language comic opera of the mid- and late-eighteenth century. In Part I of this dissertation, I explore the performance history of La calamita, present the first plot synopsis and English translation of the libretto, and describe the variants between Carlo Goldoni’s 1752 libretto and the revised version created for Salieri’s opera. I have collated Salieri’s holograph score, Österreichische Nationalbibliothek, Vienna, Mus. Hs. 16.508, with four copies having different relationships to it, and I propose a stemma that represents the relationships between these five sources. The analyses in Part II contribute to our understanding of formal practices in eighteenth-century drammi giocosi. My study of Salieri’s La calamita reveals his reliance on a clearly defined binary structure, referred to in this dissertation as “operatic binary form,” in almost half of the arias, ensembles, and instrumental movements of this opera. Salieri’s consistent use of operatic binary form led me to explore its use in drammi giocosi by other prominent composers of this time, including Baldassare Galuppi’s La calamita de’ cuori (1752), Wolfgang Amadeus Mozart’s Il dissoluto punito, ossia Il Don Giovanni (1787), and selected arias by Pasquale Anfossi, Florian Leopold Gassmann, Giuseppe Gazzaniga, Franz Joseph Haydn, Giovanni Paisiello, and Niccolò Piccinni dating from 1760 to 1774. This study showed that Salieri and his peers adhered to a recognizable tonal plan and set of design elements in their operatic binary forms, and that their arias fall into three distinct categories defined by the tonality at the beginning of the second half of the binary structure. The analysis presented here adds to our present understanding of operatic form in mid- and late-century drammi giocosi and shows that in La calamita de’ cuori, Salieri was following the normative formal procedures of his time.

Language-based Techniques for Practical and Trustworthy Secure Multi-party Computations

Secure Multi-party Computation (MPC) enables a set of parties to collaboratively compute, using cryptographic protocols, a function over their private data in a way that the participants do not see each other's data, they only see the final output. Typical MPC examples include statistical computations over joint private data, private set intersection, and auctions. While these applications are examples of monolithic MPC, richer MPC applications move between "normal" (i.e., per-party local) and "secure" (i.e., joint, multi-party secure) modes repeatedly, resulting overall in mixed-mode computations. For example, we might use MPC to implement the role of the dealer in a game of mental poker -- the game will be divided into rounds of local decision-making (e.g. bidding) and joint interaction (e.g. dealing). Mixed-mode computations are also used to improve performance over monolithic secure computations. Starting with the Fairplay project, several MPC frameworks have been proposed in the last decade to help programmers write MPC applications in a high-level language, while the toolchain manages the low-level details. However, these frameworks are either not expressive enough to allow writing mixed-mode applications or lack formal specification, and reasoning capabilities, thereby diminishing the parties' trust in such tools, and the programs written using them. Furthermore, none of the frameworks provides a verified toolchain to run the MPC programs, leaving the potential of security holes that can compromise the privacy of parties' data. This dissertation presents language-based techniques to make MPC more practical and trustworthy. First, it presents the design and implementation of a new MPC Domain Specific Language, called Wysteria, for writing rich mixed-mode MPC applications. Wysteria provides several benefits over previous languages, including a conceptual single thread of control, generic support for more than two parties, high-level abstractions for secret shares, and a fully formalized type system and operational semantics. Using Wysteria, we have implemented several MPC applications, including, for the first time, a card dealing application. The dissertation next presents Wys*, an embedding of Wysteria in F*, a full-featured verification oriented programming language. Wys* improves on Wysteria along three lines: (a) It enables programmers to formally verify the correctness and security properties of their programs. As far as we know, Wys* is the first language to provide verification capabilities for MPC programs. (b) It provides a partially verified toolchain to run MPC programs, and finally (c) It enables the MPC programs to use, with no extra effort, standard language constructs from the host language F*, thereby making it more usable and scalable. Finally, the dissertation develops static analyses that help optimize monolithic MPC programs into mixed-mode MPC programs, while providing similar privacy guarantees as the monolithic versions.

An Ecological Analysis of the Potential for Moss-Based Green Roof Design

Green roofs are a maturing application of best management practices for controlling urban stormwater runoff. The majority of green roofs are planted with drought resistant, higher plant species, such as the genus Sedum. However, other plant varieties, such as mosses, may be equally applicable. Residential roofs and natural terrestrial communities were sampled in both Maryland and Tennessee to determine moss community structure and species water composition. This served as a natural analog for potential green roof moss communities. During sampling, 21 species of moss were identified throughout the 37 total sites. The average percent moss cover and water composition across all roof sites was 40.7% and 38.6%, respectively and across all natural sites, 76.7% and 47.7%, respectively. Additional maximum water holding capacity procedures were completed on sedum and 19 of the 21 sampled moss species to assess their individual potential for stormwater absorption. Sedum species on average held 166% of their biomass in water, while moss species held 732%. The results of this study are used as a basis to propose moss species that will improve green roof performance.

RISK-BASED MULTIOBJECTIVE PATH PLANNING AND DESIGN OPTIMIZATION FOR UNMANNED AERIAL VEHICLES

Safe operation of unmanned aerial vehicles (UAVs) over populated areas requires reducing the risk posed by a UAV if it crashed during its operation. We considered several types of UAV risk-based path planning problems and developed techniques for estimating the risk to third parties on the ground. The path planning problem requires making trade-offs between risk and flight time. Four optimization approaches for solving the problem were tested; a network-based approach that used a greedy algorithm to improve the original solution generated the best solutions with the least computational effort. Additionally, an approach for solving a combined design and path planning problems was developed and tested. This approach was extended to solve robust risk-based path planning problem in which uncertainty about wind conditions would affect the risk posed by a UAV.