Multi-agent temporal logic (MATL) has been proposed as a specification and verification framework for multi-agent systems (e.g. security protocols). The main charactertistic of MATL is that it allows for an independent analysis of temporal and epistemic components, and results in a model checking algorithm that extends the standard temporal logic model checking.
In this talk we present NuMAS, a symbolic model checker for multi-agent temporal logics. NuMAS is built on top of NuSMV, a state-of-the-art BDD-based symbolic model checker for temporal logic. We describe the functionalities and the architecture of NuMAS, showing how the modular features of MATL allow to exploit the building blocks for temporal logic model checking present in NuSMV