Abstract: The objective of this research is to develop tools for comprehensive design and optimization of air traffic flow management capabilities at multiple spatial and temporal resolutions: at a national airspace-wide scale and one-day time horizon (strategic time- frame); and at a regional scale (of one or a few Centers) and a two-hour time horizon (tactical time-frame). The following results were obtained in Year 4 of the project:

Abstract: Networks of autonomous coordinated robots areprototypical examples of cyber-physical systems. Already today and increasingly in the near future, robotic systems will perform a broad range of environmental monitoring and logistic tasks. Aquatic robots will monitor oceanic life and conditions. Teams of vehicles will perform exploration, firefighting and search and rescue operations.

Abstract: Oceans are drivers of global climate; they are home to some of our most important and diverse ecosystems; and they provide a substantial amount to the world’s economy as a major source of food and employment. Sound plays a vital role in the ocean ecosystem, as many organisms rely on the acoustic environment for navigation, communication, detecting predators and finding food.

Abstract: Trustworthy operation of next-generation complex power grid critical infrastructures requires mathematical and practical verification solutions to guarantee the correct infrastructural functionalities. This project develops the foundations of theoretical modeling, synthesis and real-world deployment of a formal and scalable controller code verifier for programmable logic controllers (PLCs) in cyber-physical settings. PLCs are widely used for control automation in industrial control systems.

Abstract: The objective of this project is to develop a distributed algorithmic framework, supported by a highly fault-tolerant software system, for executing critical transmission-level operations of the North American power grid using gigantic volumes of Synchrophasor data.

Abstract: The research objective of this project is to bridge two disparate paths to the control of hybrid dynamical systems—namely, symbolic model-based and Lyapunov analysis-based approaches—via convex programming in order to address major challenges in hybrid control. Hybrid systems are characterized by the presence of both continuous dynamics and discrete logic that interact with each other.

Abstract: The verification of hybrid systems requires ways of handling both the discrete and continuous dynamics, e.g., by proofs, abstraction, or approximation. Fundamentally, however, the study of the safety of hybrid systems can be shown to reduce constructively to the problem of generating invariants for their differ- ential equations. We recently focused on this core problem. We study the case of algebraic invariant equation, i.e. invariants described by a polynomial equation of the form p = 0 for a polynomial p.

Abstract:  Understanding failure in protection system using Temporal Causal Diagrams  Situational  awareness  in  large  electrical  systems  and  eventual  fault  source  identification  and  possibly prognostics is a very challenging problem. State of the art relies on a network of protection devices that include relays to detect anomalies and engage circuit breakers to isolate the faulty component(s) in the system.

Abstract: We are at the end of a four­year effort that has dramatically improved the capability of the use of RF sensors, particularly those that measure received signal strength (RSS) to sense the locations and context of people in buildings and homes.  We have investigated both systems which use RFID tags to identify a person or object, and those which use a static deployed network of transceivers for device­free localization, to locate people moving in the environment who do not carry any tag or device.  Locating people who don’t wear a de

Abstract: The objective of this project is to develop a formal methods approach to traffic management. Formal methods is an area of computer science that develops efficient techniques for proving the correct operation of systems, such as computer programs and digital circuits, and for designing systems that are correct by construction.