Symoblic Model Checking for Multi-Agent Systems Based on ATLE

Multi-agent systems (MAS) consist of multiple in-teracting autonomous agents, each possessing individual goals and knowledge. These systems are increasingly prevalent in applications such as robotics and autonomous vehicles. This paper introduces a symbolic model checking approach for MAS, utilizing concurrent game structures with epistemic(CGSE) for modeling and alter-timing temporal Logic with Epistemic (ATLE) for specifying system properties. The proposed method employs symbolic representations of the CGSE model, which are then converted into Ordered Binary Decision Diagrams (OBDDs). A symbolic model checking algorithm is developed for these OBDDs to efficiently handle large-scale systems and reduce computational complexity.