Model Checking of vGOAL

Abstract

Developing autonomous decision-making requires safety assurance. Agent programming languages like AgentSpeak and Gwendolen provide tools for programming autonomous decision-making. However, despite numerous efforts to apply model checking to these languages, challenges persist such as a faithful semantic mapping between agent programs and the generated models, efficient model generation, and efficient model checking. As an extension of the agent programming language GOAL, vGOAL has been proposed to formally specify autonomous decisions with an emphasis on safety. This paper tackles the mentioned challenges through two automated model-checking processes for vGOAL: one for Computation Tree Logic and another for Probabilistic Computation Tree Logic. Compared with the existing model-checking approaches of agent programming languages, it has three main advantages. First, it efficiently performs automated model-checking analysis for a given vGOAL specification, including efficiently generating input models for NuSMV and Storm and leveraging these efficient model checkers. Second, the semantic equivalence is established for both nondeterministic models and probabilistic models of vGOAL: from vGOAL to transition systems or DTMCs. Third, an algorithm is proposed for efficiently detecting errors, which is particularly useful for vGOAL specifications that describe complex scenarios. Validation and experiments in a real-world autonomous logistic system with three autonomous mobile robots illustrate both the efficiency and practical usability of the automated CTL and PCTL model-checking process for vGOAL.