异构多智能体系统模型检查

摘要

Model-checking,an automatic verification methodology,has been applied to verify multi-agent systems.Alternating-time temporal logic (ATL),a property specification language for multi-agent systems was also investigated.According to whether agents are able to observe the whole information of the system and whether agents are able to record the history information,agents' strategies are divided into four types.These strategy abilities are defined in semantic level of ATL,as well as other logics.However,under perfect information and perfect recall setting,all agents have the same strategy ability.Under imperfect information and/or imperfect recall setting,only agents appeared in coalition modalities 《A》φ and [[A]] φ have imperfect information and/or imperfect recall strategies,whileother agents not in A still have perfect information and perfect recall strategies.When coalition modalities are nested,same agents may have different strategy abilities to fulfill different sub formulas,which results in inconsistency.On the other hand,in practice,agents' strategy abilities are usually decided by the multi-agent systems rather than the specifications,and different agents may own different strategy abilities.This kind of multi-agent systems is called heterogeneous mutli-agent systems.To overcome these problems,this paper proposes a new formal model,called typed interpreted systems which are able to define agent's strategy abilities at syntax level.Typed interpreted systems extend interpreted systems by associating each agent with a strategy type denoting the agent's strategy ability,therefore are able to model heterogeneous mutli-agent systems.The paper investigates the semantics of ATL on this new model and proposes an EXPTIME model-checking algorithm.The model-checking algorithm is implemented in a prototype tool ShTMC.%模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑(ATL),也被给予了高度关注.根据智能体是否可以看到全局信息,分为不完全信息和完全信息;根据智能体是否可以记录历史信息,分为无记忆能力和无限记忆能力,提出了4种经典的策略类型.这些策略类型是通过ATL的语义进行刻画的.然而在一个多智能体系统中,考虑完全信息和无限记忆能力时,所有智能体都只能选择这一种策略类型;在考虑不完全信息或无记忆能力时,仅在联合模态操作《A》φ和[A]]φ々A里出现的智能体具备这种策略类型,而其他智能体还是完全信息和无限记忆能力策略类型.这可能会导致嵌套联合模态操作中智能体策略类型的不一致,且智能体策略类型取决于逻辑公式和逻辑的语义.而在实际多智能体系统中,智能体的策略类型往往取决于系统本身,且不同智能体具有不同的策略类型,即,智能体策略类型是异构的,这种多智能体系统被称为异构多智能体系统.针对这些问题提出了一种在语法层对智能体策略类型进行刻画的系统模型——带类型解释系统.带类型解释系统在已有的解释系统中为每个智能体引入策略类型这一属性,允许不同智能体具备不同的策略类型.带类型解释系统可用于异构多智能体系统的建模.针对提出的系统模型,对ATL语义进行了研究,设计了ATL模型检查算法,实现了相应的模型检查工具ShTMC.