swMATH ID: 24778
Software Authors: Čermák, P.; Lomuscio, A.; Mogavero, F.; Murano, A.
Description: MCMAS-SLK: A model checker for the verification of strategy logic specifications. 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.
Homepage: https://arxiv.org/abs/1402.2948
Related Software: MCMAS; MOCHA; EAGLE; PRISM; PRISM-games; EVE; PRALINE; VerICS; CESAR; jMocha; Uppaal; MCK; dot; GAMUT; GitHub; GIST; Gambit; z3; Yices; CPLEX
Referenced in: 19 Publications

Referencing Publications by Year