Analytic Tableaux for Verifying Agent Beliefs

For specifying and reasoning about agent beliefs of agent systems, many researchers have proposed the use of belief logics. Since agent systems are designed to operate in dynamic environments such as the Internet, it is important to model the evolution of communication systems through time in a systematic way. In this paper, we introduce a temporal belief logic called TML⁺ for formalizing agent systems; and also propose a labeled tableaux system for this logic. With the logic TML⁺ and its associated modal tableaux, we are able to reason about, and verify agent systems operating in dynamic environments.