MAS系统中agent的核心能力是其对未来行为的理性决策,因应用环境的开放性和动态变化而具有不确定性。机会发现理论可以在此类环境中发现对主体决策具有重要影响的事件或状态,可用于表达智能行为的协作计算模型。在此情况下,以机会发现理论和时态/模态逻辑为基础,采用基于Kripke框架的机会发现逻辑Lk来研究多智能体系统的形式化描述方法。对Lk的结构及语义进行了详细地描述,并验证了Lk具有可判性且能够在多项式级时间复杂度内实现。