和与积数迷的符号化模型检测

Symbolic Model Checking for Sum and Product Riddle

和与积是一个著名的数迷问题。采用公告逻辑对该问题进行建模,将其Kripke模型符号化表示为多智能体有限状态程序,并在其上采用一种基于局部命题解释系统语义的知识逻辑符号化模型检测算法计算该问题的所有解。在时态逻辑模型检测器NuSMV基础上扩展实现了本文算法,然后在相同实验平台上用动态认知建模工具DEMO对该问题进行求解。实验表明,我们的算法不仅结果正确,而且在运行效率上与DEMO相比占有绝对优势。

The Sum-and-Product Riddle is a famous number puzzle. The riddle is modeled in a modal logic called public announcement logic, which is interpreted on multi-agent Kripke model. The model is symbolically represented as a multi-agent finite state program. Based on the semantics of the logic, a symbolic model checking approach to the riddle is developed by using the symbolic model checking algorithm for logic of knowledge under the semantics of interpreted systems with local propositions. The approach is then implemented by extending the model checker NuSMV and in which the solution of the riddle is verified successfully. The riddle is also verified by using the epistemic model checker DEMO in the same experimental environment. The comparison between the experimental results from the two model checkers show that the running efficiency of our model checking approach is much higher than that of DEMO.