# zbMATH — the first resource for mathematics

Quantified epistemic logics for reasoning about knowledge in multi-agent systems. (English) Zbl 1191.68646
Summary: We introduce quantified interpreted systems, a semantics to reason about knowledge in multi-agent systems in a first-order setting. Quantified interpreted systems may be used to interpret a variety of first-order modal epistemic languages with global and local terms, quantifiers, and individual and distributed knowledge operators for the agents in the system. We define first-order modal axiomatisations for different settings, and show that they are sound and complete with respect to the corresponding semantical classes.The expressibility potential of the formalism is explored by analysing two MAS scenarios: an infinite version of the muddy children problem, a typical epistemic puzzle, and a version of the battlefield game. Furthermore, we apply the theoretical results here presented to the analysis of message passing systems [R. Fagin, J. Y. Halpern, Y. Moses and M. Y. Vardi, Reasoning about knowledge. Cambridge, MA: MIT Press (1995; Zbl 0839.68095); L. Lamport, “Time, clocks, and the ordering of events in a distributed system”, Commun. ACM 21, 558–565 (1978; Zbl 0378.68027)], and compare the results obtained to their propositional counterparts. By doing so we find that key known meta-theorems of the propositional case can be expressed as validities on the corresponding class of quantified interpreted systems.

##### MSC:
 68T27 Logic in artificial intelligence 03B42 Logics of knowledge and belief (including belief change) 68T30 Knowledge representation 68T42 Agent technology and artificial intelligence
MCK; Verics
Full Text:
##### References:
 [1] F. Belardinelli, Quantified modal logic and the ontology of physical objects, PhD thesis, Scuola Normale Superiore, Pisa, 2006 [2] Bieber, P., A logic of communication in hostile environments, (), 14-22 [3] Blackburn, P.; de Rijke, M.; Venema, Y., Modal logic, (2001), Cambridge University Press · Zbl 0988.03006 [4] () [5] Chagrov, A.; Zakharyaschev, M., Modal logic, (1997), Oxford University Press · Zbl 0871.03007 [6] Clarke, E.; Grumberg, O.; Peled, D., Model checking, (1999), MIT Press [7] Cohen, M.; Dams, M., A complete axiomatization of knowledge and cryptography, (), 77-88 [8] Cohen, P.; Levesque, H., Communicative actions for artificial agents, (), 65-72 [9] Corsi, G., A unified completeness theorem for quantified modal logics, Journal of symbolic logic, 67, 1483-1510, (2002) · Zbl 1043.03015 [10] Corsi, G., BF, CBF and Lewis semantics, Logique et analyse, 103-122, (2005) · Zbl 1077.03008 [11] Degtyarev, A.; Fisher, M.; Konev, B., Monodic temporal resolution, ACM transactions on computational logic (TOCL), 7, 1, 108-150, (2006) · Zbl 1367.03035 [12] Degtyarev, A.; Fisher, M.; Lisitsa, A., Equality and monodic first-order temporal logic, Studia logica, 72, 147-156, (2002) · Zbl 1011.03007 [13] Dembiński, P., Verics: A tool for verifying timed automata and estelle specifications, (), 278-283 · Zbl 1031.68546 [14] Fagin, R.; Halpern, J.; Moses, Y.; Vardi, M., Reasoning about knowledge, (1995), MIT Press · Zbl 0839.68095 [15] Fagin, R.; Halpern, J.; Vardi, M., What can machines know? on the properties of knowledge in distributed systems, Journal of the ACM, 39, 2, 328-376, (1992) · Zbl 0799.68179 [16] Fitting, M.; Mendelsohn, R., First-order modal logic, (1998), Kluwer Dordrecht · Zbl 1025.03001 [17] Follesdal, D., Knowledge, identity, and existence, Theoria, 23, 1, 1-27, (1967) · Zbl 0174.00904 [18] Gammie, M.; van der Meyden, R., MCK: model checking the logic of knowledge, (), 479-483 · Zbl 1103.68614 [19] Garson, J., Quantification in modal logic, (), 267-323 · Zbl 1003.03519 [20] Halpern, J.; Fagin, R., Modelling knowledge and action in distributed systems, Distributed computing, 3, 4, 159-179, (1989) · Zbl 0685.68076 [21] Halpern, J.; Shore, R., Reasoning about common knowledge with infinitely many agents, Information and computation, 191, 1, 1-40, (2004) · Zbl 1078.03014 [22] Hintikka, Y., Knowledge, identity, and existence, Nous, 1, 1, 33-62, (1962) [23] Hodkinson, I., Monodic packed fragment with equality is decidable, Studia logica, 72, 185-197, (2002) · Zbl 1011.03008 [24] Hodkinson, I., Complexity of monodic guarded fragments over linear and real time, Annals of pure and applied logic, 138, 94-125, (2006) · Zbl 1093.03009 [25] Hodkinson, I.; Wolter, F.; Zakharyaschev, M., Decidable fragment of first-order temporal logics, Annals of pure and applied logic, 106, 1-3, 85-134, (2000) · Zbl 0999.03015 [26] Hodkinson, I.; Wolter, F.; Zakharyaschev, M., Decidable and undecidable fragments of first-order branching temporal logics, (), 393-402 [27] Hodkinson, I.; Kontchakov, R.; Kurucz, A.; Wolter, F.; Zakharyaschev, M., On the computational complexity of decidable fragments of first-order linear temporal logics, (), 91-98 [28] van der Hoek, W.; Meyer, J.J.Ch., Making some issues of implicit knowledge explicit, International journal of foundations of computer science, 3, 2, 193-223, (1992) · Zbl 0759.68082 [29] van der Hoek, W.; Meyer, J.J.Ch.; Treur, J., Formal semantics of temporal epistemic reflection logic, (), 332-352 [30] Hughes, G.; Cresswell, M., A new introduction to modal logic, (1996), Routledge · Zbl 0855.03002 [31] Huth, M.; Ryan, M., Logic in computer science: modelling and reasoning about systems, (2004), Cambridge University Press · Zbl 1073.68001 [32] Kaneko, M.; Nagashima, T., Game logic and its applications 1, Studia logica, 57, 325-354, (1996) · Zbl 0858.03035 [33] Kaneko, M.; Nagashima, T., Game logic and its applications 2, Studia logica, 58, 273-303, (1997) · Zbl 0871.03030 [34] Kripke, S., A completeness theorem in modal logic, Journal of symbolic logic, 24, 1-14, (1959) · Zbl 0091.00902 [35] Jager, T., An actualist semantics for quantified modal logic, Notre dame journal of formal logic, 23, 335-349, (1982) [36] Lakemeyer, G., Limited reasoning in first-order knowledge bases, Artificial intelligence, 71, 2, 213-255, (1994) · Zbl 0820.68117 [37] Lakemeyer, G., Limited reasoning in first-order knowledge bases with full introspection, Artificial intelligence, 84, 1-2, 209-255, (1996) [38] 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 [39] Levesque, H., Knowledge representation and reasoning, Annual reviews computer science, 30, 1, 81-108, (1986) [40] Lewis, D., On the plurality of worlds, (1986), Blackwell [41] Liu, Y.; Lakemeyer, G.; Levesque, H., A logic of limited belief for reasoning with disjunctive information, (), 587-597 [42] Liu, Y.; Levesque, H., Tractable reasoning in first-order knowledge bases with disjunctive information, (), 639-644 [43] Lomuscio, A.; Colombetti, M., QLB: A quantified logic for belief, () [44] A. Lomuscio, F. Raimondi, MCMAS: a tool for verifying multi-agent systems, in: Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS06), Springer, pp. 450-454 [45] Lomuscio, A.; Ryan, M., On the relation between interpreted systems and Kripke models, () [46] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent systems, vol. 1, (1992), Springer-Verlag [47] McMillan, K., Symbolic model checking: an approach to the state explosion problem, (1993), Kluwer Academic Publishers [48] Meyden, R., Axioms for knowledge and time in distributed systems with perfect recall, (), 448-457 [49] Meyer, J.-J.Ch.; van der Hoek, W., Epistemic logic for AI and computer science, (1995), Cambridge University Press · Zbl 0838.03021 [50] Moore, R.C., The role of logic in knowledge representation and commonsense reasoning, (), 428-433 [51] Moore, R.C., A formal theory of knowledge and action, () [52] Panangaden, P.; Taylor, K., Concurrent common knowledge: defining agreement for asynchronous systems, Distributed computing, 6, 2, 73-93, (1992) · Zbl 0773.68009 [53] Parikh, R.; Ramanujam, R., Distributed processes and the logic of knowledge, (), 256-268 · Zbl 0565.68025 [54] 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 [55] Rao, A.; Georgeff, M., Modeling rational agents within a BDI-architectures, (), 473-484 · Zbl 0765.68194 [56] Reynolds, M., Axiomatising first-order temporal logic: until and Since over linear time, Studia logica, 57, 2/3, 279-302, (1996) · Zbl 0864.03015 [57] Shehtman, V., Completeness and incompleteness in first-order modal logic: an overview, (), 27-30 · Zbl 1141.03313 [58] Sturm, H.; Wolter, F.; Zakharyaschev, M., Monodic epistemic predicate logic, (), 329-344 · Zbl 0998.03011 [59] Sturm, H.; Wolter, F.; Zakharyaschev, M., Common knowledge and quantification, Economic theory, 19, 157-186, (2002) · Zbl 0994.03008 [60] Thomason, R., Some completeness results for modal predicate calculi, (), 56-76 · Zbl 0188.32002 [61] Wolter, F., First order common knowledge logics, Studia logica, 65, 249-271, (2000) · Zbl 0963.03024 [62] Wolter, F.; Zakharyaschev, M., Decidable fragments of first-order modal logics, Journal of symbolic logic, 66, 3, 1415-1438, (2001) · Zbl 0996.03010 [63] Wolter, F.; Zakharyaschev, M., Axiomatizing the monodic fragment of first-order temporal logic, Annals of pure and applied logic, 118, 1-2, 133-145, (2002) · Zbl 1031.03023 [64] Wooldridge, M., An introduction to multi-agent systems, (2002), John Wiley [65] Wooldridge, M., Computationally grounded theories of agency, (), 13-22 [66] Wooldridge, M., Reasoning about rational agents, (2000), MIT Press · Zbl 0998.68094 [67] Wooldridge, M., Verifying that agents implement a communication language, (), 52-57 [68] Wooldridge, M.; Fisher, M.; Huget, M.; Parsons, S., Model checking for multiagent systems: the mable language and its applications, International journal on artificial intelligence tools, 15, 2, 195-226, (2006) [69] Wooldridge, M.; Fisher, M.; Huget, M.; Parsons, S., Model checking multiagent systems with MABLE, (), 952-959 [70] Wozna, B.; Lomuscio, A., A temporal epistemic logic with a reset operation, (), 574-581
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.