随着计算机网络以及基于网络的分布式计算的发展,对于Agent系统的研究,已成为人工智能领域中一个新的研究热点.基于Agent的技术被认为是软件领域中的一次重大突破.该文提出了一种基于时序逻辑的Agent形式化模型.VSK-t逻辑是一种对处在特定环境中的计算Agent的信息特征进行推理的多模态逻辑.VSK-t逻辑可以描述环境中客观真的事物、环境中可访问的或可知的信息,以及Agent能感知到的环境信息,最后还可描述Agent真正知道的信息,同时,时序逻辑的灵活性和动态性更好地描述了Agent的动态性质.系统中Agent的行为能力是与其所处环境的时间密切相关的,Agent不会执行那些自己在某些时间没有能力执行的动作,而Agent的感知能力也是随时间变化而变化的.这样的描述是合乎理性的.用形式化方法构建了一种基于VSK-t逻辑的Agent形式化模型.定义了VSK-t逻辑的语法规则,语义框架.提出了相应的公理体系,并对其合理性进行了充分的阐述.讨论了Agent所具有的性质,提出并详细证明了一系列理论结果.证明了VSK-t逻辑的无矛盾性、完全性以及完备性.通过具体示例说明了该逻辑的应用.讨论了该模型的特点.提出了今后的一些研究工作.