Reliable Decision Making in Autonomous Vehicles

Gleifer Vaz Alves, Louise Dennis, Lucas Fernandes, Michael Fisher

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


The use of Autonomous Vehicles (AVs) on our streets is soon to be a reality; increasingly, interacting with such AVs will be part of our daily routine. However, we will certainly need to assure the reliable behaviour of an AV, especially when some unexpected scenarios (e.g. harsh environments, obstacles, emergencies) are taken into account. In this article we use an intelligent agent approach to capture the high-level decision-making process within an AV and then use formal verification techniques to automatically, and strongly, analyse the required behaviours. Specifically, we use the MCAPL framework, wherein our core agent is implemented using the GWENDOLEN agent programming language, and to which we can apply model checking via the AJPF model checker. By performing such formal verification on our agent, we are able to prove that the AV’s decision-making process, embedded within the GWENDOLEN agent plans, matches our requirements. As examples, we will verify (formal) properties in order to determine whether the agent behaves in a reliable manner through three different levels of emergency displayed in a simple urban traffic environment.

Original languageEnglish
Title of host publicationValidation and Verification of Automated Systems
Subtitle of host publicationResults of the ENABLE-S3 Project
EditorsA Leitner, D Watzenig, J Ibanez-Guzman
PublisherSpringer Nature
Number of pages13
ISBN (Electronic)9783030146283
ISBN (Print)978-3-030-14627-6
Publication statusPublished - 2020

Publication series

NameValidation and Verification of Automated Systems: Results of the ENABLE-S3 Project


Dive into the research topics of 'Reliable Decision Making in Autonomous Vehicles'. Together they form a unique fingerprint.

Cite this