In the next few decades, autonomous vehicles will become an integral part of the traffic flow on highways. However, they will constitute only a small fraction of all vehicles on the road. This research develops technologies to employ autonomous vehicles already in the stream to improve traffic flow of human-controlled vehicles. The goal is to mitigate undesirable jamming, traffic waves, and to ultimately reduce the fuel consumption. Contemporary control of traffic flow, such as ramp metering and variable speed limits, is largely limited to local and highly aggregate approaches. This research represents a step towards global control of traffic using a few autonomous vehicles, and it provides the mathematical, computational, and engineering structure to address and employ these new connections. Even if autonomous vehicles can provide only a small percentage reduction in fuel consumption, this will have a tremendous economic and environmental impact due to the heavy dependence of the transportation system on non-renewable fuels. The project is highly collaborative and interdisciplinary, involving personnel from different disciplines in engineering and mathematics. It includes the training of PhD students and a postdoctoral researcher, and outreach activities to disseminate traffic research to the broader public. This project develops new models, computational methods, software tools, and engineering solutions to employ autonomous vehicles to detect and mitigate traffic events that adversely affect fuel consumption and congestion. The approach is to combine the data measured by autonomous vehicles in the traffic flow, as well as other traffic data, with appropriate macroscopic traffic models to detect and predict congestion trends and events. Based on this information, the loop is closed by carefully following prescribed velocity controllers that are demonstrated to reduce congestion. These controllers require detection and response times that are beyond the limit of a human's ability. The choice of the best control strategy is determined via optimization approaches applied to the multiscale traffic model and suitable fuel consumption estimation. The communication between the autonomous vehicles, combined with the computational and control tasks on each individual vehicle, require a cyber-physical approach to the problem. This research considers new types of traffic models (micro-macro models, network approaches for higher-order models), new control algorithms for traffic flow regulation, and new sensing and control paradigms that are enabled by a small number of controllable systems available in a flow.

This project addresses the foundational problem of knowledge within cyber-physical systems (CPS), i.e., systems that combine aspects such as communication, computation, and physics. A single system observes its environment through sensors and interacts through actuators. Neither is perfect. Thus, the CPS's internal view of the world is blurry and its actions are imprecise. CPS are still analyzed with methods that do not distinguish between truth in the world and an internal view thereof, resulting in a mismatch between the behavior of theoretical models and their real-world counterparts. How could they be trusted to perform safety-critical tasks? This project addresses this critical insufficiency by developing methods to reason about knowledge and learning in CPS. The project pursues the development of new logical principles for verifying knowledge-aware CPS. This project investigates how to make the mismatch between the world and the partial perception through sensors explicit and how to achieve provably correct control in theory as well as practice despite this mismatch. By investigating changing knowledge in a changing world, this project contributes to a fundamental feature without which CPS can never be truly safe and efficient at the same time. The project's broader significance and importance are a result of the widespread attention that CPS gain in many safety-critical areas, such as in aviation and automotive industries. One reason for safety gaps in such CPS is that formal verification techniques are still largely knowledge-agnostic, and verifiable solutions overly pessimistic. This project addresses these issues and provides tools that allow for incorporating knowledge about the environment's intentions into the models to derive provably correct, but justifiably optimistic, and thus efficient, behavior. By their logical nature, these techniques are applicable to a wide range of CPS and, thus, contribute significantly to numerous applications. Results obtained within this project will be demonstrated in CPS models and laboratory robot scenarios, and will be shared in courses and with industrial partners. The technical approach that this project pursues develops a new modeling language, logic, and proof calculus for verifying knowledge-aware CPS. The knowledge paradigm used allows CPS controllers to seamlessly acquire knowledge about the world but also about other agents in the system, i.e., other controllers. Knowledge is the key to interactions between different agents. This project investigates how an explicit model of world perception and agent intentions - and knowledge of these perceptions and intentions - allows CPS agents to act, based on more efficient, but still provably safe control in multi-agent scenarios. The methods will be implemented in the verification tool KeYmaera and demonstrated in formal verification on different case study applications such as car scenarios.

In the next few decades, autonomous vehicles will become an integral part of the traffic flow on highways. However, they will constitute only a small fraction of all vehicles on the road. This research develops technologies to employ autonomous vehicles already in the stream to improve traffic flow of human-controlled vehicles. The goal is to mitigate undesirable jamming, traffic waves, and to ultimately reduce the fuel consumption. Contemporary control of traffic flow, such as ramp metering and variable speed limits, is largely limited to local and highly aggregate approaches. This research represents a step towards global control of traffic using a few autonomous vehicles, and it provides the mathematical, computational, and engineering structure to address and employ these new connections. Even if autonomous vehicles can provide only a small percentage reduction in fuel consumption, this will have a tremendous economic and environmental impact due to the heavy dependence of the transportation system on non-renewable fuels. The project is highly collaborative and interdisciplinary, involving personnel from different disciplines in engineering and mathematics. It includes the training of PhD students and a postdoctoral researcher, and outreach activities to disseminate traffic research to the broader public. This project develops new models, computational methods, software tools, and engineering solutions to employ autonomous vehicles to detect and mitigate traffic events that adversely affect fuel consumption and congestion. The approach is to combine the data measured by autonomous vehicles in the traffic flow, as well as other traffic data, with appropriate macroscopic traffic models to detect and predict congestion trends and events. Based on this information, the loop is closed by carefully following prescribed velocity controllers that are demonstrated to reduce congestion. These controllers require detection and response times that are beyond the limit of a human's ability. The choice of the best control strategy is determined via optimization approaches applied to the multiscale traffic model and suitable fuel consumption estimation. The communication between the autonomous vehicles, combined with the computational and control tasks on each individual vehicle, require a cyber-physical approach to the problem. This research considers new types of traffic models (micro-macro models, network approaches for higher-order models), new control algorithms for traffic flow regulation, and new sensing and control paradigms that are enabled by a small number of controllable systems available in a flow.

In the next few decades, autonomous vehicles will become an integral part of the traffic flow on highways. However, they will constitute only a small fraction of all vehicles on the road. This research develops technologies to employ autonomous vehicles already in the stream to improve traffic flow of human-controlled vehicles. The goal is to mitigate undesirable jamming, traffic waves, and to ultimately reduce the fuel consumption. Contemporary control of traffic flow, such as ramp metering and variable speed limits, is largely limited to local and highly aggregate approaches. This research represents a step towards global control of traffic using a few autonomous vehicles, and it provides the mathematical, computational, and engineering structure to address and employ these new connections. Even if autonomous vehicles can provide only a small percentage reduction in fuel consumption, this will have a tremendous economic and environmental impact due to the heavy dependence of the transportation system on non-renewable fuels. The project is highly collaborative and interdisciplinary, involving personnel from different disciplines in engineering and mathematics. It includes the training of PhD students and a postdoctoral researcher, and outreach activities to disseminate traffic research to the broader public. This project develops new models, computational methods, software tools, and engineering solutions to employ autonomous vehicles to detect and mitigate traffic events that adversely affect fuel consumption and congestion. The approach is to combine the data measured by autonomous vehicles in the traffic flow, as well as other traffic data, with appropriate macroscopic traffic models to detect and predict congestion trends and events. Based on this information, the loop is closed by carefully following prescribed velocity controllers that are demonstrated to reduce congestion. These controllers require detection and response times that are beyond the limit of a human's ability. The choice of the best control strategy is determined via optimization approaches applied to the multiscale traffic model and suitable fuel consumption estimation. The communication between the autonomous vehicles, combined with the computational and control tasks on each individual vehicle, require a cyber-physical approach to the problem. This research considers new types of traffic models (micro-macro models, network approaches for higher-order models), new control algorithms for traffic flow regulation, and new sensing and control paradigms that are enabled by a small number of controllable systems available in a flow.

Title: CPS: Breakthrough: Compositional Modeling of Cyberphysical Systems This project is devoted to the discovery of new mathematical modeling techniques for Cyber-Physical Systems. In particular, the research involves devising novel conceptual methods for assembling systems from subsystems, and for reasoning about the behavior of systems in terms of the behavior of their subsystems, which may be computational or physical. The results enable scientists and engineers to develop more realistic models of the systems they are designing, and to obtain greater insights into their eventual behavior, without having to build costly prototypes. The intellectual merits are the new notions of system behavior being developed that unify the computational and the physical, and the mathematical operators and laws governing the relationships between systems and subsystems. The project's broader significance and importance lie in the increased pace of innovation within Cyber-Physical System design that the new modeling techniques make possible, and the curricular enhancements that the novel conceptual frameworks under development support. The specific research program of this project involves the development of a novel modeling paradigm, Generalized Synchronization Trees (GSTs), into a rich framework for both describing Cyber-Physical Systems (CPSs) and studying their behavior under interconnection. GSTs are inspired by Milner's use of Synchronization Trees (STs) to model interconnected computing processes, but GSTs generalize the mathematical structure of their forebears in such a way as to encompass systems with discrete ("Cyber") as well as continuous ("Physical") dynamics. As Milner did with STs, the PIs are developing an algebraic theory of composition for GSTs. Such theories have a particular advantage over non-algebraic ones: because the composition of two (or more) objects results in an object of the same type, composition operators can be nested to build large structures out of smaller ones. Thus, the theory of GSTs is inherently compositional. The development of the theory involves five distinct but complementary endeavors. Standard models for cyber-physical systems are being encoded as GSTs in a semantically robust way; meaningful notions of composition and congruence for CPSs are being described and studied algebraically; the interplay between behavioral equivalence and the preservation of system properties is being investigated; a notion of real-time (or clock time) is under consideration for GSTs; and GSTs are being assessed as modeling tools for practical design scenarios.

This project represents a cross-disciplinary collaborative research effort on developing rigorous, closed-loop approaches for designing, simulating, and verifying medical devices. The work will open fundamental new approaches for radically accelerating the pace of medical device innovation, especially in the sphere of cardiac-device design. Specific attention will be devoted to developing advanced formal methods-based approaches for analyzing controller designs for safety and effectiveness; and devising methods for expediting regulatory and other third-party reviews of device designs. The project team includes members with research backgrounds in computer science, electrical engineering, biophysics, and cardiology; the PIs will use a coordinated approach that balances theoretical, experimental and practical concerns to yield results that are intended to transform the practice of device design while also facilitating the translation of new cardiac therapies into practice. The proposed effort will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behaviors match designers' intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The scientific work being proposed will serve this vision by providing mathematically robust techniques for analyzing and verifying the behavior of medical devices, for modeling and simulating heart dynamics, and for conducting closed-loop verification of proposed therapeutic approaches. The acceleration in medical device innovation achievable as a result of the proposed research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly. It will also yield a collection of tools and techniques that will be applicable in the design of other types of devices. Finally, it will contribute to the development of human resources and the further inclusion of under-represented groups via its extensive education and outreach programs, including intensive workshop experiences for undergraduates.

This project represents a cross-disciplinary collaborative research effort on developing rigorous, closed-loop approaches for designing, simulating, and verifying medical devices. The work will open fundamental new approaches for radically accelerating the pace of medical device innovation, especially in the sphere of cardiac-device design. Specific attention will be devoted to developing advanced formal methods-based approaches for analyzing controller designs for safety and effectiveness; and devising methods for expediting regulatory and other third-party reviews of device designs. The project team includes members with research backgrounds in computer science, electrical engineering, biophysics, and cardiology; the PIs will use a coordinated approach that balances theoretical, experimental and practical concerns to yield results that are intended to transform the practice of device design while also facilitating the translation of new cardiac therapies into practice. The proposed effort will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behaviors match designers' intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The scientific work being proposed will serve this vision by providing mathematically robust techniques for analyzing and verifying the behavior of medical devices, for modeling and simulating heart dynamics, and for conducting closed-loop verification of proposed therapeutic approaches. The acceleration in medical device innovation achievable as a result of the proposed research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly. It will also yield a collection of tools and techniques that will be applicable in the design of other types of devices. Finally, it will contribute to the development of human resources and the further inclusion of under-represented groups via its extensive education and outreach programs, including intensive workshop experiences for undergraduates.

Traditionally, the design of urban transit services has been based on limited sampling data collected through surveys and censuses, which are often dated and incomplete. Lacking massive online feeds from multiple transit modes makes it hard to achieve real-time equilibrium in demand and supply relationship through cyber-control, which eventually manifests into multiple urban transportation issues: (i) lengthy last-mile transit due to non-supply, (ii) prolonged waiting due to undersupply, and (iii) excessive idle mileage due to oversupply. This project addresses these issues by focusing on two types of transportation systems in metropolitan areas: (i) public bike rental sharing systems and (ii) fleet-oriented ride sharing systems. The public bike rental sharing systems are used to allow commuters to rent bikes near public transit stations for the last mile of their trips. The fleet-oriented ride sharing systems schedule a fleet of participating vehicles for ride sharing among passengers in which shared ridership reduces individual fare paid by passengers, increases the profit of taxi drivers, and can improve the availability of service. The theory and practice of transportation sharing systems have typically focused on isolated individual transportation modes. The project will collect massive multi-modal online feeds from metropolitan information infrastructure to model dynamic behaviors of transportation systems, and then utilize massive micro-level trip information to apply fine-grained real-time control to handle rapid changes in dynamic metropolitan environments. General principles and design methodologies will be designed to build multi-modal, integrated urban transportation systems. These research discoveries will be applied toward commercial applications. Long-term deployment problem of bike stations will be addressed, especially in the low-income districts, to provide suggestions on the station deployment and assessment for specific deployment plans. The project also solves the short-term bike maintenance issue to balance the usage of shared bikes to prevent quick deterioration of rental bikes, and improve availability of bike rental services in real time. This project will also study fleet-oriented ride sharing systems that decide fares based on real-time supply/demand ratio to handle dynamic metropolitan scenarios. This project will support two Ph.D. students who will receive innovation and technology translation training through close interactions with municipal governments and small-business companies. Such partnerships expedite the adoption of cutting-edge technology, evaluate research solutions in operational environments, and obtain user feedback to trigger further innovations. The project will improve the efficiency of existing transportation systems under sharing economy and ultimately the work would noticeably improve the quality of every-day life in metropolitan areas across the United States.

One of the challenges for the future cyber-physical systems is the exploration of large design spaces. Evolutionary algorithms (EAs), which embody a simplified computational model of the mutation and selection mechanisms of natural evolution, are known to be effective for design optimization. However, the traditional formulations are limited to choosing values for a predetermined set of parameters within a given fixed architecture. This project explores techniques, based on the idea of hidden genes, which enable EAs to select a variable number of components, thereby expanding the explored design space to include selection of a system's architecture. Hidden genetic optimization algorithms have a broad range of potential applications in cyber-physical systems, including automated construction systems, transportation systems, micro-grid systems, and space systems. The project integrates education with research by involving students ranging from high school through graduate school in activities commensurate with their skills, and promotes dissemination of the research results through open source distribution of algorithm implementation code and participation in the worldwide Global Trajectory Optimization Competition. Instead of using a single layer of coding to represent the variables of the system in current EAs, this project investigates adding a second layer of coding to enable hiding some of the variables, as needed, during the search for the optimal system's architecture. This genetic hiding concept is found in nature and provides a natural way of handling system architectures covering a range of different sizes in the design space. In addition, the standard mutation and selection operations in EAs will be replaced by new operations that are intended to extract the full potential of the hidden gene model. Specific applications include space mission design, microgrid optimization, and traffic network signal coordinated planning.

Securing critical networked cyber-physical systems (NCPSs) such as the power grid or transportation systems has emerged as a major national and global priority. The networked nature of such systems renders them vulnerable to a range of attacks both in cyber and physical domains as corroborated by recent threats such as the Stuxnet worm. Developing security mechanisms for such NCPSs significantly differs from traditional networked systems due to interdependence between cyber and physical subsystems (with attacks originating from either subsystem), possible cooperation between attackers or defenders, and the presence of human decision makers in the loop. The main goal of this research is to develop the necessary science and engineering tools for designing NCPS security solutions that are applicable to a broad range of application domains. This project will develop a multidisciplinary framework that weaves together principles from cybersecurity, control theory, networking and criminology. The framework will include novel security mechanisms for NCPSs founded on solid control-theoretic and related notions, analytical tools that allow incorporation of bounded human rationality in NCPS security, and experiments with real-world attack scenarios. A newly built cross-institutional NCPS simulator will be used to evaluate the proposed mechanisms in realistic environments. This research transcends specific cyber-physical systems domains and provides the necessary tools to building secure and trustworthy NCPSs. The broader impacts include a new infrastructure for NCPS research and education, training of students, new courses, and outreach events focused on under-represented student groups