CPS: Synergy: Collaborative Research: Efficient Traffic Management: A Formal Methods Approach

题目：有效的交通管理：一种正式方法这个项目的目标是开发一种正式的交通管理方法。形式化方法是计算机科学的一个领域，它发展了有效的技术来证明系统的正确操作，如计算机程序和数字电路，以及设计结构正确的系统。本项目将这种形式扩展到交通网络，其中正确性规范包括消除拥塞，确保高速公路吞吐量保持在最小阈值以上，队列最终总是清空等。然后的任务是设计信号时序和匝道计量策略，以满足这些规范。为了完成这项任务，该项目利用了现有的、经过验证的交通流数学模型的固有结构，并开发了计算效率高的设计技术。研究结果用南加州210州际公路的真实交通数据进行了测试。项目的教育部分包括交通网络建模和控制的课程开发，特别是该项目的正式方法方法，并组织研讨会，培训交通工程师和运营从业者使用软件工具和项目的方法。为了满足使用时间逻辑表达的丰富控制目标，该项目利用了现有的、经过验证的交通模型的分段仿射特性，并派生出有效的有限状态抽象，这些抽象构成了构造正确控制综合的基础。为了确保可扩展性，该项目进一步利用了固有的单调性和可分解性，并将其分解为稀疏连接的子系统。第一个研究任务是开发一个用于信号交叉口和高速公路交通控制的信号配时和匝道计量策略的设计框架。第二项任务是协调控制高速公路匝道和附近的信号交叉口，以解决诸如体育赛事后高速公路需求激增或高速公路上发生事故时必须调整信号设置以有利于绕行路线的情况。第三个任务是追求利用概率正确性保证的需求统计数据的设计，以及包含最优性要求的设计，例如最小化旅行时间。通过使用210州际公路旅行通道的交通数据校准的高保真仿真模型来验证结果。

Title: Efficient Traffic Management: A Formal Methods ApproachThe 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.