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

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