Proving epistemic and temporal properties from knowledge based programs

Abstract

In this work we investigate two approaches for representing and reasoning about knowledge evolution in Multi-Agent System MAS. We use the language of the Logic of Time and Knowledge TKL [5] as a specification language for the whole system, and for each agent, we use Knowledge Based Programs KBP,[4]. We propose a method to translate a a KBP system into a set of TKL formulas. The translation method presented provides an strategy to model and prove properties of MAS without being attached to local or global representations, giving the alternative to switch from one representation to another. We also present a formal model of computation to our KBP system and prove the correctness our translation function w.r.t. this model.In order to illustrate usefulness of the translation method two examples are presented: the Muddy Children Puzzle and the Bit Exchange Protocol. © 2008 Springer Berlin Heidelberg.