MCMAS: A Model Checker for the Verification of Multi-Agent Systems

tic modalities for correctness [16]. The release described in this abstract is a complete rebuild of a preliminary experimental checker [14]. The model input language includes variables and basic types and it implements the semantics of interpreted systems, thereby naturally supporting the modularity present in agent-based systems. MCMAS implements OBDD-based algorithms optimised for interpreted systems and supports fairness, counter-example generation, and interactive execution (both in explicit and symbolic mode). MCMAS has been used in a variety of scenarios including web-services, diagnosis, and security. MCMAS is released under GNU-GPL. 2 Multi-Agent Systems Formalisms Multi-Agent Systems (MAS) formalisms are typically built on extensions of computree logic (CTL). For the purposes of this abstract we consider specifications given in the following language L built from a set of propositional atoms p P, and a set of agents i A (G A denotes a set of agents): The research describe...

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Alessio Lomuscio, Hongyang Qu, Franco Raimondi
• Keywords: CAV 2009, Formalisms Multi-Agent Systems, Hardware, Interpreted Systems, Multi-agent Systems