Model Checking Russian Cards

This webpage contains the source of the implementations of the Russian Cards five hand protocol referred to in the article titled Model Checking Russian Cards ( pdf ) that has been presented at the Third Workshop on Model Checking in Artificial Intelligence (MoChArt '05). In the article the structure of these programs is explained and (identical) excerpts of these listed programs are given with the explanations. (It will later appear in the Electronic Notes in Theoretical Computer Science.)

MCK

• rus.mck specifies Russian Cards.
• rus.mck.out is the output MCK produces with rus.mck as input. This lists the results of verification of epistemic formulas.

Some other, more efficient, MCK scripts may be added later to the website.

The MCK homepage is http://www.cse.unsw.edu.au/~mck/ .

DEMO

• RUS.hs is the Haskell source specifying Russian Cards.
• rus_demo.c is a C program that generates the initial epistemic state used in DEMO.

• RUSnew.hs is the much improved Haskell source specifying Russian Cards including model generation - it is only referred to but not detailed in the MoChArt submission.

More information on DEMO can be found on http://homepages.cwi.nl/~jve/papers/04/demo/ .

MCMAS

• rus.mcmas specifies Russian Cards in MCMAS.
• rus.mcmas.out 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.

The MCMAS homepage is http://www.cs.ucl.ac.uk/staff/f.raimondi/MCMAS/