Li Tan. In the proceedings of the 16th International Conference on Computer-Aided Verification (CAV'04), Boston, MA, Volume 3114 of Lecture Notes in Computer Science, Springer-Verlag, 2004
We introduce an integrated tool for implementing and playing various diagnostic games. The tool uses a semantics hierarchy introduced in [Tan02] to improve code sharing among different diagnostic games and reduce the cost of introducing a new game. PlayGame synthesizes the winning strategy for a game using the evidence that is an abstract and uniform encoding of the proof computed by a checker, and hence instead of relying on a particular checker the tool works on a variety of checkers that can be extended to produce such evidence. PlayGame implements a µ-calculus game and a full range of equivalence/preorder games on the Concurrency Workbench-New Century (CWB-NC).