Added Value of Probabilistic Model Checking of <i>vGOAL</i> for Autonomous Systems

Abstract

Agent programming languages have long been studied for programming autonomous decisions. Traditional model checking is commonly used to verify their properties, particularly safety. However, probabilistic model checking has seen limited use in verifying agent programming languages despite the inherent uncertainty in autonomous systems. vGOAL supports both automated traditional and probabilistic model checking, whereas other agent programming languages mainly support traditional methods or lack model-checking capabilities entirely. This paper investigates the added value of probabilistic model checking of vGOAL in the development of autonomous systems, specifically focusing on the performance improvement of a logistic autonomous system. We developed a performance analysis component on top of the PCTL model checking process of vGOAL. Through an empirical analysis of 380 scenarios, we explore how probabilistic model checking can improve system performance and reliability. Our experimental results demonstrate that the probabilistic model checking of vGOAL offers unique advantages in handling uncertainty and optimizing system performance.