1. Verification and control of continuous and hybrid systems

In control problems, "complex" models, such as systems of differential equations, are usually checked against "simple" specifications, such as stability, set invariance, controllability and observability. In formal analysis (verification), "rich" specifications such as languages and formulas of temporal logics, are checked against "simple" models of software programs and digital circuits, such as (finite) transition graphs. The most widespread specifications include safety, i.e., something bad never happens and liveness, i.e., something good eventually happens. We are developing computational tools for bridging in this gap, and therefore allowing for specifying the properties of continuous and hybrid systems in a rich language, with automatic verification and controller synthesis.

2. Formal approaches to planning and control of robot motion

Robot motion tasks are usually specified simply as "Go form A to B and avoid collisions". By using tools from formal methods, concurrency, and control theory, we extend motion specification languages to arbitrary temporal and logic statements given in natural language, and develop tools for provably correct automatic deployment of robots and teams of robots from such specifications.

2.1 Hierarchical abstractions for planning and control of robotic swarms

Specifying, planning, and controlling the motion of very large teams of small and inexpensive mobile robots, or swarms, is a challenging problem. We use tools from differential geometry and formal analysis to construct a hierarchical abstraction framework for robotic swarms. In this framework, high level swarm specifications given in terms of temporal and logic statements about a small set of essential features of the swarm are automatically converted into provably correct robot control and local communication strategies.

2.2 Automatic deployment of autonomous cars in a miniature Robotic Urban-Like Environment (RULE).

RULE is an experimental platform for automatic deployment of robotic cars in an urban-like environment. The cars are Khepera III miniature robots with processing, sensing, and communication capabilities. The "city" has streets, intersections, traffic lights, and parking spots, and can be easily reconfigured. The goal is to be able to simultaneously deploy multiple cars from human-like, rich specifications about visiting regions of interest in the city such as "Visit Road 1 and then Road 2, in this order, infinitely often. If Intersection 1 is ever reached, then Road 4 should never be entered. Park in the next available parking slot", etc.

3. Modeling, analysis, and control of bacterial metabolic and gene networks

Bacteria continuously respond to environmental changes through a complicated mechanism consisting of an interplay between metabolic and genetic networks. Through hundreds of chemical reactions, the metabolic network converts nutrients from the environment to elements necessary for growth and survival of the cell. Most of these chemical reactions are regulated by enzymes produced by a genetic network. In turn, the expression of the genes from the genetic network is regulated by its own products and metabolites produced by the metabolic network.

3.1 Genome scale metabolic analysis

We use tools from convex analysis to study the robustness of metabolism to mutations and environmental changes, to understand evolutionary constraints, and to design gene perturbations and environmental conditions leading to specific desired phenotypes.

3.2 Modeling, analysis, synthesis, and control of gene networks

By using techniques from formal analysis and control theory, we develop tools for analysis, synthesis, and control of gene networks. We are particularly interested in synthetic gene networks.