Card games as pointer structures: case studies in mobile CSP modelling

TL;DR

This paper explores modeling card games as pointer structures using CSP and FDR, revealing new insights into game solvability and proposing techniques applicable to mobile system modeling.

Contribution

It introduces novel CSP modeling approaches for card games as pointer structures, demonstrating their effectiveness and potential for modeling mobile systems.

Findings

High percentages of winnable games identified

Modeling techniques reduce symmetric state complexity

Techniques suggest new methods for mobile CSP modeling

Abstract

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.