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.
Keywords for this software
References in zbMATH (referenced in 31 articles )
Showing results 21 to 31 of 31.
Sorted by year (- Luo, Xiangyu; Su, Kaile; Gu, Ming; Wu, Lijun; Yang, Jinji: Symbolic model checking the knowledge in Herbivore protocol (2011)
- van Ditmarsch, Hans; Herzig, Andreas; de Lima, Tiago: From situation calculus to dynamic epistemic logic (2011)
- Dechesne, Francien; Wang, Yanjing: To know or not to know: Epistemic approaches to security protocol verification (2010)
- Belardinelli, F.; Lomuscio, A.: Quantified epistemic logics for reasoning about knowledge in multi-agent systems (2009)
- Belardinelli, Francesco; Lomuscio, Alessio: A complete quantified epistemic logic for reasoning about message passing systems (2009)
- Belardinelli, Francesco; Lomuscio, Alessio: First-order linear-time epistemic logic with group knowledge: an axiomatisation of the monodic fragment (2009)
- Lomuscio, Alessio; Penczek, Wojciech; Qu, Hongyang: Towards partial order reduction for model checking temporal epistemic logic (2009)
- Kahl, Wolfram: Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types (2008)
- Lomuscio, Alessio; Penczek, Wojciech; Woźna, Bożena: Bounded model checking for knowledge and real time (2007)
- Raimondi, Franco; Lomuscio, Alessio: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams (2007)
- 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