We develop a framework for traffic management and control using formal methods. By drawing on techniques from model-checking and correct-by-construction synthesis, we ensure that traffic flows are guaranteed to satisfy desirable objectives expressed using linear temporal logic, including conditions such as:
Our techniques take advantage of inherent structure in traffic networks such as monotonicity properties, decomposability into sparsely connected subsystems, and hybrid dynamics. In particular, exploiting such structure allows efficient computation of finite state abstractions for the traffic flow dynamics. This paves the way for scalable design methodologies applicable to freeway ramp metering and traffic signal timing. This project is supported by a recently-funded NSF grant under the CPS Program.
In this work, we design control policies to reroute congested freeway traffic to an adjacent arterial corridor. As a proof-of-concept, we focus on a segment of I-210 in Arcadia, CA and the adjacent Colorado St./Huntington Dr. arterial corridor. We use in-house simulation software, calibrated with measured traffic data, to provide a detailed assessment of our control algorithms. This project requires developing: a theoretical foundation for a coordinated control approach which leverages results from other ongoing projects; a high-fidelity simulation tool calibrated with measured data for verification and analysis; a web-based environment for rapid prototyping and visualization of results. This project is supported by California Partners for Advanced Transportation Technology (PATH).
We consider the problem of controlling probabilistic systems, modeled as Markov Decision Processes, to achieve objectives expressed in linear temporal logic. We aim to bridge the gap between automata- and graph-theoretic techniques well-suited for verification and synthesis of nondeterministic systems and the statistical approaches for probabilistic systems primarily developed in the machine learning community. Our approach draws on results from, among other domains, probabilistic model checking, the theory of Markov chains, machine learning, and graph theory.
We propose a general traffic network flow model particularly suitable for analysis as a dynamical system, and we qualitatively analyze equilibrium flows as well as convergence. Flows at a junction are determined by downstream supply of capacity (lack of congestion) as well as upstream demand of traffic wishing to flow through the junction. This approach is rooted in the celebrated Cell Transmission Model for freeway traffic flow. Unlike related results which rely on certain system cooperativity properties, our model generally does not possess these properties. We show that the lack of such properties is in fact a useful feature that allows traffic control methods, such as ramp metering, to be effective. Additionally, we show that such networks do possess a much weaker property known as componentwise monotonicity, and we use tools from contraction theory and small gain theory to analyze the resulting dynamics. Finally, we leverage these results to develop a linear program for optimal ramp metering.
We investigate methods for synthesizing switching policies for networked dynamical systems that are capable of operating in various modes. Such hybrid systems often operate autonomously in each mode, and a supervisory controller switches between modes to guarantee certain criteria such as safety or performance. Applications include multiagent surveillance and ramp metering strategies for traffic networks.
We present a sum-of-squares approach to verifying a state-based safety constraint of a network consisting of interconnected subsystems. We offer an approach that relies on the interconnection structure and equilibrium-independent input-output properties of the subsystems and therefore does not suffer from the shortcomings of related approaches such as an arbitrary parameterization of barrier functions or exact knowledge of the system equilibrium, which may be unknown for large systems.
We consider the problem of formation control of a team of mobile agents when only a subset of the agents know the desired size scaling of the formation. The remaining agents implement a cooperative control law using only local interagent position information such that the agents converge to the desired formation scaled by the desired size. The control laws that we design require only knowledge of relative displacement to neighboring agents, i.e. no communication among the agents. By allowing the size of the formation to change, the group can dynamically adapt to changes in the environment such as unforeseen obstacles, adapt to changes in group objectives, or respond to threats.
We consider agents acting noncooperatively in a networked, dynamic game setting and seek to design appropriate incentives to close the gap between what is possible with cooperative control, and what happens in the noncooperative environment. We pose the problem as a convex optimization problem and demonstrate our approach theoretically in the setting of energy management in buildings, and future work will investigate methods for applying our approach to a building on the UC Berkeley campus.
The purpose of this course project is to predict the votes of US Supreme Court justices using oral argument transcripts. By analyzing the Justices' comments and questions posed to each arguing party, we are able to provide predictions as to how the justices will vote. See the project webpage here.
During Summer 2012, I worked at NASA's Jet Propulsion Lab in Pasadena, CA. I researched primitive body navigation focusing on state estimation techniques for landing spacecraft on primitive bodies such as comets and asteroids. Primitive bodies pose unique challenges for guidance, navigation and control as they are often irregularly shaped, have irregular gravitational fields, and can outgas, introducing severe disturbances. Additionally, in contrast to larger astronomical bodies that are well-studied, useful information such as landmark features, exact positioning, and inertial data are largely unknown. I investigated methods for state estimation that incorporates data from a variety of sensors and is robust to outliers to allow sample return missions from these small bodies.