eighty-twenty

This talk reported on exploring the use of CSP in implementing a Game Semantics model-checker. Traditional model checkers don’t give soundness, completeness or compositionality — but game semantics can.

Game semantics are a series of alternating “moves” between the player (P/player/program) and the opponent (O/opponent/environment). The CSP model for game semantics has channels Q and A for questions and answers respectively. The examples look like continuation-passing-style transformed parallel-functional expressions in codename — but in CSP, which is a slightly weird language.

Their system uses LTL over finite traces. They’ve implemented a compiler from a program to the CSP representation of the game semantics for the program. The language looks imperative and algol-like. The programs are compiled into a transition system; some of the input parameters controlling the size of the transition system are set ahead of time — in the examples shown, generally the size of the input was fixed at 2 (eg. a bubblesort with arraylen = 2, and a Queue ADT with size = 2). The transition diagrams look like Satnam’s butterfly diagrams!

Using CSP instead of regular expressions to model game semantics turns out to be a clear win in terms of performance.

They implemented an algorithm that finds the minimal model for a transition diagram, but while it drastically reduces the state count in the model, the algorithm itself is really slow — just using the straight model, without minimising it, turns out to be a more efficient use of resources.