Symbolic Model-checking for Resource-Bounded ATL
Natasha Alechina, Brian S. Logan, Hoang Nga Nguyen, Franco Raimondi, Leonardo Mostarda · Middlesex University Research Repository (Middlesex University Of London) · 2015
In this paper we present a symbolic implementation of a model checking algorithm for the verification of properties expressed in Resource-Bounded Alternating Time Temporal Logic (RB-ATL).The implementation is based on the model checker MCMAS.We evaluate the performance of our implementation using simple multiagent model checking problems of increasing complexity.