保证计算机系统的正确性和可靠性是计算机研究和开发人员的首要任务。模型检测是保证计算机系统正确性和可靠性的有力手段。当人们对复杂系统进行建模和分析时,往往需要考虑到事件发生的不确定性、发生事件的时限和完成事件所付出的代价等因素,实时随机系统模型检测就是研究这类情况下的模型检测问题。实时随机系统模型检测是诞生于二十世纪九十年代的一个活跃的研究领域,目前已取得很多重要的理论研究成果,并取得广泛的实际应用。为验证实时随机系统的行为是否满足一定性质的要求,可以采用模型检测的方法。如果系统的行为不满足性质的要求,可生成相应的反例。进一步地,为控制含不确定性的系统的行为,可以根据系统的模型和性质的要求,合成适当的控制器,以控制系统的运行。本文正是围绕实时随机系统的分析、诊断与控制,开展了一定的研究。实时随机系统的典型模型包括离散(连续)时间Markov链、离散(连续)时间Markov决策过程、概率时间自动机。本文围绕离散(连续)时间Markov决策过程、概率时间自动机及其扩展模型,开展了如下研究:1、面向概率时间自动机的两个扩展模型—代价概率时间自动机和区间概率时间自动机,研究了模型检测问题:(1)以代价概率时间自动机模型来描述系统,研究在一定概率下限条件下的最优成本求解问题。将该模型扩展为多代价概率时间自动机,研究在一定概率下限和辅助成本上限约束条件下的主成本最小值的求解问题。针对每个问题,给出了求解算法和验证的实例。(2)提出了区间概率时间自动机模型,来描述离散迁移概率为区间值的实时随机系统,并研究了区间概率时间自动机的模型检测问题。其核心问题是该模型上的最大概率计算问题。通过基于zone的反向宽度优先搜索算法,得到宽松区间Markov决策过程。由于问题的等价性,将区间概率时间自动机上的最大概率计算问题转换为后者的最大概率计算问题。给出了宽松区间Markov决策过程上最大概率的计算方法。2、面向概率时间自动机和连续时间Markov决策过程,研究了模型检测时的反例生成问题:(1)研究了模型检测概率时间自动机的反例生成问题。给出了模型检测概率时间自动机的反例的定义,给出了快速计算该反例的步骤和算法。在深入分析上述方法的基础上,给出了计算该反例的精化算法。(2)研究了连续时间Markov决策过程上可达性的反例生成问题。在掌握连续时间Markov决策过程上的可达性验证算法的基础上,给出了连续时间Markov决策过程上可达性的反例的概念,并给出了高效地计算该反例的步骤和算法。讨论了该算法成立所依赖的调度类型。3、面向离散时间Markov决策过程,研究了冲突容忍规约背景下的控制器合成问题:提出了一种描述冲突容忍规约的时序逻辑—冲突容忍的含过去时操作符的PCTL*(CT-PPCTL*)。研究了基于CT-PPCTL*的Markov决策过程的控制器合成问题。给出了该问题的总体解决方案。