## Software Model Checking Based on Game Semantics and CSP

#### by Tony Garnock-Jones / @leastfixedpoint

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.