Abstract
Probabilistic temporal logics of knowledge have been used to specify multi-agent systems. In this paper, we introduce a probabilistic temporal logic of knowledge called PTLK for expressing time, knowledge, and probability in multi-agent systems. Then, in order to overcome the state explosion in model checking PTLK we propose an abstraction procedure for model checking PTLK. The rough idea of the abstraction approach is to partition the state space into several equivalence classes which consist of the set of abstract states. The probability distribution between abstract states is defined as an interval for computing the approximation of the concrete system. Finally, the model checking algorithm in PTLK is developed.
Supported by the National Natural Science Foundation of China No. 60773049, the People with Ability Foundation of Jiangsu University No. 07JDG014, the Fundamental Research Project of the Natural Science in Colleges of Jiangsu Province No. 08KJD520015, the Ph.D. Programs Foundation of Ministry of Education of China No. 20093227110005.
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
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (2000)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Enea, C., Dima, C.: Abstractions of Multi-agent Systems. In: Burkhard, H.-D., Lindemann, G., Verbrugge, R., Varga, L.Z. (eds.) CEEMAS 2007. LNCS (LNAI), vol. 4696, pp. 11–21. Springer, Heidelberg (2007)
Cohen, M., Dam, M., Lomuscio, A., Russo, F.: Abstraction in model checking multi-agent systems. In: Proc. of 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 945–952 (2009)
de Ferreira, N.C., Fisher, M., van der Hoek, W.: Practical Reasoning for Uncertain Agents. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 82–94. Springer, Heidelberg (2004)
Cao, Z.: Model Checking for Epistemic and Temporal Properties of Uncertain Agents. In: Shi, Z.-Z., Sadananda, R. (eds.) PRIMA 2006. LNCS (LNAI), vol. 4088, pp. 46–58. Springer, Heidelberg (2006)
Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-Agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003)
Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2002)
Su, K., Sattar, A., Luo, X.: Model Checking Temporal Logics of Knowledge Via OBDDs. Comput. J. 50(4), 403–420 (2007)
Hansson, H., Jonsson, B.: A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing 6, 512–535 (1994)
Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptology 1(1), 65–75 (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhou, C., Sun, B., Liu, Z. (2010). Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge. In: Wang, F.L., Deng, H., Gao, Y., Lei, J. (eds) Artificial Intelligence and Computational Intelligence. AICI 2010. Lecture Notes in Computer Science(), vol 6319. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16530-6_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-16530-6_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16529-0
Online ISBN: 978-3-642-16530-6
eBook Packages: Computer ScienceComputer Science (R0)