zbMATH — the first resource for mathematics

A hybrid of tense logic $$S4_T$$ and multi-agent logic with interacting agents. (English) Zbl 07324611
Summary: In this paper we introduce a temporal multi-agent logic $$S4_T^{\mathcal{IA}}$$, which implements interacting agents. Logic $$S4_T^{\mathcal{IA}}$$ is defined semantically as the set of all formulas of the appropriate propositional language that are valid in special Kripke models. The models are based on $$S4$$-like time frames, i.e., with reflexive and transitive time-accessibility relations. Agents knowledge-accessibility relations $$R_i$$, defined independently for each individual agent, are $$S5$$-relations on $$R$$-time clusters, and interaction of the agents consists of passing knowledge along arbitrary paths of such relations. The key result of the paper is an algorithm for checking satisfiability and recognizing theorems of $$S4_T^{\mathcal{IA}}$$. We also prove the effective finite model property for the logic $$S4_T^{\mathcal{IA}}$$.
MSC:
 68 Computer science 03 Mathematical logic and foundations
Full Text:
References:
 [1] H. Barringer, M. Fisher, D. Gabbay, G. Gough, Advances in Temporal Logic, Appl. Logic Ser., 16, Kluwer Academic Publ., Dordrecht, 1999 · Zbl 0931.00025 [2] R. H. Bordini, M. Fisher, W. Visser, M. Wooldridge, “Model Checking Rational Agents”, IEEE Intelligent Systems, 19:4 (2004), 46-52 [3] J. Dix, M. Fisher, H. Levesque, L. Sterling, “Special Issue on Logic-Based Agent Implementation, Editorial”, Ann. Math. Artificial Intelligence, 41:2-4 (2004), 131-133 [4] R. Fagin, J. Geanakoplos, J. Halpern, M. Y. Vardi, “The Hierarchical Approach to Modeling Knowledge and Common Knowledge”, International J. Game Theory, 28:3 (1999), 331-365 · Zbl 1061.68556 [5] R. Fagin, J. Halpern, Y. Moses, M. Vardi, Reasoning About Knowledge, MIT Press, Cambridge, 1995 · Zbl 0839.68095 [6] M. Fisher, “Temporal Development Methods for Agent-Based Systems”, J. Autonomous Agents Multi-Agent Systems, 10:1 (2005), 41-66 [7] D. M. Gabbay, I. M. Hodkinson, “An Axiomatisation of the Temporal Logic with Until and Since over the Real Numbers”, J. Logic Computation, 1 (1990), 229-260 · Zbl 0744.03018 [8] R. Goldblatt, Logics of Time and Computation, CSLI Lecture Notes, 7, Stanford Uviv., Stanford, CA, 1992 · Zbl 0635.03024 [9] W. van der Hoek, M. Wooldridge, “Towards a Logic of Rational Agency”, Log. J. IGPL, 11:2 (2003), 135-159 · Zbl 1029.03014 [10] J. Halpern, R. Shore, “Reasoning about Common Knowledge with Infinitely Many Agents”, Inform. Comput., 191:1 (2004), 1-40 · Zbl 1078.03014 [11] J. Y. Halpern, “Reasoning about knowledge: A survey”, Handbook of Logic in Articial Intelligence and Logic Programming, Vol. 4, Oxford Univ. Press, New York, 1995, 1-34 [12] J. Hendler, “Agents and the Semantic Web”, IEEE Intelligent Systems, 16:2 (2001), 30-37 [13] I. Hodkinson, “Temporal Logic and Automata”, Chapter II of Temporal Logic, Mathematical Foundations and Computational Aspects, Vol. 2, Clarendon Press, Oxford, 2000, 30-72 [14] V. V. Rybakov, “A Criterion for Admissibility of Rules in the Modal System $$S4$$ and the Intuitionistic Logic”, Algebra and Logic, 23:5 (1984), 369 - 384 (Engl. Translation) · Zbl 0598.03013 [15] V. V. Rybakov, Admissible of Logical Inference Rules, Stud. Logic Found. Math., 136, Elsevier Sci. Publ., North-Holland, 1997 · Zbl 0872.03002 [16] V. V. Rybakov, “Logical Consecutions in Intransitive Temporal Linear Logic of Finite Intervals”, J. Logic Computation, 15:5 (2005), 633-657 · Zbl 1091.03002 [17] V. V. Rybakov, “Logical Consecutions in Discrete Linear Temporal Logic”, J. Symbolic Logic, 70:4 (2005), 1137-1149 · Zbl 1110.03010 [18] V. V. Rybakov, “Linear Temporal Logic with Until and Before on Integer Numbers, Deciding Algorithms”, Computer Science - Theory and Applications, Lecture Notes in Computer Sci., 3967, Springer, Berlin-Heidelberg, 2006, 322-334 · Zbl 1185.03022 [19] V. V. Rybakov, “Until-Since Temporal logic Based on Parallel Time with Common Past. Dedecinding algorithms”, Logical Foundations of Computer Science, LFCS’07, New York, Lecture Notes in Computer Sci., 4514, Springer, Berlin-Heidelberg, 2007, 486-497 · Zbl 1132.03324 [20] V. Rybakov, “Multi-Agent Logics with Interacting Agents Based on Linear Temporal Logic. Deciding Algorithms”, ICAISC 2008 (International Conference on Artificial Intelligence and Soft Computing), accepted, to be published at LNCS, Springer [21] J. Benthem, J. A. Bergstra, “Logic of Transition Systems”, J. Logic, Language and Information, 3:4 (1994), 247-283 · Zbl 0827.03019 [22] J. van Benthem, The Logic of Time, Kluwer Acad. Publ., Dordrecht, 1991 · Zbl 0758.03012 [23] M. Wooldridge, G. Weiss, P. Ciancarini (ed.), Agent-Oriented Software Engineering II, Lecture Notes in Computer Sci., 2222, Springer, Berlin-Heidelberg, 2001 · Zbl 0983.68771 [24] M. Wooldridge, P. E. Dunne, “The Computational Complexity of Agent Verification”, Intelligent Agents VIII, Lecture Notes in Comuter Sci., 2333, Springer, Berlin-Heidelberg, 2002, 115-127 · Zbl 1050.68632
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.