Cristian-Ioan Vasile successfully defended his PhD thesis titled Motion Planning and Control: A Formal Methods Approach
Derya Aksaray is moving to a postdoctoral position at MIT: Computer Science and Artificial Intelligence Laboratory.
The new BU Robotics Lab was featured in the January 30 issue of New Scientist. The full article is available at https://www.newscientist.com/article/2075364-future-delivery-drones-start-learning-how-to-fly-on-their-own/
We bring together synthetic biology and micron-scale robotics to engineer the emergence of desired behaviors in populations of bacterial and mammalian cells. This project is supported by a National Science Foundation (NSF) five-year, $4.5 million Cyber-Physical Systems Program (CPS) Frontier grant.Drawing on experts in control theory, computer science, synthetic biology, robotics and design automation, the team includes Professor Calin Belta (ME, ECE, SE), the lead principal investigator, and Assistant Professor Douglas Densmore (ECE, BME, Bioinformatics) from the BU College of Engineering; University of Pennsylvania Professor Vijay Kumar; and MIT Professor Ron Weiss, who directs the Institute’s Synthetic Biology Center; and members of SRI International.
NSF press release
BU COE press release:
Collaboration with DENSO Corporation, Japan on anomaly learning and monitoring for automotive systems
Anomaly detection is the problem of finding patterns from data that do not conform to “expected” or “normal” behavior. Anomaly detection has been used in a wide range of applications, such as intrusion detection for cyber-security, fault detection in safety critical systems, video surveillance of illicit activities, and maritime surveillance. In this project, we focus on automotive applications, where there seems to be a particular need for systems that can automatically monitor, detect, and respond to such behaviors. To this goal, we bring together concepts and tools from formal methods and machine learning.
The HyNeSs lab joined the MIT-led National Science Foundation Science and Technology Center on “Emergent Behaviors of Integrated Cellular Systems”. More information at: ebics.net
NSF CPS- 1446151: Synergy: Collaborative Research: Efficient Traffic Management: A Formal Methods Approach, Role: PI of BU team (collaboration with UC Berkeley)
Abstract (also available at http://www.nsf.gov/awardsearch/showAward?AWD_ID=1446151&HistoricalAwards=false)
Title: Efficient Traffic Management: A Formal Methods Approach
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. This project extends this formalism to traffic networks where correctness specifications include eliminating congestion, ensuring that the freeway throughput remains over a minimum threshold, that queues are always eventually emptied, etc. The task is then to design signal timing and ramp metering strategies to meet such specifications. To accomplish this task, the project takes advantage of the inherent structure of existing, validated mathematical models of traffic flow and develops computationally efficient design techniques. The results are tested with real traffic data from the Interstate 210 travel corridor in Southern California. The educational component of the project includes course development on modeling and control of traffic networks, featuring in particular the formal methods approach of this project, and organizing workshops to train traffic engineers and operation practitioners on the use of software tools and methodologies of the project.
To meet rich control objectives expressed using temporal logic, the project exploits the piecewise affine nature of existing, validated traffic models, and derives efficient finite state abstractions that form the basis of correct-by-construction control synthesis. To ensure scalability, the project further takes advantage of inherent monotonicity properties and decomposibility into sparsely connected subsystems. The first research task is to develop a design framework for signal timing and ramp metering strategies for signalized intersections and freeway traffic control. The second task is the coordinated control of freeway onramps and nearby signalized intersections to address situations such as a freeway demand surge after a sporting event, or an accident on the freeway when signal settings must be adjusted to favor a detour route. The third task is to pursue designs that exploit the statistics of demand for probabilistic correctness guarantees, as well as designs that incorporate optimality requirements, such as minimizing travel time. Validation of the results is pursued with high-fidelity simulation models calibrated using traffic data from the Interstate 210 travel corridor.
Abstract (also available at http://www.nsf.gov/awardsearch/showAward?AWD_ID=1426907)
How much autonomy should a robotic system have in a safety critical application? The proposed project addresses this fundamental question. Consider a disaster relief scenario in which an autonomous aerial vehicle (a robot) is required to monitor some areas of interest, while fighting fires and searching for survivors. The survivors should be provided medical assistance and the fires should be extinguished, with priority given to stabilizing and extracting survivors. During the mission, the aerial vehicle should stay away from areas where explosions are likely, so it can continue to do its job. An emergency medical technician (EMT) and firefighter specify the robot?s mission in a way that can be easily understood by the robot. During the execution, depending on what is discovered, the robot makes decisions on its own as long as the high-level specification is not violated. If this is not the case (e.g., there is an obstacle blocking the access to a survivor), the system initiates a dialog with the firefighter and EMT, who provide instructions to help the robot safely cope with the unexpected situation. The research plan of this project is integrated with an education and outreach plan that includes a rich spectrum of robotic-related activities for university and high-school students.
This research project combines ideas and techniques from robot motion planning, formal verification, and control theory to provide a rigorous answer to the question of how much autonomy a robot should be given. A specification language inspired by temporal logics is used to communicate the mission to the robot, whose motions are directed by a hierarchical controller. At the top level, automata game techniques and two discretization schemes, one based on cellular decomposition and the other one on randomized sampling, are used. At the low level, input-output linearization combined with path and vector field following are used to implement the high level plans in quadrotors and differential drive ground vehicles. The human-robot negotiation process is based on the internal representation of temporal logic formulas and their quantitative semantics. While directed at robotics, the project impacts a number of safety critical areas, such as cyber physical systems (construction of correct-by-design systems), air traffic control (design of safe minimum-energy paths for airplanes taking off and landing in a crowded airport), etc.
NSF CMMI-1400167: “Combining Optimality and Correctness in Control Systems”, Role: PI (single PI)
Abstract (also available at http://www.nsf.gov/awardsearch/showAward?AWD_ID=1400167&HistoricalAwards=false)
Optimal control is an area of engineering focused at maintaining systems close to desired behaviors, while at the same optimizing certain costs. Examples include driving a vehicle along a trajectory while minimizing fuel consumption, controlling a set of thermostats in a building to follow a desired temperature profile while maintaining electricity consumption to a minimum, etc. Formal verification is an area of computer science focused at proving the correctness of system designs. The systems are computer programs and digital circuits, while correctness specifications include safety (making sure nothing bad happens) and liveness (making sure something good eventually happens). With the increasing integration of physical and digital systems into safety critical cyber physical systems, there is a need for computational tools that combine optimal control and correctness requirements. This project establishes a connection between optimal control and formal verification and impacts a large number of areas where correctness and optimality are crucial, such as air traffic control (design safe minimum-energy paths for airplanes taking off and landing in a crowded airport), vehicle autonomy (e.g., persistent surveillance for disaster relief), medical robotics (optimality and safety are fundamental in the robotic needle steering problem), etc. The education and outreach plan includes related courses at the undergraduate and graduate level, the involvement of undergraduate and high school students in research, collaborations with elementary school robotics teams, and the involvement of the Principal Investigator in high school summer internship programs.
The results of this project will include formulations and solutions to optimal control problems with correctness requirements expressed as temporal logic formulas for both finite and infinite systems, in both probabilistic and non-probabilistic setups. The systems under consideration are finite-state transition systems and Markov decisions processes, and infinite-state discrete-time (stochastic) linear systems and piecewise affine systems. Correctness is specified as formulas of Linear Temporal Logic. The optimization objectives include classical average costs per stage and quadratics over state and control variables, as well as some special costs induced by particular specifications. Central to the approach are receding-horizon implementations of the optimal control strategies. The main application area is autonomous vehicle control for search and rescue in disaster relief scenarios.