Model Checking Sum and Product Authors
Hans van Ditmarsch, Ji Ruan · 2005
University of Groningen, Netherlands, [email protected]. We model the well-known Sum-and-Product problem in amodal logic, and verify its solution in a model checker. The modal logic ispublic announcement logic. This logic contains operators for knowledge,but also for the informational consequences of public announcements.The logic is interpreted on multi-agent Kripke models.The information in the riddle can be represented in the traditional way bynumber pairs, so that Sum knows their sum and Product their product,but also as an interpreted system, so that Sum and Product at leastknow their local state. We show that the di erent representations areisomorphic.The riddle is then implemented and its solution veri ed in the epistemicmodel checker DEMO. This can be done, we think, surprisingly elegantly.It involves reformulations to facilitate the computation.