Abstract
With the recent development of many model-checkers for the temporal logic of knowledge, abstraction techniques are necessary to increase the size of the systems that can be verified. In this paper, we introduce several abstraction techniques for interpreted systems and we prove several preservation results. These results consider the temporal logic of knowledge under Kleene’s 3-valued interpretation along infinite and maximal finite paths.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Chechik, M., Easterbrook, S.M., Petrovykh, V.: Model-checking over multi-valued logics. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 72–98. Springer, Heidelberg (2001)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL, pp. 238–252 (1977)
Dams, D.: Abstract Interpretation and Partial Refinement for Model Checking. PhD thesis, Technische Universität Eindhoven (1996)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)
Ginsberg, M.: Multivalued logics. A uniform approach to inference in artificial intelligence. Computational Intelligence 4, 265–316 (1988)
Konikowska, B., Penczek, W.: Model checking for multivalued logic of knowledge and time. In: Proceedings of AAMAS, pp. 169–176 (2006)
Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer, Heidelberg (1992)
O’Neill, K.R., Halpern, J.Y.: Secrecy in multiagent systems. CoRR, cs.CR/0307057 (2003)
Tiplea, F.L., Enea, C.: Abstractions of data types. Acta Informatica 42(8-9), 639–671 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Enea, C., Dima, C. (2007). Abstractions of Multi-agent Systems. In: Burkhard, HD., Lindemann, G., Verbrugge, R., Varga, L.Z. (eds) Multi-Agent Systems and Applications V. CEEMAS 2007. Lecture Notes in Computer Science(), vol 4696. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75254-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-75254-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75253-0
Online ISBN: 978-3-540-75254-7
eBook Packages: Computer ScienceComputer Science (R0)