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

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

  1. Kouvaros, Panagiotis; Lomuscio, Alessio: Parameterised verification for multi-agent systems (2016)
  2. Woźna-Szcześniak, Bożena; Zbrzezny, Andrzej: Checking EMTLK properties of timed interpreted systems via bounded model checking (2016)
  3. Konur, Savas; Fisher, Michael; Schewe, Sven: Combined model checking for temporal, probabilistic, and real-time logics (2013)
  4. van Ditmarsch, Hans; van der Hoek, Wiebe; Ruan, Ji: Connecting dynamic epistemic and temporal epistemic logics (2013)
  5. Lomuscio, Alessio; Penczek, Wojciech: Symbolic model checking for temporal-epistemic logic (2012)
  6. van Ditmarsch, Hans; Herzig, Andreas; de Lima, Tiago: From situation calculus to dynamic epistemic logic (2011)
  7. Dechesne, Francien; Wang, Yanjing: To know or not to know: Epistemic approaches to security protocol verification (2010)
  8. Belardinelli, F.; Lomuscio, A.: Quantified epistemic logics for reasoning about knowledge in multi-agent systems (2009)
  9. Kahl, Wolfram: Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types (2008)
  10. Lomuscio, Alessio; Penczek, Wojciech; Woźna, Bożena: Bounded model checking for knowledge and real time (2007)
  11. Raimondi, Franco; Lomuscio, Alessio: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams (2007)
  12. Gammie, Peter; van der Meyden, Ron: MCK: Model checking the logic of knowledge (2004)

Further publications can be found at: