Implementação e verificação formal de planos de um agente racional modelado para condução de um veículo autônomo

Abstract

Autonomous vehicles, in the not too distant future, will be a reality in urban traffic. Currently, various research is being conducted to develop this new technology. The main goal of said research is to create and implement vehicle systems capable, and without human interaction, of making their own decisions. In this work, we will discuss the use of a rational agent to model the behavior of an autonomous vehicle, where a basic driving mechanism is considered. The scenario presented here is to define the following agent abilities: perform rides, move through a simulated environment, obstacle avoidance of static and known barriers, and given a situation when a collision is unavoidable; the agent will try to assure the least amount of (physical) damage to the vehicle possible. The approach taken to create this agent is with the Gwendolen programming language. Once formed, it will be implemented in a Java developed environment. The Java environment is then responsible for storing all information about locations were the agent may move during its performance. Once complete, the use of a UPD protocol will be implemented to receive messages through a local network from the Java environment. This is to create a graphical representation of when changes occur caused by the agent in the said environment. Since all software is prone to errors, it is necessary to verify the decisions taken by the agent. Evidence of such a need is easily understood through the basic knowledge of human impact, specifically human casualties. If a decisional flaw occurs in the system while controlling an autonomous vehicle it could directly impact human life. Such validation, shall be shown, can be performed with formal verification techniques. For this, linear temporal logic formulae is used to formally specify all the properties expected for the agent to hold. The Model Checking Program Technique with AJPF (Agent Java Pathfinder) then makes the verification possible. The latter is a tool which is used to verify agent properties during its run-time. Its purpose is to guarantee that a property hold and show true data to an investigation of an occurring error. Thus, this work proposes an implementation of a rational agent and the formal verification of its decision-making process, where such agent represent an autonomous vehicle in different simulated scenarios. With this work, it is was concluded that it is possible to develop an agent in the Gwendolen language modeled as an autonomous vehicle. In addition to this, the properties of such agent can be formally verified through the model checker using the AJPF tool.