Reasoning about Time, Action and Knowledge in Multi-Agent Systems

• Thesis Abstract.
• Download it.

Russian Cards Problem

• DEMO
  • RUS.hs is the Haskell source specifying Russian Cards Problem in DEMO
  • DEMO homepage.
• MCK
  • rus.mck specifies Russian Cards Problem in MCK
  • rus.mck.txt is the output MCK produces with rus.mck as input. This lists the results of verification of epistemic formulas.
  • MCK homepage.
• MCMAS
  • rus.mcmas specifies Russian Cards in MCMAS.
  • rus.mcmas.txt is the output MCMAS produces with rus.mcmas as input. This lists the results of verification of epistemic formulas.
  • rus_mcmas.c is a C program that generates rus.mcmas.
  • MCMAS homepage.

Sum And Product Problem

• DEMO
  • SNP.hs is the Haskell source specifying Sum And Product Problem in DEMO
  • SNP.txt shows interaction with the model.

Tic-Tac-Toe Problem

• MOCHA implementation
  • ttt.mocha is the result of translating Tic-Tac-Toe GDL specification to RML specification using GDL2RML. It is served as an input for ATL model checker MOCHA.