The increasing use of autonomy for safety-critical tasks, from operating power grids to driving cars, has led to an acute need for reliable and secure systems. The ideal approach to obtaining rigorous reliability guarantees is to automatically construct systems from formal specifications using correct-by-construction synthesis. A new dimension in this area is the synthesis of randomized systems, which, as we show in this thesis, enables a broad range of new applications in safe autonomy and other fields. This is because randomness can provide several crucial benefits to a system, including robustness, variety, and unpredictability. For example, a robot following a random route can be harder for an adversary to intercept, making the system more secure; a synthetic data generator for a machine learning algorithm can use randomness to produce diverse training data, making the ML model more robust. The key question, then, is how can we automatically synthesize a system with random behavior but formal guarantees? This thesis proposes a theory of algorithmic improvisation enabling the correct-by-construction synthesis of randomized systems, and explores its applications to safe autonomy.

The first part of the thesis studies the theory of algorithmic improvisation in depth. We begin by introducing the core computational problem of control improvisation (CI), which requires constructing an improviser, a randomized algorithm generating sequences of symbols subject to hard, soft, and randomness constraints. We develop a general approach to building improvisers, instantiate it to obtain efficient synthesis algorithms in some cases, and prove hardness results for others. Next, we generalize CI to the reactive control improvisation (RCI) problem, which allows us to synthesize open systems that interact with an adversarial environment. We again give efficient algorithms for constructing improvising strategies in some useful cases, and hardness results in others. Finally, we investigate language-based improvisation, using a probabilistic programming language (PPL) to provide greater control over the distribution of the improviser. We design a domain-specific PPL, Scenic, for defining distributions over scenes, configurations of physical objects and agents. Scenic significantly decreases the effort required to specify the complex environments of systems like self-driving cars.

In the second part of the thesis, we demonstrate how algorithmic improvisation can help with the design, analysis, and testing of autonomous systems. First, we show how to synthesize randomized planners for mobile robots, for example a patrolling security robot which uses randomness to make its route less predictable while still guaranteeing safety. Next, we study using algorithmic improvisation to create human models with realistic stochasticity and tunable behavior, a vital prerequisite for the design of a system which interacts with people. Finally, we propose a methodology for using language-based improvisation to train, test, and debug cyber-physical systems like autonomous cars by generating synthetic data from customizable distributions. We apply our methodology to an industrial neural network, finding bugs in the system, eliminating them through retraining, and boosting the performance of the network beyond what could be achieved with prior techniques by using Scenic to design training sets in a more intelligent way.

In summary, algorithmic improvisation is a mathematical framework for synthesizing randomized systems satisfying formal specifications. It has already proved useful in a wide range of fields, including robotics, cyber-physical systems, computer music, and machine learning, and shows promise in a variety of further applications to the design of secure and dependable systems.