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

近几年,模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑（ATL）,也被给予了高度关注.根据智能体是否可以看到全局信息分为不完全信息和完全信息;根据智能体是否可以记录历史信息分为无记忆能力和无限记忆能力,提出了四种经典的策略类型.这些策略类型是通过ATL的语义进行刻画的.然而,在一个多智能体系统中,考虑完全信息和无限记忆能力时,所有智能体都只能选择这一种策略类型;在考虑不完全信息或无记忆能力时,仅在联合模态操作<>φ和的[[A]]φ里出现的智能体具备这种策略类型,而其他智能体还是完全信息和无限记忆能力策略类型.这可能会导致嵌套联合模态操作中智能体策略类型的不一致,且智能体策略类型取决于逻辑公式和逻辑的语义.而在实际多智能体系统中,智能体的策略类型往往取决于系统本身,且不同智能体具有不同的策略类型,即智能体策略类型是异构的,这种多智能体系统被称为异构多智能体系统.针对这些问题,本文提出了一种在语法层对智能体策略类型进行刻画的系统模型,即带类型解释系统.带类型解释系统在已有的解释系统中为每个智能体引入"策略类型"这一属性,允许不同智能体具备不同的策略类型.带类型解释系统可用于异构多智能体系统的建模.针对新提出的系统模型,对ATL语义进行了研究,设计了ATL模型检查算法,实现了相应的模型检查工具ShTMC.