Unmanned air-traffic management (UTM): Formalization, a prototype implementation, and performance evaluation

Unmanned Aircraft Systems (UAS) are being increasingly used in delivery, infrastructure surveillance, fire-fighting, and agriculture. According to the Federal Aviation Administration (FAA), the number of active small commercial unmanned aircraft is going to grow from 385K in 2019 to 828K by 2024. UAS traffic management (UTM) system for low-altitude airspace is therefore immediately necessary for its safe and high-density use. In this paper, we propose the first formalization of FAA's Concept of Operations for UTM for building and analyzing traffic management protocols and systems. We formalize FAA's notion of operation volumes (OVs) that express aircraft intent in terms of 4D blocks of airspace and associated real-time deadlines. We present a prototype coordination protocol using OVs, involving participating aircraft and an airspace manager. We formally analyze the safe separation and liveness properties of the protocol. Our analyses showcase how the de-conflicting and liveness of the system can be proven assuming each aircraft conforms to the deadlines specified by OVs. Through extensive simulations, we evaluate the performance of the protocol in terms of workload and response delays. Our experiments show that the workload on the airspace manager and the response time of each aircraft grow linearly with respect to the number of aircraft. The experiments also delineate the trade-off between performance, workload, and violation rate across different strategies for generating OVs. Lastly, we implement a UTM violation detection and resolution mechanism on top of our protocol. We include a simple fault injection technique that introduces failures with different probabilities. We demonstrate how to use it to empirically evaluate the impact of aircraft failure on the safety of surrounding aircraft, and how the performance of the airspace manager changes under different failure probabilities.

Differential Privacy for Sequential Algorithms

We study the differential privacy of sequential statistical inference and learning algorithms that are characterized by random termination time. Using the two examples: sequential probability ratio test and sequential empirical risk minimization, we show that the number of steps such algorithms execute before termination can jeopardize the differential privacy of the input data in a similar fashion as their outputs, and it is impossible to use the usual Laplace mechanism to achieve standard differentially private in these examples. To remedy this, we propose a notion of weak differential privacy and demonstrate its equivalence to the standard case for large i.i.d. samples. We show that using the Laplace mechanism, weak differential privacy can be achieved for both the sequential probability ratio test and the sequential empirical risk minimization with proper performance guarantees. Finally, we provide preliminary experimental results on the Breast Cancer Wisconsin (Diagnostic) and Landsat Satellite Data Sets from the UCI repository.

Optimistic Optimization for Statistical Model Checking with Regret Bounds

We explore application of multi-armed bandit algorithms to statistical model checking (SMC) of Markov chains initialized to a set of states. We observe that model checking problems requiring maximization of probabilities of sets of execution over all choices of the initial states, can be formulated as a multi-armed bandit problem, for appropriate costs and rewards. Therefore, the problem can be solved using multi-fidelity hierarchical optimistic optimization (MFHOO). Bandit algorithms, and MFHOO in particular, give (regret) bounds on the sample efficiency which rely on the smoothness and the near-optimality dimension of the objective function, and are a new addition to the existing types of bounds in the SMC literature. We present a new SMC tool---HooVer---built on these principles and our experiments suggest that: Compared with exact probabilistic model checking tools like Storm, HooVer scales better; compared with the statistical model checking tool PlasmaLab, HooVer can require much less data to achieve comparable results.

Online monitoring for safe pedestrian-vehicle interactions

As autonomous systems begin to operate amongst humans, methods for safe interaction must be investigated. We consider an example of a small autonomous vehicle in a pedestrian zone that must safely maneuver around people in a free-form fashion. We investigate two key questions: How can we effectively integrate pedestrian intent estimation into our autonomous stack. Can we develop an online monitoring framework to give formal guarantees on the safety of such human-robot interactions. We present a pedestrian intent estimation framework that can accurately predict future pedestrian trajectories given multiple possible goal locations. We integrate this into a reachability-based online monitoring scheme that formally assesses the safety of these interactions with nearly real-time performance (approximately 0.3 seconds). These techniques are integrated on a test vehicle with a complete in-house autonomous stack, demonstrating effective and safe interaction in real-world experiments.

CyPhyHouse: A Programming, Simulation, and Deployment Toolchain for Heterogeneous Distributed Coordination

Programming languages, libraries, and development tools have transformed the application development processes for mobile computing and machine learning. This paper introduces the CyPhyHouse - a toolchain that aims to provide similar programming, debugging, and deployment benefits for distributed mobile robotic applications. Users can develop hardware-agnostic, distributed applications using the high-level, event driven Koord programming language, without requiring expertise in controller design or distributed network protocols. The modular, platform-independent middleware of CyPhyHouse implements these functionalities using standard algorithms for path planning (RRT), control (MPC), mutual exclusion, etc. A high-fidelity, scalable, multi-threaded simulator for Koord applications is developed to simulate the same application code for dozens of heterogeneous agents. The same compiled code can also be deployed on heterogeneous mobile platforms. The effectiveness of CyPhyHouse in improving the design cycles is explicitly illustrated in a robotic testbed through development, simulation, and deployment of a distributed task allocation application on in-house ground and aerial vehicles.

Porting Code Across Simple Mobile Robots

The StarL programming framework aims to simplify development of distributed robotic applications by providing easy-to-use language constructs for communication and control. It has been used to develop applications such as formation control, distributed tracking, and collaborative search. In this paper, we present a complete redesign of the StarL language and its runtime system which enables us to achieve portability of robot programs across platforms. Thus, the same application program, say, for distributed tracking, can now be compiled and deployed on multiple, heterogeneous robotic platforms. Towards portability, this we first define the semantics of StarL programs in a way that is largely platform independent, except for a few key platform-dependent parameters that capture the worst-case execution and sensing delays and resolution of sensors. Next, we present a design of the StarL runtime system, including a robot controller, that meets the above semantics. The controller consists of a platform-independent path planner implemented using RRTs and a platform-dependent way-point tracker that is implemented using the control commands available for the platform. We demonstrate portability of StarL applications using simulation results for two different robotic platforms, and several applications.

Safe and Stabilizing Distributed Multi-Path Cellular Flows

We study the problem of distributed traffic control in the partitioned plane, where the movement of all entities (robots, vehicles, etc.) within each partition (cell) is coupled. Establishing liveness in such systems is challenging, but such analysis will be necessary to apply such distributed traffic control algorithms in applications like coordinating robot swarms and the intelligent highway system. We present a formal model of a distributed traffic control protocol that guarantees minimum separation between entities, even as some cells fail. Once new failures cease occurring, in the case of a single target, the protocol is guaranteed to self-stabilize and the entities with feasible paths to the target cell make progress towards it. For multiple targets, failures may cause deadlocks in the system, so we identify a class of non-deadlocking failures where all entities are able to make progress to their respective targets. The algorithm relies on two general principles: temporary blocking for maintenance of safety and local geographical routing for guaranteeing progress. Our assertional proofs may serve as a template for the analysis of other distributed traffic control protocols. We present simulation results that provide estimates of throughput as a function of entity velocity, safety separation, single-target path complexity, failure-recovery rates, and multi-target path complexity.