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.

翻译：一些魔术动作，例如多种纸牌魔术，包含人类的计算或逻辑操作。如何确保这些魔术动作的逻辑正确性？本文通过案例研究，运用模型检测技术来探究典型的纸牌魔术。首先，一种称为“收水功测试”的纸牌魔术的计算操作可通过魔术算法描述。其次，逻辑正确性用时态逻辑公式刻画。在此基础上，该魔术动作的逻辑正确性问题被简化为模型检测问题。因此，魔术动作模型检测技术旨在从逻辑与计算角度，验证所设计的魔术动作是否符合设计者的预期与要求。