Extending Urban Multi-Lane Spatial Logic to Formalise Road Junction Rules
Open Access
- 21 October 2021
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 348, 1-19
- https://doi.org/10.4204/eptcs.348.1
Abstract
During the design of autonomous vehicles (AVs), several stages should include a verification process to guarantee that the AV is driving safely on the roads. One of these stages is to assure the AVs abide by the road traffic rules. To include road traffic rules in the design of an AV, a precise and unambiguous formalisation of these rules is needed. However, only recently this has been pointed out as an issue for the design of AVs and the few works on this only capture the temporal aspects of the rules, leaving behind the spatial aspects. Here, we extend the spatial traffic logic, Urban Multi-lane Spatial Logic, to formalise a subset of the UK road junction rules, where both temporal and spatial aspects of the rules are captured. Our approach has an abstraction level for urban road junctions that could easily promote the formalisation of the whole set of road junction rules and we exemplarily formalise three of the UK road junction rules. Once we have the whole set formalised, we will model, implement, and formally verify the behaviour of an AV against road traffic rules so that guidelines for the creation of a Digital Highway Code for AVs can be established.This publication has 22 references indexed in Scilit:
- Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOLLecture Notes in Computer Science, 2017
- Formalising a Hazard Warning Communication Protocol with Timed AutomataLecture Notes in Computer Science, 2017
- Verifying the safety of lane change maneuvers of self-driving vehicles based on formalized traffic rulesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2017
- ARSENAL: Automatic Requirements Specification Extraction from Natural LanguageLecture Notes in Computer Science, 2016
- Proving Safety of Traffic Manoeuvres on Country RoadsLecture Notes in Computer Science, 2013
- An Abstract Model for Proving Safety of Multi-lane Traffic ManoeuvresLecture Notes in Computer Science, 2011
- Translating between Language and Logic: What Is Easy and What Is DifficultLecture Notes in Computer Science, 2011
- The Spotlight PrinciplePublished by Springer Science and Business Media LLC ,2007
- A Tutorial on UppaalLecture Notes in Computer Science, 2004
- A theory of timed automataTheoretical Computer Science, 1994