MCMAS-SLK

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.


References in zbMATH (referenced in 20 articles )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Belardinelli, Francesco; Demri, Stéphane: Strategic reasoning with a bounded number of resources: the quest for tractability (2021)
  2. Kwiatkowska, Marta; Norman, Gethin; Parker, David; Santos, Gabriel: Automatic verification of concurrent stochastic systems (2021)
  3. Belardinelli, Francesco; Lomuscio, Alessio; Murano, Aniello; Rubin, Sasha: Verification of multi-agent systems with public actions against strategy logic (2020)
  4. Gardy, Patrick; Bouyer, Patricia; Markey, Nicolas: Dependences in strategy logic (2020)
  5. Gutierrez, Julian; Najib, Muhammad; Perelli, Giuseppe; Wooldridge, Michael: Automated temporal equilibrium analysis: verification and synthesis of multi-player games (2020)
  6. Jamroga, Wojciech; Konikowska, Beata; Kurpiewski, Damian; Penczek, Wojciech: Multi-valued verification of strategic ability (2020)
  7. Murano, Aniello; Parente, Mimmo; Rubin, Sasha; Sorrentino, Loredana: Model-checking graded computation-tree logic with finite path semantics (2020)
  8. Gutierrez, Julian; Harrenstein, Paul; Perelli, Giuseppe; Wooldridge, Michael: Nash equilibrium and bisimulation invariance (2019)
  9. Jamroga, Wojciech; Malvone, Vadim; Murano, Aniello: Natural strategic ability (2019)
  10. Aminof, Benjamin; Malvone, Vadim; Murano, Aniello; Rubin, Sasha: Graded modalities in strategy logic (2018)
  11. Čermák, Petr; Lomuscio, Alessio; Mogavero, Fabio; Murano, Aniello: Practical verification of multi-agent systems against \textscSlkspecifications (2018)
  12. Gutierrez, Julian; Perelli, Giuseppe; Wooldridge, Michael: Imperfect information in reactive modules games (2018)
  13. Malvone, Vadim; Mogavero, Fabio; Murano, Aniello; Sorrentino, Loredana: Reasoning about graded strategy quantifiers (2018)
  14. Huang, Chung-Hao; Schewe, Sven; Wang, Farn: Model-checking iterated games (2017)
  15. Mogavero, Fabio; Murano, Aniello; Perelli, Giuseppe; Vardi, Moshe Y.: Reasoning about strategies: on the satisfiability problem (2017)
  16. Chen, Qingliang; Su, Kaile; Sattar, Abdul; Luo, Xiangyu; Chen, Aixiang: A first-order coalition logic for BDI-agents (2016)
  17. Laroussinie, François; Markey, Nicolas: Augmenting ATL with strategy contexts (2015)
  18. Toumi, Alexis; Gutierrez, Julian; Wooldridge, Michael: A tool for the automated verification of Nash equilibria in concurrent games (2015)
  19. Čermák, Petr; Lomuscio, Alessio; Mogavero, Fabio; Murano, Aniello: MCMAS-SLK: A model checker for the verification of strategy logic specifications (2014) ioport
  20. Mogavero, Fabio; Murano, Aniello; Perelli, Giuseppe; Vardi, Moshe Y.: Reasoning about strategies: on the model-checking problem (2014)