Monitoring of Traffic Manoeuvres with Imprecise Information

TL;DR

This paper presents a method for monitoring traffic maneuvers using Multi-Lane Spatial Logic, accounting for data errors, by transforming the problem into a decidable first-order theory to verify if spatial properties hold robustly over time.

Contribution

It introduces an approach to verify MLSL properties over transition sequences with data errors by reducing the problem to the first-order theory of real-closed fields, enabling robust monitoring.

Findings

The method can verify MLSL properties with spatial and temporal data errors.

The transformation into real-closed fields makes the verification decidable.

Robustness of MLSL properties under data inaccuracies is effectively checked.

Abstract

In monitoring, we algorithmically check if a single behavior satisfies a property. Here, we consider monitoring for Multi-Lane Spatial Logic (MLSL). The behavior is given as a finite transition sequence of MLSL and the property is that a spatial MLSL formula should hold at every point in time within the sequence. In our procedure we transform the transition sequence and the formula to the first-order theory of real-closed fields, which is decidable, such that the resulting formula is valid iff the MLSL formula holds throughout the transition sequence. We then assume that temporal data may have an error of up to $\varepsilon$, and that spatial data may have an error of up to $\delta$. We extend our procedure to check if the MLSL formula $\varepsilon$-$\delta$-robustly holds throughout the transition sequence.