A stochastically verifiable decision making framework for autonomous ground vehicles

A framework is presented for probabilistic verification of Autonomous Vehicles' (AV) decisions by rational agents onboard. The AV's are assumed to be equipped with the necessary perception and control systems, which are needed for their awareness of the environment and enable them to make decisions. The decisions arrived at by the agents are verified by the probabilistic model checking techniques presented. The objective of the new framework is to reduce design complexity of decision making while ensuring verifiability of the decisions made by the rational agents. Probabilistic Timed Programs (PTPs) are used to model the environmental scenarios and Probabilistic Computational Tree Logic (PCTL) to specify the properties to be verified. Both PTP and PCTL are deployed by use of the PRISM model checker. For demonstration purposes, the Robot Operating System (ROS) and the Gazebo simulator are used to model and test the vehicle systems and their signal processing. sEnglish Publisher, the high abstraction level programming tool, is used along with a Jason agent architecture to provide rules and plans for decision making. Matlab is relied on to assist in programming the perception and control systems in the demonstration.