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:

- Infinitely often, each queue is completely emptied
- Onramp spillover never occurs
- Whenever a road becomes congested, it eventually becomes uncongested
- A signal remains green for no less than 30s but no more than 90s if there is waiting cross traffic, or no more than 120s otherwise

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.

**S. Coogan**, E. A. Gol, M. Arcak, C. Belta, “Traffic network control from temporal logic specifications,”*IEEE Transactions on Control of Network Systems*, 2015. Accepted. (pdf)**S. Coogan**, E. A. Gol, M. Arcak, C. Belta, “Controlling a network of signalized intersections from temporal logical specifications,”*Proceedings of the 2015 American Control Conference*, 2015, pp. 3919–3924. (pdf)**S. Coogan**, M. Arcak, “Efficient finite abstraction of mixed monotone systems,”*Proceedings the the 18th ACM International Conference on Hybrid Systems: Computation and Control*, 2015, pp. 58–67. (pdf).**Best student paper award****S. Coogan**, M. Arcak, “Freeway traffic control from linear temporal logic specifications,”*Proceedings of the 5th ACM/IEEE International Conference on Cyber-Physical Systems*, 2014, pp. 36–47. (pdf)

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).

**S. Coogan**, G. Gomes, E. Kim, M. Arcak, P. Varaiya, “Offset optimization for a network of signalized intersections via semidefinite relaxation,” 2015. Submitted.

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.

- D. Sadigh, E. S. Kim,
**S. Coogan**, S. Sastry, S. Seshia, “A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications,”*Proceedings of the 52nd IEEE Conference on Decision and Control*, 2013, pp. 5951–5956. (pdf)

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.

**S. Coogan**, M. Arcak, “ Stability of Traffic Flow Networks with a Polytree Topology,”*Automatica*, 2015. Provisionally accepted. (pdf)**S. Coogan**, M. Arcak, “A compartmental model for traffic networks and its dynamical behavior,”*IEEE Transactions on Automatic Control*, to appear 2015. Accepted. (pdf, extended arXiv)**S. Coogan**, M. Arcak, “Dynamical properties of a compartmental model for traffic networks,”*Proceedings of the 2014 American Control Conference*, 2014, pp. 2511–2516. (pdf)

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.

**S. Coogan**, M. Arcak, “A computational approach to synthesizing guards for hybrid systems,”*Systems & Control Letters*, vol. 73, pp. 25–32, Nov. 2014. (pdf)**S. Coogan**, M. Arcak, “Guard synthesis for safety of hybrid systems using sum of squares programming,”*Proceedings of the 51st IEEE Conference on Decision and Control*, 2012, pp. 6138–6143. (pdf)

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.

**S. Coogan**, M. Arcak, “A dissipativity approach to safety verification for interconnected systems,”*IEEE Transactions on Automatic Control*, vol. 60, pp. 1722–1727, June 2015. (pdf)**S. Coogan**, M. Arcak, “Verifying safety of interconnected passive systems using SOS programming,”*Proceedings of the 52nd IEEE Conference on Decision and Control*, 2013, pp. 5951–5956. (pdf)

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.

**S. Coogan**, M. Arcak, “Scaling the size of a formation using relative position feedback,”*Automatica*, vol. 48, no. 10, pp. 2677–2685, Oct. 2012. (pdf)**S. Coogan**, M. Arcak, “Formation control with size scaling using relative displacement feedback,”*Proceedings of the 2012 American Control Conference*, 2012, pp. 3877–3882. (pdf)**S. Coogan**, M. Arcak, M. Egerstedt, “Scaling the size of a multiagent formation via distributed feedback,”*Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference*, 2011, pp. 994–999. (pdf)

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.

**S. Coogan**, L. Ratliff, D. Calderone, C. Tomlin, S. Sastry, “Energy management via pricing in LQ dynamic games,”*Proceedings of the 2013 American Control Conference*, 2013, pp. 443–448. (pdf)- L. Ratliff,
**S. Coogan**, D. Calderone, S. Sastry, “Pricing in linear-quadratic dynamic games,”*Proceedings of the Fiftieth Annual Allerton Conference on Communication, Control, and Computing*, 2012, pp. 1798–1805. (pdf)

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.