Efficient Model Checking with Semantically-Equivalent Models for vGOAL

Model checking offers a powerful approach to ensuring safety and reliability in autonomous systems. However, existing modelchecking approaches for agent programming languages (APLs) face challenges in equivalent semantic mapping, efficient model generation, and integration with high-performance model checkers. We present a computation tree logic (CTL) model-checking framework for vGOAL, where both the interpreter and model-checking framework share the same state update implementations. Our framework establishes semantically equivalent models of vGOAL programs, implements efficient state space generation, and integrates with the NuSMV model checker. Through a case study of an autonomous logistic system with up to three robots, we demonstrate significant improvements in model-checking efficiency, enabling verification of complex autonomous systems.

Authors

• Yi Yang
• Tom Holvoet

Keywords

• CTL Model Checking
• vGOAL
• Autonomous Decision-Making