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 19 articles )

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

  1. Ezekiel, J.; Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems (2017)
  2. Pardo, Raúl; Balliu, Musard; Schneider, Gerardo: Formalising privacy policies in social networks (2017)
  3. Belardinelli, Francesco; Lomuscio, Alessio: A three-value abstraction technique for the verification of epistemic properties in multi-agent systems (2016)
  4. Kouvaros, Panagiotis; Lomuscio, Alessio: Parameterised verification for multi-agent systems (2016)
  5. Woźna-Szcześniak, Bożena; Zbrzezny, Andrzej: Checking EMTLK properties of timed interpreted systems via bounded model checking (2016)
  6. Konur, Savas; Fisher, Michael; Schewe, Sven: Combined model checking for temporal, probabilistic, and real-time logics (2013)
  7. van Ditmarsch, Hans; van der Hoek, Wiebe; Ruan, Ji: Connecting dynamic epistemic and temporal epistemic logics (2013)
  8. Lomuscio, Alessio; Penczek, Wojciech: Symbolic model checking for temporal-epistemic logic (2012)
  9. Gammie, Peter: Verified synthesis of knowledge-based programs in finite synchronous environments (2011)
  10. Huang, Xiaowei; Luo, Cheng; van der Meyden, Ron: Improved bounded model checking for a fair branching-time temporal epistemic logic (2011)
  11. Lomuscio, Alessio; Qu, Hongyang; Russo, Francesco: Automatic data-abstraction in model checking multi-agent systems (2011)
  12. Luo, Xiangyu; Su, Kaile; Gu, Ming; Wu, Lijun; Yang, Jinji: Symbolic model checking the knowledge in Herbivore protocol (2011)
  13. van Ditmarsch, Hans; Herzig, Andreas; de Lima, Tiago: From situation calculus to dynamic epistemic logic (2011)
  14. Dechesne, Francien; Wang, Yanjing: To know or not to know: Epistemic approaches to security protocol verification (2010)
  15. Belardinelli, F.; Lomuscio, A.: Quantified epistemic logics for reasoning about knowledge in multi-agent systems (2009)
  16. Kahl, Wolfram: Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types (2008)
  17. Lomuscio, Alessio; Penczek, Wojciech; Woźna, Bożena: Bounded model checking for knowledge and real time (2007)
  18. Raimondi, Franco; Lomuscio, Alessio: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams (2007)
  19. Gammie, Peter; van der Meyden, Ron: MCK: Model checking the logic of knowledge (2004)


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