Making model checking feasible for GOAL

Abstract

Agent Programming Languages have been studied for over 20 years for programming complex decision-making for autonomous systems. The GOAL agent programming language is particularly interesting since it depends on automated planning based on beliefs and goals to determine behavior rather than preprogrammed planning by developers. Model checking is a powerful verification technique to guarantee the safety of an autonomous system. Despite studies of model checking in other agent programming languages, GOAL lacks support for model checking of GOAL programs. The fundamental challenge is to make GOAL programs feasible for model checking. In this paper, we tackle this fundamental issue. First, we formalize the syntax and semantics of the logic underpinning stratified single-agent GOAL programs. Second, we devise an algorithm for transforming a stratified single-agent GOAL program to a transition system that is equivalent in terms of operational semantics, enabling model checking. Third, we develop an automated translator for a stratified single-agent GOAL program. The translator consists of (1) the automated transformation of a GOAL program into its operational semantically equivalent transition system, and (2) the interface generation of the generated transition system into a Prism model, an input for two probabilistic symbolic model checkers: Storm and Prism. Moreover, we point out that we will extend the applicability of the transformation algorithm and its implementation to all stratified GOAL programs.