Towards formalization and monitoring of microscopic traffic parameters using temporal logic

TL;DR

This paper introduces a formal methods framework using Signal Temporal Logic to specify and monitor safety properties in traffic networks, enabling detection of violations and conformities in vehicle trajectories within smart city infrastructure.

Contribution

It develops a specification-based monitoring approach for traffic safety using formal logic, tested on simulated highway data, to identify violations and conformities in real-time vehicle behavior.

Findings

The approach effectively differentiates violating from conforming trajectories.

Statistical analysis confirms the method's reliability in safety assessment.

Framework can assist traffic management in hazard detection and system automation.

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 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.