MCMAS

MCMAS: A Model Checker for the Verification of Multi-Agent Systems. While temporal logic in its various forms has proven essential to reason about reactive systems, agent-based scenarios are typically specified by considering high-level agents attitudes. In particular, specification languages based on epistemic logic [7], or logics for knowledge, have proven useful in a variety of areas including robotics, security protocols, web-services, etc. For example, security specifications involving anonymity [4] are known to be naturally expressible in epistemic formalisms as they explicitly state the lack of different kinds of knowledge of the principals.


References in zbMATH (referenced in 73 articles )

Showing results 61 to 73 of 73.
Sorted by year (citations)
  1. Guelev, Dimitar P.; Dima, Cătălin; Enea, Constantin: An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking (2011)
  2. Huang, Xiaowei; Luo, Cheng; van der Meyden, Ron: Improved bounded model checking for a fair branching-time temporal epistemic logic (2011)
  3. Lomuscio, Alessio; Qu, Hongyang; Russo, Francesco: Automatic data-abstraction in model checking multi-agent systems (2011)
  4. Luo, Xiangyu; Su, Kaile; Gu, Ming; Wu, Lijun; Yang, Jinji: Symbolic model checking the knowledge in Herbivore protocol (2011)
  5. Dechesne, Francien; Wang, Yanjing: To know or not to know: Epistemic approaches to security protocol verification (2010)
  6. Alechina, Natasha; Logan, Brian; Nguyen Hoang Nga; Rakib, Abdur: Verifying time and communication costs of rule-based reasoners (2009)
  7. Boureanu, Ioana; Cohen, Mika; Lomuscio, Alessio: Automatic verification of temporal-epistemic properties of cryptographic protocols (2009)
  8. Cohen, Mika; Dam, Mads; Lomuscio, Alessio; Qu, Hongyang: A data symmetry reduction technique for temporal-epistemic logic (2009)
  9. Lomuscio, Alessio; Penczek, Wojciech; Qu, Hongyang: Towards partial order reduction for model checking temporal epistemic logic (2009)
  10. Lomuscio, Alessio; Qu, Hongyang; Raimondi, Franco: MCMAS: a model checker for the verification of multi-agent systems (2009) ioport
  11. Engelhardt, Kai; Gammie, Peter; van der Meyden, Ron: Model checking knowledge and linear time: PSPACE cases (2007)
  12. Lomuscio, Alessio; Raimondi, Franco; Woźna, Bożena: Verification of the TESLA protocol in MCMAS-X (2007)
  13. Lomuscio, Alessio; Raimondi, Franco: \textscmcmas: a model checker for multi-agent systems (2006)