Engineering advances have enabled systems that are increasingly complex while, simultaneously, expectations for the closed-loop behavior of these systems have become more demanding. The resulting combination of complexity and desired behavior requires correct-by-design approaches to system analysis and control. In this dissertation, we develop a class of scalable and automated verification and control synthesis techniques for networked systems. To motivate our study and to demonstrate the applicability of our results, we focus on transportation networks.

The formal analysis and synthesis approaches which are the emphasis of much of this dissertation require a discrete representation of the system in the form of a finite abstraction for the system's behavior. A finite abstraction models the states and dynamics of the system with a finite set of properties and transitions which capture all the phenomena of interest. We first present a broad class of systems which are mixed monotone, that is, systems for which the state evolution can be decomposed into an increasing and decreasing component. For such systems, we develop an efficient abstraction algorithm to enable correct-by-design control synthesis. We then use this approach to synthesize control strategies for transportation flow networks.

We next turn our attention to qualitative analysis of the dynamics present in traffic flow networks. We propose a macroscopic network flow model in continuous time suitable for analysis as a dynamical system, and we analyze equilibrium flows as well as convergence. We show that the same mixed monotone property that enables efficient abstraction allows us to prove global asymptotic stability by embedding the flow network in a larger system.

These contributions provide the theoretical foundation for correct-by-design control of a large class of networked physical systems. By focusing on transportation networks, we show concretely how these results apply to a domain that is of considerable practical importance.