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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Dixon, C., Nalon, C., Fisher, M.: Tableaux for Temporal Logics of Knowledge: Synchronous Systems of Perfect Recall Or No Learning. In: Proc. of 10th Int. Symp. on Temporal Representation and Reasoning, Australia (2003)
Fagin, R., Vardi, M.: Knowledge and Implicit Knowledge in a Distributed Environment. In: Conf. on Theoretical Aspects of Reasoning about Knowledge, pp. 187–206 (1986)
Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Knowledge-Based Programs. Distributed Computing 10(4), 199–225 (1997)
Lehmann, D.: Knowledge, common knowledge, and related puzzles. In: Proc. 3rd Ann. ACM Conf. on Principles of Distributed Computing, pp. 62–67 (1984)
Lamport, L.: Time, Clocks and the Ordering of Events in a Distributed System. Communications of the ACM 21(7), 558–565 (1978)
Meyden, R., Shilov, N.: Model Checking Knowledge and Time in Syst. with Perfect Recall. Found. of Soft. Techn. and Theoret. Comp. Science, 432–445 (1999)
Lomuscio, A., Raimondi, F.: Model Checking Knowledge, Strategies and Games in Multi-agent Systems. In: AAMAS 2006: 5th Int. Joint Conf. on Autonomous Agents and Multi-agent Systems, pp. 161–168 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benevides, M., Delgado, C., Carlini, M. (2008). Proving Epistemic and Temporal Properties from Knowledge Based Programs. In: Zaverucha, G., da Costa, A.L. (eds) Advances in Artificial Intelligence - SBIA 2008. SBIA 2008. Lecture Notes in Computer Science(), vol 5249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88190-2_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-88190-2_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88189-6
Online ISBN: 978-3-540-88190-2
eBook Packages: Computer ScienceComputer Science (R0)