Computing Running Game with Automata Theory

Abstract

This paper examines a common but unverified claim in a strand of published work applying automata theory to game design: that specifying a game as a finite automaton yields a complete, bug-resistant design. Prior work has already modeled endless-running games with finite state machines, including tested, shipped implementations [8], [9]; the contribution here is different. We take a two-level running game from this literature, give it, for the first time in this line of work, an explicit five-tuple automaton definition — formally an ε-NFA, though the tabulated transition relation is single-valued — and machine-checkable transition tables (Tables 3 and 4) rather than a diagram and prose description alone, and build a reference implementation directly from those tables. Doing so surfaced a real specification defect: three states had no valid continuation for any input, meaning the automaton as originally described could not be completed to a win state along certain valid paths. We report this as a case study in applying lightweight completeness and reachability auditing — standard practice in hardware and software finite-state-machine verification, but not evident in this game-design literature — backed by a 2,000-run randomized fuzz test (100% totality pass rate) and mutation testing (89.4% of 66 mutants killed, after an independent rerun caught and fixed a reproducibility bug in the test harness itself, and survivor analysis guided four added test cases), and we test the audit directly against a published claim that automata-based game design of this kind “covers infinitely many possibilities” of play and yields “minimum bugs” [3]. In the one case examined, that claim did not hold until the audited defect was fixed.