Sciweavers

Share
CAV
2009
Springer

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

12 years 4 days ago
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...
Alessio Lomuscio, Hongyang Qu, Franco Raimondi
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2009
Where CAV
Authors Alessio Lomuscio, Hongyang Qu, Franco Raimondi
Comments (0)
books