Prof. Dr. Gleifer Vaz Alves

Federal University of Technology in Paraná, Brazil

Abstract

In this talk, we show how to formalise, model, and implement the so-called Road Junction rules on an agent that represents an AV (Autonomous Vehicle). Our agent-based approach aims to formally verify the basic behaviour of an AV-agent against some traffic rules (specifically the Road Junction rules). We present a formalisation using LTL logic, the use of UPPAAL model checker to model and verify time constraints, the use of a BDI (Belief-Desire-Intention) language (named Gwendolen) to implement an AV-agent, and also the use of AJPF model checker to formally verify the agent's behaviour on a Road Junction scenario. At last, we (briefly) discuss related issues like safety, regulations, ethical behaviour and stakeholders.