UC Berkeley

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. When building these types of systems, we cannot simply add randomness in an ad hoc way: we need provable guarantees that the system is safe and satisfies our desired specifications. The key question, then, is how can we automatically synthesize a system with random behavior but formal guarantees? Our answer to this question is algorithmic improvisation. 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 control improvisation (CI), the core computational problem of algorithmic improvisation, which requires constructing an improviser, a randomized algorithm generating finite 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 for several practical classes of CI problems, and prove hardness results for more difficult classes. Next, we generalize CI to the reactive control improvisation (RCI) problem, which allows us to synthesize open systems that interact with an uncontrolled and potentially adversarial environment: our goal is an improvising strategy that ensures the hard, soft, and randomness constraints hold no matter what actions are taken by the 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, a variant of algorithmic improvisation which uses a probabilistic programming language to provide greater control over the distribution of the improviser. We design a domain-specific probabilistic programming language, Scenic, for defining distributions over scenes, configurations of physical objects and agents. Scenic significantly decreases the effort required to specify the highly 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 and efficiency requirements. 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 convolutional neural network for object detection, 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.