Abstract: 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. B

Key words: Symbolic model checking, Multi-agent system, Temporal logic, Public announcement logic