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

arXiv: https://arxiv.org/abs/1402.2948 · HTML: https://mlsanity.com/paper/1402.2948/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Feb 2014.

## Built on by (most cited first, 2 of 2)

- [Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions](https://mlsanity.com/paper/2201.09616/) (2022)
- [A Neuro-Symbolic Approach to Strategy Synthesis for Strategic Logics](https://mlsanity.com/paper/2606.17962/) (2026)

## Abstract (arXiv)

We introduce MCMAS-SLK, a BDD-based model checker for the verification of systems against specifications expressed in a novel, epistemic variant of strategy logic. We give syntax and semantics of the specification language and introduce a labelling algorithm for epistemic and strategy logic modalities. We provide details of the checker which can also be used for synthesising agents' strategies so that a specification is satisfied by the system. We evaluate the efficiency of the implementation by discussing the results obtained for the dining cryptographers protocol and a variant of the cake-cutting problem.