Showing 1–2 of 2 results for author: Zaki, M H
-
Towards formalization and monitoring of microscopic traffic parameters using temporal logic
Authors:
Mariam Nour,
Mohamed H. Zaki
Abstract:
Smart cities are revolutionizing the transportation infrastructure by the integration of technology. However, ensuring that various transportation system components are operating as expected and in a safe manner is a great challenge. In this work, we propose the use of formal methods as a means to specify and reason about the traffic network's complex properties. Formal methods provide a flexible…
▽ More
Smart cities are revolutionizing the transportation infrastructure by the integration of technology. However, ensuring that various transportation system components are operating as expected and in a safe manner is a great challenge. In this work, we propose the use of formal methods as a means to specify and reason about the traffic network's complex properties. Formal methods provide a flexible tool to define the safe operation of the traffic network by capturing non-conforming behavior, exploring various possible states of the traffic scene, and detecting any inconsistencies within it. Hence, we develop specification-based monitoring for the analysis of traffic networks using the formal language, Signal Temporal Logic. We develop monitors that identify safety-related behavior such as conforming to speed limits and maintaining appropriate headway. The framework is tested using a calibrated micro-simulated highway scenario and offline specification-based monitoring is applied to individual vehicle trajectories to understand whether they violate or satisfy the defined safety specifications. Statistical analysis of the outputs show that our approach can differentiate violating from conforming vehicle trajectories based on the defined specifications. This work can be utilized by traffic management centers to study the traffic stream properties, identify possible hazards, and provide valuable feedback for automating the traffic monitoring systems.
△ Less
Submitted 12 October, 2021;
originally announced October 2021.
-
Exploring DMD-type Algorithms for Modeling Signalised Intersections
Authors:
Kazi Redwan Shabab,
Shakib Mustavee,
Shaurya Agarwal,
Mohamed H. Zaki,
Sajal Das
Abstract:
This paper explores a novel data-driven approach based on recent developments in Koopman operator theory and dynamic mode decomposition (DMD) for modeling signalized intersections. Vehicular flow and queue formation on signalized intersections have complex nonlinear dynamics, making system identification, modeling, and controller design tasks challenging. We employ a Koopman theoretic approach to…
▽ More
This paper explores a novel data-driven approach based on recent developments in Koopman operator theory and dynamic mode decomposition (DMD) for modeling signalized intersections. Vehicular flow and queue formation on signalized intersections have complex nonlinear dynamics, making system identification, modeling, and controller design tasks challenging. We employ a Koopman theoretic approach to transform the original nonlinear dynamics into locally linear infinite-dimensional dynamics. The data-driven approach relies entirely on spatio-temporal snapshots of the traffic data. We investigate several key aspects of the approach and provide insights into the usage of DMD-type algorithms for application in adaptive signalized intersections. To demonstrate the utility of the obtained linearized dynamics, we perform prediction of the queue lengths at the intersection; and compare the results with the state-of-the-art long short term memory (LSTM) method. The case study involves the morning peak vehicle movements and queue lengths at two Orlando area signalized intersections. It is observed that DMD-based algorithms are able to capture complex dynamics with a linear approximation to a reasonable extent.
△ Less
Submitted 13 July, 2021;
originally announced July 2021.