Word cloud obtained from concatenating the introduction sections of my published papers!

Efficient Traffic Management

We are seeking formal methods approaches to control traffic network. We use formal control synthesis and verification tools to reason about certain behaviors for the vehicular flow. We find control policies for signalizing intersections and design ramp metering strategies that guarantee behaviors such as avoidance of gridlocks, liveness of traffic flow in all the transportation links and desired temporal constraints on the traffic signals. Using formal methods, we treat transportation networks as the way computer software are designed and verified. Using assume-guarantee reasoning schemes, we are able to scale our methods to large networks of arterial and freeway traffic and their combination.

Optimal and Robust Control from Timed Temporal Logic Specifications

We seek control strategies for linear and piecewise affine systems from rich, complex specifications described by temporal logics. Using set-invariance theories, we construct control invariant sets  that correspond to the behavior desired by the specification. We find controls optimally in a receding horizon fashion subject to the system constraints and invariant sets. We are able to provide performance guarantees for our approach.

Controlling a Group of Robots from Spatio-Temporal Logic Specifications

We use spatio-temporal logic (SpaTeL) to describe mission specifications for a group of planar robots. SpaTel enables describing both robotic configurations and time varying requirements in a natural and convenient way. We provide an automated method to optimally control the robots with minimum total displacements.