Talk "Model Checking Knowledge-based Programs"

by Alexander Knapp

Sat, 16 March 2013 at 11:30 am in Rome, Italy

Joint work with: Heribert Mühlberger

Abstract: Knowledge-based programs include epistemic guards for abstracting from the details how agents may learn certain facts. The interpretation of knowledge-based programs depends on which states are reached in executions, which itself depends on what may be known by the agents. We outline an approach to model checking such programs by applying the must/cannot analysis of synchronous programming languages.