CAREER: Correct-By-Design Control of Traffic Flow Networks

现代城市容纳的人口比以往任何时候都多，导致交通网络达到或接近满负荷运行。此外，下一代交通系统将包括互联车辆、互联基础设施和自动化程度的提高，在可预见的未来，这些进步必须与传统技术共存。为了适应这些快速发展的进步，需要更智能、更有效地使用现有的基础设施，并保证性能、安全性和互操作性。本项目的目标是发展大规模交通网络交通流控制的基础理论和领域驱动技术。廉价传感器、无线技术和物联网（IoT）的最新进展使车辆和基础设施实现了实时连接，为高效优化的交通系统提供了丰富的数据和前所未有的机会。主要的技术目标是开发设计正确的技术和算法，确保这些运输系统满足所需的操作规范。为了实现这一目标，该项目将首先从丰富的数据流中开发交通流模型，然后利用这些模型来实现可扩展的控制方法。此外，本计画将整合一项雄心勃勃的教育计划，其中包括重新设计的本科生控制理论入门课程。这门课程将被重新调整，重点关注现代控制领域的挑战，并在控制大挑战设计竞赛中达到高潮，学生们将为一辆自动驾驶的比例模型汽车设计一个控制器，然后用他们的设计进行比赛。为了实现满足交通网络丰富设计规范要求的系统，该项目将特别侧重于将验证和综合的正式方法的强大技术引入大规模物理网络。这些形式化方法最初是为指定和验证软件和硬件系统的正确行为而开发的，现在一个重要的研究目标是确保这些方法在应用于物理控制系统时是可扩展的、可适应的和可靠的。该项目将侧重于以下目标：i)发展交通网络动态行为的理论和模型，捕捉特定领域的现象，如拥堵传播；ii)确定交通流动态将如何随着车辆越来越多地配备自主能力而变化；iii)识别和利用交通流网络的内在结构，以实现可扩展的形式化方法进行验证和综合；iv)利用通过行业合作获得的数据来开发概率正确的交通流网络控制。由于运输系统的复杂性和相互依赖性日益增加，临时办法已不够用，因此这些目标解决了日益需要系统地保证交通网络的性能。该项目的研究活动将使用通过与工业界的持续合作获得的真实交通数据。该项目的预期成果是一套可扩展的算法，将通过此次合作在试点交通网络上进行测试。此外，该项目将建立适用于交通领域以外的基础理论。

Modern cities accommodate more people than ever before, leading to transportation networks that operate at or near capacity. In addition, the next generation of transportation systems will include connected vehicles, connected infrastructure, and increased automation, and these advances must coexist with legacy technology into the foreseeable future. Accommodating these rapidly developing advancements requires smarter and more efficient use of existing infrastructure with guarantees of performance, safety, and interoperability. The goal of this project is to develop fundamental theory and domain-driven techniques for controlling traffic flow in large-scale transportation networks. Recent advances in inexpensive sensors, wireless technology, and the Internet of Things (IoT) enable real-time connectivity of vehicles and infrastructure that offers abundant data and unprecedented opportunities for efficient and optimized transportation systems. The main technical goal is to develop techniques and algorithms that are correct-by-design, ensuring that these transportation systems satisfy required operating specifications. In pursuit of this goal, the project will first develop models of traffic flow from rich data streams and then will leverage these models to enable scalable control approaches. In addition, this project will integrate an ambitious education plan that includes a redesigned introductory course in control theory for undergraduates. The course will be restructured to focus on modern challenges in control, culminating in a Control Grand Challenge design competition in which students will design a controller for an autonomous, scale-model car and then compete with their design. To achieve systems that satisfy the rich design specifications demanded of traffic networks, the project will especially focus on bringing powerful techniques from formal methods for verification and synthesis to large-scale physical networks. These formal methods were originally developed for specifying and verifying the correct behavior of software and hardware systems, and an important research objective now is to ensure these approaches are scalable, adaptable, and reliable when applied to physical control systems. The project will focus on the following objectives: i) Develop theory and models for the dynamic behavior of traffic networks that captures domain-specific phenomena such as congestion propagation, ii) Determine how traffic flow dynamics will change as vehicles are increasingly equipped with autonomous capabilities, iii) Identify and exploit intrinsic structure in traffic flow networks to enable scalable formal methods for verification and synthesis, and iv) Use data available through industry collaborations to develop probabilistically correct control of traffic flow networks. These objectives address a growing need for systematic guarantees of performance in traffic networks as the increasing complexity and interdependence of transportation systems renders ad hoc approaches insufficient. The research activities of this project will use real traffic data available through ongoing collaborations with industry. An expected outcome of this project is a suite of scalable algorithms that will be tested on a pilot traffic network available through this collaboration. In addition, the project will establish foundational theory applicable outside the traffic domain.