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.