Embedded systems, from automobiles and aircraft to autonomous robots for space exploration, are becoming ubiquitous. A future is envisioned in which large networks of increasingly autonomous embedded systems operate robustly and reliably. Increased levels of automation will require to on-line represent and process huge amounts of data for the design of control schemes that guarantee safety while maintaining performance. A bottleneck in advancement in this direction is complexity. Complexity is established by the natural scale of the system and by the interaction of the physical devices with logic-based control, which create a large number of system behaviors. Current methods in the control synthesis in embedded and hybrid systems usually assume small system size and perfect state measurements. While in some cases such assumptions are satisfied, several realistic applications have large system size and imperfect or partial measurements.
To address these problems, this NSF CAREER project is developing a dynamic feedback approach (state estimation plus control) for the monitoring and recovery of multi-agent systems modeled as infinite state transition systems with logic and timed transitions. This approach relies on partial order theory as a key enabler to overcome computational difficulties arising from large system size and from the interaction of continuous evolution and logic. By exploiting partial order structures on the set of states and inputs, this method provides an efficient alternative to enumeration approaches and exhaustive searches, which are common practice in embedded programming. This research is expected to extend our current ability to build provably safe and reliable large-scale multi-agent systems, with potential impact on railway and air traffic control systems, intelligent transportation systems, and large robot teams in adversarial environments
are ubiquitous in our lives, from transportation networks, to air-traffic control, to the power grid, to smart homes. These systems comprise physical devices, such as vehicles or aircrafts, and embedded computation and wireless communication ability. The continuous decrease of computation and wireless communication technology are pushing these systems toward increased levels of autonomy. A major example is transportation systems, in which vehicles are being equipped with systems that allow them to talk to each other and with the surrounding infrastructure to warn the driver of incoming collisions and to eventually issue overrides to ensure safety. While the potential for improvement in terms of safety, efficiency, and comfort is enormous, the main concern is how to design these systems so that they are provably safe. This is crucial given their life-critical role. Addressing this concern is particularly difficult given that these systems are hybrid, that is, they are described by both Newton’s laws and by logic rules, they are high-dimensional (there are many agents), and only partial information is often available to any given agent. Because of these characteristics, formal methods developed in control theory and computer science to design systems in such a way that they are provably safe are often of limited applicability due to computational complexity bottlenecks. In this project, we have focused on transportation networks, and have developed techniques for safety verification and design, which leverage the structure of the application domain to obtain algorithms with linear and polynomial complexity. These techniques exploit the fact that the continuous system dynamics are order preserving, that is, larger inputs lead to larger displacements and speeds. In particular, imperfect information, due to missing communication or noisy sensors, is explicitly accounted for in the design and verification tasks. The algorithms were demonstrated on an experimental test-bed composed of in-scale dynamic vehicles engaged in several cooperative and competitive negotiations of roundabouts, merges, and intersections, involving also human-driven vehicles. We believe that the techniques that we have developed will be used by the automotive industry to solve verification and design tasks of safety-critical systems. Our work will thus contribute to making ubiquitous systems, such as intelligent transportation, safer and more efficient.
