Reasoning about Resource-Sensitive Multi-Agents
Norihiro Kamide · InTech eBooks · 2011
IntroductionAims.Formalizing common knowledge reasoning in multi-agent systems is of growing importance in Computer Science, Artificial Intelligence, Economics, Philosophy and Psychology.Obtaining a concrete logical foundation for common knowledge reasoning plays an important role for formal treatment and verification of multi-agent systems.For this reason, formalizing common knowledge reasoning is also a traditional issue for multi-agent epistemic logics (Fagin et al., 1995;Halpern & Moses, 1992;Lismont & Mongin, 1994;Meyer & van der Hoek, 1995).The aim of this paper is to formalize more fine-grained common knowledge reasoning by a new logical foundation based on Girard's linear logics.Common knowledge.The notion of common knowledge was probably first introduced by Lewis (Lewis, 1969).This notion is briefly explained below.Let A be a fixed set of agents and α be an idea.Suppose that α belongs to the common knowledge of A, and i and j are some members of A. Then, we have the facts "both i and j know α", "i knows that j knows α" and "j knows that i knows α".Moreover, we also have the facts "i knows that j knows that i knows α", and so on.Then, these nesting structures develop an infinite hierarchy as a result.Iterative interpretation.Suppose that the underlying multi-agent logic has the knowledge operators ♥ 1 , ♥ 2 , ..., ♥ n , in which a formula ♥ i α means "the agent i knows α."The common knowledge of a formula α is defined below.For any m ≥ 0, an expression K m means the setis interpreted as the null symbol.The common knowledge ♥ c α of α is defined by using an infinitary conjunction as the so-called iterative interpretation of common knowledge: ♥ c α := {♥α |♥∈ m∈ω K m }.Then, the formula ♥ c α means "α is common knowledge of agents."Common knowledge logics.Common knowledge logics (CKLs) are multi-agent epistemic logics with some knowledge and common knowledge operators (Fagin et al., 1995;Halpern & Moses, 1992;Lismont & Mongin, 1994;Meyer & van der Hoek, 1995).So far, CKLs have been studied based on classical logic (CL).On the other hand, CL is not so appropriate for expressing more fine-grained reasoning such as resource-sensitive, concurrency-centric and constructive reasoning.Thus, CKLs based on non-classical logics have been required for expressing such fine-grained reasoning.Linear logics.Girard's linear logics (LLs) (Girard, 1987), which are most promising and useful non-classical logics in Computer Science, are logics that can naturally represent the concepts 8 www.intechopen.com