The first half of this thesis provides a framework for engineers to model control systems and construct algorithmic pipelines for control synthesis. By explicitly capturing system structure, this framework gives users the flexibility to rapidly iterate over and leverage a library of optimizations for control synthesis. We demonstrate this framework in the context of abstraction-based control, a synthesis workflow that translates continuous systems into finite state machines by throwing away high precision information. Different optimization techniques such as multi-scale grids, lazy abstraction, and decomposed synthesis, can all be expressed as modifications to a computational pipeline. We demonstrate computational gains while synthesizing safe motion primitives for numerous robotic examples.
The second half addresses distributed control synthesis where multiple controllers act as agents that seek to jointly satisfy a specification and are restricted by some communication topology. We introduce parametric assume-guarantee contracts as a formalism to derive guarantees about the closed loop behavior of a collection of interacting components. Dynamic contracts allow contract parameters to change at runtime and enable coordination of multiple interacting sub-systems. These results are demonstrated in the context of a freeway ramp meter and an adjacent arterial network.