MCK

MCK: Model checking knowledge. MCK is a model checker for the logic of knowledge, developed at the School of Computer Science and Engineering at the University of New South Wales. The system is intended as a testbed for a variety of approaches to model checking the logic of knowledge. The novelty of this model checker is that it supports several different ways of defining knowledge given a description of a multi-agent system and the observations made by the agents: observation alone; observation and clock; and synchonrous and asynchronous perfect recall of all observations. Both linear and branching time temporal operators are supported. Earlier releases of MCK were based primarily on BDD-based model checking algorithms, but MCK now also supports bounded model checking as well as explicit state model checking.


References in zbMATH (referenced in 30 articles )

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

1 2 next

  1. Belardinelli, Francesco; Condurache, Rodica; Dima, Cătălin; Jamroga, Wojciech; Knapik, Michal: Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol (2021)
  2. Machado, Vitor; Benevides, Mario: Populational announcement logic (PPAL) (2020)
  3. Jamroga, Wojciech; Knapik, Michał; Kurpiewski, Damian; Mikulski, Łukasz: Approximate verification of strategic abilities under imperfect information (2019)
  4. Čermák, Petr; Lomuscio, Alessio; Mogavero, Fabio; Murano, Aniello: Practical verification of multi-agent systems against \textscSlkspecifications (2018)
  5. Ezekiel, J.; Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems (2017)
  6. Pardo, Raúl; Balliu, Musard; Schneider, Gerardo: Formalising privacy policies in social networks (2017)
  7. Belardinelli, Francesco; Lomuscio, Alessio: A three-value abstraction technique for the verification of epistemic properties in multi-agent systems (2016)
  8. Chen, Qingliang; Su, Kaile; Sattar, Abdul; Luo, Xiangyu; Chen, Aixiang: A first-order coalition logic for BDI-agents (2016)
  9. Kouvaros, Panagiotis; Lomuscio, Alessio: Parameterised verification for multi-agent systems (2016)
  10. Woźna-Szcześniak, Bożena; Zbrzezny, Andrzej: Checking EMTLK properties of timed interpreted systems via bounded model checking (2016)
  11. Zbrzezny, Agnieszka M.; Zbrzezny, Andrzej: Verifying real-time properties of multi-agent systems via SMT-based bounded model checking (2016)
  12. Xu, Yongsheng; Yang, Guowu; Chang, Zhengwei; Zheng, Desheng; Guo, Wensheng: Terminal satisfiability in GSTE (2014)
  13. Konur, Savas; Fisher, Michael; Schewe, Sven: Combined model checking for temporal, probabilistic, and real-time logics (2013)
  14. van Ditmarsch, Hans; van der Hoek, Wiebe; Ruan, Ji: Connecting dynamic epistemic and temporal epistemic logics (2013)
  15. Lomuscio, Alessio; Penczek, Wojciech: Symbolic model checking for temporal-epistemic logic (2012)
  16. Gammie, Peter: Verified synthesis of knowledge-based programs in finite synchronous environments (2011)
  17. Guelev, Dimitar P.; Dam, Mads: An epistemic predicate (\mathrmCTL^*) for finite control (\pi)-processes (2011)
  18. Huang, Xiaowei; Luo, Cheng; van der Meyden, Ron: Improved bounded model checking for a fair branching-time temporal epistemic logic (2011)
  19. Lomuscio, Alessio; Qu, Hongyang; Russo, Francesco: Automatic data-abstraction in model checking multi-agent systems (2011)
  20. Luo, Xiangyu; Su, Kaile; Gu, Ming; Wu, Lijun; Yang, Jinji: Symbolic model checking the knowledge in Herbivore protocol (2011)

1 2 next


Further publications can be found at: http://cgi.cse.unsw.edu.au/~mck/pmck/mcks/publications