×

A complete quantified epistemic logic for reasoning about message passing systems. (English) Zbl 1175.68430

Sadri, Fariba (ed.) et al., Computational logic in multi-agent systems. 8th international workshop, CLIMA VIII, Porto, Portugal, September 10–11, 2007. Revised selected and invited papers. Berlin: Springer (ISBN 978-3-540-88832-1/pbk). Lecture Notes in Computer Science 5056. Lecture Notes in Artificial Intelligence, 248-267 (2009).
Summary: We investigate quantified interpreted systems, a semantics to model multi-agent systems in which the agents can reason about individuals, their properties, and relationships among them. The semantics naturally extends interpreted systems to first-order by introducing a domain of individuals. We present a first-order epistemic language interpreted on this semantics and prove soundness and completeness of the quantified modal system QS\(5^{\text{D}}_n\), an axiomatisation for these structures. Finally, we exemplify the use of the logic by modeling message passing systems, a relevant class of interpreted systems analysed in epistemic logic.
For the entire collection see [Zbl 1155.68010].

MSC:

68T27 Logic in artificial intelligence
03B42 Logics of knowledge and belief (including belief change)
68T42 Agent technology and artificial intelligence

Software:

AVISPA; MCK
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Armando, A., et al.: The Avispa tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005) · Zbl 1081.68523 · doi:10.1007/11513988_27
[2] Ågotnes, T., van der Hoek, W., Wooldridge, M.: Quantified Coalition Logic. In: Proceedings of IJCAI, Hyderabad, India, January 6-12, 2007, pp. 1181–1186 (2007) · Zbl 1169.03020
[3] Belardinelli, F., Lomuscio, A.: A Quantified Epistemic Logic to reason about Multi-Agent Systems. In: Proceedings of AAMAS 2007, Honolulu, Hawaii (2007) · Zbl 1191.68646
[4] Belardinelli, F., Lomuscio, A.: Quantified Epistemic Logics with Flexible Terms. In: LORI workshop on Logic, Rationality and Interaction, Beijing, August 5-9 (2007) · Zbl 1191.68646
[5] Bieber, P.: A logic of communication in hostile environments. In: CSFW, pp. 14–22 (1990) · doi:10.1109/CSFW.1990.128181
[6] Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge, UP (2001) · Zbl 0988.03006
[7] Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford University Press, Oxford (1997) · Zbl 0871.03007
[8] Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
[9] Dams, M., Cohen, M.: A complete axiomatisation of knowledge and cryptography. In: LICS (2007)
[10] Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT Press, Cambridge (1995) · Zbl 0839.68095
[11] Fagin, R., Halpern, J., Vardi, M.: What can machines know? on the properties of knowledge in distributed systems. J. ACM 39(2), 328–376 (1992) · Zbl 0799.68179 · doi:10.1145/128749.150945
[12] Fitting, M., Mendelsohn, R.: First-order Modal Logic. Kluwer, Dordrecht (1999) · Zbl 1025.03001
[13] 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) · Zbl 1103.68614 · doi:10.1007/978-3-540-27813-9_41
[14] Halpern, J., Fagin, R.: Modelling knowledge and action in distributed systems. Distributed Computing 3(4), 159–179 (1989) · Zbl 0685.68076 · doi:10.1007/BF01784885
[15] Garson, J.: Quantification in modal logic. Handbook of Philosophical Logic, vol. 2, pp. 249–307 (1984) · Zbl 0875.03050 · doi:10.1007/978-94-009-6259-0_5
[16] Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable fragment of first-order temporal logics. Ann. Pure Appl. Logic 106(1-3), 85–134 (2000) · Zbl 0999.03015 · doi:10.1016/S0168-0072(00)00018-X
[17] van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: Proceedings of AAMAS 2002, pp. 1167–1174. ACM Press, New York (2002)
[18] Hughes, G., Cresswell, M.: A New Introduction to Modal Logic. Routledge (1996) · Zbl 0855.03002 · doi:10.4324/9780203290644
[19] Kripke, S.: A Completeness Theorem in Modal Logic. J. Sym. Log. 24, 1–14 (1959) · Zbl 0091.00902 · doi:10.2307/2964568
[20] Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communication of the ACM 21(7), 558–565 (1978) · Zbl 0378.68027 · doi:10.1145/359545.359563
[21] Lomuscio, A., Colombetti, M.: QLB: a quantified logic for belief. In: Jennings, N.R., Wooldridge, M.J., Müller, J.P. (eds.) ECAI-WS 1996 and ATAL 1996. LNCS, vol. 1193. Springer, Heidelberg (1996)
[22] Lomuscio, A., Ryan, M.: On the relation between interpreted systems and kripke models. In: Wobcke, W., Pagnucco, M., Zhang, C. (eds.) Agents and Multi-Agent Systems Formalisms, Methodologies, and Applications. LNCS (LNAI), vol. 1441. Springer, Heidelberg (1997)
[23] Lomuscio, A., Penczek, W., Wozna, B.: Bounded model checking knowledge and real time. Artificial Intelligence (to appear) · Zbl 1168.68422 · doi:10.1016/j.artint.2007.05.005
[24] Meyer, J.-J., van der Hoek, W.: Making some issues of implicit knowledge explicit. Int. J. of Foundations of Computer Science 3(2), 193–223 (1992) · Zbl 0759.68082 · doi:10.1142/S0129054192000139
[25] Meyer, J.-J.C., van der Hoek, W.: Epistemic Logic for AI and Computer Science. Cambridge University Press, Cambridge (1995) · Zbl 0868.03001 · doi:10.1017/CBO9780511569852
[26] Penczek, W., Lomuscio, A.: Verifying Epistemic Properties of multi-agent systems via bounded model checking. Fund. Inform. 55(2), 167–185 (2003) · Zbl 1111.68512
[27] Quine, W.v.O.: Quantifiers and Propositional Attitudes. Journal of Philosophy 53, 177–187 (1956) · doi:10.2307/2022451
[28] Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic 5(2), 235–251 (2007) · Zbl 1122.68076 · doi:10.1016/j.jal.2005.12.010
[29] Solanki, M.: A Compositional Framework for the Specification, Verification and Runtime Validation of Reactive Web Service. PhD thesis (2005)
[30] Solanki, M., Cau, A., Zedan, H.: ASDL: a wide spectrum language for designing web services. In: WWW, pp. 687–696. ACM, New York (2006)
[31] Spoletini, P.: Verification of Temporal Specification via Model Checking. PhD thesis, Politecnico di Milano, Dipartimento di Elettronica e Informatica (2006)
[32] Sturm, H., Wolter, F., Zakharyaschev, M.: Monodic epistemic predicate logic. In: Brewka, G., Moniz Pereira, L., Ojeda-Aciego, M., de Guzmán, I.P. (eds.) JELIA 2000. LNCS (LNAI), vol. 1919, pp. 329–344. Springer, Heidelberg (2000) · Zbl 0998.03011 · doi:10.1007/3-540-40006-0_23
[33] Sturm, H., Wolter, F., Zakharyaschev, M.: Common knowledge and quantification. Economic Theory 19, 157–186 (2002) · Zbl 0994.03008 · doi:10.1007/s001990100201
[34] Viganó, F.: A Framework for Model Checking Institutions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 129–145. Springer, Heidelberg (2007) · Zbl 1196.68291 · doi:10.1007/978-3-540-74128-2_9
[35] Wolter, F., Zakharyaschev, P.: Decidable fragments of first-order modal logics. J. Symb. Log. 66(3), 1415–1438 (2001) · Zbl 0996.03010 · doi:10.2307/2695115
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.