Spatio-Temporal Framework for Verifying Safety Rules in Autonomous Vehicles

With the increasing prevalence of vehicle driving automation systems (henceforth colloquially referred to as autonomous) on roads, the frequency and severity of accidents involving these vehicles have exceeded initially anticipated. It heightens global awareness of the need to enhance the safety standards of autonomous cars. One way to increase the safety of autonomous vehicles in this regard is by imposing safety rules on them, which they must respect. For instance, a safety designer could require that "the ego vehicle should always maintain a distance of at least 4 seconds from the vehicle in front." Such safety rules often mix space and time in their expression, which makes them challenging to check via classical frameworks based on temporal logic. In this paper, we propose the definition of a formal framework dedicated to verifying spatiotemporal properties related to vehicles within a road network. One can then employ the designed framework to assess offline if a given driving scenario is safe concerning specified properties of this kind. More interestingly, one of the essential framework features is that it allows, given a current traffic configuration, to evaluate whether it is safe for the ego vehicle to perform this or that action based on projected futures under some traffic hypotheses, thus safeguarding the ego vehicle's driving policy. While still in its infancy, the proposed framework paves the way for defining a Domain-Specific Language for specifying these safety rules; it may consequently serve as an integral part of autonomous vehicles' safety assessment process, of both physical ones and ones within simulators.