Specification and verification of multi-agent systems

Abstract

Overview. Multi agent systems (MAS) provide an important framework for formalizing various problems in computer science, artificial intelligence, game theory, social choice theory, etc. Modal logics are amongst the most suitable and versatile logical formalisms for specification and verification of computational systems. Here, we present an overview of some important developments in the area. We introduce modal logics used for specification of temporal, epistemic, and strategic properties of systems; then, we present some model checking algorithms, and discuss the computational complexity of the model checking problem. Finally, we consider symbolic (compact) representations of systems based on Binary Decision Diagrams (BDD) and propositional logic formulas, and show how the representations change the algorithmic side of model checking. We also discuss other techniques that help to reduce the complexity and make the verification feasible even for large systems. © 2012 Springer-Verlag.