Abstract: This poster summarizes our recently awarded grant on computationally aware cyber-physical systems (CPSs). The objective of this project is to generate new fundamental science for CPSs that enables more accurate and faster trajectory synthesis for controllers with nonlinear plants, or nonlinear constraints that encode obstacles. The approach is to utilize hybrid control to switch between models whose accuracy is normalized by their computational burden.

Abstract: KeYmaera X is a theorem prover for specifying and verifying correctness properties of hybrid systems (systems that mix discrete and continuous dynamics). KeYmaera X implements differential dynamic logic (dL) and provides a high degree of control over automated proof search.

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: Scientific challenges: How can multiple cooperative cyber-physical systems communicate and coordinate to accomplish complex high-level tasks within unknown, dynamic and adversarial environments?

Abstract: The project aims to establish a Cyber-Physical Infrastructure for urban environments and address fundamental problems that involve data collection, resource allocation, real-time decision making, safety, and security.

Abstract: Despite the integration of advanced cyber technologies in monitoring and communication in electric power networks, design and development of control systems, and in particular, Remedial Action Schemes (RAS) tend to evolve at a very slow pace. The objective of this research is to study new distributed system modeling techniques to faithfully capture the physical and communication  system characteristics  as well as the "wave" like propagation of some disturbances.

Abstract: Motivation and goal: The whole-system design and modeling of complex medical robotics involves analog sensors and actuators; discrete software controllers; piecewise, non-linear, discontinuous biological tissues/media; and probabilistic human administrators. In the best case, the failure of such systems risks limb. In the worst, life.