Abstract
In this paper, we introduce a real-time temporal knowledge logic, called RTKL, which is a combination of real-time temporal logic and knowledge logic. It is showed that temporal modalities such as “always in an interval”, “until in an interval”, and knowledge modalities such as “knowledge in an interval” and “common knowledge in an interval” can be expressed in such a logic. The model checking algorithm is given. Furthermore, we add cooperation modalities to RTKL and get a new logic RATKL, which can express not only real-time temporal and epistemic properties but also cooperation properties. The model checking algorithm for RATKL is also given.
This work was supported by the National Science Foundation of China under Grant 60473036.
Chapter PDF
Similar content being viewed by others
References
R. Alur, L. de Alfaro, T. A. Henzinger, S. C. Krishnan, F. Y. C. Mang, S. Qadeer, S. K. Rajamni, and S, Tasiran, MOCHA user manual, University of Berkeley Report, 2000.
R. Alur and T. A. Henzinger. Alternating-time temporal logic. In Journal of the ACM, 49(5): 672–713.
M. Bourahla and M. Benmohamed. Model Checking Multi-Agent Systems. In Informalica 29: 189–197, 2005.
E. M. Clarke, J. O. Grumberg, and D. A. Peled. Model checking. The MIT Press, 1999.
H. van Ditmarsch, W van der Hoek, and B. P. Kooi. Dynamic Epistemic Logic with Assignment, in AAMAS05, ACM Inc, New York, vol. 1, 141–148, 2005.
N. de C. Ferreira, M. Fisher, W. van der Hoek: Logical Implementation of Uncertain Agents. Proc. EPIA-05, LNAI 3808, pp536–547.
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Common knowledge revisited, Annals of Pure and Applied Logic 96: 89–105, 1999.
J. Y. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. J ACM, 1990, 37(3): 549–587.
W. van der Hoek and M. Wooldridge. Model Checking Knowledge, and Time. In Proceedings of SPIN 2002, LNCS 2318, 95–111, 2002.
W. van der Hoek and M. Wooldridge. Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications. Studia Logica, 75: 125–157, 2003.
M. Kacprzak, A. Lomuscio and W. Penczek. Verification of multiagent systems via unbounded model checking. In Proceedings of the 3rd International Conference on Autonomous Agents and Multiagent Systems (AAMAS-04), 2004.
M. Wooldridge, M. Fisher, M. Huget, and S. Parsons. Model checking multiagent systems with mable. In Proceedings of the First International Conference on Autonomous Agents and Multiagent Systems (AAMAS-02), 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 International Federation for Information Processing
About this paper
Cite this paper
Cao, Z. (2006). Model Checking for Real-Time Temporal, Cooperation and Epistemic Properties. In: Shi, Z., Shimohara, K., Feng, D. (eds) Intelligent Information Processing III. IIP 2006. IFIP International Federation for Information Processing, vol 228. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-44641-7_7
Download citation
DOI: https://doi.org/10.1007/978-0-387-44641-7_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-44639-4
Online ISBN: 978-0-387-44641-7
eBook Packages: Computer ScienceComputer Science (R0)