Card games as pointer structures: case studies in mobile CSP modelling
This work addresses modeling challenges in mobile systems for researchers in formal methods, but it is incremental as it builds on existing CSP techniques.
The authors tackled the problem of modeling card games as pointer structures using CSP refinement checker FDR, revealing much higher percentages of winnable games than previously believed for two such games.
The author has long enjoyed using the CSP refinement checker FDR to solve puzzles, as witnessed by examples in \cite{tpc,ucs}. Recent experiments have shown that a number of games of patience (card games for one) are now well within bounds. We discuss the modelling approaches used to tackle these and avoid symmetric states. For two such games we reveal much higher percentages of winnable games than was previously believed. The techniques developed for some of these card games -which employ various dynamic patterns of cards - suggest techniques for modelling pointer structures in CSP and FDR analogous to those used with the pi-calculus. Most of these use CSP's ability to express mobile systems.