MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications

摘要

In this paper we presented MCMAS-SLK, a novel symbolic model checker for the verification of systems against specifications given in SLK. A notable feature of the approach is that it allows for the automatic verification of sophisticated game concepts such as various forms of equilibria, including Nash equilibria. Since MCMAS-SLK also supports epistemic modalities, this further enables us to express specifications concerning individual and group knowledge of cooperation properties; these are commonly employed when reasoning about multi-agent systems.