Enhancing Confidence of the vGOAL Interpreter Using SAT Solving

Abstract

Agent programming languages and their interpreters are crucial in autonomous decision-making. While formal methods are extensively utilized to ensure the correctness of agent programs, their application for verifying the implementation correctness of interpreters remains infrequent. To formally specify and verify autonomous decision-making, we proposed vGOAL and implemented its interpreter. The implementation correctness of the vGOAL interpreter is crucial for users to gain trust in the vGOAL approach. Using program verification is one option, yet this would require a huge effort to verify the correctness of the vGOAL interpreter.

In this paper, we propose integrating an SAT-solving component into the vGOAL interpreter to enhance confidence in its core component: minimal model generation. The SAT-solving component consists of two subcomponents: an SAT-encoding component and an SAT solver. Leveraging PySAT for its interface to advanced solvers, our main contribution lies in the SAT encoding. We devise an algorithm to encode the inputs and outputs of the core component into a satisfiable CNF formula. Importantly, we justify that this algorithm generates a satisfiable CNF formula only if the result is correct. We demonstrate the practicality and efficiency of this SAT-solving approach using a case study involving an autonomous transportation system with three mobile robots.