魔术中逻辑动作的模型检测
Model Checking Logical Actions in Magic Tricks
AI总结：
本文提出魔术模型检测（MTMC）技术，将纸牌魔术的逻辑正确性问题归约为模型检测问题，以验证魔术设计是否符合预期。
摘要：
一些魔术（MT），例如多种纸牌魔术（CM），由人类计算或逻辑动作组成。如何确保这些魔术的逻辑正确性？本文采用模型检测（MC）技术，通过一个案例研究来考察一种典型的纸牌魔术。首先，一种名为“手随公事”的纸牌魔术的计算操作可以用魔术算法（MAR）来描述。其次，其逻辑正确性由一个时序逻辑公式刻画。在此基础上，该魔术的逻辑正确性问题被归约为模型检测问题。因此，魔术模型检测（MTMC）技术旨在从逻辑和计算的角度验证一个设计好的魔术是否符合其设计者的预期和要求。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
