多智能体系统(Multi-Agent System,MAS)由多个自主智能体组成,这些智能体共同工作在同一环境中,并与环境实时交互,协调完成系统功能。为了描述MAS的不确定性以及动态性,研究者向系统模型中引入概率因子,形成了随机MAS(Stochastic MAS)。概率时间交替时态逻辑(Probabilistic Alternating-Time Temporal Logic,PATL/PATL*)可用于描述与验证并发随机MAS。然而,针对该时态逻辑的模型检测算法大多是基于特定的轮换MAS(Turn-Based MAS),而对于一般的模型系统,仍没有最优的解决策略。此外,针对该时态逻辑的可满足性问题也没有可行的判定算法。因此,提出可描述并发随机MAS的新型时态逻辑,并解决相应时态逻辑的可满足性以及模型检测问题成为本文的研究核心。首先,本文提出一种新型基于概率的时态逻辑:概率时间交替μ-演算(Prob-abilistic Alternating-Time μ-Calculus,PAMC)。PAMC 可用于描述与验证并发随机MAS,它是对时间交替μ-演算(Alternating-Time μ-Calculus,AMC)的概率扩展。PAMC将AMC中联合模态<<A>>ψ替换为概率联合模态<<A>>(?)kψ,概率性描述了一组智能体的策略选择问题。PAMC既包含了 AMC也涵盖了概率模态μ-演算(Probabilistic Modal μ-Calculus,PμTL),且 PAMC与PATL 及 PATL*是不可比较的。其次,本文分析了 PAMC的可满足性问题,并提出了相应的判定算法。本文利用相交图以及最大独立集,通过检测是否存在一个概率分布满足最大独立集内各公式的概率约束条件,继而判定PAMC公式是否可满足。通过上述方式将PAMC的可满足性问题归约到奇偶博弈(Parity Game)问题上:玩家0在博弈中存在一条获胜策略当且仅当PAMC公式可满足。PAMC可满足性问题的复杂度为2-EXPTIME。再者,本文在AMC以及μ-PCTL的模型检测算法基础上,提出了 PAMC模型检测算法。PAMC 在概率并发博弈结构(Probabilistic Concurrent Game Structure,PCGS)上的模型检测复杂度为UP∩co-UP,且针对该模型检测算法,存在某个常量c,使其在O((|φ|·|M|c·dep(φ)时间内可判定。最后,本文设计并实现了 PAMC可满足性检测工具PAMCSolver,它是目前第一个可以判定(概率)时间交替时态逻辑以及PμTL可满足性问题的检测工具。