Model Checking Logical Actions in Magic Tricks

TL;DR

The paper tackles producing reliable verification for computation-based magic tricks, modeling a trick like sousuigongcishi with a Magic Trick Model (MTM) and a Magic Algorithm (MAR), and reframing correctness as temporal properties verifiable by model checking. It develops Algorithms 2–6 to check CTL/ITL properties such as $AF(p \land empty)$, $AFp$, $AGp$, $EFp$, and $EGp$ and proves time bounds of $O(mn)$ for these checks, with the atomic proposition $p$ expressing matching card halves. The work contributes a formal framework (MTM, magic automata, MAR), a concrete verification suite, and an empirical Matlab-based evaluation validating the approach on the shousuigongcishi case. It demonstrates the practicality of MTMC for validating logical designs in magical performances and lays a path for scaling to more complex tricks and for complementary verification methods like theorem proving.

Abstract

Some Magic Tricks (MT), such as many kinds of Card Magic (CM), consisting of human computational or logical actions. How to ensure the logical correctness of these MTs? In this paper, the Model Checking (MC) technique is employed to study a typical CM via a case study. First, computational operations of a CM called shousuigongcishi can be described by a Magic Algorithm (MAR). Second, the logical correctness is portrayed by a temporal logic formula. On the basis of it, this MT logical correctness problem is reduced to the model checking problem. As a result, the Magic Trick Model Checking (MTMC) technique aims to verify whether a designed MT meets its architect's anticipation and requirements, or not, in terms of logic and computations.

Figures (2)

• Figure 1: MC results of $AF(p \land empty)$ and running time
• Figure 2: MC results