A BDI-VSK-T Logic-based Formal Model Of Agent System

With the development of technology of internet and computer communication,research about Agent and Mult-Agent system has become to be a important field of DAI.The main research are based on BDI model and VSK. model. BDI model of Agent system show that how to describe the relation among all mental states and activity of cooperation, behavior and planning of Agent in order to direct the construction of Agent system. VSK-t logic is a kind of temporal-based multi modal logic for reasoning about the information properties of the agent suited in some environment. Using this logic, we can express what is objectively true of the environment, what is visible or knowable of the environment to individual agent, the information the agents perceives of the environment, and finally what the agents actually know about the environment. This text try to inosculate BDI logic, VSK. logic and temporal logic of agent system, in order to reach a certain goal or make a action choice by its mental states and subjective and objective cognition. Then temporal logic-based formalization of Agent model BDI-VSK-T is put forward in this text.It is expanded based on BDI logic, VSK logic, inosculates BDI logic and VSK logic, then redefine Semantic Frame temporally ,build accessible world by temporal structure. The time structure of a world is a time tree, in which branch stands for action choice of Agent in corresponding time, at the same, following mode operators are defined: V(Visibility) operator accessing the environment, S (Perception) operator perceiving the environment, K (Knowledge) knowledge operator, B(believe) believe operator(desire) desire operator, I(intention) intention operator, they represent separately the information of environment that the agents are capable of accessing, perceiving and knowing; and the mental senses of Agent ,that is the believe ,desire and intention. Moreover, temporal operators are introduced. O (next)next operator, ◇(eventually) possible operator and □ (always) always operator, they represent Agent and the environment Agent suited in the future. So this logic can describe the relation among mental sense .environment and time and how they influence agent's choice. Under this semantic interpretation, Semantic Frame by accessible world is built and Axiomatisation is put forward and also the proof of soundness, consistency and completeness of the model are given at last.